Proof step 1 from proof restrict-SF-eq-FOWs-eq (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  bel0 |SF l = bel1 |SF l, bel0.FOWs(t, l) ≠ bel1.FOWs(t, l) ⊦

Rule argument

Additional information

Proof step 2 from proof restrict-SF-eq-FOWs-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  bel0.filter(λ be. be = SF ∨ be.l = l) = bel1.filter(λ be. be = SF ∨ be.l = l), bel0.FOWs(t, l) ≠ bel1.FOWs(t, l) ⊦

Rule argument

Additional information

Used simplifier rules: B-restrict-SF-l: ⊦ bel |SF l = bel.filter(λ be. be = SF ∨ be.l = l);

Proof step 3 from proof restrict-SF-eq-FOWs-eq (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  [].filter(λ be. be = SF ∨ be.l = l) = bel1.filter(λ be. be = SF ∨ be.l = l), [].FOWs(t, l) ≠ bel1.FOWs(t, l) ⊦

• Proof step 12:

  (be + bel).filter(λ be. be = SF ∨ be.l = l) = bel1.filter(λ be. be = SF ∨ be.l = l), (be + bel).FOWs(t, l) ≠ bel1.FOWs(t, l), ∀ l, bel1, t. ¬(bel.filter(λ be. be = SF ∨ be.l = l) = bel1.filter(λ be. be = SF ∨ be.l = l) ∧ bel.FOWs(t, l) ≠ bel1.FOWs(t, l)) ⊦

Rule argument

Additional information

Used simplifier rules: List('a) freely generated by [], +;;

Proof step 4 from proof restrict-SF-eq-FOWs-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  [] = bel1.filter(λ be. be = SF ∨ be.l = l), [] ≠ bel1.FOWs(t, l) ⊦

Rule argument

Additional information

Used simplifier rules: FOWs-base: ⊦ [].FOWs(t, l) = []; ⊦ [].filter(p) = []; (s)

Proof step 5 from proof restrict-SF-eq-FOWs-eq (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 6:

  [] = (be + bel).filter(λ be. be = SF ∨ be.l = l), [] ≠ (be + bel).FOWs(t, l), ∀ l, t. ¬([] = bel.filter(λ be. be = SF ∨ be.l = l) ∧ [] ≠ bel.FOWs(t, l)) ⊦

Rule argument

Additional information

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

Proof step 6 from proof restrict-SF-eq-FOWs-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  bel.filter(λ be. be = SF ∨ be.l = l) = [], be.l ≠ l, be ≠ SF, ∀ l0, t0. [] ≠ bel.filter(λ be. be = SF ∨ be.l = l0) ∨ [] = bel.FOWs(t0, l0) ⊦ be '.FOWs(t, l) = [] ∧ bel.FOWs(t, l) = []

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 ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a + x = a ' + x; (s) ⊦ a ' ≠ []; (s) ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s)

Proof step 7 from proof restrict-SF-eq-FOWs-eq (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 8:

  bel.filter(λ be. be = SF ∨ be.l = l) = [], be = W(l1, v), be.l ≠ l, be ≠ SF, ∀ l0, t0. [] ≠ bel.filter(λ be. be = SF ∨ be.l = l0) ∨ [] = bel.FOWs(t0, l0) ⊦ be '.FOWs(t, l) = [] ∧ bel.FOWs(t, l) = []

• Proof step 10:

  bel.filter(λ be. be = SF ∨ be.l = l) = [], be = FO(l1), be.l ≠ l, be ≠ SF, ∀ l0, t0. [] ≠ bel.filter(λ be. be = SF ∨ be.l = l0) ∨ [] = bel.FOWs(t0, l0) ⊦ be '.FOWs(t, l) = [] ∧ bel.FOWs(t, l) = []

Rule argument

Additional information

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

Proof step 8 from proof restrict-SF-eq-FOWs-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  bel.filter(λ be. be = SF ∨ be.l = l) = [], bel.FOWs(t, l) ≠ [], l1 ≠ l, ∀ l0, t0. [] ≠ bel.filter(λ be. be = SF ∨ be.l = l0) ∨ [] = bel.FOWs(t0, l0) ⊦

Rule argument

Additional information

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

Proof step 9 from proof restrict-SF-eq-FOWs-eq (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l, t

Proof step 10 from proof restrict-SF-eq-FOWs-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  bel.filter(λ be. be = SF ∨ be.l = l) = [], bel.FOWs(t, l) ≠ [], l1 ≠ l, ∀ l0, t0. [] ≠ bel.filter(λ be. be = SF ∨ be.l = l0) ∨ [] = bel.FOWs(t0, l0) ⊦

Rule argument

Additional information

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

Proof step 11 from proof restrict-SF-eq-FOWs-eq (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l, t

Proof step 12 from proof restrict-SF-eq-FOWs-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  (be = SF ∨ be.l = l ⊃ be ';[]) + bel.filter(λ be. be = SF ∨ be.l = l) = bel1.filter(λ be. be = SF ∨ be.l = l), be '.FOWs(t, l) + bel.FOWs(t, l) ≠ bel1.FOWs(t, l), ∀ l0, bel0, t0. bel.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ bel.FOWs(t0, l0) = bel0.FOWs(t0, l0) ⊦

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 + x = a ' + x; (s) ⊦ (a ' + x).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s)

Proof step 13 from proof restrict-SF-eq-FOWs-eq (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 14:

  be ' + bel.filter(λ be. be = SF ∨ be.l = l) = bel1.filter(λ be. be = SF ∨ be.l = l), be '.FOWs(t, l) + bel.FOWs(t, l) ≠ bel1.FOWs(t, l), ∀ l0, bel0, t0. bel.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ bel.FOWs(t0, l0) = bel0.FOWs(t0, l0), be = SF ∨ be.l = l ⊦

• Proof step 24:

  [] + bel.filter(λ be. be = SF ∨ be.l = l) = bel1.filter(λ be. be = SF ∨ be.l = l), be '.FOWs(t, l) + bel.FOWs(t, l) ≠ bel1.FOWs(t, l), be.l ≠ l, be ≠ SF, ∀ l0, bel0, t0. bel.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ bel.FOWs(t0, l0) = bel0.FOWs(t0, l0) ⊦

Rule argument

Additional information

Proof step 14 from proof restrict-SF-eq-FOWs-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  be ' + bel.filter(λ be. be = SF ∨ be.l = l) = bel1.filter(λ be. be = SF ∨ be.l = l), be '.FOWs(t, l) + bel.FOWs(t, l) ≠ bel1.FOWs(t, l), be ∈ bel1, ∀ l0, bel0, t0. bel.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ bel.FOWs(t0, l0) = bel0.FOWs(t0, l0), be = SF ∨ be.l = l ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ x.filter(p) ↔ a ∈ x ∧ p(a); (s) a: ⊦ (x + y) + z = x + y + z; from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list

Proof step 15 from proof restrict-SF-eq-FOWs-eq (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 16:

  be ' + bel.filter(λ be. be = SF ∨ be.l = l) = (be0 + bel0).filter(λ be. be = SF ∨ be.l = l), be '.FOWs(t, l) + bel.FOWs(t, l) ≠ (be0 + bel0).FOWs(t, l), be ∈ be0 + bel0, ∀ l0, bel0, t0. bel.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ bel.FOWs(t0, l0) = bel0.FOWs(t0, l0), ∀ be, bel, l, t. ¬ ( be ' + bel.filter(λ be. be = SF ∨ be.l = l) = bel0.filter(λ be. be = SF ∨ be.l = l) ∧ be '.FOWs(t, l) + bel.FOWs(t, l) ≠ bel0.FOWs(t, l) ∧ be ∈ bel0 ∧ (∀ l0, bel0, t0. bel.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ bel.FOWs(t0, l0) = bel0.FOWs(t0, l0)) ∧ (be = SF ∨ be.l = l)), be = SF ∨ be.l = l ⊦

Rule argument

Additional information

Used simplifier rules: List('a) freely generated by [], +;; ⊦ [].filter(p) = []; (s) ⊦ x + y = [] ↔ x = [] ∧ y = []; (s) ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 16 from proof restrict-SF-eq-FOWs-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  be ' + bel.filter(λ be. be = SF ∨ be.l = l) = (be0 = SF ∨ be0.l = l ⊃ be0 ';[]) + bel0.filter(λ be. be = SF ∨ be.l = l), be '.FOWs(t, l) + bel.FOWs(t, l) ≠ be0 '.FOWs(t, l) + bel0.FOWs(t, l), ∀ l0, bel0, t0. bel.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ bel.FOWs(t0, l0) = bel0.FOWs(t0, l0), ∀ be1, bel1, l0, t0. be1 ' + bel1.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ be1 '.FOWs(t0, l0) + bel1.FOWs(t0, l0) = bel0.FOWs(t0, l0) ∨ ¬ be1 ∈ bel0 ∨ ¬(∀ l0, bel0, t0. bel1.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ bel1.FOWs(t0, l0) = bel0.FOWs(t0, l0)) ∨ be1 ≠ SF ∧ be1.l ≠ l0, be = SF ∨ be.l = l, be = be0 ∨ be ∈ 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).filter(p) = (p(a) ⊃ a ';[]) + x.filter(p); (s)

Proof step 17 from proof restrict-SF-eq-FOWs-eq (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 18:

  be ' + bel.filter(λ be. be = SF ∨ be.l = l) = be0 ' + bel0.filter(λ be. be = SF ∨ be.l = l), be '.FOWs(t, l) + bel.FOWs(t, l) ≠ be0 '.FOWs(t, l) + bel0.FOWs(t, l), ∀ be1, bel1, l0, t0. be1 ' + bel1.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ be1 '.FOWs(t0, l0) + bel1.FOWs(t0, l0) = bel0.FOWs(t0, l0) ∨ ¬ be1 ∈ bel0 ∨ ¬(∀ l0, bel0, t0. bel1.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ bel1.FOWs(t0, l0) = bel0.FOWs(t0, l0)) ∨ be1 ≠ SF ∧ be1.l ≠ l0, ∀ l0, bel0, t0. bel.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ bel.FOWs(t0, l0) = bel0.FOWs(t0, l0), be = be0 ∨ be ∈ bel0, be = SF ∨ be.l = l, be0 = SF ∨ be0.l = l ⊦

• Proof step 20:

  be ' + bel.filter(λ be. be = SF ∨ be.l = l) = [] + bel0.filter(λ be. be = SF ∨ be.l = l), be '.FOWs(t, l) + bel.FOWs(t, l) ≠ be0 '.FOWs(t, l) + bel0.FOWs(t, l), be0.l ≠ l, be0 ≠ SF, ∀ be1, bel1, l0, t0. be1 ' + bel1.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ be1 '.FOWs(t0, l0) + bel1.FOWs(t0, l0) = bel0.FOWs(t0, l0) ∨ ¬ be1 ∈ bel0 ∨ ¬(∀ l0, bel0, t0. bel1.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ bel1.FOWs(t0, l0) = bel0.FOWs(t0, l0)) ∨ be1 ≠ SF ∧ be1.l ≠ l0, ∀ l0, bel0, t0. bel.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ bel.FOWs(t0, l0) = bel0.FOWs(t0, l0), be = be0 ∨ be ∈ bel0, be = SF ∨ be.l = l ⊦

Rule argument

Additional information

Proof step 18 from proof restrict-SF-eq-FOWs-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  bel.filter(λ be. be = SF ∨ be.l = l) = bel0.filter(λ be. be = SF ∨ be.l = l), bel.FOWs(t, l) ≠ bel0.FOWs(t, l), ∀ be1, bel1, l0, t0. be1 ' + bel1.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ be1 '.FOWs(t0, l0) + bel1.FOWs(t0, l0) = bel0.FOWs(t0, l0) ∨ ¬ be1 ∈ bel0 ∨ ¬(∀ l0, bel0, t0. bel1.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ bel1.FOWs(t0, l0) = bel0.FOWs(t0, l0)) ∨ be1 ≠ SF ∧ be1.l ≠ l0, ∀ l0, bel0, t0. bel.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ bel.FOWs(t0, l0) = bel0.FOWs(t0, l0), be0 = SF ∨ be0.l = l ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ # x = # z → (x + y = z + y0 ↔ x = z ∧ y = y0); (ws) ⊦ a ' + x = a0 ' + y ↔ a = a0 ∧ x = y; (ws)

Proof step 19 from proof restrict-SF-eq-FOWs-eq (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: l, bel0, t

Proof step 20 from proof restrict-SF-eq-FOWs-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  be ' + bel.filter(λ be. be = SF ∨ be.l = l) = bel0.filter(λ be. be = SF ∨ be.l = l), be '.FOWs(t, l) + bel.FOWs(t, l) ≠ be0 '.FOWs(t, l) + bel0.FOWs(t, l), be0.l ≠ l, be0 ≠ SF, be ∈ bel0, ∀ be1, bel1, l0, t0. be1 ' + bel1.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ be1 '.FOWs(t0, l0) + bel1.FOWs(t0, l0) = bel0.FOWs(t0, l0) ∨ ¬ be1 ∈ bel0 ∨ ¬(∀ l0, bel0, t0. bel1.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ bel1.FOWs(t0, l0) = bel0.FOWs(t0, l0)) ∨ be1 ≠ SF ∧ be1.l ≠ l0, ∀ l0, bel0, t0. bel.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ bel.FOWs(t0, l0) = bel0.FOWs(t0, l0), be = SF ∨ be.l = l ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ x.filter(p) ↔ a ∈ x ∧ p(a); (s) a: ⊦ (x + y) + z = x + y + z; from specification list in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ [] + x = x; (s)

Proof step 21 from proof restrict-SF-eq-FOWs-eq (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 22:

  be ' + bel.filter(λ be. be = SF ∨ be.l = l) = bel0.filter(λ be. be = SF ∨ be.l = l), be '.FOWs(t, l) + bel.FOWs(t, l) ≠ be0 '.FOWs(t, l) + bel0.FOWs(t, l), be0.l ≠ l, be0 ≠ SF, be ∈ bel0, ∀ l0, bel0, t0. bel.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ bel.FOWs(t0, l0) = bel0.FOWs(t0, l0), ∀ be1, bel1, l0, t0. be1 ' + bel1.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ be1 '.FOWs(t0, l0) + bel1.FOWs(t0, l0) = bel0.FOWs(t0, l0) ∨ ¬ be1 ∈ bel0 ∨ ¬(∀ l0, bel0, t0. bel1.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ bel1.FOWs(t0, l0) = bel0.FOWs(t0, l0)) ∨ be1 ≠ SF ∧ be1.l ≠ l0, be = SF ∨ be.l = l, be ' + bel.filter(λ be. be = SF ∨ be.l = l) ≠ bel0.filter(λ be. be = SF ∨ be.l = l) ∨ be '.FOWs(t, l) + bel.FOWs(t, l) = bel0.FOWs(t, l) ∨ ¬ be ∈ bel0 ∨ ¬(∀ l0, bel0, t0. bel.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ bel.FOWs(t0, l0) = bel0.FOWs(t0, l0)) ∨ be ≠ SF ∧ be.l ≠ l ⊦

Rule argument

Additional information

Used terms: be, bel, l, t

Proof step 22 from proof restrict-SF-eq-FOWs-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  be ' + bel.filter(λ be. be = SF ∨ be.l = l) = bel0.filter(λ be. be = SF ∨ be.l = l), be '.FOWs(t, l) + bel.FOWs(t, l) ≠ be0 '.FOWs(t, l) + bel0.FOWs(t, l), be0.l ≠ l, be0 ≠ SF, be ∈ bel0, ∀ be1, bel1, l0, t0. be1 ' + bel1.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ be1 '.FOWs(t0, l0) + bel1.FOWs(t0, l0) = bel0.FOWs(t0, l0) ∨ ¬ be1 ∈ bel0 ∨ ¬(∀ l0, bel0, t0. bel1.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ bel1.FOWs(t0, l0) = bel0.FOWs(t0, l0)) ∨ be1 ≠ SF ∧ be1.l ≠ l0, ∀ l0, bel0, t0. bel.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ bel.FOWs(t0, l0) = bel0.FOWs(t0, l0), be = SF ∨ be.l = l, be '.FOWs(t, l) + bel.FOWs(t, l) = bel0.FOWs(t, l) ∨ be ≠ SF ∧ be.l ≠ l ⊦

Rule argument

Additional information

Proof step 23 from proof restrict-SF-eq-FOWs-eq (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

Used simplifier rules: FOWs-one-W: ⊦ W(l0, v) '.FOWs(t, l) = (l = l0 ⊃ W(v, t) ';[]); FOWs-one-FO: ⊦ FO(l0) '.FOWs(t, l) = (l = l0 ⊃ FO(t) ';[]); Bevent freely generated by SF, W, FO;; ⊦ FO(l).l = l; (s) ⊦ FO(l) ≠ SF; (s) ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ W(l, v).l = l; (s) ⊦ W(l, v) ≠ SF; (s)

Proof step 24 from proof restrict-SF-eq-FOWs-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  bel.filter(λ be. be = SF ∨ be.l = l) = bel1.filter(λ be. be = SF ∨ be.l = l), be '.FOWs(t, l) + bel.FOWs(t, l) ≠ bel1.FOWs(t, l), be.l ≠ l, be ≠ SF, ∀ l0, bel0, t0. bel.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ bel.FOWs(t0, l0) = bel0.FOWs(t0, l0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s)

Proof step 25 from proof restrict-SF-eq-FOWs-eq (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 26:

  bel.filter(λ be. be = SF ∨ be.l = l) = bel1.filter(λ be. be = SF ∨ be.l = l), be '.FOWs(t, l) + bel.FOWs(t, l) ≠ bel1.FOWs(t, l), be.l ≠ l, be ≠ SF, ∀ l0, bel0, t0. bel.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ bel.FOWs(t0, l0) = bel0.FOWs(t0, l0), bel.filter(λ be. be = SF ∨ be.l = l) ≠ bel1.filter(λ be. be = SF ∨ be.l = l) ∨ bel.FOWs(t, l) = bel1.FOWs(t, l) ⊦

Rule argument

Additional information

Used terms: l, bel1, t

Proof step 26 from proof restrict-SF-eq-FOWs-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  bel.FOWs(t, l) = bel1.FOWs(t, l), bel.filter(λ be. be = SF ∨ be.l = l) = bel1.filter(λ be. be = SF ∨ be.l = l), be '.FOWs(t, l) ≠ [], be.l ≠ l, be ≠ SF, ∀ l0, bel0, t0. bel.filter(λ be. be = SF ∨ be.l = l0) ≠ bel0.filter(λ be. be = SF ∨ be.l = l0) ∨ bel.FOWs(t0, l0) = bel0.FOWs(t0, l0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x = y + x ↔ y = []; (s)

Proof step 27 from proof restrict-SF-eq-FOWs-eq (previous step) (back to tree)

User applied rule constructor cut

And closed the goal!

Rule argument

Additional information

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