Proof step 1 from proof isPropFO-delpos-eq-delfirst (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  bel -1l FO(l) ≠ bel -p n, isPropFO(n, l, bel) ⊦

Rule argument

Additional information

Proof step 2 from proof isPropFO-delpos-eq-delfirst (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ 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 4:

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

Rule argument

Additional information

Used terms: n, l, bel

Proof step 3 from proof isPropFO-delpos-eq-delfirst (previous step) (back to tree)

A spec-lemma

Proof step 4 from proof isPropFO-delpos-eq-delfirst (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

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

Rule argument

Additional information

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

Proof step 5 from proof isPropFO-delpos-eq-delfirst (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 6:

  (be + bel0)[n] = FO(l), be + bel0 ≠ [], (be + bel0) -1l FO(l) ≠ (be + bel0) -p n, n < #(be + bel0), ∀ m. m < n → (be + bel0)[m] ≠ SF ∧ ((be + bel0)[m].W? ∨ (be + bel0)[m].FO? → (be + bel0)[m].l ≠ l), ∀ n, l. ¬ ( bel0[n] = FO(l) ∧ bel0 -1l FO(l) ≠ bel0 -p n ∧ bel0 ≠ [] ∧ n < # bel0 ∧ (∀ m. m < n → bel0[m] ≠ SF ∧ (bel0[m].W? ∨ bel0[m].FO? → bel0[m].l ≠ l))) ⊦

Rule argument

Additional information

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

Proof step 6 from proof isPropFO-delpos-eq-delfirst (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  (be ' + bel0)[n] = FO(l), (be ' + bel0) -1l FO(l) ≠ (be ' + bel0) -p n, n ≤ # bel0, ∀ n0, l0. bel0[n0] ≠ FO(l0) ∨ bel0 -1l FO(l0) = bel0 -p n0 ∨ bel0 = [] ∨ ¬ n0 < # bel0 ∨ ¬(∀ m. m < n0 → bel0[m] ≠ SF ∧ (bel0[m].W? ∨ bel0[m].FO? → bel0[m].l ≠ l0)), ∀ m. m < n → (be ' + bel0)[m] ≠ SF ∧ ((be ' + bel0)[m].W? ∨ (be ' + bel0)[m].FO? → (be ' + bel0)[m].l ≠ l) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) 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) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s)

Proof step 7 from proof isPropFO-delpos-eq-delfirst (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 8:

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

Rule argument

Additional information

Used simplifier rules: Nat freely generated by 0, +1;; ⊦ (a ' + x)[0] = a; (s) ⊦ (a ' + x) -p 0 = x; (s) ⊦ 0 ≤ m; (s) ⊦ ¬ n < 0; (s) ⊦ (a ' + x) -1l a = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 8 from proof isPropFO-delpos-eq-delfirst (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

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

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 +1 = m + 1; (s) ⊦ m + 1 ≤ n ↔ m < n; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a + x = a ' + x; (s) ⊦ (a ' + x) -p (n + 1) = a + (x -p n); (s) ⊦ (a ' + x)[n + 1] = x[n]; (s)

Proof step 9 from proof isPropFO-delpos-eq-delfirst (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ a ≠ b → (b ' + x) -1l a = b ' + (x -1l a)

• Proof step 11:

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

• Proof step 13:

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

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: FO(l), be, bel0

Proof step 10 from proof isPropFO-delpos-eq-delfirst (previous step) (back to tree)

A spec-lemma

Proof step 11 from proof isPropFO-delpos-eq-delfirst (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

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

Proof step 12 from proof isPropFO-delpos-eq-delfirst (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < 0; (s) ⊦ FO(l) ≠ SF; (s) ⊦ ¬ FO(l).W?; (s) ⊦ FO(l).FO?; (s) ⊦ (a ' + x)[0] = a; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ FO(l).l = l; (s) Used terms: 0

Proof step 13 from proof isPropFO-delpos-eq-delfirst (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

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

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws)

Proof step 14 from proof isPropFO-delpos-eq-delfirst (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

Used terms: n1, l

Proof step 15 from proof isPropFO-delpos-eq-delfirst (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

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

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s) ⊦ m < n → n ≠ 0; (s) trans-Nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 16 from proof isPropFO-delpos-eq-delfirst (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

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