Proof step 1 from proof product-ok-refine-cext-imp-aext (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), ¬(aren(aa) = ren(a0) ↔ true), oinj(aext), oinj(ext), Πok(ext, cext, ren, cren), Πok(ext, aext, ren, aren) ⊦

Rule argument

Additional information

Proof step 2 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ Πok(lext, rext, lren, rren) ↔ inj(lren) ∧ inj(rren) ∧ surj(lren, rren) ∧ sharingok(lext, rext, lren, rren)

• Proof step 4:

  aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), ¬(aren(aa) = ren(a0) ↔ true), inj(ren), inj(aren), oinj(ext), oinj(aext), sharingok(ext, aext, ren, aren), surj(ren, aren), Πok(ext, cext, ren, cren) ⊦

Rule argument

Additional information

Used terms: ext, aext, ren, aren

Proof step 3 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

A spec-lemma

Proof step 4 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ sharingok(lext, rext, lren, rren) ↔ (∀ la, ra. (lren(la) = rren(ra) → lext(la) ≠ None ∧ rext(ra) ≠ None ∧ lext(la) = rext(ra)) ∧ (¬ cod(rren)(lren(la)) ∧ ¬ cod(lren)(rren(ra)) ∧ lext(la) ≠ None ∧ rext(ra) ≠ None → lext(la) ≠ rext(ra)))

• Proof step 6:

  aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), ¬(aren(aa) = ren(a0) ↔ true), inj(aren), inj(ren), oinj(aext), oinj(ext), surj(ren, aren), Πok(ext, cext, ren, cren), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)) ⊦

Rule argument

Additional information

Used terms: ext, aext, ren, aren

Proof step 5 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

A spec-lemma

Proof step 6 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 7:

  aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), ¬(aren(aa) = ren(a0) ↔ true), inj(ren), inj(aren), oinj(ext), oinj(aext), surj(ren, aren), Πok(ext, cext, ren, cren), ren(a0) = aren(aa) → ext(a0) ≠ None ∧ aext(aa) ≠ None ∧ ext(a0) = aext(aa), ¬ cod(aren)(ren(a0)) ∧ ¬ cod(ren)(aren(aa)) ∧ ext(a0) ≠ None ∧ aext(aa) ≠ None → ext(a0) ≠ aext(aa), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)) ⊦

Rule argument

Additional information

Used terms: a0, aa

Proof step 7 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), aren(aa) ≠ ren(a0), inj(ren), inj(aren), oinj(ext), oinj(aext), surj(ren, aren), Πok(ext, cext, ren, cren), ¬ cod(aren)(ren(a0)) ∧ ¬ cod(ren)(aren(aa)) → ext(a0) ≠ Some(e), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ Some(a) ≠ None; (s) ⊦ Πok(lext, rext, lren, rren) ∧ lren(la) = rren(ra) → (lext(la) = None ↔ false); (as)

Proof step 8 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ Πok(lext, rext, lren, rren) ↔ inj(lren) ∧ inj(rren) ∧ surj(lren, rren) ∧ sharingok(lext, rext, lren, rren)

• Proof step 10:

  aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), aren(aa) ≠ ren(a0), inj(cren), inj(aren), inj(ren), oinj(aext), oinj(ext), sharingok(ext, cext, ren, cren), surj(ren, cren), surj(ren, aren), ¬ cod(aren)(ren(a0)) ∧ ¬ cod(ren)(aren(aa)) → ext(a0) ≠ Some(e), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)) ⊦

Rule argument

Additional information

Used terms: ext, cext, ren, cren

Proof step 9 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ sharingok(lext, rext, lren, rren) ↔ (∀ la, ra. (lren(la) = rren(ra) → lext(la) ≠ None ∧ rext(ra) ≠ None ∧ lext(la) = rext(ra)) ∧ (¬ cod(rren)(lren(la)) ∧ ¬ cod(lren)(rren(ra)) ∧ lext(la) ≠ None ∧ rext(ra) ≠ None → lext(la) ≠ rext(ra)))

• Proof step 12:

  aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), aren(aa) ≠ ren(a0), inj(ren), inj(aren), inj(cren), oinj(ext), oinj(aext), surj(ren, aren), surj(ren, cren), ¬ cod(aren)(ren(a0)) ∧ ¬ cod(ren)(aren(aa)) → ext(a0) ≠ Some(e), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)) ⊦

Rule argument

Additional information

Used terms: ext, cext, ren, cren

Proof step 11 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

A spec-lemma

Proof step 12 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), aren(aa) ≠ ren(a0), inj(cren), inj(aren), inj(ren), oinj(aext), oinj(ext), surj(ren, cren), surj(ren, aren), ¬ cod(aren)(ren(a0)) ∧ ¬ cod(ren)(aren(aa)) → ext(a0) ≠ Some(e), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)) ⊦

Rule argument

Additional information

Proof step 13 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 14:

  aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), ext(a0) = None, aren(aa) ≠ ren(a0), inj(ren), inj(aren), inj(cren), oinj(ext), oinj(aext), surj(ren, aren), surj(ren, cren), ¬ cod(aren)(ren(a0)) ∧ ¬ cod(ren)(aren(aa)) → ext(a0) ≠ Some(e), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)) ⊦

• Proof step 16:

  aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), aren(aa) ≠ ren(a0), ext(a0) ≠ None, inj(ren), inj(aren), inj(cren), oinj(ext), oinj(aext), surj(ren, aren), surj(ren, cren), ¬ cod(aren)(ren(a0)) ∧ ¬ cod(ren)(aren(aa)) → ext(a0) ≠ Some(e), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)) ⊦

Rule argument

Additional information

Used formulas: ext(a0) = None

Proof step 14 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), ext(a0) = None, aren(aa) ≠ ren(a0), inj(ren), inj(aren), inj(cren), oinj(ext), oinj(aext), surj(ren, aren), surj(ren, cren), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ Some(a) ≠ None; (s)

Proof step 15 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a0, ca0

Proof step 16 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), aren(aa) ≠ ren(a0), ext(a0) ≠ None, inj(cren), inj(aren), inj(ren), oinj(aext), oinj(ext), surj(ren, cren), surj(ren, aren), ¬ cod(aren)(ren(a0)) ∧ ¬ cod(ren)(aren(aa)) → ext(a0) ≠ Some(e), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)) ⊦

Rule argument

Additional information

Proof step 17 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 18:

  aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), aren(aa) ≠ ren(a0), ext(a0) ≠ None, inj(ren), inj(aren), inj(cren), oinj(ext), oinj(aext), surj(ren, aren), surj(ren, cren), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)) ⊦ ¬ cod(aren)(ren(a0)) ∧ ¬ cod(ren)(aren(aa))

• Proof step 42:

  aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), aren(aa) ≠ ren(a0), ext(a0) ≠ Some(e), ext(a0) ≠ None, inj(ren), inj(aren), inj(cren), oinj(ext), oinj(aext), surj(ren, aren), surj(ren, cren), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)) ⊦

Rule argument

Additional information

Proof step 18 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 19:

  aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), aren(aa) ≠ ren(a0), ext(a0) ≠ None, cod(aren)(ren(a0)), inj(cren), inj(aren), inj(ren), oinj(aext), oinj(ext), surj(ren, cren), surj(ren, aren), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)) ⊦

• Proof step 31:

  aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), aren(aa) ≠ ren(a0), ext(a0) ≠ None, cod(ren)(aren(aa)), inj(cren), inj(aren), inj(ren), oinj(aext), oinj(ext), surj(ren, cren), surj(ren, aren), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)) ⊦

Rule argument

Additional information

Proof step 19 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  aext(aa) = Some(e), aren(aa0) = ren(a0), cext(ca0) = Some(e), cren(ca0) = ren(a0), aren(aa) ≠ ren(a0), ext(a0) ≠ None, inj(ren), inj(aren), inj(cren), oinj(ext), oinj(aext), surj(ren, aren), surj(ren, cren), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ cod(f)(b) ↔ (∃ a. f(a) = b); (as)

Proof step 20 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 21:

  aext(aa) = Some(e), aren(aa0) = ren(a0), cext(ca0) = Some(e), cren(ca0) = ren(a0), aa0 ≠ aa, aren(aa) ≠ ren(a0), ext(a0) ≠ None, inj(cren), inj(aren), inj(ren), oinj(aext), oinj(ext), surj(ren, cren), surj(ren, aren), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)) ⊦

Rule argument

Additional information

Used formulas: aa0 = aa

Proof step 21 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 22:

  aext(aa) = Some(e), aren(aa0) = ren(a0), cext(ca0) = Some(e), cren(ca0) = ren(a0), aa0 ≠ aa, aren(aa) ≠ ren(a0), ext(a0) ≠ None, inj(ren), inj(aren), inj(cren), oinj(ext), oinj(aext), surj(ren, aren), surj(ren, cren), ren(a0) = aren(aa0) → ext(a0) ≠ None ∧ aext(aa0) ≠ None ∧ ext(a0) = aext(aa0), ¬ cod(aren)(ren(a0)) ∧ ¬ cod(ren)(aren(aa0)) ∧ ext(a0) ≠ None ∧ aext(aa0) ≠ None → ext(a0) ≠ aext(aa0), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)) ⊦

Rule argument

Additional information

Used terms: a0, aa0

Proof step 22 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  aext(aa) = Some(e), aren(aa0) = ren(a0), cext(ca0) = Some(e), cren(ca0) = ren(a0), ext(a0) = aext(aa0), aa0 ≠ aa, aext(aa0) ≠ None, aren(aa) ≠ ren(a0), inj(ren), inj(aren), inj(cren), oinj(ext), oinj(aext), surj(ren, aren), surj(ren, cren), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ cod(f)(f(a)); (s)

Proof step 23 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 24:

  aext(aa) = Some(e), aren(aa0) = ren(a0), cext(ca0) = Some(e), cren(ca0) = ren(a0), ext(a0) = aext(aa0), aa0 ≠ aa, aext(aa0) ≠ None, aren(aa) ≠ ren(a0), inj(cren), inj(aren), inj(ren), oinj(aext), oinj(ext), surj(ren, cren), surj(ren, aren), ren(a0) = cren(ca0) → ext(a0) ≠ None ∧ cext(ca0) ≠ None ∧ ext(a0) = cext(ca0), ¬ cod(cren)(ren(a0)) ∧ ¬ cod(ren)(cren(ca0)) ∧ ext(a0) ≠ None ∧ cext(ca0) ≠ None → ext(a0) ≠ cext(ca0), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)) ⊦

Rule argument

Additional information

Used terms: a0, ca0

Proof step 24 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  Some(e) = aext(aa0), aext(aa) = Some(e), aren(aa0) = ren(a0), cext(ca0) = Some(e), cren(ca0) = ren(a0), ext(a0) = Some(e), aa0 ≠ aa, aren(aa) ≠ ren(a0), inj(cren), inj(aren), inj(ren), oinj(aext), oinj(ext), surj(ren, cren), surj(ren, aren), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ cod(f)(f(a)); (s) ⊦ Some(a) ≠ None; (s)

Proof step 25 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 26:

  aext(aa) = aext(aa0), aren(aa0) = ren(a0), cext(ca0) = aext(aa0), cren(ca0) = ren(a0), ext(a0) = aext(aa0), aa0 ≠ aa, aren(aa) ≠ ren(a0), inj(ren), inj(aren), inj(cren), oinj(ext), oinj(aext), surj(ren, aren), surj(ren, cren), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)) ⊦

Rule argument

Additional information

Proof step 26 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 27:

  aext(aa) = aext(aa0), aren(aa0) = ren(a0), cext(ca0) = aext(aa0), cren(ca0) = ren(a0), ext(a0) = aext(aa0), aa0 ≠ aa, aren(aa) ≠ ren(a0), inj(cren), inj(aren), inj(ren), oinj(aext), oinj(ext), surj(ren, cren), surj(ren, aren), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)) ⊦

Rule argument

Additional information

Used formulas: aa0 = aa

Proof step 27 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

  ⊦ oinj(of) ∧ of(a1) ≠ None → (of(a1) = of(a2) ↔ a1 = a2)

• Proof step 29:

  aext(aa) = aext(aa0), aren(aa0) = ren(a0), cext(ca0) = aext(aa0), cren(ca0) = ren(a0), ext(a0) = aext(aa0), aa0 ≠ aa, aren(aa) ≠ ren(a0), inj(ren), inj(aren), inj(cren), oinj(ext), oinj(aext), surj(ren, aren), surj(ren, cren), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)) ⊦ oinj(aext) ∧ aext(aa) ≠ None

Rule argument

Additional information

Used terms: aext, aa, aa0

Proof step 28 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

A spec-lemma

Proof step 29 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  None = aext(aa0), aext(aa) = None, aren(aa0) = ren(a0), cext(ca0) = None, cren(ca0) = ren(a0), ext(a0) = None, aa0 ≠ aa, aren(aa) ≠ ren(a0), inj(cren), inj(aren), inj(ren), oinj(aext), oinj(ext), surj(ren, cren), surj(ren, aren), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)) ⊦

Rule argument

Additional information

Proof step 30 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a0, ca0

Proof step 31 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 32:

  aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), ren(a) = aren(aa), aren(aa) ≠ ren(a0), ext(a0) ≠ None, inj(ren), inj(aren), inj(cren), oinj(ext), oinj(aext), surj(ren, aren), surj(ren, cren), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ cod(f)(b) ↔ (∃ a. f(a) = b); (as)

Proof step 32 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 33:

  aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), ren(a) = aren(aa), aren(aa) ≠ ren(a0), ext(a0) ≠ None, inj(cren), inj(aren), inj(ren), oinj(aext), oinj(ext), surj(ren, cren), surj(ren, aren), ren(a) = aren(aa) → ext(a) ≠ None ∧ aext(aa) ≠ None ∧ ext(a) = aext(aa), ¬ cod(aren)(ren(a)) ∧ ¬ cod(ren)(aren(aa)) ∧ ext(a) ≠ None ∧ aext(aa) ≠ None → ext(a) ≠ aext(aa), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)) ⊦

Rule argument

Additional information

Used terms: a, aa

Proof step 33 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), ext(a) = Some(e), ren(a) = aren(aa), aren(aa) ≠ ren(a0), ext(a0) ≠ None, inj(cren), inj(aren), inj(ren), oinj(aext), oinj(ext), surj(ren, cren), surj(ren, aren), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ cod(f)(f(a)); (s) ⊦ Some(a) ≠ None; (s)

Proof step 34 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 35:

  aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), ext(a) = Some(e), ren(a) = aren(aa), aren(aa) ≠ ren(a0), ext(a0) ≠ None, inj(ren), inj(aren), inj(cren), oinj(ext), oinj(aext), surj(ren, aren), surj(ren, cren), ren(a0) = cren(ca0) → ext(a0) ≠ None ∧ cext(ca0) ≠ None ∧ ext(a0) = cext(ca0), ¬ cod(cren)(ren(a0)) ∧ ¬ cod(ren)(cren(ca0)) ∧ ext(a0) ≠ None ∧ cext(ca0) ≠ None → ext(a0) ≠ cext(ca0), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)) ⊦

Rule argument

Additional information

Used terms: a0, ca0

Proof step 35 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), ext(a0) = Some(e), ext(a) = Some(e), ren(a) = aren(aa), aren(aa) ≠ ren(a0), inj(ren), inj(aren), inj(cren), oinj(ext), oinj(aext), surj(ren, aren), surj(ren, cren), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ cod(f)(f(a)); (s) ⊦ Some(a) ≠ None; (s)

Proof step 36 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 37:

  aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), ext(a) = Some(e), ext(a0) = Some(e), ren(a) = aren(aa), a0 ≠ a, aren(aa) ≠ ren(a0), inj(cren), inj(aren), inj(ren), oinj(aext), oinj(ext), surj(ren, cren), surj(ren, aren), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)) ⊦

Rule argument

Additional information

Used formulas: a0 = a

Proof step 37 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 38:

  aext(aa) = ext(a), cext(ca0) = ext(a), cren(ca0) = ren(a0), ext(a0) = ext(a), ren(a) = aren(aa), a0 ≠ a, aren(aa) ≠ ren(a0), inj(ren), inj(aren), inj(cren), oinj(ext), oinj(aext), surj(ren, aren), surj(ren, cren), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)) ⊦

Rule argument

Additional information

Proof step 38 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 39:

  ⊦ oinj(of) ∧ of(a1) ≠ None → (of(a1) = of(a2) ↔ a1 = a2)

• Proof step 40:

  aext(aa) = ext(a), cext(ca0) = ext(a), cren(ca0) = ren(a0), ext(a0) = ext(a), ren(a) = aren(aa), a0 ≠ a, aren(aa) ≠ ren(a0), inj(cren), inj(aren), inj(ren), oinj(aext), oinj(ext), surj(ren, cren), surj(ren, aren), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)) ⊦ oinj(ext) ∧ ext(a) ≠ None

Rule argument

Additional information

Used terms: ext, a0, a

Proof step 39 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

A spec-lemma

Proof step 40 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  aext(aa) = None, cext(ca0) = None, cren(ca0) = ren(a0), ext(a0) = None, ext(a) = None, ren(a) = aren(aa), a0 ≠ a, aren(aa) ≠ ren(a0), inj(ren), inj(aren), inj(cren), oinj(ext), oinj(aext), surj(ren, aren), surj(ren, cren), ∀ la, ra. (ren(la) = aren(ra) → ext(la) ≠ None ∧ aext(ra) ≠ None ∧ ext(la) = aext(ra)) ∧ (¬ cod(aren)(ren(la)) ∧ ¬ cod(ren)(aren(ra)) ∧ ext(la) ≠ None ∧ aext(ra) ≠ None → ext(la) ≠ aext(ra)), ∀ la, ra. (ren(la) = cren(ra) → ext(la) ≠ None ∧ cext(ra) ≠ None ∧ ext(la) = cext(ra)) ∧ (¬ cod(cren)(ren(la)) ∧ ¬ cod(ren)(cren(ra)) ∧ ext(la) ≠ None ∧ cext(ra) ≠ None → ext(la) ≠ cext(ra)) ⊦

Rule argument

Additional information

Proof step 41 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a0, ca0

Proof step 42 from proof product-ok-refine-cext-imp-aext (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a0, ca0