Proof step 1 from proof FO-in-FOWs (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(FO(t0) ∈ bel.FOWs(t, l) ↔ t = t0 ∧ FO(l) ∈ bel) ⊦

Rule argument

Additional information

Proof step 2 from proof FO-in-FOWs (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  ¬(FO(t0) ∈ (be + bel0).FOWs(t, l) ↔ t = t0 ∧ FO(l) ∈ be + bel0), ∀ t0, t, l. FO(t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ FO(l) ∈ bel0 ⊦

Rule argument

Additional information

Used simplifier rules: FOWs-base: ⊦ [].FOWs(t, l) = []; List('a) freely generated by [], +;; ⊦ ¬ a ∈ []; (s)

Proof step 3 from proof FO-in-FOWs (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  ¬(FO(t0) ∈ be '.FOWs(t, l) ∨ FO(t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ (FO(l) = be ∨ FO(l) ∈ bel0)), ∀ t0, t, l. FO(t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ FO(l) ∈ 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 + y) + z = x + y + z; from specification list ⊦ a ∈ a0 ' + x ↔ a = a0 ∨ a ∈ x; (s) ⊦ a + x = a ' + x; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s)

Proof step 4 from proof FO-in-FOWs (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 5:

  be = SF, ¬(FO(t0) ∈ be '.FOWs(t, l) ∨ FO(t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ (FO(l) = be ∨ FO(l) ∈ bel0)), ∀ t0, t, l. FO(t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ FO(l) ∈ bel0 ⊦

• Proof step 7:

  be = W(l0, v), ¬(FO(t0) ∈ be '.FOWs(t, l) ∨ FO(t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ (FO(l) = be ∨ FO(l) ∈ bel0)), ∀ t0, t, l. FO(t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ FO(l) ∈ bel0 ⊦

• Proof step 14:

  be = FO(l0), ¬(FO(t0) ∈ be '.FOWs(t, l) ∨ FO(t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ (FO(l) = be ∨ FO(l) ∈ bel0)), ∀ t0, t, l. FO(t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ FO(l) ∈ bel0 ⊦

Rule argument

Additional information

Used simplifier rules: Bevent freely generated by SF, W, FO;;

Proof step 5 from proof FO-in-FOWs (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  ¬(FO(t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ FO(l) ∈ bel0), ∀ t0, t, l. FO(t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ FO(l) ∈ bel0 ⊦

Rule argument

Additional information

Used simplifier rules: FOWs-one-SF: ⊦ SF '.FOWs(t, l) = []; ⊦ FO(l) ≠ SF; (s) ⊦ ¬ a ∈ []; (s)

Proof step 6 from proof FO-in-FOWs (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t0, t, l

Proof step 7 from proof FO-in-FOWs (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  ¬(FO(t0) ∈ (l = l0 ⊃ W(v, t) ';[]) ∨ FO(t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ FO(l) ∈ bel0), ∀ t0, t, l. FO(t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ FO(l) ∈ bel0 ⊦

Rule argument

Additional information

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

Proof step 8 from proof FO-in-FOWs (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 9:

  ∀ t0, t, l. FO(t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ FO(l) ∈ bel0, FO(t0) ∈ (l = l0 ⊃ W(v, t) ';[]) ∨ FO(t0) ∈ bel0.FOWs(t, l) ⊦ t = t0 ∧ FO(l) ∈ bel0

• Proof step 12:

  t = t0, FO(l) ∈ bel0, ¬ FO(t0) ∈ (l = l0 ⊃ W(v, t) ';[]), ¬ FO(t0) ∈ bel0.FOWs(t, l), ∀ t0, t, l. FO(t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ FO(l) ∈ bel0 ⊦

Rule argument

Additional information

Proof step 9 from proof FO-in-FOWs (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 10:

  FO(t0) ∈ (l = l0 ⊃ W(v, t) ';[]), ∀ t0, t, l. FO(t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ FO(l) ∈ bel0 ⊦ t = t0 ∧ FO(l) ∈ bel0

• Proof step 11:

  FO(t0) ∈ bel0.FOWs(t, l), ∀ t0, t, l. FO(t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ FO(l) ∈ bel0 ⊦ t = t0 ∧ FO(l) ∈ bel0

Rule argument

Additional information

Proof step 10 from proof FO-in-FOWs (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ []; (s) ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ FO(tid) ≠ W(v, tid0); (s) Used formulas: l = l0

Proof step 11 from proof FO-in-FOWs (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t0, t, l

Proof step 12 from proof FO-in-FOWs (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  FO(l) ∈ bel0, ¬ FO(t0) ∈ (l = l0 ⊃ W(v, t0) ';[]), ¬ FO(t0) ∈ bel0.FOWs(t0, l), ∀ t0, t, l. FO(t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ FO(l) ∈ bel0 ⊦

Rule argument

Additional information

Proof step 13 from proof FO-in-FOWs (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t0, t0, l

Proof step 14 from proof FO-in-FOWs (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  ¬(FO(t0) ∈ (l = l0 ⊃ FO(t) ';[]) ∨ FO(t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ (l = l0 ∨ FO(l) ∈ bel0)), ∀ t0, t, l. FO(t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ FO(l) ∈ bel0 ⊦

Rule argument

Additional information

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

Proof step 15 from proof FO-in-FOWs (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 16:

  ∀ t0, t, l. FO(t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ FO(l) ∈ bel0, FO(t0) ∈ (l = l0 ⊃ FO(t) ';[]) ∨ FO(t0) ∈ bel0.FOWs(t, l) ⊦ t = t0 ∧ (l = l0 ∨ FO(l) ∈ bel0)

• Proof step 19:

  t = t0, ¬ FO(t0) ∈ (l = l0 ⊃ FO(t) ';[]), ¬ FO(t0) ∈ bel0.FOWs(t, l), ∀ t0, t, l. FO(t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ FO(l) ∈ bel0, l = l0 ∨ FO(l) ∈ bel0 ⊦

Rule argument

Additional information

Proof step 16 from proof FO-in-FOWs (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 17:

  FO(t0) ∈ (l = l0 ⊃ FO(t) ';[]), ∀ t0, t, l. FO(t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ FO(l) ∈ bel0 ⊦ t = t0 ∧ (l = l0 ∨ FO(l) ∈ bel0)

• Proof step 18:

  FO(t0) ∈ bel0.FOWs(t, l), ∀ t0, t, l. FO(t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ FO(l) ∈ bel0 ⊦ t = t0 ∧ (l = l0 ∨ FO(l) ∈ bel0)

Rule argument

Additional information

Proof step 17 from proof FO-in-FOWs (previous step) (back to tree)

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ []; (s) ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ FO(tid) = FO(tid0) ↔ tid = tid0; (s) Used formulas: l = l0

Proof step 18 from proof FO-in-FOWs (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t0, t, l

Proof step 19 from proof FO-in-FOWs (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  l ≠ l0, FO(l) ∈ bel0, ¬ FO(t0) ∈ bel0.FOWs(t0, l), ∀ t0, t, l. FO(t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ FO(l) ∈ bel0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ []; (s) ⊦ a ∈ a0 ' ↔ a = a0; (s)

Proof step 20 from proof FO-in-FOWs (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: t0, t0, l