Proof step 1 from proof isPropFO-restrict-SF-l-head (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

Proof step 2 from proof isPropFO-restrict-SF-l-head (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

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

Proof step 3 from proof isPropFO-restrict-SF-l-head (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  ((be + bel0) -p n).filter(λ be. be = SF ∨ be.l = l) ≠ ((be + bel0).filter(λ be. be = SF ∨ be.l = l)).tail, isPropFO(n, l, be + bel0), ∀ n, l. ¬((bel0 -p n).filter(λ be. be = SF ∨ be.l = l) ≠ (bel0.filter(λ be. be = SF ∨ be.l = l)).tail ∧ isPropFO(n, l, bel0)) ⊦

Rule argument

Additional information

Used simplifier rules: isPropFO-empty: ⊦ ¬ isPropFO(n, l, []); List('a) freely generated by [], +;; ⊦ [] -p n = []; (s) ⊦ [].filter(p) = []; (s)

Proof step 4 from proof isPropFO-restrict-SF-l-head (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ((be ' + bel0) -p n).filter(λ be. be = SF ∨ be.l = l) ≠ ((be = SF ∨ be.l = l ⊃ be ';[]) + bel0.filter(λ be. be = SF ∨ be.l = l)).tail, isPropFO(n, l, be ' + bel0), ∀ n0, l0. (bel0 -p n0).filter(λ be. be = SF ∨ be.l = l0) = (bel0.filter(λ be. be = SF ∨ be.l = l0)).tail ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

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

Proof step 5 from proof isPropFO-restrict-SF-l-head (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 6:

  ((be ' + bel0) -p n).filter(λ be. be = SF ∨ be.l = l) ≠ (be ' + bel0.filter(λ be. be = SF ∨ be.l = l)).tail, isPropFO(n, l, be ' + bel0), ∀ n0, l0. (bel0 -p n0).filter(λ be. be = SF ∨ be.l = l0) = (bel0.filter(λ be. be = SF ∨ be.l = l0)).tail ∨ ¬ isPropFO(n0, l0, bel0), be = SF ∨ be.l = l ⊦

• Proof step 15:

  ((be ' + bel0) -p n).filter(λ be. be = SF ∨ be.l = l) ≠ ([] + bel0.filter(λ be. be = SF ∨ be.l = l)).tail, be.l ≠ l, be ≠ SF, isPropFO(n, l, be ' + bel0), ∀ n0, l0. (bel0 -p n0).filter(λ be. be = SF ∨ be.l = l0) = (bel0.filter(λ be. be = SF ∨ be.l = l0)).tail ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

Proof step 6 from proof isPropFO-restrict-SF-l-head (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ((be ' + bel0) -p n).filter(λ be0. be0 = SF ∨ be0.l = be.l) ≠ bel0.filter(λ be0. be0 = SF ∨ be0.l = be.l), be ≠ SF, isPropFO(n, be.l, be ' + bel0), ∀ n0, l0. (bel0 -p n0).filter(λ be. be = SF ∨ be.l = l0) = (bel0.filter(λ be. be = SF ∨ be.l = l0)).tail ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

Used simplifier rules: isPropFO-leading-SF: ⊦ ¬ isPropFO(n, l, SF ' + bel); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x).tail = x; (s)

Proof step 7 from proof isPropFO-restrict-SF-l-head (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 8:

  n = n1 +1, ((be ' + bel0) -p n).filter(λ be0. be0 = SF ∨ be0.l = be.l) ≠ bel0.filter(λ be0. be0 = SF ∨ be0.l = be.l), be ≠ SF, isPropFO(n, be.l, be ' + bel0), ∀ n0, l0. (bel0 -p n0).filter(λ be. be = SF ∨ be.l = l0) = (bel0.filter(λ be. be = SF ∨ be.l = l0)).tail ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

Used simplifier rules: Nat freely generated by 0, +1;; ⊦ (a ' + x) -p 0 = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 8 from proof isPropFO-restrict-SF-l-head (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  be ' + (bel0 -p n1).filter(λ be0. be0 = SF ∨ be0.l = be.l) ≠ bel0.filter(λ be0. be0 = SF ∨ be0.l = be.l), be ≠ SF, isPropFO(n1 + 1, be.l, be ' + bel0), ∀ n0, l0. (bel0 -p n0).filter(λ be. be = SF ∨ be.l = l0) = (bel0.filter(λ be. be = SF ∨ be.l = l0)).tail ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ a + x = a ' + x; (s) ⊦ (a ' + x) -p (n + 1) = a + (x -p n); (s)

Proof step 9 from proof isPropFO-restrict-SF-l-head (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

  (be ' + bel0)[n1 + 1] = FO(be.l), be ' + (bel0 -p n1).filter(λ be0. be0 = SF ∨ be0.l = be.l) ≠ bel0.filter(λ be0. be0 = SF ∨ be0.l = be.l), be ≠ SF, n1 + 1 < #(be ' + bel0), ∀ n0, l0. (bel0 -p n0).filter(λ be. be = SF ∨ be.l = l0) = (bel0.filter(λ be. be = SF ∨ be.l = l0)).tail ∨ ¬ isPropFO(n0, l0, bel0), ∀ m. m < n1 + 1 → (be ' + bel0)[m] ≠ SF ∧ ((be ' + bel0)[m].W? ∨ (be ' + bel0)[m].FO? → (be ' + bel0)[m].l ≠ be.l) ⊦

Rule argument

Additional information

Used terms: n1 + 1, be.l, be ' + bel0

Proof step 10 from proof isPropFO-restrict-SF-l-head (previous step) (back to tree)

Lemma isPropFO-def

Proof step 11 from proof isPropFO-restrict-SF-l-head (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  bel0[n1] = FO(be.l), be ' + (bel0 -p n1).filter(λ be0. be0 = SF ∨ be0.l = be.l) ≠ bel0.filter(λ be0. be0 = SF ∨ be0.l = be.l), be ≠ SF, bel0 ≠ [], n1 < # bel0, ∀ m. ¬ n1 < m → (be ' + bel0)[m] ≠ SF ∧ ((be ' + bel0)[m].W? ∨ (be ' + bel0)[m].FO? → (be ' + bel0)[m].l ≠ be.l), ∀ n0, l0. (bel0 -p n0).filter(λ be. be = SF ∨ be.l = l0) = (bel0.filter(λ be. be = SF ∨ be.l = l0)).tail ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ (a ' + x)[n + 1] = x[n]; (s)

Proof step 12 from proof isPropFO-restrict-SF-l-head (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 13:

  bel0[n1] = FO(be.l), be ' + (bel0 -p n1).filter(λ be0. be0 = SF ∨ be0.l = be.l) ≠ bel0.filter(λ be0. be0 = SF ∨ be0.l = be.l), be ≠ SF, bel0 ≠ [], n1 < # bel0, ¬ n1 < 0 → (be ' + bel0)[0] ≠ SF ∧ ((be ' + bel0)[0].W? ∨ (be ' + bel0)[0].FO? → (be ' + bel0)[0].l ≠ be.l), ∀ n0, l0. (bel0 -p n0).filter(λ be. be = SF ∨ be.l = l0) = (bel0.filter(λ be. be = SF ∨ be.l = l0)).tail ∨ ¬ isPropFO(n0, l0, bel0), ∀ m. ¬ n1 < m → (be ' + bel0)[m] ≠ SF ∧ ((be ' + bel0)[m].W? ∨ (be ' + bel0)[m].FO? → (be ' + bel0)[m].l ≠ be.l) ⊦

Rule argument

Additional information

Used terms: 0

Proof step 13 from proof isPropFO-restrict-SF-l-head (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  bel0[n1] = FO(be.l), be ' + (bel0 -p n1).filter(λ be0. be0 = SF ∨ be0.l = be.l) ≠ bel0.filter(λ be0. be0 = SF ∨ be0.l = be.l), be ≠ SF, bel0 ≠ [], n1 < # bel0, ¬ be.FO?, ¬ be.W?, ∀ m. ¬ n1 < m → (be ' + bel0)[m] ≠ SF ∧ ((be ' + bel0)[m].W? ∨ (be ' + bel0)[m].FO? → (be ' + bel0)[m].l ≠ be.l), ∀ n0, l0. (bel0 -p n0).filter(λ be. be = SF ∨ be.l = l0) = (bel0.filter(λ be. be = SF ∨ be.l = l0)).tail ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

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

Proof step 14 from proof isPropFO-restrict-SF-l-head (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

Used simplifier rules: Bevent freely generated by SF, W, FO;; ⊦ FO(l).l = l; (s) ⊦ FO(l) ≠ SF; (s) ⊦ FO(l).FO?; (s) ⊦ W(l, v).l = l; (s) ⊦ W(l, v) ≠ SF; (s) ⊦ ¬ W(l, v).FO?; (s) ⊦ W(l, v).W?; (s)

Proof step 15 from proof isPropFO-restrict-SF-l-head (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  ((be ' + bel0) -p n).filter(λ be. be = SF ∨ be.l = l) ≠ (bel0.filter(λ be. be = SF ∨ be.l = l)).tail, be.l ≠ l, be ≠ SF, isPropFO(n, l, be ' + bel0), ∀ n0, l0. (bel0 -p n0).filter(λ be. be = SF ∨ be.l = l0) = (bel0.filter(λ be. be = SF ∨ be.l = l0)).tail ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

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

Proof step 16 from proof isPropFO-restrict-SF-l-head (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 17:

  n = 0, ((be ' + bel0) -p n).filter(λ be. be = SF ∨ be.l = l) ≠ (bel0.filter(λ be. be = SF ∨ be.l = l)).tail, be.l ≠ l, be ≠ SF, isPropFO(n, l, be ' + bel0), ∀ n0, l0. (bel0 -p n0).filter(λ be. be = SF ∨ be.l = l0) = (bel0.filter(λ be. be = SF ∨ be.l = l0)).tail ∨ ¬ isPropFO(n0, l0, bel0) ⊦

• Proof step 20:

  n = n1 +1, ((be ' + bel0) -p n).filter(λ be. be = SF ∨ be.l = l) ≠ (bel0.filter(λ be. be = SF ∨ be.l = l)).tail, be.l ≠ l, be ≠ SF, isPropFO(n, l, be ' + bel0), ∀ n0, l0. (bel0 -p n0).filter(λ be. be = SF ∨ be.l = l0) = (bel0.filter(λ be. be = SF ∨ be.l = l0)).tail ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

Used simplifier rules: Nat freely generated by 0, +1;;

Proof step 17 from proof isPropFO-restrict-SF-l-head (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  bel0.filter(λ be. be = SF ∨ be.l = l) ≠ (bel0.filter(λ be. be = SF ∨ be.l = l)).tail, be.l ≠ l, be ≠ SF, isPropFO(0, l, be ' + bel0), ∀ n0, l0. (bel0 -p n0).filter(λ be. be = SF ∨ be.l = l0) = (bel0.filter(λ be. be = SF ∨ be.l = l0)).tail ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x) -p 0 = x; (s)

Proof step 18 from proof isPropFO-restrict-SF-l-head (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ 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: ⊦ (a ' + x)[0] = a; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ m +1 = m + 1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ m + 1 ≠ 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ ¬ n < 0; (s) ⊦ FO(l) ≠ SF; (s) ⊦ FO(l).l = l; (s) Used terms: 0, l, be ' + bel0

Proof step 19 from proof isPropFO-restrict-SF-l-head (previous step) (back to tree)

Lemma isPropFO-def

Proof step 20 from proof isPropFO-restrict-SF-l-head (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  (bel0 -p n1).filter(λ be. be = SF ∨ be.l = l) ≠ (bel0.filter(λ be. be = SF ∨ be.l = l)).tail, be.l ≠ l, be ≠ SF, isPropFO(n1, l, bel0), ∀ n0, l0. (bel0 -p n0).filter(λ be. be = SF ∨ be.l = l0) = (bel0.filter(λ be. be = SF ∨ be.l = l0)).tail ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

Used simplifier rules: isPropFO-rec: ⊦ be.l ≠ l ∧ be ≠ SF → (isPropFO(n + 1, l, be ' + bel) ↔ isPropFO(n, l, bel)); c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m +1 = m + 1; (s) ⊦ [] + x = x; (s) ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s) ⊦ a + x = a ' + x; (s) ⊦ (a ' + x) -p (n + 1) = a + (x -p n); (s)

Proof step 21 from proof isPropFO-restrict-SF-l-head (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n1, l