Proof step 1 from proof B-postfix-weak-one (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(be ' ⊒w be0 ' + bel ↔ be0 = be ∧ bel = []) ⊦

Rule argument

Additional information

Proof step 2 from proof B-postfix-weak-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ∀ l. (be = SF ∨ be.l = l ⊃ be ';[]) ⊒ (be0 = SF ∨ be0.l = l ⊃ be0 ';[]) + bel.filter(λ be. be = SF ∨ be.l = l) ⊦ be0 = be ∧ bel = []

Rule argument

Additional information

Used simplifier rules: B-postfix-weak: ⊦ bel0 ⊒w bel1 ↔ (∀ l. bel0 |SF l ⊒ bel1 |SF l); B-restrict-SF-l: ⊦ bel |SF l = bel.filter(λ be. be = SF ∨ be.l = l); ⊦ x ⊒ x; (s) ⊦ a '.filter(p) = (p(a) ⊃ a ';[]); (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + [] = x; (s) ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s)

Proof step 3 from proof B-postfix-weak-one (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 4:

  bel = [], ∀ l. (be = SF ∨ be.l = l ⊃ be ';[]) ⊒ (be0 = SF ∨ be0.l = l ⊃ be0 ';[]) + bel.filter(λ be. be = SF ∨ be.l = l) ⊦ be0 = be ∧ bel = []

• Proof step 17:

  bel = be1 + bel0, ∀ l. (be = SF ∨ be.l = l ⊃ be ';[]) ⊒ (be0 = SF ∨ be0.l = l ⊃ be0 ';[]) + bel.filter(λ be. be = SF ∨ be.l = l) ⊦ be0 = be ∧ bel = []

Rule argument

Additional information

Used simplifier rules: List('a) freely generated by [], +;;

Proof step 4 from proof B-postfix-weak-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  be0 ≠ be, ∀ l. (be = SF ∨ be.l = l ⊃ be ';[]) ⊒ (be0 = SF ∨ be0.l = l ⊃ be0 ';[]) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + [] = x; (s) ⊦ [].filter(p) = []; (s)

Proof step 5 from proof B-postfix-weak-one (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 6:

  be0 ≠ be, (be = SF ∨ be.l = be.l ⊃ be ';[]) ⊒ (be0 = SF ∨ be0.l = be.l ⊃ be0 ';[]), ∀ l. (be = SF ∨ be.l = l ⊃ be ';[]) ⊒ (be0 = SF ∨ be0.l = l ⊃ be0 ';[]) ⊦

Rule argument

Additional information

Used terms: be.l

Proof step 6 from proof B-postfix-weak-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  be0 ≠ be, be ' ⊒ (be0 = SF ∨ be0.l = be.l ⊃ be0 ';[]), ∀ l. (be = SF ∨ be.l = l ⊃ be ';[]) ⊒ (be0 = SF ∨ be0.l = l ⊃ be0 ';[]) ⊦

Rule argument

Additional information

Proof step 7 from proof B-postfix-weak-one (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 8:

  be0 ≠ be, be ' ⊒ be0 ', ∀ l. (be = SF ∨ be.l = l ⊃ be ';[]) ⊒ (be0 = SF ∨ be0.l = l ⊃ be0 ';[]), be0 = SF ∨ be0.l = be.l ⊦

• Proof step 10:

  be0.l ≠ be.l, be0 ≠ SF, be0 ≠ be, be ' ⊒ [], ∀ l. (be = SF ∨ be.l = l ⊃ be ';[]) ⊒ (be0 = SF ∨ be0.l = l ⊃ be0 ';[]) ⊦

Rule argument

Additional information

Proof step 8 from proof B-postfix-weak-one (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ x ⊒ y ↔ (∃ z. z + y = x)

Rule argument

Additional information

Used simplifier rules: ⊦ a ' = x + a0 ' ↔ a = a0 ∧ x = []; (ws) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: be ', be0 '

Proof step 9 from proof B-postfix-weak-one (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof B-postfix-weak-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  be0.l ≠ be.l, be0 ≠ SF, be0 ≠ be, ∀ l. (be = SF ∨ be.l = l ⊃ be ';[]) ⊒ (be0.l = l ⊃ be0 ';[]) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x ⊒ []; (s)

Proof step 11 from proof B-postfix-weak-one (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 12:

  be0.l ≠ be.l, be0 ≠ SF, be0 ≠ be, (be = SF ∨ be.l = be0.l ⊃ be ';[]) ⊒ (be0.l = be0.l ⊃ be0 ';[]), ∀ l. (be = SF ∨ be.l = l ⊃ be ';[]) ⊒ (be0.l = l ⊃ be0 ';[]) ⊦

Rule argument

Additional information

Used terms: be0.l

Proof step 12 from proof B-postfix-weak-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  be0.l ≠ be.l, be0 ≠ SF, be0 ≠ be, (be = SF ⊃ SF ';[]) ⊒ be0 ', ∀ l. (be = SF ∨ be.l = l ⊃ be ';[]) ⊒ (be0.l = l ⊃ be0 ';[]) ⊦

Rule argument

Additional information

Proof step 13 from proof B-postfix-weak-one (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 14:

  be = SF, be0.l ≠ be.l, be0 ≠ SF, be0 ≠ be, (be = SF ⊃ SF ';[]) ⊒ be0 ', ∀ l. (be = SF ∨ be.l = l ⊃ be ';[]) ⊒ (be0.l = l ⊃ be0 ';[]) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ [] ⊒ x ↔ x = []; (s) ⊦ a ' ≠ []; (s) Used formulas: be = SF

Proof step 14 from proof B-postfix-weak-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  be0.l ≠ SF.l, be0 ≠ SF, SF ' ⊒ be0 ', ∀ l. SF ' ⊒ (be0.l = l ⊃ be0 ';[]) ⊦

Rule argument

Additional information

Proof step 15 from proof B-postfix-weak-one (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ x ⊒ y ↔ (∃ z. z + y = x)

Rule argument

Additional information

Used simplifier rules: ⊦ a ' = x + a0 ' ↔ a = a0 ∧ x = []; (ws) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: SF ', be0 '

Proof step 16 from proof B-postfix-weak-one (previous step) (back to tree)

A spec-lemma

Proof step 17 from proof B-postfix-weak-one (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 18:

  bel = be1 + bel0, (be = SF ∨ be.l = be1.l ⊃ be ';[]) ⊒ (be0 = SF ∨ be0.l = be1.l ⊃ be0 ';[]) + bel.filter(λ be. be = SF ∨ be.l = be1.l), ∀ l. (be = SF ∨ be.l = l ⊃ be ';[]) ⊒ (be0 = SF ∨ be0.l = l ⊃ be0 ';[]) + bel.filter(λ be. be = SF ∨ be.l = l) ⊦ be0 = be ∧ bel = []

Rule argument

Additional information

Used terms: be1.l

Proof step 18 from proof B-postfix-weak-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  (be = SF ∨ be.l = be1.l ⊃ be ';[]) ⊒ (be0 = SF ∨ be0.l = be1.l ⊃ be0 ';[]) + be1 ' + bel0.filter(λ be. be = SF ∨ be.l = be1.l), ∀ l. (be = SF ∨ be.l = l ⊃ be ';[]) ⊒ (be0 = SF ∨ be0.l = l ⊃ be0 ';[]) + (be1 = SF ∨ be1.l = l ⊃ be1 ';[]) + bel0.filter(λ be. be = SF ∨ be.l = l) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a + x = a ' + x; (s) ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s)

Proof step 19 from proof B-postfix-weak-one (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 20:

  be ' ⊒ (be0 = SF ∨ be0.l = be1.l ⊃ be0 ';[]) + be1 ' + bel0.filter(λ be. be = SF ∨ be.l = be1.l), ∀ l. (be = SF ∨ be.l = l ⊃ be ';[]) ⊒ (be0 = SF ∨ be0.l = l ⊃ be0 ';[]) + (be1 = SF ∨ be1.l = l ⊃ be1 ';[]) + bel0.filter(λ be. be = SF ∨ be.l = l), be = SF ∨ be.l = be1.l ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ [] ⊒ x ↔ x = []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 20 from proof B-postfix-weak-one (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 21:

  be ' ⊒ be0 ' + be1 ' + bel0.filter(λ be. be = SF ∨ be.l = be1.l), ∀ l. (be = SF ∨ be.l = l ⊃ be ';[]) ⊒ (be0 = SF ∨ be0.l = l ⊃ be0 ';[]) + (be1 = SF ∨ be1.l = l ⊃ be1 ';[]) + bel0.filter(λ be. be = SF ∨ be.l = l), be = SF ∨ be.l = be1.l, be0 = SF ∨ be0.l = be1.l ⊦

• Proof step 23:

  be0.l ≠ be1.l, be0 ≠ SF, be ' ⊒ [] + be1 ' + bel0.filter(λ be. be = SF ∨ be.l = be1.l), ∀ l. (be = SF ∨ be.l = l ⊃ be ';[]) ⊒ (be0 = SF ∨ be0.l = l ⊃ be0 ';[]) + (be1 = SF ∨ be1.l = l ⊃ be1 ';[]) + bel0.filter(λ be. be = SF ∨ be.l = l), be = SF ∨ be.l = be1.l ⊦

Rule argument

Additional information

Proof step 21 from proof B-postfix-weak-one (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

  ⊦ x ⊒ y ↔ (∃ z. z + y = x)

Rule argument

Additional information

Used simplifier rules: ⊦ x + a ' + y = a0 ' ↔ x = [] ∧ a = a0 ∧ y = []; (ws) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: be ', be0 ' + be1 ' + bel0.filter(λ be. be = SF ∨ be.l = be1.l)

Proof step 22 from proof B-postfix-weak-one (previous step) (back to tree)

A spec-lemma

Proof step 23 from proof B-postfix-weak-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  be0.l ≠ be1.l, be0 ≠ SF, be ' ⊒ be1 ' + bel0.filter(λ be. be = SF ∨ be.l = be1.l), ∀ l. (be = SF ∨ be.l = l ⊃ be ';[]) ⊒ (be0.l = l ⊃ be0 ';[]) + (be1 = SF ∨ be1.l = l ⊃ be1 ';[]) + bel0.filter(λ be. be = SF ∨ be.l = l), be = SF ∨ be.l = be1.l ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s)

Proof step 24 from proof B-postfix-weak-one (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

  ⊦ x ⊒ y ↔ (∃ z. z + y = x)

• Proof step 26:

  be0.l ≠ be1.l, be0 ≠ SF, ∀ l. (be = SF ∨ be.l = l ⊃ be ';[]) ⊒ (be0.l = l ⊃ be0 ';[]) + (be1 = SF ∨ be1.l = l ⊃ be1 ';[]) + bel0.filter(λ be. be = SF ∨ be.l = l), ∃ z. z + be1 ' + bel0.filter(λ be. be = SF ∨ be.l = be1.l) = be ', be = SF ∨ be.l = be1.l ⊦

Rule argument

Additional information

Used terms: be ', be1 ' + bel0.filter(λ be. be = SF ∨ be.l = be1.l)

Proof step 25 from proof B-postfix-weak-one (previous step) (back to tree)

A spec-lemma

Proof step 26 from proof B-postfix-weak-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  bel0.filter(λ be0. be0 = SF ∨ be0.l = be.l) = [], be0.l ≠ be.l, be0 ≠ SF, ∀ l. (be = SF ∨ be.l = l ⊃ be ';[]) ⊒ (be0.l = l ⊃ be0 ';[]) + (be = SF ∨ be.l = l ⊃ be ';[]) + bel0.filter(λ be. be = SF ∨ be.l = l) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + a ' + y = a0 ' ↔ x = [] ∧ a = a0 ∧ y = []; (ws)

Proof step 27 from proof B-postfix-weak-one (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 28:

  bel0.filter(λ be0. be0 = SF ∨ be0.l = be.l) = [], be0.l ≠ be.l, be0 ≠ SF, (be = SF ∨ be.l = be0.l ⊃ be ';[]) ⊒ (be0.l = be0.l ⊃ be0 ';[]) + (be = SF ∨ be.l = be0.l ⊃ be ';[]) + bel0.filter(λ be. be = SF ∨ be.l = be0.l) ⊦

Rule argument

Additional information

Used terms: be0.l

Proof step 28 from proof B-postfix-weak-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  bel0.filter(λ be0. be0 = SF ∨ be0.l = be.l) = [], be0.l ≠ be.l, be0 ≠ SF, (be = SF ⊃ SF ';[]) ⊒ be0 ' + (be = SF ⊃ SF ';[]) + bel0.filter(λ be. be = SF ∨ be.l = be0.l) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 29 from proof B-postfix-weak-one (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 30:

  bel0.filter(λ be0. be0 = SF ∨ be0.l = be.l) = [], be = SF, be0.l ≠ be.l, be0 ≠ SF, (be = SF ⊃ SF ';[]) ⊒ be0 ' + (be = SF ⊃ SF ';[]) + bel0.filter(λ be. be = SF ∨ be.l = be0.l) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ [] + x = x; (s) ⊦ [] ⊒ x ↔ x = []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used formulas: be = SF

Proof step 30 from proof B-postfix-weak-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  bel0.filter(λ be. be.l = SF.l) = [], be0.l ≠ SF.l, be0 ≠ SF, SF ' ⊒ be0 ' + SF ' + bel0.filter(λ be. be = SF ∨ be.l = be0.l) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 31 from proof B-postfix-weak-one (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

  ⊦ x ⊒ y ↔ (∃ z. z + y = x)

Rule argument

Additional information

Used simplifier rules: ⊦ x + a ' + y = a0 ' ↔ x = [] ∧ a = a0 ∧ y = []; (ws) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: SF ', be0 ' + SF ' + bel0.filter(λ be. be = SF ∨ be.l = be0.l)

Proof step 32 from proof B-postfix-weak-one (previous step) (back to tree)

A spec-lemma