Proof step 1 from proof isPropFO-cons-leading-FO (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  FO(t) ' + (bel.FOWs(t, l)).tail ≠ bel.FOWs(t, l), isPropFO(n, l, bel) ⊦

Rule argument

Additional information

Proof step 2 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  FO(t) ' + ((be + bel0).FOWs(t, l)).tail ≠ (be + bel0).FOWs(t, l), isPropFO(n, l, be + bel0), ∀ t, l, n. ¬(FO(t) ' + (bel0.FOWs(t, l)).tail ≠ bel0.FOWs(t, l) ∧ isPropFO(n, l, bel0)) ⊦

Rule argument

Additional information

Used simplifier rules: FOWs-base: ⊦ [].FOWs(t, l) = []; isPropFO-empty: ⊦ ¬ isPropFO(n, l, []); List('a) freely generated by [], +;; ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 3 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  FO(t) ' + (be '.FOWs(t, l) + bel0.FOWs(t, l)).tail ≠ be '.FOWs(t, l) + bel0.FOWs(t, l), isPropFO(n, l, be ' + bel0), ∀ t0, l0, n0. FO(t0) ' + (bel0.FOWs(t0, l0)).tail = bel0.FOWs(t0, l0) ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

Used simplifier rules: FOWs-append: ⊦ (bel0 + bel1).FOWs(t, l) = bel0.FOWs(t, l) + bel1.FOWs(t, l); ⊦ a + x = a ' + x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 4 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 5:

  be = W(l1, v), FO(t) ' + (be '.FOWs(t, l) + bel0.FOWs(t, l)).tail ≠ be '.FOWs(t, l) + bel0.FOWs(t, l), isPropFO(n, l, be ' + bel0), ∀ t0, l0, n0. FO(t0) ' + (bel0.FOWs(t0, l0)).tail = bel0.FOWs(t0, l0) ∨ ¬ isPropFO(n0, l0, bel0) ⊦

• Proof step 17:

  be = FO(l1), FO(t) ' + (be '.FOWs(t, l) + bel0.FOWs(t, l)).tail ≠ be '.FOWs(t, l) + bel0.FOWs(t, l), isPropFO(n, l, be ' + bel0), ∀ t0, l0, n0. FO(t0) ' + (bel0.FOWs(t0, l0)).tail = bel0.FOWs(t0, l0) ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

Used simplifier rules: FOWs-one-SF: ⊦ SF '.FOWs(t, l) = []; isPropFO-leading-SF: ⊦ ¬ isPropFO(n, l, SF ' + bel); Bevent freely generated by SF, W, FO;; ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 5 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  FO(t) ' + ((l = l1 ⊃ W(v, t) ';[]) + bel0.FOWs(t, l)).tail ≠ (l = l1 ⊃ W(v, t) ';[]) + bel0.FOWs(t, l), isPropFO(n, l, W(l1, v) ' + bel0), ∀ t0, l0, n0. FO(t0) ' + (bel0.FOWs(t0, l0)).tail = bel0.FOWs(t0, l0) ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

Used simplifier rules: FOWs-one-W: ⊦ W(l0, v) '.FOWs(t, l) = (l = l0 ⊃ W(v, t) ';[]);

Proof step 6 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 7:

  FO(t) ' + ([] + bel0.FOWs(t, l)).tail ≠ (l = l1 ⊃ W(v, t) ';[]) + bel0.FOWs(t, l), l ≠ l1, isPropFO(n, l, W(l1, v) ' + bel0), ∀ t0, l0, n0. FO(t0) ' + (bel0.FOWs(t0, l0)).tail = bel0.FOWs(t0, l0) ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

Used simplifier rules: isPropFO-not-leading-W: ⊦ ¬ isPropFO(n, l, W(l, v) ' + bel); ⊦ (a ' + x).tail = x; (s) ⊦ # y = # y0 → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) ⊦ a ' = a0 ' ↔ a = a0; (s) ⊦ FO(tid) ≠ W(v, tid0); (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 7 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  FO(t) ' + (bel0.FOWs(t, l)).tail ≠ bel0.FOWs(t, l), l ≠ l1, isPropFO(n, l, W(l1, v) ' + bel0), ∀ t0, l0, n0. FO(t0) ' + (bel0.FOWs(t0, l0)).tail = bel0.FOWs(t0, l0) ∨ ¬ 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 8 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 9:

  n = 0, FO(t) ' + (bel0.FOWs(t, l)).tail ≠ bel0.FOWs(t, l), l ≠ l1, isPropFO(n, l, W(l1, v) ' + bel0), ∀ t0, l0, n0. FO(t0) ' + (bel0.FOWs(t0, l0)).tail = bel0.FOWs(t0, l0) ∨ ¬ isPropFO(n0, l0, bel0) ⊦

• Proof step 12:

  n = n1 +1, FO(t) ' + (bel0.FOWs(t, l)).tail ≠ bel0.FOWs(t, l), l ≠ l1, isPropFO(n, l, W(l1, v) ' + bel0), ∀ t0, l0, n0. FO(t0) ' + (bel0.FOWs(t0, l0)).tail = bel0.FOWs(t0, l0) ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

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

Proof step 9 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  FO(t) ' + (bel0.FOWs(t, l)).tail ≠ bel0.FOWs(t, l), l ≠ l1, isPropFO(0, l, W(l1, v) ' + bel0), ∀ t0, l0, n0. FO(t0) ' + (bel0.FOWs(t0, l0)).tail = bel0.FOWs(t0, l0) ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

Proof step 10 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ 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 + y) + z = x + y + z; from specification list ⊦ W(l, v) ≠ FO(l0); (s) Used terms: 0, l, W(l1, v) ' + bel0

Proof step 11 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

Lemma isPropFO-def

Proof step 12 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  FO(t) ' + (bel0.FOWs(t, l)).tail ≠ bel0.FOWs(t, l), l ≠ l1, isPropFO(n1 + 1, l, W(l1, v) ' + bel0), ∀ t0, l0, n0. FO(t0) ' + (bel0.FOWs(t0, l0)).tail = bel0.FOWs(t0, l0) ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s)

Proof step 13 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ be.l ≠ l ∧ be ≠ SF → (isPropFO(n + 1, l, be ' + bel) ↔ isPropFO(n, l, bel))

• Proof step 15:

  FO(t) ' + (bel0.FOWs(t, l)).tail ≠ bel0.FOWs(t, l), W(l1, v).l ≠ l, W(l1, v) ≠ SF, l ≠ l1, isPropFO(n1, l, bel0), ∀ t0, l0, n0. FO(t0) ' + (bel0.FOWs(t0, l0)).tail = bel0.FOWs(t0, l0) ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ W(l, v).l = l; (s) ⊦ W(l, v) ≠ SF; (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: l, n1, W(l1, v), bel0

Proof step 14 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

Lemma isPropFO-rec

Proof step 15 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  FO(t) ' + (bel0.FOWs(t, l)).tail ≠ bel0.FOWs(t, l), l1 ≠ l, isPropFO(n1, l, bel0), ∀ t0, l0, n0. FO(t0) ' + (bel0.FOWs(t0, l0)).tail = bel0.FOWs(t0, l0) ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ W(l, v) ≠ SF; (s) ⊦ W(l, v).l = l; (s)

Proof step 16 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t, l, n1

Proof step 17 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  FO(t) ' + ((l = l1 ⊃ FO(t) ';[]) + bel0.FOWs(t, l)).tail ≠ (l = l1 ⊃ FO(t) ';[]) + bel0.FOWs(t, l), isPropFO(n, l, FO(l1) ' + bel0), ∀ t0, l0, n0. FO(t0) ' + (bel0.FOWs(t0, l0)).tail = bel0.FOWs(t0, l0) ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

Used simplifier rules: FOWs-one-FO: ⊦ FO(l0) '.FOWs(t, l) = (l = l0 ⊃ FO(t) ';[]);

Proof step 18 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 19:

  FO(t) ' + ((l = l1 ⊃ FO(t) ';[]) + bel0.FOWs(t, l)).tail ≠ (l = l1 ⊃ FO(t) ';[]) + bel0.FOWs(t, l), l ≠ l1, isPropFO(n, l, FO(l1) ' + bel0), ∀ t0, l0, n0. FO(t0) ' + (bel0.FOWs(t0, l0)).tail = bel0.FOWs(t0, l0) ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ (a ' + x).tail = x; (s) ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) a: ⊦ (x + y) + z = x + y + z; from specification list Used formulas: l = l1

Proof step 19 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  FO(t) ' + (bel0.FOWs(t, l)).tail ≠ bel0.FOWs(t, l), l ≠ l1, isPropFO(n, l, FO(l1) ' + bel0), ∀ t0, l0, n0. FO(t0) ' + (bel0.FOWs(t0, l0)).tail = bel0.FOWs(t0, l0) ∨ ¬ 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 20 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 21:

  n = 0, FO(t) ' + (bel0.FOWs(t, l)).tail ≠ bel0.FOWs(t, l), l ≠ l1, isPropFO(n, l, FO(l1) ' + bel0), ∀ t0, l0, n0. FO(t0) ' + (bel0.FOWs(t0, l0)).tail = bel0.FOWs(t0, l0) ∨ ¬ isPropFO(n0, l0, bel0) ⊦

• Proof step 24:

  n = n1 +1, FO(t) ' + (bel0.FOWs(t, l)).tail ≠ bel0.FOWs(t, l), l ≠ l1, isPropFO(n, l, FO(l1) ' + bel0), ∀ t0, l0, n0. FO(t0) ' + (bel0.FOWs(t0, l0)).tail = bel0.FOWs(t0, l0) ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

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

Proof step 21 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  FO(t) ' + (bel0.FOWs(t, l)).tail ≠ bel0.FOWs(t, l), l ≠ l1, isPropFO(0, l, FO(l1) ' + bel0), ∀ t0, l0, n0. FO(t0) ' + (bel0.FOWs(t0, l0)).tail = bel0.FOWs(t0, l0) ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

Proof step 22 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

  ⊦ 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 + y) + z = x + y + z; from specification list ⊦ FO(l) = FO(l0) ↔ l = l0; (s) Used terms: 0, l, FO(l1) ' + bel0

Proof step 23 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

Lemma isPropFO-def

Proof step 24 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  FO(t) ' + (bel0.FOWs(t, l)).tail ≠ bel0.FOWs(t, l), l ≠ l1, isPropFO(n1 + 1, l, FO(l1) ' + bel0), ∀ t0, l0, n0. FO(t0) ' + (bel0.FOWs(t0, l0)).tail = bel0.FOWs(t0, l0) ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s)

Proof step 25 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

  ⊦ be.l ≠ l ∧ be ≠ SF → (isPropFO(n + 1, l, be ' + bel) ↔ isPropFO(n, l, bel))

• Proof step 27:

  FO(t) ' + (bel0.FOWs(t, l)).tail ≠ bel0.FOWs(t, l), FO(l1).l ≠ l, FO(l1) ≠ SF, l ≠ l1, isPropFO(n1, l, bel0), ∀ t0, l0, n0. FO(t0) ' + (bel0.FOWs(t0, l0)).tail = bel0.FOWs(t0, l0) ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ FO(l).l = l; (s) ⊦ FO(l) ≠ SF; (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: l, n1, FO(l1), bel0

Proof step 26 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

Lemma isPropFO-rec

Proof step 27 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  FO(t) ' + (bel0.FOWs(t, l)).tail ≠ bel0.FOWs(t, l), l1 ≠ l, isPropFO(n1, l, bel0), ∀ t0, l0, n0. FO(t0) ' + (bel0.FOWs(t0, l0)).tail = bel0.FOWs(t0, l0) ∨ ¬ isPropFO(n0, l0, bel0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ FO(l) ≠ SF; (s) ⊦ FO(l).l = l; (s)

Proof step 28 from proof isPropFO-cons-leading-FO (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t, l, n1