Proof step 1 from proof PhIOAut (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  IOAut?(IOAut(lstart, lstep, lext)), IOAut?(IOAut(rstart, rstep, rext)), Πhok(lext, rext, lren, rren, hideext), ¬ IOAut?(Πh(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren, hideext)) ⊦

Rule argument

Additional information

Proof step 2 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  IOAut?(IOAut(rstart, rstep, rext)), IOAut?(IOAut(lstart, lstep, lext)), inj(lren), inj(rren), oinj(hideext), osurj(hideext), sharingok(lext, rext, lren, rren), surj(lren, rren), ¬ IOAut?(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Πh(lext, rext, lren, rren, hideext))), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

Used simplifier rules: hidingproductok-def: ⊦ Πhok(lext, rext, lren, rren, hideext) ↔ inj(lren) ∧ inj(rren) ∧ surj(lren, rren) ∧ sharingok(lext, rext, lren, rren) ∧ hidingok(lext, rext, lren, rren, hideext); hidingok-def: ⊦ hidingok(lext, rext, lren, rren, hideext) ↔ oinj(hideext) ∧ osurj(hideext) ∧ (∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra))); hidingproduct-def: ⊦ Πh(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren, hideext) = IOAut (Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Πh(lext, rext, lren, rren, hideext));

Proof step 3 from proof PhIOAut (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ IOAut?(IOAut(start, step, ext)) ↔ (∃ s. start(s) ∧ oinj(ext))

• Proof step 5:

  IOAut?(IOAut(lstart, lstep, lext)), IOAut?(IOAut(rstart, rstep, rext)), inj(rren), inj(lren), oinj(hideext), osurj(hideext), sharingok(lext, rext, lren, rren), surj(lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ s. ¬(Π(lstart, rstart)(s) ∧ oinj(Πh(lext, rext, lren, rren, hideext))) ⊦

Rule argument

Additional information

Used terms: Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Πh(lext, rext, lren, rren, hideext)

Proof step 4 from proof PhIOAut (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  IOAut?(IOAut(rstart, rstep, rext)), IOAut?(IOAut(lstart, lstep, lext)), inj(lren), inj(rren), oinj(hideext), osurj(hideext), sharingok(lext, rext, lren, rren), surj(lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), (∀ s. ¬ Π(lstart, rstart)(s)) ∨ ¬ oinj(Πh(lext, rext, lren, rren, hideext)) ⊦

Rule argument

Additional information

Proof step 6 from proof PhIOAut (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ IOAut?(IOAut(start, step, ext)) ↔ (∃ s. start(s) ∧ oinj(ext))

• Proof step 8:

  IOAut?(IOAut(lstart, lstep, lext)), inj(rren), inj(lren), oinj(hideext), osurj(hideext), sharingok(lext, rext, lren, rren), surj(lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∃ s. rstart(s) ∧ oinj(rext), (∀ s. ¬ Π(lstart, rstart)(s)) ∨ ¬ oinj(Πh(lext, rext, lren, rren, hideext)) ⊦

Rule argument

Additional information

Used terms: rstart, rstep, rext

Proof step 7 from proof PhIOAut (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  IOAut?(IOAut(lstart, lstep, lext)), inj(lren), inj(rren), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), (∀ s. ¬ Π(lstart, rstart)(s)) ∨ ¬ oinj(Πh(lext, rext, lren, rren, hideext)) ⊦

Rule argument

Additional information

Proof step 9 from proof PhIOAut (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ IOAut?(IOAut(start, step, ext)) ↔ (∃ s. start(s) ∧ oinj(ext))

• Proof step 11:

  inj(rren), inj(lren), oinj(hideext), oinj(rext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∃ s. lstart(s) ∧ oinj(lext), (∀ s. ¬ Π(lstart, rstart)(s)) ∨ ¬ oinj(Πh(lext, rext, lren, rren, hideext)) ⊦

Rule argument

Additional information

Used terms: lstart, lstep, lext

Proof step 10 from proof PhIOAut (previous step) (back to tree)

A spec-lemma

Proof step 11 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), (∀ s. ¬ Π(lstart, rstart)(s)) ∨ ¬ oinj(Πh(lext, rext, lren, rren, hideext)) ⊦

Rule argument

Additional information

Proof step 12 from proof PhIOAut (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 13:

  inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ s. ¬ Π(lstart, rstart)(s) ⊦

• Proof step 14:

  inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), ¬ oinj(Πh(lext, rext, lren, rren, hideext)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

Proof step 13 from proof PhIOAut (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: lrstart-def: ⊦ Π(lstart, rstart)((ls, rs)) ↔ lstart(ls) ∧ rstart(rs); Used terms: (ls, rs)

Proof step 14 from proof PhIOAut (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

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

• Proof step 16:

  inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∃ pa, pa0. ¬(Πh(lext, rext, lren, rren, hideext)(pa) ≠ None ∧ Πh(lext, rext, lren, rren, hideext)(pa) = Πh(lext, rext, lren, rren, hideext)(pa0) → pa = pa0) ⊦

Rule argument

Additional information

Used terms: Πh(lext, rext, lren, rren, hideext)

Proof step 15 from proof PhIOAut (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  Πh(lext, rext, lren, rren, hideext)(pa) = Πh(lext, rext, lren, rren, hideext)(pa0), pa ≠ pa0, Πh(lext, rext, lren, rren, hideext)(pa0) ≠ None, inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

Proof step 17 from proof PhIOAut (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 18:

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

• Proof step 19:

  Πok(lext, rext, lren, rren) ↔ inj(lren) ∧ inj(rren) ∧ surj(lren, rren) ∧ sharingok(lext, rext, lren, rren), Πh(lext, rext, lren, rren, hideext)(pa) = Πh(lext, rext, lren, rren, hideext)(pa0), pa ≠ pa0, Πh(lext, rext, lren, rren, hideext)(pa0) ≠ None, inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

Used terms: lext, rext, lren, rren

Proof step 18 from proof PhIOAut (previous step) (back to tree)

Lemma productok-def

Proof step 19 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  Πh(lext, rext, lren, rren, hideext)(pa) = Πh(lext, rext, lren, rren, hideext)(pa0), pa ≠ pa0, Πh(lext, rext, lren, rren, hideext)(pa0) ≠ None, inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

Proof step 20 from proof PhIOAut (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ surj(lren, rren) ↔ (∀ pa. (∃ la. pa = lren(la)) ∨ (∃ ra. pa = rren(ra)))

• Proof step 22:

  Πh(lext, rext, lren, rren, hideext)(pa) = Πh(lext, rext, lren, rren, hideext)(pa0), pa ≠ pa0, Πh(lext, rext, lren, rren, hideext)(pa0) ≠ None, inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ pa. (∃ la. pa = lren(la)) ∨ (∃ ra. pa = rren(ra)) ⊦

Rule argument

Additional information

Used terms: lren, rren

Proof step 21 from proof PhIOAut (previous step) (back to tree)

Lemma surj-def

Proof step 22 from proof PhIOAut (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 23:

  Πh(lext, rext, lren, rren, hideext)(pa) = Πh(lext, rext, lren, rren, hideext)(pa0), pa ≠ pa0, Πh(lext, rext, lren, rren, hideext)(pa0) ≠ None, inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), Πok(lext, rext, lren, rren), ∀ pa. (∃ la. pa = lren(la)) ∨ (∃ ra. pa = rren(ra)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), (∃ la. pa = lren(la)) ∨ (∃ ra. pa = rren(ra)) ⊦

Rule argument

Additional information

Used terms: pa

Proof step 23 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  Πh(lext, rext, lren, rren, hideext)(pa) = Πh(lext, rext, lren, rren, hideext)(pa0), pa ≠ pa0, Πh(lext, rext, lren, rren, hideext)(pa0) ≠ None, inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ pa. (∃ la. pa = lren(la)) ∨ (∃ ra. pa = rren(ra)), pa = lren(la) ∨ pa = rren(ra) ⊦

Rule argument

Additional information

Proof step 24 from proof PhIOAut (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 25:

  Πh(lext, rext, lren, rren, hideext)(pa) = Πh(lext, rext, lren, rren, hideext)(pa0), pa ≠ pa0, Πh(lext, rext, lren, rren, hideext)(pa0) ≠ None, inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), pa = lren(la) ∨ pa = rren(ra), (∃ la. pa0 = lren(la)) ∨ (∃ ra. pa0 = rren(ra)) ⊦

Rule argument

Additional information

Used terms: pa0

Proof step 25 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  Πh(lext, rext, lren, rren, hideext)(pa) = Πh(lext, rext, lren, rren, hideext)(pa0), pa ≠ pa0, Πh(lext, rext, lren, rren, hideext)(pa0) ≠ None, inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), pa = lren(la) ∨ pa = rren(ra), pa0 = lren(la0) ∨ pa0 = rren(ra0) ⊦

Rule argument

Additional information

Proof step 26 from proof PhIOAut (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

  ⊦ 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 28:

  Πh(lext, rext, lren, rren, hideext)(pa) = Πh(lext, rext, lren, rren, hideext)(pa0), pa ≠ pa0, Πh(lext, rext, lren, rren, hideext)(pa0) ≠ None, inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)), pa0 = lren(la0) ∨ pa0 = rren(ra0), pa = lren(la) ∨ pa = rren(ra) ⊦

Rule argument

Additional information

Used terms: lext, rext, lren, rren

Proof step 27 from proof PhIOAut (previous step) (back to tree)

Lemma sharingok-def

Proof step 28 from proof PhIOAut (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 29:

  pa = lren(la), Πh(lext, rext, lren, rren, hideext)(pa) = Πh(lext, rext, lren, rren, hideext)(pa0), pa ≠ pa0, Πh(lext, rext, lren, rren, hideext)(pa0) ≠ None, inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), pa0 = lren(la0) ∨ pa0 = rren(ra0) ⊦

• Proof step 74:

  pa = rren(ra), Πh(lext, rext, lren, rren, hideext)(pa) = Πh(lext, rext, lren, rren, hideext)(pa0), pa ≠ pa0, Πh(lext, rext, lren, rren, hideext)(pa0) ≠ None, inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), pa0 = lren(la0) ∨ pa0 = rren(ra0) ⊦

Rule argument

Additional information

Proof step 29 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  Πh(lext, rext, lren, rren, hideext)(lren(la)) = Πh(lext, rext, lren, rren, hideext)(pa0), lren(la) ≠ pa0, Πh(lext, rext, lren, rren, hideext)(pa0) ≠ None, inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)), pa0 = lren(la0) ∨ pa0 = rren(ra0) ⊦

Rule argument

Additional information

Proof step 30 from proof PhIOAut (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 31:

  ⊦ Πhok(lext, rext, lren, rren, hideext) → Πh(lext, rext, lren, rren, hideext)(lren(la)) = ((hideext o lext))(la)

• Proof step 32:

  Πh(lext, rext, lren, rren, hideext)(lren(la)) = Πh(lext, rext, lren, rren, hideext)(pa0), lren(la) ≠ pa0, Πh(lext, rext, lren, rren, hideext)(pa0) ≠ None, inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), Πok(lext, rext, lren, rren), ¬ Πhok(lext, rext, lren, rren, hideext), ∀ 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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), pa0 = lren(la0) ∨ pa0 = rren(ra0) ⊦

• Proof step 35:

  ((hideext o lext))(la) = Πh(lext, rext, lren, rren, hideext)(pa0), lren(la) ≠ pa0, Πh(lext, rext, lren, rren, hideext)(pa0) ≠ None, inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), Πhok(lext, rext, lren, rren, hideext), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), pa0 = lren(la0) ∨ pa0 = rren(ra0) ⊦

Rule argument

Additional information

Used terms: rext, lren, lext, rren, la, hideext

Proof step 31 from proof PhIOAut (previous step) (back to tree)

Lemma lrexth-def-left

Proof step 32 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  Πh(lext, rext, lren, rren, hideext)(lren(la)) = Πh(lext, rext, lren, rren, hideext)(pa0), lren(la) ≠ pa0, Πh(lext, rext, lren, rren, hideext)(pa0) ≠ None, inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)), pa0 = lren(la0) ∨ pa0 = rren(ra0) ⊦ surj(lren, rren) ∧ sharingok(lext, rext, lren, rren)

Rule argument

Additional information

Used simplifier rules: hidingproductok-def: ⊦ Πhok(lext, rext, lren, rren, hideext) ↔ inj(lren) ∧ inj(rren) ∧ surj(lren, rren) ∧ sharingok(lext, rext, lren, rren) ∧ hidingok(lext, rext, lren, rren, hideext); hidingok-def: ⊦ hidingok(lext, rext, lren, rren, hideext) ↔ oinj(hideext) ∧ osurj(hideext) ∧ (∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)));

Proof step 33 from proof PhIOAut (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 34:

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

Rule argument

Additional information

Used terms: lext, rext, lren, rren

Proof step 34 from proof PhIOAut (previous step) (back to tree)

Lemma productok-def

Proof step 35 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  (lext(la) ≠ None ⊃ hideext(lext(la).get);None) = Πh(lext, rext, lren, rren, hideext)(pa0), lren(la) ≠ pa0, Πh(lext, rext, lren, rren, hideext)(pa0) ≠ None, inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)), pa0 = lren(la0) ∨ pa0 = rren(ra0) ⊦

Rule argument

Additional information

Used simplifier rules: hidingproductok-def: ⊦ Πhok(lext, rext, lren, rren, hideext) ↔ inj(lren) ∧ inj(rren) ∧ surj(lren, rren) ∧ sharingok(lext, rext, lren, rren) ∧ hidingok(lext, rext, lren, rren, hideext); hidingok-def: ⊦ hidingok(lext, rext, lren, rren, hideext) ↔ oinj(hideext) ∧ osurj(hideext) ∧ (∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra))); ⊦ ((og o of))(a) = (of(a) ≠ None ⊃ og(of(a).get);None); (s)

Proof step 36 from proof PhIOAut (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 37:

  hideext(lext(la).get) = Πh(lext, rext, lren, rren, hideext)(pa0), lext(la) ≠ None, lren(la) ≠ pa0, Πh(lext, rext, lren, rren, hideext)(pa0) ≠ None, inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), pa0 = lren(la0) ∨ pa0 = rren(ra0) ⊦

Rule argument

Additional information

Proof step 37 from proof PhIOAut (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 38:

  hideext(e0) = Πh(lext, rext, lren, rren, hideext)(pa0), lext(la) = Some(e0), lext(la) ≠ None, lren(la) ≠ pa0, Πh(lext, rext, lren, rren, hideext)(pa0) ≠ None, inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)), pa0 = lren(la0) ∨ pa0 = rren(ra0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ opt ≠ None → (get = opt.get ↔ opt = Some(get)); (elim) Used terms: lext(la), e0

Proof step 38 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  hideext(e0) = Πh(lext, rext, lren, rren, hideext)(pa0), lext(la) = Some(e0), hideext(e0) ≠ None, lren(la) ≠ pa0, inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)), pa0 = lren(la0) ∨ pa0 = rren(ra0) ⊦

Rule argument

Additional information

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

Proof step 39 from proof PhIOAut (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 40:

  hideext(e0) = Πh(lext, rext, lren, rren, hideext)(pa0), lext(la) = Some(e0), pa0 = lren(la0), hideext(e0) ≠ None, lren(la) ≠ pa0, inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

• Proof step 51:

  hideext(e0) = Πh(lext, rext, lren, rren, hideext)(pa0), lext(la) = Some(e0), pa0 = rren(ra0), hideext(e0) ≠ None, lren(la) ≠ pa0, inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

Proof step 40 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  hideext(e0) = Πh(lext, rext, lren, rren, hideext)(lren(la0)), lext(la) = Some(e0), hideext(e0) ≠ None, la ≠ la0, inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ inj(f) → (f(a1) = f(a2) ↔ a1 = a2); (s)

Proof step 41 from proof PhIOAut (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 42:

  ⊦ Πhok(lext, rext, lren, rren, hideext) → Πh(lext, rext, lren, rren, hideext)(lren(la)) = ((hideext o lext))(la)

• Proof step 43:

  hideext(e0) = ((hideext o lext))(la0), lext(la) = Some(e0), hideext(e0) ≠ None, la ≠ la0, inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πhok(lext, rext, lren, rren, hideext), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

Used simplifier rules: hidingproductok-def: ⊦ Πhok(lext, rext, lren, rren, hideext) ↔ inj(lren) ∧ inj(rren) ∧ surj(lren, rren) ∧ sharingok(lext, rext, lren, rren) ∧ hidingok(lext, rext, lren, rren, hideext); hidingok-def: ⊦ hidingok(lext, rext, lren, rren, hideext) ↔ oinj(hideext) ∧ osurj(hideext) ∧ (∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra))); Used terms: rext, lren, lext, rren, la0, hideext

Proof step 42 from proof PhIOAut (previous step) (back to tree)

Lemma lrexth-def-left

Proof step 43 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 44:

  hideext(e0) = (lext(la0) ≠ None ⊃ hideext(lext(la0).get);None), lext(la) = Some(e0), hideext(e0) ≠ None, la ≠ la0, inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)) ⊦

Rule argument

Additional information

Used simplifier rules: hidingproductok-def: ⊦ Πhok(lext, rext, lren, rren, hideext) ↔ inj(lren) ∧ inj(rren) ∧ surj(lren, rren) ∧ sharingok(lext, rext, lren, rren) ∧ hidingok(lext, rext, lren, rren, hideext); hidingok-def: ⊦ hidingok(lext, rext, lren, rren, hideext) ↔ oinj(hideext) ∧ osurj(hideext) ∧ (∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra))); ⊦ ((og o of))(a) = (of(a) ≠ None ⊃ og(of(a).get);None); (s)

Proof step 44 from proof PhIOAut (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 45:

  hideext(e0) = hideext(lext(la0).get), lext(la) = Some(e0), hideext(e0) ≠ None, la ≠ la0, lext(la0) ≠ None, inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

Proof step 45 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

  lext(la) = Some(lext(la0).get), hideext(lext(la0).get) ≠ None, la ≠ la0, lext(la0) ≠ None, inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ oinj(of) ∧ of(a1) ≠ None → (of(a1) = of(a2) ↔ a1 = a2); (s)

Proof step 46 from proof PhIOAut (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 47:

  lext(la) = Some(e0), lext(la0) = Some(e0), hideext(e0) ≠ None, la ≠ la0, lext(la0) ≠ None, inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ opt ≠ None → (get = opt.get ↔ opt = Some(get)); (elim) Used terms: lext(la0), e0

Proof step 47 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 48:

  lext(la) = Some(e0), lext(la0) = Some(e0), hideext(e0) ≠ None, la ≠ la0, inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)) ⊦

Rule argument

Additional information

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

Proof step 48 from proof PhIOAut (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 49:

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

• Proof step 50:

  lext(la0) = Some(e0), lext(la) = Some(e0), hideext(e0) ≠ None, la ≠ la0, inj(lren), inj(rren), lstart(ls), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ la, la0. lext(la) ≠ None ∧ lext(la) = lext(la0) → la = la0 ⊦

Rule argument

Additional information

Used terms: lext

Proof step 49 from proof PhIOAut (previous step) (back to tree)

A spec-lemma

Proof step 50 from proof PhIOAut (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ Some(a) ≠ None; (s) Used terms: la, la0

Proof step 51 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 52:

  hideext(e0) = Πh(lext, rext, lren, rren, hideext)(rren(ra0)), lext(la) = Some(e0), hideext(e0) ≠ None, lren(la) ≠ rren(ra0), inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)) ⊦

Rule argument

Additional information

Proof step 52 from proof PhIOAut (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 53:

  ⊦ Πhok(lext, rext, lren, rren, hideext) → Πh(lext, rext, lren, rren, hideext)(rren(ra)) = ((hideext o rext))(ra)

• Proof step 54:

  hideext(e0) = ((hideext o rext))(ra0), lext(la) = Some(e0), hideext(e0) ≠ None, lren(la) ≠ rren(ra0), inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πhok(lext, rext, lren, rren, hideext), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

Used simplifier rules: hidingproductok-def: ⊦ Πhok(lext, rext, lren, rren, hideext) ↔ inj(lren) ∧ inj(rren) ∧ surj(lren, rren) ∧ sharingok(lext, rext, lren, rren) ∧ hidingok(lext, rext, lren, rren, hideext); hidingok-def: ⊦ hidingok(lext, rext, lren, rren, hideext) ↔ oinj(hideext) ∧ osurj(hideext) ∧ (∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra))); Used terms: rext, ra0, lren, lext, rren, hideext

Proof step 53 from proof PhIOAut (previous step) (back to tree)

Lemma lrexth-def-right

Proof step 54 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 55:

  hideext(e0) = (rext(ra0) ≠ None ⊃ hideext(rext(ra0).get);None), lext(la) = Some(e0), hideext(e0) ≠ None, lren(la) ≠ rren(ra0), inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)) ⊦

Rule argument

Additional information

Used simplifier rules: hidingproductok-def: ⊦ Πhok(lext, rext, lren, rren, hideext) ↔ inj(lren) ∧ inj(rren) ∧ surj(lren, rren) ∧ sharingok(lext, rext, lren, rren) ∧ hidingok(lext, rext, lren, rren, hideext); hidingok-def: ⊦ hidingok(lext, rext, lren, rren, hideext) ↔ oinj(hideext) ∧ osurj(hideext) ∧ (∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra))); ⊦ ((og o of))(a) = (of(a) ≠ None ⊃ og(of(a).get);None); (s)

Proof step 55 from proof PhIOAut (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 56:

  hideext(e0) = hideext(rext(ra0).get), lext(la) = Some(e0), hideext(e0) ≠ None, lren(la) ≠ rren(ra0), rext(ra0) ≠ None, inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

Proof step 56 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 57:

  lext(la) = Some(rext(ra0).get), hideext(rext(ra0).get) ≠ None, lren(la) ≠ rren(ra0), rext(ra0) ≠ None, inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ oinj(of) ∧ of(a1) ≠ None → (of(a1) = of(a2) ↔ a1 = a2); (s)

Proof step 57 from proof PhIOAut (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 58:

  lext(la) = Some(e0), rext(ra0) = Some(e0), hideext(e0) ≠ None, lren(la) ≠ rren(ra0), rext(ra0) ≠ None, inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ opt ≠ None → (get = opt.get ↔ opt = Some(get)); (elim) Used terms: rext(ra0), e0

Proof step 58 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 59:

  lext(la) = Some(e0), rext(ra0) = Some(e0), hideext(e0) ≠ None, lren(la) ≠ rren(ra0), inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)) ⊦

Rule argument

Additional information

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

Proof step 59 from proof PhIOAut (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 60:

  lext(la) = Some(e0), rext(ra0) = Some(e0), hideext(e0) ≠ None, lren(la) ≠ rren(ra0), inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), lren(la) = rren(ra0) → lext(la) ≠ None ∧ rext(ra0) ≠ None ∧ lext(la) = rext(ra0), ¬ cod(rren)(lren(la)) ∧ ¬ cod(lren)(rren(ra0)) ∧ lext(la) ≠ None ∧ rext(ra0) ≠ None → lext(la) ≠ rext(ra0), ∀ 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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

Used terms: la, ra0

Proof step 60 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 61:

  lext(la) = Some(e0), rext(ra0) = Some(e0), hideext(e0) ≠ None, lren(la) ≠ rren(ra0), inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦ ¬ cod(rren)(lren(la)) ∧ ¬ cod(lren)(rren(ra0))

Rule argument

Additional information

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

Proof step 61 from proof PhIOAut (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 62:

  lext(la) = Some(e0), rext(ra0) = Some(e0), hideext(e0) ≠ None, lren(la) ≠ rren(ra0), cod(rren)(lren(la)), inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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 68:

  lext(la) = Some(e0), rext(ra0) = Some(e0), hideext(e0) ≠ None, lren(la) ≠ rren(ra0), cod(lren)(rren(ra0)), inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)) ⊦

Rule argument

Additional information

Proof step 62 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 63:

  lext(la) = Some(e0), rext(ra0) = Some(e0), rren(ra) = lren(la), hideext(e0) ≠ None, lren(la) ≠ rren(ra0), inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

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

Proof step 63 from proof PhIOAut (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 64:

  lext(la) = Some(e0), rext(ra0) = Some(e0), rren(ra) = lren(la), hideext(e0) ≠ None, lren(la) ≠ rren(ra0), inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), 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), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

Used terms: la, ra

Proof step 64 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 65:

  lext(la) = Some(e0), rext(ra) = Some(e0), rext(ra0) = Some(e0), rren(ra) = lren(la), hideext(e0) ≠ None, lren(la) ≠ rren(ra0), inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

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

Proof step 65 from proof PhIOAut (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 66:

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

• Proof step 67:

  lext(la) = Some(e0), rext(ra0) = Some(e0), rext(ra) = Some(e0), rren(ra) = lren(la), hideext(e0) ≠ None, lren(la) ≠ rren(ra0), inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ ra, ra0. rext(ra) ≠ None ∧ rext(ra) = rext(ra0) → ra = ra0 ⊦

Rule argument

Additional information

Used terms: rext

Proof step 66 from proof PhIOAut (previous step) (back to tree)

A spec-lemma

Proof step 67 from proof PhIOAut (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ Some(a) ≠ None; (s) Used terms: ra, ra0

Proof step 68 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 69:

  lext(la) = Some(e0), lren(la0) = rren(ra0), rext(ra0) = Some(e0), hideext(e0) ≠ None, lren(la) ≠ rren(ra0), inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

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

Proof step 69 from proof PhIOAut (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 70:

  lext(la) = Some(e0), lren(la0) = rren(ra0), rext(ra0) = Some(e0), hideext(e0) ≠ None, lren(la) ≠ rren(ra0), inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), lren(la0) = rren(ra0) → lext(la0) ≠ None ∧ rext(ra0) ≠ None ∧ lext(la0) = rext(ra0), ¬ cod(rren)(lren(la0)) ∧ ¬ cod(lren)(rren(ra0)) ∧ lext(la0) ≠ None ∧ rext(ra0) ≠ None → lext(la0) ≠ rext(ra0), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

Used terms: la0, ra0

Proof step 70 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 71:

  lext(la0) = Some(e0), lext(la) = Some(e0), lren(la0) = rren(ra0), rext(ra0) = Some(e0), hideext(e0) ≠ None, lren(la) ≠ rren(ra0), inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

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

Proof step 71 from proof PhIOAut (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 72:

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

• Proof step 73:

  lext(la) = Some(e0), lext(la0) = Some(e0), lren(la0) = rren(ra0), rext(ra0) = Some(e0), hideext(e0) ≠ None, lren(la) ≠ rren(ra0), inj(lren), inj(rren), lstart(ls), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ la, la0. lext(la) ≠ None ∧ lext(la) = lext(la0) → la = la0 ⊦

Rule argument

Additional information

Used terms: lext

Proof step 72 from proof PhIOAut (previous step) (back to tree)

A spec-lemma

Proof step 73 from proof PhIOAut (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ Some(a) ≠ None; (s) Used terms: la, la0

Proof step 74 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 75:

  Πh(lext, rext, lren, rren, hideext)(rren(ra)) = Πh(lext, rext, lren, rren, hideext)(pa0), rren(ra) ≠ pa0, Πh(lext, rext, lren, rren, hideext)(pa0) ≠ None, inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)), pa0 = lren(la0) ∨ pa0 = rren(ra0) ⊦

Rule argument

Additional information

Proof step 75 from proof PhIOAut (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 76:

  ⊦ Πhok(lext, rext, lren, rren, hideext) → Πh(lext, rext, lren, rren, hideext)(rren(ra)) = ((hideext o rext))(ra)

• Proof step 77:

  Πh(lext, rext, lren, rren, hideext)(rren(ra)) = Πh(lext, rext, lren, rren, hideext)(pa0), rren(ra) ≠ pa0, Πh(lext, rext, lren, rren, hideext)(pa0) ≠ None, inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), Πok(lext, rext, lren, rren), ¬ Πhok(lext, rext, lren, rren, hideext), ∀ 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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), pa0 = lren(la0) ∨ pa0 = rren(ra0) ⊦

• Proof step 80:

  ((hideext o rext))(ra) = Πh(lext, rext, lren, rren, hideext)(pa0), rren(ra) ≠ pa0, Πh(lext, rext, lren, rren, hideext)(pa0) ≠ None, inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), Πhok(lext, rext, lren, rren, hideext), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), pa0 = lren(la0) ∨ pa0 = rren(ra0) ⊦

Rule argument

Additional information

Used terms: rext, ra, lren, lext, rren, hideext

Proof step 76 from proof PhIOAut (previous step) (back to tree)

Lemma lrexth-def-right

Proof step 77 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 78:

  Πh(lext, rext, lren, rren, hideext)(rren(ra)) = Πh(lext, rext, lren, rren, hideext)(pa0), rren(ra) ≠ pa0, Πh(lext, rext, lren, rren, hideext)(pa0) ≠ None, inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)), pa0 = lren(la0) ∨ pa0 = rren(ra0) ⊦ surj(lren, rren) ∧ sharingok(lext, rext, lren, rren)

Rule argument

Additional information

Used simplifier rules: hidingproductok-def: ⊦ Πhok(lext, rext, lren, rren, hideext) ↔ inj(lren) ∧ inj(rren) ∧ surj(lren, rren) ∧ sharingok(lext, rext, lren, rren) ∧ hidingok(lext, rext, lren, rren, hideext); hidingok-def: ⊦ hidingok(lext, rext, lren, rren, hideext) ↔ oinj(hideext) ∧ osurj(hideext) ∧ (∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)));

Proof step 78 from proof PhIOAut (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 79:

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

Rule argument

Additional information

Used terms: lext, rext, lren, rren

Proof step 79 from proof PhIOAut (previous step) (back to tree)

Lemma productok-def

Proof step 80 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 81:

  (rext(ra) ≠ None ⊃ hideext(rext(ra).get);None) = Πh(lext, rext, lren, rren, hideext)(pa0), rren(ra) ≠ pa0, Πh(lext, rext, lren, rren, hideext)(pa0) ≠ None, inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)), pa0 = lren(la0) ∨ pa0 = rren(ra0) ⊦

Rule argument

Additional information

Used simplifier rules: hidingproductok-def: ⊦ Πhok(lext, rext, lren, rren, hideext) ↔ inj(lren) ∧ inj(rren) ∧ surj(lren, rren) ∧ sharingok(lext, rext, lren, rren) ∧ hidingok(lext, rext, lren, rren, hideext); hidingok-def: ⊦ hidingok(lext, rext, lren, rren, hideext) ↔ oinj(hideext) ∧ osurj(hideext) ∧ (∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra))); ⊦ ((og o of))(a) = (of(a) ≠ None ⊃ og(of(a).get);None); (s)

Proof step 81 from proof PhIOAut (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 82:

  hideext(rext(ra).get) = Πh(lext, rext, lren, rren, hideext)(pa0), rext(ra) ≠ None, rren(ra) ≠ pa0, Πh(lext, rext, lren, rren, hideext)(pa0) ≠ None, inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), pa0 = lren(la0) ∨ pa0 = rren(ra0) ⊦

Rule argument

Additional information

Proof step 82 from proof PhIOAut (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 83:

  hideext(e0) = Πh(lext, rext, lren, rren, hideext)(pa0), rext(ra) = Some(e0), rext(ra) ≠ None, rren(ra) ≠ pa0, Πh(lext, rext, lren, rren, hideext)(pa0) ≠ None, inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)), pa0 = lren(la0) ∨ pa0 = rren(ra0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ opt ≠ None → (get = opt.get ↔ opt = Some(get)); (elim) Used terms: rext(ra), e0

Proof step 83 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 84:

  hideext(e0) = Πh(lext, rext, lren, rren, hideext)(pa0), rext(ra) = Some(e0), hideext(e0) ≠ None, rren(ra) ≠ pa0, inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)), pa0 = lren(la0) ∨ pa0 = rren(ra0) ⊦

Rule argument

Additional information

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

Proof step 84 from proof PhIOAut (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 85:

  hideext(e0) = Πh(lext, rext, lren, rren, hideext)(pa0), pa0 = lren(la0), rext(ra) = Some(e0), hideext(e0) ≠ None, rren(ra) ≠ pa0, inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

• Proof step 108:

  hideext(e0) = Πh(lext, rext, lren, rren, hideext)(pa0), pa0 = rren(ra0), rext(ra) = Some(e0), hideext(e0) ≠ None, rren(ra) ≠ pa0, inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

Proof step 85 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 86:

  hideext(e0) = Πh(lext, rext, lren, rren, hideext)(lren(la0)), rext(ra) = Some(e0), hideext(e0) ≠ None, rren(ra) ≠ lren(la0), inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)) ⊦

Rule argument

Additional information

Proof step 86 from proof PhIOAut (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 87:

  ⊦ Πhok(lext, rext, lren, rren, hideext) → Πh(lext, rext, lren, rren, hideext)(lren(la)) = ((hideext o lext))(la)

• Proof step 88:

  hideext(e0) = ((hideext o lext))(la0), rext(ra) = Some(e0), hideext(e0) ≠ None, rren(ra) ≠ lren(la0), inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πhok(lext, rext, lren, rren, hideext), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

Used simplifier rules: hidingproductok-def: ⊦ Πhok(lext, rext, lren, rren, hideext) ↔ inj(lren) ∧ inj(rren) ∧ surj(lren, rren) ∧ sharingok(lext, rext, lren, rren) ∧ hidingok(lext, rext, lren, rren, hideext); hidingok-def: ⊦ hidingok(lext, rext, lren, rren, hideext) ↔ oinj(hideext) ∧ osurj(hideext) ∧ (∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra))); Used terms: rext, lren, lext, rren, la0, hideext

Proof step 87 from proof PhIOAut (previous step) (back to tree)

Lemma lrexth-def-left

Proof step 88 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 89:

  hideext(e0) = (lext(la0) ≠ None ⊃ hideext(lext(la0).get);None), rext(ra) = Some(e0), hideext(e0) ≠ None, rren(ra) ≠ lren(la0), inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)) ⊦

Rule argument

Additional information

Used simplifier rules: hidingproductok-def: ⊦ Πhok(lext, rext, lren, rren, hideext) ↔ inj(lren) ∧ inj(rren) ∧ surj(lren, rren) ∧ sharingok(lext, rext, lren, rren) ∧ hidingok(lext, rext, lren, rren, hideext); hidingok-def: ⊦ hidingok(lext, rext, lren, rren, hideext) ↔ oinj(hideext) ∧ osurj(hideext) ∧ (∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra))); ⊦ ((og o of))(a) = (of(a) ≠ None ⊃ og(of(a).get);None); (s)

Proof step 89 from proof PhIOAut (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 90:

  hideext(e0) = hideext(lext(la0).get), rext(ra) = Some(e0), hideext(e0) ≠ None, lext(la0) ≠ None, rren(ra) ≠ lren(la0), inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

Proof step 90 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 91:

  rext(ra) = Some(lext(la0).get), hideext(lext(la0).get) ≠ None, lext(la0) ≠ None, rren(ra) ≠ lren(la0), inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ oinj(of) ∧ of(a1) ≠ None → (of(a1) = of(a2) ↔ a1 = a2); (s)

Proof step 91 from proof PhIOAut (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 92:

  lext(la0) = Some(e0), rext(ra) = Some(e0), hideext(e0) ≠ None, lext(la0) ≠ None, rren(ra) ≠ lren(la0), inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ opt ≠ None → (get = opt.get ↔ opt = Some(get)); (elim) Used terms: lext(la0), e0

Proof step 92 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 93:

  lext(la0) = Some(e0), rext(ra) = Some(e0), hideext(e0) ≠ None, rren(ra) ≠ lren(la0), inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)) ⊦

Rule argument

Additional information

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

Proof step 93 from proof PhIOAut (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 94:

  lext(la0) = Some(e0), rext(ra) = Some(e0), hideext(e0) ≠ None, rren(ra) ≠ lren(la0), inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), lren(la0) = rren(ra) → lext(la0) ≠ None ∧ rext(ra) ≠ None ∧ lext(la0) = rext(ra), ¬ cod(rren)(lren(la0)) ∧ ¬ cod(lren)(rren(ra)) ∧ lext(la0) ≠ None ∧ rext(ra) ≠ None → lext(la0) ≠ rext(ra), ∀ 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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

Used terms: la0, ra

Proof step 94 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 95:

  lext(la0) = Some(e0), rext(ra) = Some(e0), hideext(e0) ≠ None, rren(ra) ≠ lren(la0), inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦ ¬ cod(rren)(lren(la0)) ∧ ¬ cod(lren)(rren(ra))

Rule argument

Additional information

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

Proof step 95 from proof PhIOAut (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 96:

  lext(la0) = Some(e0), rext(ra) = Some(e0), hideext(e0) ≠ None, rren(ra) ≠ lren(la0), cod(rren)(lren(la0)), inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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 102:

  lext(la0) = Some(e0), rext(ra) = Some(e0), hideext(e0) ≠ None, rren(ra) ≠ lren(la0), cod(lren)(rren(ra)), inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)) ⊦

Rule argument

Additional information

Proof step 96 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 97:

  lext(la0) = Some(e0), rext(ra) = Some(e0), rren(ra0) = lren(la0), hideext(e0) ≠ None, rren(ra) ≠ lren(la0), inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

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

Proof step 97 from proof PhIOAut (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 98:

  lext(la0) = Some(e0), rext(ra) = Some(e0), rren(ra0) = lren(la0), hideext(e0) ≠ None, rren(ra) ≠ lren(la0), inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), lren(la0) = rren(ra0) → lext(la0) ≠ None ∧ rext(ra0) ≠ None ∧ lext(la0) = rext(ra0), ¬ cod(rren)(lren(la0)) ∧ ¬ cod(lren)(rren(ra0)) ∧ lext(la0) ≠ None ∧ rext(ra0) ≠ None → lext(la0) ≠ rext(ra0), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)) ⊦

Rule argument

Additional information

Used terms: la0, ra0

Proof step 98 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 99:

  lext(la0) = Some(e0), rext(ra0) = Some(e0), rext(ra) = Some(e0), rren(ra0) = lren(la0), hideext(e0) ≠ None, rren(ra) ≠ lren(la0), inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)) ⊦

Rule argument

Additional information

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

Proof step 99 from proof PhIOAut (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 100:

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

• Proof step 101:

  lext(la0) = Some(e0), rext(ra) = Some(e0), rext(ra0) = Some(e0), rren(ra0) = lren(la0), hideext(e0) ≠ None, rren(ra) ≠ lren(la0), inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ ra, ra0. rext(ra) ≠ None ∧ rext(ra) = rext(ra0) → ra = ra0 ⊦

Rule argument

Additional information

Used terms: rext

Proof step 100 from proof PhIOAut (previous step) (back to tree)

A spec-lemma

Proof step 101 from proof PhIOAut (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ Some(a) ≠ None; (s) Used terms: ra, ra0

Proof step 102 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 103:

  lext(la0) = Some(e0), lren(la) = rren(ra), rext(ra) = Some(e0), hideext(e0) ≠ None, rren(ra) ≠ lren(la0), inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

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

Proof step 103 from proof PhIOAut (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 104:

  lext(la0) = Some(e0), lren(la) = rren(ra), rext(ra) = Some(e0), hideext(e0) ≠ None, rren(ra) ≠ lren(la0), inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), 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), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

Used terms: la, ra

Proof step 104 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 105:

  lext(la) = Some(e0), lext(la0) = Some(e0), lren(la) = rren(ra), rext(ra) = Some(e0), hideext(e0) ≠ None, rren(ra) ≠ lren(la0), inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

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

Proof step 105 from proof PhIOAut (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 106:

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

• Proof step 107:

  lext(la0) = Some(e0), lext(la) = Some(e0), lren(la) = rren(ra), rext(ra) = Some(e0), hideext(e0) ≠ None, rren(ra) ≠ lren(la0), inj(lren), inj(rren), lstart(ls), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ la, la0. lext(la) ≠ None ∧ lext(la) = lext(la0) → la = la0 ⊦

Rule argument

Additional information

Used terms: lext

Proof step 106 from proof PhIOAut (previous step) (back to tree)

A spec-lemma

Proof step 107 from proof PhIOAut (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ Some(a) ≠ None; (s) Used terms: la, la0

Proof step 108 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 109:

  hideext(e0) = Πh(lext, rext, lren, rren, hideext)(rren(ra0)), rext(ra) = Some(e0), hideext(e0) ≠ None, ra ≠ ra0, inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ inj(f) → (f(a1) = f(a2) ↔ a1 = a2); (s)

Proof step 109 from proof PhIOAut (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 110:

  ⊦ Πhok(lext, rext, lren, rren, hideext) → Πh(lext, rext, lren, rren, hideext)(rren(ra)) = ((hideext o rext))(ra)

• Proof step 111:

  hideext(e0) = ((hideext o rext))(ra0), rext(ra) = Some(e0), hideext(e0) ≠ None, ra ≠ ra0, inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πhok(lext, rext, lren, rren, hideext), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

Used simplifier rules: hidingproductok-def: ⊦ Πhok(lext, rext, lren, rren, hideext) ↔ inj(lren) ∧ inj(rren) ∧ surj(lren, rren) ∧ sharingok(lext, rext, lren, rren) ∧ hidingok(lext, rext, lren, rren, hideext); hidingok-def: ⊦ hidingok(lext, rext, lren, rren, hideext) ↔ oinj(hideext) ∧ osurj(hideext) ∧ (∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra))); Used terms: rext, ra0, lren, lext, rren, hideext

Proof step 110 from proof PhIOAut (previous step) (back to tree)

Lemma lrexth-def-right

Proof step 111 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 112:

  hideext(e0) = (rext(ra0) ≠ None ⊃ hideext(rext(ra0).get);None), rext(ra) = Some(e0), hideext(e0) ≠ None, ra ≠ ra0, inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)) ⊦

Rule argument

Additional information

Used simplifier rules: hidingproductok-def: ⊦ Πhok(lext, rext, lren, rren, hideext) ↔ inj(lren) ∧ inj(rren) ∧ surj(lren, rren) ∧ sharingok(lext, rext, lren, rren) ∧ hidingok(lext, rext, lren, rren, hideext); hidingok-def: ⊦ hidingok(lext, rext, lren, rren, hideext) ↔ oinj(hideext) ∧ osurj(hideext) ∧ (∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra))); ⊦ ((og o of))(a) = (of(a) ≠ None ⊃ og(of(a).get);None); (s)

Proof step 112 from proof PhIOAut (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 113:

  hideext(e0) = hideext(rext(ra0).get), rext(ra) = Some(e0), hideext(e0) ≠ None, ra ≠ ra0, rext(ra0) ≠ None, inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

Proof step 113 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 114:

  rext(ra) = Some(rext(ra0).get), hideext(rext(ra0).get) ≠ None, ra ≠ ra0, rext(ra0) ≠ None, inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(rext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ oinj(of) ∧ of(a1) ≠ None → (of(a1) = of(a2) ↔ a1 = a2); (s)

Proof step 114 from proof PhIOAut (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 115:

  rext(ra) = Some(e0), rext(ra0) = Some(e0), hideext(e0) ≠ None, ra ≠ ra0, rext(ra0) ≠ None, inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ opt ≠ None → (get = opt.get ↔ opt = Some(get)); (elim) Used terms: rext(ra0), e0

Proof step 115 from proof PhIOAut (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 116:

  rext(ra) = Some(e0), rext(ra0) = Some(e0), hideext(e0) ≠ None, ra ≠ ra0, inj(rren), inj(lren), lstart(ls), oinj(hideext), oinj(rext), oinj(lext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(lext, rext, lren, rren), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ 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)) ⊦

Rule argument

Additional information

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

Proof step 116 from proof PhIOAut (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 117:

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

• Proof step 118:

  rext(ra0) = Some(e0), rext(ra) = Some(e0), hideext(e0) ≠ None, ra ≠ ra0, inj(lren), inj(rren), lstart(ls), oinj(lext), oinj(hideext), osurj(hideext), rstart(rs), sharingok(lext, rext, lren, rren), surj(lren, rren), Πok(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)), ∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)), ∀ ra, ra0. rext(ra) ≠ None ∧ rext(ra) = rext(ra0) → ra = ra0 ⊦

Rule argument

Additional information

Used terms: rext

Proof step 117 from proof PhIOAut (previous step) (back to tree)

A spec-lemma

Proof step 118 from proof PhIOAut (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ Some(a) ≠ None; (s) Used terms: ra, ra0