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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  ¬(W(v, t0) ∈ (be + bel0).FOWs(t, l) ↔ t = t0 ∧ W(l, v) ∈ be + bel0), ∀ v, t0, t, l. W(v, t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ W(l, v) ∈ 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 W-in-FOWs (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  ¬(W(v, t0) ∈ be '.FOWs(t, l) ∨ W(v, t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ (W(l, v) = be ∨ W(l, v) ∈ bel0)), ∀ v, t0, t, l. W(v, t0) ∈ bel0.FOWs(t, l) ↔ t = t0 ∧ W(l, v) ∈ 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 W-in-FOWs (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 5:

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

• Proof step 7:

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

• Proof step 14:

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

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

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

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: v, t0, t, l

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

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

Rule argument

Additional information

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

Proof step 8 from proof W-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:

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

• Proof step 12:

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

Rule argument

Additional information

Proof step 9 from proof W-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:

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

• Proof step 11:

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

Rule argument

Additional information

Proof step 10 from proof W-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) ⊦ W(v, tid) = W(v0, tid0) ↔ v = v0 ∧ tid = tid0; (ws) ⊦ W(l, v) = W(l0, v0) ↔ l = l0 ∧ v = v0; (ws) Used formulas: l = l0

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

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: v, t0, t, l

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

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

Rule argument

Additional information

Used simplifier rules: ⊦ W(v, tid) = W(v0, tid0) ↔ v = v0 ∧ tid = tid0; (ws) ⊦ a ∈ a0 ' ↔ a = a0; (s) ⊦ W(l, v) = W(l0, v0) ↔ l = l0 ∧ v = v0; (ws)

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: v, t0, t0, l

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

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

Proof step 15 from proof W-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:

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

• Proof step 19:

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

Rule argument

Additional information

Proof step 16 from proof W-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:

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

• Proof step 18:

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

Rule argument

Additional information

Proof step 17 from proof W-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 18 from proof W-in-FOWs (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: v, t0, t, l

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

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

Rule argument

Additional information

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: v, t0, t0, l