Proof step 1 from proof SFTrainling-prop-FO (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  SFTrailing(bq), isPropFO(n, l, bq(t)), ¬ SFTrailing(bq(t := bq(t) -p n)) ⊦

Rule argument

Additional information

Proof step 2 from proof SFTrainling-prop-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  (t = t0 ⊃ bq(t0) -p n;bq(t0)) ≠ [], isPropFO(n, l, bq(t)), SF ∈ (t = t0 ⊃ bq(t0) -p n;bq(t0)).butlast, SF ∈ (t = t0 ⊃ bq(t0) -p n;bq(t0)), ∀ t. bq(t) = [] ∨ ¬ SF ∈ bq(t).butlast ⊦

Rule argument

Additional information

Used simplifier rules: SFTrailing: ⊦ SFTrailing(bq) ↔ (∀ t. bq(t) = [] ∨ ¬ SF ∈ bq(t).butlast); bin-01: x ≠ [] ⊦ a ∈ x.butlast → a ∈ x; (forward) from specification list-last

Proof step 3 from proof SFTrainling-prop-FO (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 4:

  t = t0, bq(t0) -p n ≠ [], isPropFO(n, l, bq(t)), SF ∈ (t = t0 ⊃ bq(t0) -p n;bq(t0)), SF ∈ (t = t0 ⊃ bq(t0) -p n;bq(t0)).butlast, ∀ t. bq(t) = [] ∨ ¬ SF ∈ bq(t).butlast ⊦

• Proof step 18:

  bq(t0) ≠ [], t ≠ t0, isPropFO(n, l, bq(t)), SF ∈ (t = t0 ⊃ bq(t0) -p n;bq(t0)), SF ∈ (t = t0 ⊃ bq(t0) -p n;bq(t0)).butlast, ∀ t. bq(t) = [] ∨ ¬ SF ∈ bq(t).butlast ⊦

Rule argument

Additional information

Proof step 4 from proof SFTrainling-prop-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  bq(t0) -p n ≠ [], isPropFO(n, l, bq(t0)), SF ∈ (bq(t0) -p n).butlast, SF ∈ bq(t0), ∀ t. bq(t) = [] ∨ ¬ SF ∈ bq(t).butlast ⊦

Rule argument

Additional information

Used simplifier rules: isPropFO-SF-in-delpos: ⊦ isPropFO(n, l, bel) → (SF ∈ bel -p n ↔ SF ∈ bel); bin-01: x ≠ [] ⊦ a ∈ x.butlast → a ∈ x; (forward) from specification list-last

Proof step 5 from proof SFTrainling-prop-FO (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 6:

  bq(t0) -p n ≠ [], isPropFO(n, l, bq(t0)), SF ∈ bq(t0), SF ∈ (bq(t0) -p n).butlast, bq(t0) = [] ∨ ¬ SF ∈ bq(t0).butlast ⊦

Rule argument

Additional information

Used terms: t0

Proof step 6 from proof SFTrainling-prop-FO (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 7:

  bq(t0) -p n ≠ [], isPropFO(n, l, bq(t0)), SF ∈ (bq(t0) -p n).butlast, SF ∈ bq(t0), ¬ SF ∈ bq(t0).butlast ⊦

Rule argument

Additional information

Used simplifier rules: bin-01: x ≠ [] ⊦ a ∈ x.butlast → a ∈ x; (forward) from specification list-last ⊦ [] -p n = []; (s)

Proof step 7 from proof SFTrainling-prop-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  SF = bq(t0).last, bq(t0) -p n ≠ [], isPropFO(n, l, bq(t0)), SF ∈ bq(t0), SF ∈ (bq(t0) -p n).butlast, ¬ SF ∈ bq(t0).butlast ⊦

Rule argument

Additional information

Used simplifier rules: bin-02: ⊦ ¬ a ∈ x.butlast ∧ a ∈ x → a = x.last; (forward) from specification list-last

Proof step 8 from proof SFTrainling-prop-FO (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:

  SF = bq(t0).last, bq(t0)[n] = FO(l), bq(t0) -p n ≠ [], n < # bq(t0), SF ∈ (bq(t0) -p n).butlast, SF ∈ bq(t0), ¬ SF ∈ bq(t0).butlast, ∀ m. m < n → bq(t0)[m] ≠ SF ∧ (bq(t0)[m].W? ∨ bq(t0)[m].FO? → bq(t0)[m].l ≠ l) ⊦

Rule argument

Additional information

Used terms: n, l, bq(t0)

Proof step 9 from proof SFTrainling-prop-FO (previous step) (back to tree)

Lemma isPropFO-def

Proof step 10 from proof SFTrainling-prop-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  SF = bq(t0).last, bq(t0)[n] = FO(l), bq(t0) -p n ≠ [], bq(t0) ≠ [], n < # bq(t0), SF ∈ (bq(t0) -p n).butlast, ¬ SF ∈ bq(t0).butlast, ∀ m. m < n → bq(t0)[m] ≠ SF ∧ (bq(t0)[m].W? ∨ bq(t0)[m].FO? → bq(t0)[m].l ≠ l) ⊦

Rule argument

Additional information

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

Proof step 11 from proof SFTrainling-prop-FO (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 12:

  bq(t0) -p n = bel + be ', SF = bq(t0).last, bq(t0)[n] = FO(l), bq(t0) -p n ≠ [], bq(t0) ≠ [], n < # bq(t0), SF ∈ bel, ¬ SF ∈ bq(t0).butlast, ∀ m. m < n → bq(t0)[m] ≠ SF ∧ (bq(t0)[m].W? ∨ bq(t0)[m].FO? → bq(t0)[m].l ≠ l) ⊦

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: bq(t0) -p n, be, bel

Proof step 12 from proof SFTrainling-prop-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  bq(t0) -p n = bel + be ', SF = bq(t0).last, bq(t0)[n] = FO(l), bq(t0) ≠ [], n < # bq(t0), SF ∈ bel, ¬ SF ∈ bq(t0).butlast, ∀ m. m < n → bq(t0)[m] ≠ SF ∧ (bq(t0)[m].W? ∨ bq(t0)[m].FO? → bq(t0)[m].l ≠ l) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ a ' ≠ []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list

Proof step 13 from proof SFTrainling-prop-FO (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 14:

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

Rule argument

Additional information

Used simplifier rules: x ≠ [] ⊦ a = x.last ∧ y = x.butlast ↔ x = y + a '; (elim) Used terms: bq(t0), be0, bel0

Proof step 14 from proof SFTrainling-prop-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list

Proof step 15 from proof SFTrainling-prop-FO (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 16:

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

Rule argument

Additional information

Proof step 16 from proof SFTrainling-prop-FO (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  ⊦ n < # x → (x + y) -p n = (x -p n) + y

Rule argument

Additional information

Used simplifier rules: ⊦ n < # x → (x + a ')[n] = x[n]; (s) ⊦ x + a ' = y + a0 ' ↔ x = y ∧ a = a0; (ws) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ #(x + y) = # x + # y; (s) ⊦ # a ' = 0 +1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m < n → ¬ n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ # x = 0 ↔ x = []; (s) ⊦ ¬ a ∈ x → ¬ a ∈ x -p n; (as) ⊦ ¬ n < # x → (x + y)[n] = y[n - # x]; (s) ⊦ ¬ m < n → (n < m ↔ n ≠ m); (ss) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m - m = 0; (s) ⊦ a '[0] = a; (s) ⊦ FO(l) ≠ SF; (s) Used terms: n, bel0, SF '

Proof step 17 from proof SFTrainling-prop-FO (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof SFTrainling-prop-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  bq(t0) ≠ [], t ≠ t0, isPropFO(n, l, bq(t)), SF ∈ bq(t0).butlast, SF ∈ bq(t0), ∀ t. bq(t) = [] ∨ ¬ SF ∈ bq(t).butlast ⊦

Rule argument

Additional information

Used simplifier rules: bin-01: x ≠ [] ⊦ a ∈ x.butlast → a ∈ x; (forward) from specification list-last

Proof step 19 from proof SFTrainling-prop-FO (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t0