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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  isPropFO(n, l, bel), ¬ bel ⊒w bel -p n ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  isPropFO(n, l, bel), ¬ bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ (bel -p n).filter(λ be. be = SF ∨ be.l = l0) ⊦

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);

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

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

  l = l0, isPropFO(n, l, bel), ¬ bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ (bel -p n).filter(λ be. be = SF ∨ be.l = l0) ⊦

• Proof step 11:

  l ≠ l0, isPropFO(n, l, bel), ¬ bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ (bel -p n).filter(λ be. be = SF ∨ be.l = l0) ⊦

Rule argument

Additional information

Used formulas: l = l0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  isPropFO(n, l0, bel), ¬ bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ (bel -p n).filter(λ be. be = SF ∨ be.l = l0) ⊦

Rule argument

Additional information

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 6:

  ⊦ isPropFO(n, l, bel) → bel -p n |SF l = (bel |SF l).tail

• Proof step 7:

  isPropFO(n, l0, bel), ¬ bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ (bel -p n).filter(λ be. be = SF ∨ be.l = l0), isPropFO(n, l0, bel) → bel -p n |SF l0 = (bel |SF l0).tail ⊦

Rule argument

Additional information

Used terms: n, l0, bel

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

Lemma isPropFO-restrict-SF-l-head

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  (bel -p n).filter(λ be. be = SF ∨ be.l = l0) = (bel.filter(λ be. be = SF ∨ be.l = l0)).tail, isPropFO(n, l0, bel), ¬ bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ (bel -p n).filter(λ be. be = SF ∨ be.l = l0) ⊦

Rule argument

Additional information

Used simplifier rules: B-restrict-SF-l: ⊦ bel |SF l = bel.filter(λ be. be = SF ∨ be.l = l);

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 9:

  (bel -p n).filter(λ be. be = SF ∨ be.l = l0) = bel0, bel.filter(λ be. be = SF ∨ be.l = l0) = be0 + bel0, bel.filter(λ be. be = SF ∨ be.l = l0) ≠ [], isPropFO(n, l0, bel), ¬ bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ (bel -p n).filter(λ be. be = SF ∨ be.l = l0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ x.filter(p) = [] → (x -p n).filter(p) = []; (s) ⊦ x ⊒ []; (s) x ≠ [] ⊦ a = x.head ∧ y = x.tail ↔ x = a + y; (elim) Used terms: bel.filter(λ be. be = SF ∨ be.l = l0), be0, bel0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  bel.filter(λ be. be = SF ∨ be.l = l0) = be0 ' + (bel -p n).filter(λ be. be = SF ∨ be.l = l0), bel.filter(λ be. be = SF ∨ be.l = l0) ≠ [], isPropFO(n, l0, bel), be0 ∈ bel, ¬ bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ (bel -p n).filter(λ be. be = SF ∨ be.l = l0), be0 = SF ∨ be0.l = l0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ x.filter(p) ↔ a ∈ x ∧ p(a); (s) a: ⊦ (x + y) + z = x + y + z; from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ a + x = a ' + x; (s)

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

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ n < # x ∧ ¬ p(x[n]) → (x -p n).filter(p) = x.filter(p)

• Proof step 13:

  l ≠ l0, isPropFO(n, l, bel), ¬ bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ (bel -p n).filter(λ be. be = SF ∨ be.l = l0) ⊦ n < # bel ∧ ¬(bel[n] = SF ∨ bel[n].l = l0)

Rule argument

Additional information

Used simplifier rules: ⊦ x ⊒ x; (s) Used terms: bel, n, λ be. be = SF ∨ be.l = l0

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  bel ≠ [], l ≠ l0, n < # bel, isPropFO(n, l, bel), ¬ bel.filter(λ be. be = SF ∨ be.l = l0) ⊒ (bel -p n).filter(λ be. be = SF ∨ be.l = l0) ⊦ bel[n].l ≠ l0 ∧ bel[n] ≠ SF

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ x ⊒ x; (s) ⊦ # x ≤ n → x -p n = x; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ isPropFO(n, l, bel) ↔ n < # bel ∧ bel[n] = FO(l) ∧ (∀ m. m < n → bel[m] ≠ SF ∧ (bel[m].W? ∨ bel[m].FO? → bel[m].l ≠ l))

Rule argument

Additional information

Used simplifier rules: ⊦ FO(l).l = l; (s) ⊦ FO(l) ≠ SF; (s) Used terms: n, l, bel

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

Lemma isPropFO-def