Proof step 1 from proof oplus-same-writes-eq (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  fowl0 |W = fowl1 |W, ¬(v ⊕ fowl0 = v ⊕ fowl1 ↔ true) ⊦

Rule argument

Additional information

Proof step 2 from proof oplus-same-writes-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  fowl0.filter(.W?) = fowl1.filter(.W?), v ⊕ fowl0 ≠ v ⊕ fowl1 ⊦

Rule argument

Additional information

Used simplifier rules: filterwrites-def: ⊦ fowl |W = fowl.filter(λ fow. fow.W?);

Proof step 3 from proof oplus-same-writes-eq (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  [].filter(.W?) = fowl1.filter(.W?), v ⊕ [] ≠ v ⊕ fowl1 ⊦

• Proof step 10:

  (fow + fowl).filter(.W?) = fowl1.filter(.W?), v ⊕ (fow + fowl) ≠ v ⊕ fowl1, ∀ fowl1, v. ¬(fowl.filter(.W?) = fowl1.filter(.W?) ∧ v ⊕ fowl ≠ v ⊕ fowl1) ⊦

Rule argument

Additional information

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

Proof step 4 from proof oplus-same-writes-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  [] = fowl1.filter(.W?), v ≠ v ⊕ fowl1 ⊦

Rule argument

Additional information

Used simplifier rules: overwrite-base: ⊦ v ⊕ [] = v; ⊦ [].filter(p) = []; (s)

Proof step 5 from proof oplus-same-writes-eq (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 6:

  [] = (fow + fowl).filter(.W?), v ≠ v ⊕ (fow + fowl), ∀ v. ¬([] = fowl.filter(.W?) ∧ v ≠ v ⊕ fowl) ⊦

Rule argument

Additional information

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

Proof step 6 from proof oplus-same-writes-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  fowl.filter(.W?) = [], v ≠ v ⊕ (fow ' + fowl), ¬ fow.W?, ∀ v0. v0 = v0 ⊕ fowl ⊦

Rule argument

Additional information

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

Proof step 7 from proof oplus-same-writes-eq (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 8:

  fowl.filter(.W?) = [], fow = FO(t), v ≠ v ⊕ (fow ' + fowl), ¬ fow.W?, ∀ v0. v0 = v0 ⊕ fowl ⊦

Rule argument

Additional information

Used simplifier rules: overwrite-rec2: ⊦ v ⊕ (W(v0, t) ' + fowl) = v0 ⊕ fowl; FOW freely generated by FO, W;; a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ W(v, tid).W?; (s)

Proof step 8 from proof oplus-same-writes-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  fowl.filter(.W?) = [], v ≠ v ⊕ fowl, ∀ v0. v0 = v0 ⊕ fowl ⊦

Rule argument

Additional information

Used simplifier rules: overwrite-rec1: ⊦ v ⊕ (FO(t) ' + fowl) = v ⊕ fowl; ⊦ ¬ FO(tid).W?; (s) a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 9 from proof oplus-same-writes-eq (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: v

Proof step 10 from proof oplus-same-writes-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  (fow.W? ⊃ fow ';[]) + fowl.filter(.W?) = fowl1.filter(.W?), v ⊕ (fow ' + fowl) ≠ v ⊕ fowl1, ∀ fowl0, v0. fowl.filter(.W?) ≠ fowl0.filter(.W?) ∨ v0 ⊕ fowl = v0 ⊕ fowl0 ⊦

Rule argument

Additional information

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

Proof step 11 from proof oplus-same-writes-eq (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 12:

  fow ' + fowl.filter(.W?) = fowl1.filter(.W?), v ⊕ (fow ' + fowl) ≠ v ⊕ fowl1, fow.W?, ∀ fowl0, v0. fowl.filter(.W?) ≠ fowl0.filter(.W?) ∨ v0 ⊕ fowl = v0 ⊕ fowl0 ⊦

• Proof step 22:

  [] + fowl.filter(.W?) = fowl1.filter(.W?), v ⊕ (fow ' + fowl) ≠ v ⊕ fowl1, ¬ fow.W?, ∀ fowl0, v0. fowl.filter(.W?) ≠ fowl0.filter(.W?) ∨ v0 ⊕ fowl = v0 ⊕ fowl0 ⊦

Rule argument

Additional information

Proof step 12 from proof oplus-same-writes-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  fow ' + fowl.filter(.W?) = fowl1.filter(.W?), v ⊕ (fow ' + fowl) ≠ v ⊕ fowl1, fow.W?, fow ∈ fowl1, ∀ fowl0, v0. fowl.filter(.W?) ≠ fowl0.filter(.W?) ∨ v0 ⊕ fowl = v0 ⊕ fowl0 ⊦

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 13 from proof oplus-same-writes-eq (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 14:

  fow ' + fowl.filter(.W?) = fowl1.filter(.W?), fow = W(v1, t), v ⊕ (fow ' + fowl) ≠ v ⊕ fowl1, fow.W?, fow ∈ fowl1, ∀ fowl0, v0. fowl.filter(.W?) ≠ fowl0.filter(.W?) ∨ v0 ⊕ fowl = v0 ⊕ fowl0 ⊦

Rule argument

Additional information

Used simplifier rules: overwrite-rec1: ⊦ v ⊕ (FO(t) ' + fowl) = v ⊕ fowl; FOW freely generated by FO, W;; a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ¬ FO(tid).W?; (s)

Proof step 14 from proof oplus-same-writes-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  W(v1, t) ' + fowl.filter(.W?) = fowl1.filter(.W?), v1 ⊕ fowl ≠ v ⊕ fowl1, W(v1, t) ∈ fowl1, ∀ fowl0, v0. fowl.filter(.W?) ≠ fowl0.filter(.W?) ∨ v0 ⊕ fowl = v0 ⊕ fowl0 ⊦

Rule argument

Additional information

Used simplifier rules: overwrite-rec2: ⊦ v ⊕ (W(v0, t) ' + fowl) = v0 ⊕ fowl; ⊦ W(v, tid).W?; (s) ⊦ 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 oplus-same-writes-eq (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 16:

  W(v1, t) ' + fowl.filter(.W?) = (fow + fowl0).filter(.W?), v1 ⊕ fowl ≠ v ⊕ (fow + fowl0), W(v1, t) ∈ fow + fowl0, ∀ fowl0, v0. fowl.filter(.W?) ≠ fowl0.filter(.W?) ∨ v0 ⊕ fowl = v0 ⊕ fowl0, ∀ v1, t, fowl, v. ¬ ( W(v1, t) ' + fowl.filter(.W?) = fowl0.filter(.W?) ∧ v1 ⊕ fowl ≠ v ⊕ fowl0 ∧ W(v1, t) ∈ fowl0 ∧ (∀ fowl0, v0. fowl.filter(.W?) ≠ fowl0.filter(.W?) ∨ v0 ⊕ fowl = v0 ⊕ fowl0)) ⊦

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 oplus-same-writes-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  W(v1, t) ' + fowl.filter(.W?) = (fow.W? ⊃ fow ';[]) + fowl0.filter(.W?), v1 ⊕ fowl ≠ v ⊕ (fow ' + fowl0), ∀ v0, t0, fowl1, v2. W(v0, t0) ' + fowl1.filter(.W?) ≠ fowl0.filter(.W?) ∨ v0 ⊕ fowl1 = v2 ⊕ fowl0 ∨ ¬ W(v0, t0) ∈ fowl0 ∨ ¬(∀ fowl0, v0. fowl1.filter(.W?) ≠ fowl0.filter(.W?) ∨ v0 ⊕ fowl1 = v0 ⊕ fowl0), ∀ fowl0, v0. fowl.filter(.W?) ≠ fowl0.filter(.W?) ∨ v0 ⊕ fowl = v0 ⊕ fowl0, W(v1, t) = fow ∨ W(v1, t) ∈ fowl0 ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ W(v, tid).W?; (s) ⊦ a ∈ x.filter(p) ↔ a ∈ x ∧ p(a); (s) ⊦ a ∈ a0 ' ↔ a = a0; (s) in-14: ⊦ a ' + x = y → a ∈ y; (forward) from specification list ⊦ [] + x = x; (s) ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ 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 oplus-same-writes-eq (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 18:

  W(v1, t) ' + fowl.filter(.W?) = (fow.W? ⊃ fow ';[]) + fowl0.filter(.W?), fow = FO(t1), v1 ⊕ fowl ≠ v ⊕ (fow ' + fowl0), ∀ fowl0, v0. fowl.filter(.W?) ≠ fowl0.filter(.W?) ∨ v0 ⊕ fowl = v0 ⊕ fowl0, ∀ v0, t0, fowl1, v2. W(v0, t0) ' + fowl1.filter(.W?) ≠ fowl0.filter(.W?) ∨ v0 ⊕ fowl1 = v2 ⊕ fowl0 ∨ ¬ W(v0, t0) ∈ fowl0 ∨ ¬(∀ fowl0, v0. fowl1.filter(.W?) ≠ fowl0.filter(.W?) ∨ v0 ⊕ fowl1 = v0 ⊕ fowl0), W(v1, t) = fow ∨ W(v1, t) ∈ fowl0 ⊦

• Proof step 20:

  W(v1, t) ' + fowl.filter(.W?) = (fow.W? ⊃ fow ';[]) + fowl0.filter(.W?), fow = W(v3, t1), v1 ⊕ fowl ≠ v ⊕ (fow ' + fowl0), ∀ fowl0, v0. fowl.filter(.W?) ≠ fowl0.filter(.W?) ∨ v0 ⊕ fowl = v0 ⊕ fowl0, ∀ v0, t0, fowl1, v2. W(v0, t0) ' + fowl1.filter(.W?) ≠ fowl0.filter(.W?) ∨ v0 ⊕ fowl1 = v2 ⊕ fowl0 ∨ ¬ W(v0, t0) ∈ fowl0 ∨ ¬(∀ fowl0, v0. fowl1.filter(.W?) ≠ fowl0.filter(.W?) ∨ v0 ⊕ fowl1 = v0 ⊕ fowl0), W(v1, t) = fow ∨ W(v1, t) ∈ fowl0 ⊦

Rule argument

Additional information

Used simplifier rules: FOW freely generated by FO, W;;

Proof step 18 from proof oplus-same-writes-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  W(v1, t) ' + fowl.filter(.W?) = fowl0.filter(.W?), v1 ⊕ fowl ≠ v ⊕ fowl0, W(v1, t) ∈ fowl0, ∀ fowl0, v0. fowl.filter(.W?) ≠ fowl0.filter(.W?) ∨ v0 ⊕ fowl = v0 ⊕ fowl0, ∀ v0, t0, fowl1, v2. W(v0, t0) ' + fowl1.filter(.W?) ≠ fowl0.filter(.W?) ∨ v0 ⊕ fowl1 = v2 ⊕ fowl0 ∨ ¬ W(v0, t0) ∈ fowl0 ∨ ¬(∀ fowl0, v0. fowl1.filter(.W?) ≠ fowl0.filter(.W?) ∨ v0 ⊕ fowl1 = v0 ⊕ fowl0) ⊦

Rule argument

Additional information

Used simplifier rules: overwrite-rec1: ⊦ v ⊕ (FO(t) ' + fowl) = v ⊕ fowl; ⊦ W(v, tid).W?; (s) ⊦ 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 ⊦ FO(tid) ≠ W(v, tid0); (s) ⊦ [] + x = x; (s) ⊦ ¬ FO(tid).W?; (s)

Proof step 19 from proof oplus-same-writes-eq (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: v1, t, fowl, v

Proof step 20 from proof oplus-same-writes-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  fowl.filter(.W?) = fowl0.filter(.W?), v3 ⊕ fowl ≠ v3 ⊕ fowl0, ∀ fowl0, v0. fowl.filter(.W?) ≠ fowl0.filter(.W?) ∨ v0 ⊕ fowl = v0 ⊕ fowl0, ∀ v0, t0, fowl1, v2. W(v0, t0) ' + fowl1.filter(.W?) ≠ fowl0.filter(.W?) ∨ v0 ⊕ fowl1 = v2 ⊕ fowl0 ∨ ¬ W(v0, t0) ∈ fowl0 ∨ ¬(∀ fowl0, v0. fowl1.filter(.W?) ≠ fowl0.filter(.W?) ∨ v0 ⊕ fowl1 = v0 ⊕ fowl0) ⊦

Rule argument

Additional information

Used simplifier rules: overwrite-rec2: ⊦ v ⊕ (W(v0, t) ' + fowl) = v0 ⊕ fowl; a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ W(v, tid) = W(v0, tid0) ↔ v = v0 ∧ tid = tid0; (ws) ⊦ a ' + x = a0 ' + y ↔ a = a0 ∧ x = y; (ws) ⊦ W(v, tid).W?; (s)

Proof step 21 from proof oplus-same-writes-eq (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: fowl0, v3

Proof step 22 from proof oplus-same-writes-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  fowl.filter(.W?) = fowl1.filter(.W?), v ⊕ (fow ' + fowl) ≠ v ⊕ fowl1, ¬ fow.W?, ∀ fowl0, v0. fowl1.filter(.W?) ≠ fowl0.filter(.W?) ∨ v0 ⊕ fowl = v0 ⊕ fowl0 ⊦

Rule argument

Additional information

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

Proof step 23 from proof oplus-same-writes-eq (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 24:

  fowl.filter(.W?) = fowl1.filter(.W?), v ⊕ (fow ' + fowl) ≠ v ⊕ fowl1, ¬ fow.W?, ∀ fowl0, v0. fowl1.filter(.W?) ≠ fowl0.filter(.W?) ∨ v0 ⊕ fowl = v0 ⊕ fowl0, fowl1.filter(.W?) ≠ (fow ' + fowl).filter(.W?) ∨ v ⊕ fowl = v ⊕ (fow ' + fowl) ⊦

Rule argument

Additional information

Used terms: fow ' + fowl, v

Proof step 24 from proof oplus-same-writes-eq (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  fowl.filter(.W?) = fowl1.filter(.W?), v ⊕ fowl = v ⊕ (fow ' + fowl), v ⊕ fowl ≠ v ⊕ fowl1, ¬ fow.W?, ∀ fowl0, v0. fowl1.filter(.W?) ≠ fowl0.filter(.W?) ∨ v0 ⊕ fowl = v0 ⊕ fowl0 ⊦

Rule argument

Additional information

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

Proof step 25 from proof oplus-same-writes-eq (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: fowl1, v