Proof step 1 from proof isPropFO-other-FO-in-delpos (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(FO(l0) ∈ bel -p n ↔ FO(l0) ∈ bel), l ≠ l0, isPropFO(n, l, bel) ⊦

Rule argument

Additional information

Proof step 2 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ a ∈ x ↔ (∃ n. n < # x ∧ x[n] = a)

• Proof step 4:

  l ≠ l0, isPropFO(n, l, bel) ⊦ (∃ n0. n0 < #(bel -p n) ∧ (bel -p n)[n0] = FO(l0)) ↔ FO(l0) ∈ bel

Rule argument

Additional information

Used terms: FO(l0), bel -p n

Proof step 3 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

A spec-lemma

Proof step 4 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ a ∈ x ↔ (∃ n. n < # x ∧ x[n] = a)

• Proof step 6:

  l ≠ l0, isPropFO(n, l, bel) ⊦ (∃ n0. n0 < #(bel -p n) ∧ (bel -p n)[n0] = FO(l0)) ↔ (∃ n. n < # bel ∧ bel[n] = FO(l0))

Rule argument

Additional information

Used terms: FO(l0), bel

Proof step 5 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

A spec-lemma

Proof step 6 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 7:

  l ≠ l0, isPropFO(n, l, bel), ∃ n0. n0 < #(bel -p n) ∧ (bel -p n)[n0] = FO(l0) ⊦ ∃ n. n < # bel ∧ bel[n] = FO(l0)

• Proof step 16:

  l ≠ l0, isPropFO(n, l, bel), ∃ n. n < # bel ∧ bel[n] = FO(l0) ⊦ ∃ n0. n0 < #(bel -p n) ∧ (bel -p n)[n0] = FO(l0)

Rule argument

Additional information

Proof step 7 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  (bel -p n)[n0] = FO(l0), bel -p n ≠ [], l ≠ l0, n0 < #(bel -p n), isPropFO(n, l, bel) ⊦ ∃ n. n < # bel ∧ bel[n] = FO(l0)

Rule argument

Additional information

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

Proof step 8 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

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

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

Rule argument

Additional information

Used terms: n, l, bel

Proof step 9 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

Lemma isPropFO-def

Proof step 10 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ n + 1 < # x ∧ m < # x → (x -p m)[n] = (n < m ⊃ x[n];x[n + 1]); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n0 ≤ n ⊦ m < n - n0 ↔ m + n0 < n; (s) ⊦ [] -p n = []; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ n < # x → #(x -p n) = # x - 1; (s)

Proof step 11 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 12:

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

• Proof step 14:

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

Rule argument

Additional information

Proof step 12 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

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

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 13 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: n0

Proof step 14 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 15 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: n0 + 1

Proof step 16 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  bel[n0] = FO(l0), bel ≠ [], l ≠ l0, n0 < # bel, isPropFO(n, l, bel) ⊦ ∃ n0. n0 < #(bel -p n) ∧ (bel -p n)[n0] = FO(l0)

Rule argument

Additional information

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

Proof step 17 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

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

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

Rule argument

Additional information

Used terms: n, l, bel

Proof step 18 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

Lemma isPropFO-def

Proof step 19 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  bel[n0] = FO(l0), bel[n] = FO(l), bel ≠ [], l ≠ l0, n0 < # bel, n < # bel, ∀ m. m < n → bel[m] ≠ SF ∧ (bel[m].W? ∨ bel[m].FO? → bel[m].l ≠ l) ⊦ ∃ n1. n1 + 1 < # bel ∧ (n1 < n ⊃ bel[n1];bel[n1 + 1]) = FO(l0)

Rule argument

Additional information

Used simplifier rules: ⊦ n + 1 < # x ∧ m < # x → (x -p m)[n] = (n < m ⊃ x[n];x[n + 1]); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n0 ≤ n ⊦ m < n - n0 ↔ m + n0 < n; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ n < # x → #(x -p n) = # x - 1; (s)

Proof step 20 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 21:

  bel[n] = FO(l), bel[n0] = FO(l0), bel ≠ [], l ≠ l0, n < # bel, n0 < # bel, ∀ m. m < n → bel[m] ≠ SF ∧ (bel[m].W? ∨ bel[m].FO? → bel[m].l ≠ l) ⊦ ∃ n1. n1 + 1 < # bel ∧ (n1 < n ⊃ bel[n1];bel[n1 + 1]) = FO(l0), n0 + 1 < # bel ∧ (n0 < n ⊃ bel[n0];bel[n0 + 1]) = FO(l0)

Rule argument

Additional information

Used terms: n0

Proof step 21 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  bel[n0] = FO(l0), bel[n] = FO(l), bel ≠ [], l ≠ l0, n0 < # bel, n < # bel, ∀ m. m < n → bel[m] ≠ SF ∧ (bel[m].W? ∨ bel[m].FO? → bel[m].l ≠ l) ⊦ ∃ n1. n1 + 1 < # bel ∧ (n1 < n ⊃ bel[n1];bel[n1 + 1]) = FO(l0), n0 + 1 < # bel ∧ (n0 < n ⊃ FO(l0);bel[n0 + 1]) = FO(l0)

Rule argument

Additional information

Proof step 22 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 23:

  bel[n] = FO(l), bel[n0] = FO(l0), bel ≠ [], l ≠ l0, n < # bel, n0 < # bel, ¬ n0 < n, ∀ m. m < n → bel[m] ≠ SF ∧ (bel[m].W? ∨ bel[m].FO? → bel[m].l ≠ l) ⊦ ∃ n1. n1 + 1 < # bel ∧ (n1 < n ⊃ bel[n1];bel[n1 + 1]) = FO(l0), n0 + 1 < # bel ∧ (n0 < n ⊃ FO(l0);bel[n0 + 1]) = FO(l0)

Rule argument

Additional information

Used simplifier rules: ⊦ FO(l) = FO(l0) ↔ l = l0; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic trans-Nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic ⊦ m + 1 ≠ 0; (s) ⊦ m < n → n ≠ 0; (s) ⊦ m < n → (n ≤ m + 1 ↔ n = m + 1); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m < n → (n ≤ m ↔ false); (s) Used formulas: n0 < n

Proof step 23 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  bel[n0] = FO(l0), bel[n] = FO(l), bel ≠ [], l ≠ l0, n0 < # bel, n < # bel, n ≤ n0, ∀ m. m < n → bel[m] ≠ SF ∧ (bel[m].W? ∨ bel[m].FO? → bel[m].l ≠ l) ⊦ ∃ n1. n1 + 1 < # bel ∧ (n1 < n ⊃ bel[n1];bel[n1 + 1]) = FO(l0), n0 + 1 < # bel ∧ bel[n0 + 1] = FO(l0)

Rule argument

Additional information

Used simplifier rules: fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 24 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

User applied rule exists right

And obtained the following new goals

• Proof step 25:

  bel[n] = FO(l), bel[n0] = FO(l0), bel ≠ [], l ≠ l0, n < # bel, n0 < # bel, n ≤ n0, ∀ m. m < n → bel[m] ≠ SF ∧ (bel[m].W? ∨ bel[m].FO? → bel[m].l ≠ l) ⊦ ∃ n1. n1 + 1 < # bel ∧ (n1 < n ⊃ bel[n1];bel[n1 + 1]) = FO(l0), n0 + 1 < # bel ∧ bel[n0 + 1] = FO(l0), (n0 - 1) + 1 < # bel ∧ (n0 - 1 < n ⊃ bel[n0 - 1];bel[(n0 - 1) + 1]) = FO(l0)

Rule argument

Additional information

Used terms: n0 - 1

Proof step 25 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 26:

  bel[n0] = FO(l0), bel[n] = FO(l), (n0 - 1 < n ⊃ bel[n0 - 1];bel[(n0 - 1) + 1]) ≠ FO(l0), bel ≠ [], l ≠ l0, n0 < # bel, n < # bel, n ≤ n0, ∀ m. m < n → bel[m] ≠ SF ∧ (bel[m].W? ∨ bel[m].FO? → bel[m].l ≠ l) ⊦ ∃ n1. n1 + 1 < # bel ∧ (n1 < n ⊃ bel[n1];bel[n1 + 1]) = FO(l0), n0 + 1 < # bel ∧ bel[n0 + 1] = FO(l0)

Rule argument

Additional information

Used simplifier rules: ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic trans-Nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic ⊦ m < n → n ≠ 0; (s) leprf: ⊦ m ≤ m - 1 → m = 0; (forward) from specification nat let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat ⊦ m ≤ 0 ↔ m = 0; (s) ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s) lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ x ≠ [] → x[0] = x.head; (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 ⊦ 0 ≤ m; (s) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ ¬ n < 0; (s) ⊦ FO(l) = FO(l0) ↔ l = l0; (s)

Proof step 26 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 27:

  bel[n] = FO(l), bel[n0] = FO(l0), bel[n0 - 1] ≠ FO(l0), bel ≠ [], l ≠ l0, n < # bel, n0 < # bel, n0 - 1 < n, n ≤ n0, ∀ m. m < n → bel[m] ≠ SF ∧ (bel[m].W? ∨ bel[m].FO? → bel[m].l ≠ l) ⊦ ∃ n1. n1 + 1 < # bel ∧ (n1 < n ⊃ bel[n1];bel[n1 + 1]) = FO(l0), n0 + 1 < # bel ∧ bel[n0 + 1] = FO(l0)

• Proof step 29:

  bel[n] = FO(l), bel[n0] = FO(l0), bel[(n0 - 1) + 1] ≠ FO(l0), bel ≠ [], l ≠ l0, n < # bel, n0 < # bel, n ≤ n0, ¬ n0 - 1 < n, ∀ m. m < n → bel[m] ≠ SF ∧ (bel[m].W? ∨ bel[m].FO? → bel[m].l ≠ l) ⊦ ∃ n1. n1 + 1 < # bel ∧ (n1 < n ⊃ bel[n1];bel[n1 + 1]) = FO(l0), n0 + 1 < # bel ∧ bel[n0 + 1] = FO(l0)

Rule argument

Additional information

Proof step 27 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  bel[n] = FO(l), bel[n0] = FO(l0), bel[n0 - 1] ≠ FO(l0), bel ≠ [], l ≠ l0, n < # bel, n0 < # bel, n0 - 1 < n, (n0 - 1) + 1 < # bel, n ≤ n0, ∀ m. m < n → bel[m] ≠ SF ∧ (bel[m].W? ∨ bel[m].FO? → bel[m].l ≠ l) ⊦ ∃ n1. n1 + 1 < # bel ∧ (n1 < n ⊃ bel[n1];bel[n1 + 1]) = FO(l0), n0 + 1 < # bel ∧ bel[n0 + 1] = FO(l0)

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m < n → ¬ n < m; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ m < n → n ≠ 0; (s) ⊦ m ≤ 0 ↔ m = 0; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ x ≠ [] → x[0] = x.head; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ ¬ n < n; (s) ⊦ m +1 = m + 1; (s) trans-Nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat 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 28 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m + 1 ≠ 0; (s) ⊦ m < n → (n ≤ m + 1 ↔ n = m + 1); (s) eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic trans-Nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) ⊦ m +1 = m + 1; (s) ⊦ ¬ n < n; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ FO(l) = FO(l0) ↔ l = l0; (s) ⊦ x ≠ [] → x[0] = x.head; (s) ⊦ m ≤ 0 ↔ m = 0; (s) ⊦ m < n → n ≠ 0; (s) n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: n0, m0

Proof step 29 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  bel[n0] = FO(l0), bel[n] = FO(l), bel[(n0 - 1) + 1] ≠ FO(l0), bel ≠ [], l ≠ l0, n0 < # bel, n < # bel, n ≤ n0, n ≤ n0 - 1, ∀ m. m < n → bel[m] ≠ SF ∧ (bel[m].W? ∨ bel[m].FO? → bel[m].l ≠ l) ⊦ ∃ n1. n1 + 1 < # bel ∧ (n1 < n ⊃ bel[n1];bel[n1 + 1]) = FO(l0), n0 + 1 < # bel ∧ bel[n0 + 1] = FO(l0)

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 30 from proof isPropFO-other-FO-in-delpos (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

Used simplifier rules: Nat freely generated by 0, +1;; ⊦ m +1 = m + 1; (s) ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s) ⊦ n + 0 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m ≤ 0 ↔ m = 0; (s) ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s) lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ x ≠ [] → x[0] = x.head; (s) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ 0 ≤ m; (s) ⊦ ¬ n < 0; (s) ⊦ FO(l) = FO(l0) ↔ l = l0; (s)