Proof step 1 from proof pis-mon (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf), ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n), paf.take(n + 1))⌝ ⊦

Rule argument

Additional information

Proof step 2 from proof pis-mon (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf), ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(0 + 1), paf.take(0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + 0), paf.take(0 + 1))⌝ ⊦

• Proof step 18:

  fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf), ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(n0 +1 + 1), paf.take(n0 +1))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n0 +1), paf.take(n0 +1 + 1))⌝ , ∀ lstart, lstep, lext, rstart, rstep, rext, lren, rren, psf, paf. ¬ ( fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf) ∧ ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(n0 + 1), paf.take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n0), paf.take(n0 + 1))⌝ ) ⊦

Rule argument

Additional information

Used simplifier rules: Nat freely generated by 0, +1;;

Proof step 3 from proof pis-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf), ¬ ⌜πrs(lstep, rstep, lren, rren, psf(0) ', [])⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf(0) ' + psf(1) ', paf(0) ')⌝ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ nf.take(1) = nf(0) '; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ nf.take(2) = nf(0) ' + nf(1) '; (s) ⊦ nf.take(0) = []; (s)

Proof step 4 from proof pis-mon (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 5:

  (ls, rs) = psf(0), fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf), ¬ ⌜πrs(lstep, rstep, lren, rren, psf(0) ', [])⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf(0) ' + psf(1) ', paf(0) ')⌝ ⊦

Rule argument

Additional information

Proof step 5 from proof pis-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  (ls, rs) = psf(0), fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf), ¬ ⌜rs '⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + psf(1) ', paf(0) ')⌝ ⊦

Rule argument

Additional information

Used simplifier rules: projstate-base: ⊦ πrs(lstep, rstep, lren, rren, (ls, rs) ', []) = rs ';

Proof step 6 from proof pis-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren) = IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren))

• Proof step 8:

  (ls, rs) = psf(0), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ¬ ⌜rs '⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + psf(1) ', paf(0) ')⌝ ⊦

Rule argument

Additional information

Used terms: rext, rstep, rstart, lren, rren, lstart, lstep, lext

Proof step 7 from proof pis-mon (previous step) (back to tree)

A spec-lemma

Proof step 8 from proof pis-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  α ≠ [] ⊦ ¬ step(σ[0], α[0], σ[1]) → (frag(IOAut(start, step, ext))(σ, α) ↔ false)

• Proof step 10:

  (ls, rs) = psf(0), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ¬ ⌜rs '⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + psf(1) ', paf(0) ')⌝ ⊦ ⌜paf⌝ ≠ [] ∧ ¬ Π(lstep, rstep, lren, rren, lext, rext)(⌜psf⌝ [0], ⌜paf⌝ [0], ⌜psf⌝ [1])

Rule argument

Additional information

Used terms: Π(lext, rext, lren, rren), ⌜paf⌝ , Π(lstep, rstep, lren, rren, lext, rext), Π(lstart, rstart), ⌜psf⌝

Proof step 9 from proof pis-mon (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof pis-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  (ls, rs) = psf(0), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), Π(lstep, rstep, lren, rren, lext, rext)((ls, rs), paf(0), psf(1)), ¬ ⌜rs '⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + psf(1) ', paf(0) ')⌝ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜nf⌝ [n] = nf(n); (s) ⊦ [] ≠ ⌜nf⌝ ; (s)

Proof step 11 from proof pis-mon (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 12:

  (ls, rs) = psf(0), (ls0, rs0) = psf(1), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), Π(lstep, rstep, lren, rren, lext, rext)((ls, rs), paf(0), psf(1)), ¬ ⌜rs '⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + psf(1) ', paf(0) ')⌝ ⊦

Rule argument

Additional information

Proof step 12 from proof pis-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  (ls0, rs0) = psf(1), (ls, rs) = psf(0), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), Π(lstep, rstep, lren, rren, lext, rext)((ls, rs), paf(0), (ls0, rs0)), ¬ ⌜rs '⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (ls0, rs0) ', paf(0) ')⌝ ⊦

Rule argument

Additional information

Proof step 13 from proof pis-mon (previous step) (back to tree)

User applied rule flip equation

And obtained the following new goals

• Proof step 14:

  (ls0, rs0) = psf(1), psf(0) = (ls, rs), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), Π(lstep, rstep, lren, rren, lext, rext)((ls, rs), paf(0), (ls0, rs0)), ¬ ⌜rs '⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (ls0, rs0) ', paf(0) ')⌝ ⊦

Rule argument

Additional information

Proof step 14 from proof pis-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ Π(lstep, rstep, lren, rren, lext, rext)((ls, rs), pa, (ls0, rs0)) ↔ rs = rs0 ∧ (∃ la. lstep(ls, la, ls0) ∧ pa = lren(la) ∧ ¬ cod(rren)(pa)) ∨ ls = ls0 ∧ (∃ ra. rstep(rs, ra, rs0) ∧ pa = rren(ra) ∧ ¬ cod(lren)(pa)) ∨ (∃ la, ra. lstep(ls, la, ls0) ∧ lext(la) ≠ None ∧ pa = lren(la) ∧ rstep(rs, ra, rs0) ∧ rext(ra) ≠ None ∧ pa = rren(ra))

• Proof step 16:

  (ls0, rs0) = psf(1), psf(0) = (ls, rs), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ¬ ⌜rs '⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (ls0, rs0) ', paf(0) ')⌝ , rs = rs0 ∧ (∃ la. lstep(ls, la, ls0) ∧ paf(0) = lren(la) ∧ ¬ cod(rren)(paf(0))) ∨ ls = ls0 ∧ (∃ ra. rstep(rs, ra, rs0) ∧ paf(0) = rren(ra) ∧ ¬ cod(lren)(paf(0))) ∨ (∃ la, ra. lstep(ls, la, ls0) ∧ lext(la) ≠ None ∧ paf(0) = lren(la) ∧ rstep(rs, ra, rs0) ∧ rext(ra) ≠ None ∧ paf(0) = rren(ra)) ⊦

Rule argument

Additional information

Used terms: rext, paf(0), rs, rstep, lren, rren, rs0, lstep, lext, ls, ls0

Proof step 15 from proof pis-mon (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof pis-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  (ls0, rs0) = psf(1), psf(0) = (ls, rs), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ¬ ⌜rs '⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (ls0, rs0) ', paf(0) ')⌝ , rs = rs0 ∧ lstep(ls, la, ls0) ∧ paf(0) = lren(la) ∧ ¬ cod(rren)(paf(0)) ∨ ls = ls0 ∧ rstep(rs, ra, rs0) ∧ paf(0) = rren(ra) ∧ ¬ cod(lren)(paf(0)) ∨ lstep(ls, la0, ls0) ∧ lext(la0) ≠ None ∧ paf(0) = lren(la0) ∧ rstep(rs, ra0, rs0) ∧ rext(ra0) ≠ None ∧ paf(0) = rren(ra0) ⊦

Rule argument

Additional information

Proof step 17 from proof pis-mon (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: projstate-rec-skipL-one: ⊦ lstep(ls, la, ls0) ∧ ¬ cod(rren)(lren(la)) → πrs(lstep, rstep, lren, rren, (ls, rs) ' + (ls0, rs) ', lren(la) ') = πrs(lstep, rstep, lren, rren, (ls0, rs) ', []); projstate-base: ⊦ πrs(lstep, rstep, lren, rren, (ls, rs) ', []) = rs '; projstate-rec-addR-one: ⊦ rstep(rs, ra, rs0) ∧ ¬ cod(lren)(rren(ra)) → πrs(lstep, rstep, lren, rren, (ls, rs) ' + (ls, rs0) ', rren(ra) ') = rs ' + πrs(lstep, rstep, lren, rren, (ls, rs0) ', []); projstate-base: ⊦ πrs(lstep, rstep, lren, rren, (ls, rs) ', []) = rs '; projstate-rec-addboth-one: pa = rren(ra) ⊦ rstep(rs, ra, rs0) ∧ lren(la) = rren(ra) ∧ lstep(ls, la, ls0) → πrs(lstep, rstep, lren, rren, (ls, rs) ' + (ls0, rs0) ', pa ') = rs ' + πrs(lstep, rstep, lren, rren, (ls0, rs0) ', []); projstate-base: ⊦ πrs(lstep, rstep, lren, rren, (ls, rs) ', []) = rs '; ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ σ1 ⊑ σ1 + σ2; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ σ ⊑ σ; (s)

Proof step 18 from proof pis-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf), ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n0), paf.take(n0 + 1))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(3 + n0), paf.take(2 + n0))⌝ , ∀ lstart0, lstep0, lext0, rstart0, rstep0, rext0, lren0, rren0, psf0, paf0. ¬ fragω(Π(IOAut(lstart0, lstep0, lext0), IOAut(rstart0, rstep0, rext0), lren0, rren0))(psf0, paf0) ∨ ⌜πrs(lstep0, rstep0, lren0, rren0, psf0.take(n0 + 1), paf0.take(n0))⌝ ⊑ ⌜πrs(lstep0, rstep0, lren0, rren0, psf0.take(2 + n0), paf0.take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m +1 = m + 1; (s)

Proof step 19 from proof pis-mon (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 20:

  fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf), ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n0), paf.take(n0 + 1))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(3 + n0), paf.take(2 + n0))⌝ , ¬ fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(λ n. psf(n + 1), λ n. paf(n + 1)) ∨ ⌜πrs(lstep, rstep, lren, rren, (λ n. psf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (λ n. psf(n + 1)).take(2 + n0), (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Used terms: lstart, lstep, lext, rstart, rstep, rext, lren, rren, λ n. psf(n + 1), λ n. paf(n + 1)

Proof step 20 from proof pis-mon (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 21:

  fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf), ¬ fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(λ n. psf(n + 1), λ n. paf(n + 1)), ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n0), paf.take(n0 + 1))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(3 + n0), paf.take(2 + n0))⌝ ⊦

• Proof step 30:

  fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf), ⌜πrs(lstep, rstep, lren, rren, (λ n. psf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (λ n. psf(n + 1)).take(2 + n0), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n0), paf.take(n0 + 1))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(3 + n0), paf.take(2 + n0))⌝ ⊦

Rule argument

Additional information

Proof step 21 from proof pis-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

  ⊦ Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren) = IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren))

• Proof step 23:

  fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ¬ fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(λ n. psf(n + 1), λ n. paf(n + 1)), ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n0), paf.take(n0 + 1))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(3 + n0), paf.take(2 + n0))⌝ ⊦

Rule argument

Additional information

Used terms: rext, rstep, rstart, lren, rren, lstart, lstep, lext

Proof step 22 from proof pis-mon (previous step) (back to tree)

A spec-lemma

Proof step 23 from proof pis-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

  ⊦ frag(IOAut(start, step, ext))(σ, α) ↔ # σ = # α + ⌜1⌝ ∧ (∀ n. ⌜n⌝ < # α → step(σ[n], α[n], σ[n +1]))

• Proof step 25:

  # ⌜psf⌝ = # ⌜paf⌝ + ⌜1⌝ , ¬ fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(λ n. psf(n + 1), λ n. paf(n + 1)), ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n0), paf.take(n0 + 1))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(3 + n0), paf.take(2 + n0))⌝ , ∀ n. ⌜n⌝ < # ⌜paf⌝ → Π(lstep, rstep, lren, rren, lext, rext)(⌜psf⌝ [n], ⌜paf⌝ [n], ⌜psf⌝ [n +1]) ⊦

Rule argument

Additional information

Used terms: Π(lext, rext, lren, rren), ⌜paf⌝ , Π(lstep, rstep, lren, rren, lext, rext), Π(lstart, rstart), ⌜psf⌝

Proof step 24 from proof pis-mon (previous step) (back to tree)

A spec-lemma

Proof step 25 from proof pis-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  ¬ fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(λ n. psf(n + 1), λ n. paf(n + 1)), ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n0), paf.take(n0 + 1))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(3 + n0), paf.take(2 + n0))⌝ , ∀ n. Π(lstep, rstep, lren, rren, lext, rext)(psf(n), paf(n), psf(n + 1)) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜nf⌝ [n] = nf(n); (s) ⊦ m +1 = m + 1; (s) ⊦ ⌜m⌝ < ∞; (s) ⊦ # ⌜nf⌝ = ∞; (s) add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ⌜m⌝ + ∞ = ∞; (s)

Proof step 26 from proof pis-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

  ⊦ frag(IOAut(start, step, ext))(σ, α) ↔ # σ = # α + ⌜1⌝ ∧ (∀ n. ⌜n⌝ < # α → step(σ[n], α[n], σ[n +1]))

• Proof step 28:

  ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n0), paf.take(n0 + 1))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(3 + n0), paf.take(2 + n0))⌝ , ∀ n. Π(lstep, rstep, lren, rren, lext, rext)(psf(n), paf(n), psf(n + 1)), # ⌜λ n. psf(n + 1)⌝ ≠ # ⌜λ n. paf(n + 1)⌝ + ⌜1⌝ ∨ (∃ n. ¬ ( ⌜n⌝ < # ⌜λ n. paf(n + 1)⌝ → Π(lstep, rstep, lren, rren, lext, rext)(⌜λ n. psf(n + 1)⌝ [n], ⌜λ n. paf(n + 1)⌝ [n], ⌜λ n. psf(n + 1)⌝ [n +1]))) ⊦

Rule argument

Additional information

Used terms: Π(lext, rext, lren, rren), ⌜λ n. paf(n + 1)⌝ , Π(lstep, rstep, lren, rren, lext, rext), Π(lstart, rstart), ⌜λ n. psf(n + 1)⌝

Proof step 27 from proof pis-mon (previous step) (back to tree)

A spec-lemma

Proof step 28 from proof pis-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  ¬ Π(lstep, rstep, lren, rren, lext, rext)(psf(n + 1), paf(n + 1), psf(2 + n)), ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n0), paf.take(n0 + 1))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(3 + n0), paf.take(2 + n0))⌝ , ∀ n. Π(lstep, rstep, lren, rren, lext, rext)(psf(n), paf(n), psf(n + 1)) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ ⌜nf⌝ [n] = nf(n); (s) ⊦ m +1 = m + 1; (s) ⊦ ⌜m⌝ < ∞; (s) ⊦ # ⌜nf⌝ = ∞; (s) add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf ⊦ ⌜m⌝ + ∞ = ∞; (s)

Proof step 29 from proof pis-mon (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic Used terms: n + 1

Proof step 30 from proof pis-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 31:

  ⊦ nf.take(n + 2) = nf(0) + (λ n. nf(n + 1)).take(n + 1)

• Proof step 32:

  fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf), ⌜πrs(lstep, rstep, lren, rren, (λ n. psf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (λ n. psf(n + 1)).take(2 + n0), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n0), paf.take(n0 + 1))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(3 + n0), paf(0) + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic Used terms: paf, n0

Proof step 31 from proof pis-mon (previous step) (back to tree)

A spec-lemma

Proof step 32 from proof pis-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf), ⌜πrs(lstep, rstep, lren, rren, (λ n. psf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (λ n. psf(n + 1)).take(2 + n0), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n0), paf.take(n0 + 1))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf.take(3 + n0), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s)

Proof step 33 from proof pis-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 34:

  ⊦ nf.take(n + 3) = nf(0) + (λ n. nf(n + 1)).take(n + 2)

• Proof step 35:

  fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf), ⌜πrs(lstep, rstep, lren, rren, (λ n. psf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (λ n. psf(n + 1)).take(2 + n0), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n0), paf.take(n0 + 1))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf(0) + (λ n. psf(n + 1)).take(n0 + 2), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic Used terms: psf, n0

Proof step 34 from proof pis-mon (previous step) (back to tree)

A spec-lemma

Proof step 35 from proof pis-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf), ⌜πrs(lstep, rstep, lren, rren, (λ n. psf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (λ n. psf(n + 1)).take(2 + n0), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n0), paf.take(n0 + 1))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf(0) ' + (λ n. psf(n + 1)).take(n0 + 2), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s)

Proof step 36 from proof pis-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 37:

  ⊦ nf.take(n + 2) = nf(0) + (λ n. nf(n + 1)).take(n + 1)

• Proof step 38:

  fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf), ⌜πrs(lstep, rstep, lren, rren, (λ n. psf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf(0 + 1) + (λ n. psf((n + 1) + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n0), paf.take(n0 + 1))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf(0) ' + (psf(0 + 1) + (λ n. psf((n + 1) + 1)).take(n0 + 1)), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic Used terms: λ n. psf(n + 1), n0

Proof step 37 from proof pis-mon (previous step) (back to tree)

A spec-lemma

Proof step 38 from proof pis-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf), ⌜πrs(lstep, rstep, lren, rren, (λ n. psf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf(1) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n0), paf.take(n0 + 1))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf(0) ' + psf(1) ' + (λ n. psf(2 + n)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a + x = a ' + x; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 39 from proof pis-mon (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 40:

  (ls, rs) = psf(1), fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf), ⌜πrs(lstep, rstep, lren, rren, (λ n. psf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf(1) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n0), paf.take(n0 + 1))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf(0) ' + psf(1) ' + (λ n. psf(2 + n)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Proof step 40 from proof pis-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  (ls, rs) = psf(1), fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf), ⌜πrs(lstep, rstep, lren, rren, (λ n. psf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n0), paf.take(n0 + 1))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf(0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Proof step 41 from proof pis-mon (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 42:

  (ls, rs) = psf(1), (ls0, rs0) = psf(0), fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf), ⌜πrs(lstep, rstep, lren, rren, (λ n. psf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n0), paf.take(n0 + 1))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, psf(0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Proof step 42 from proof pis-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 43:

  (ls0, rs0) = psf(0), (ls, rs) = psf(1), fragω(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(psf, paf), ⌜πrs(lstep, rstep, lren, rren, (λ n. psf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n0), paf.take(n0 + 1))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Proof step 43 from proof pis-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 44:

  ⊦ Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren) = IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren))

• Proof step 45:

  (ls, rs) = psf(1), (ls0, rs0) = psf(0), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ⌜πrs(lstep, rstep, lren, rren, (λ n. psf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n0), paf.take(n0 + 1))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Used terms: rext, rstep, rstart, lren, rren, lstart, lstep, lext

Proof step 44 from proof pis-mon (previous step) (back to tree)

A spec-lemma

Proof step 45 from proof pis-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 46:

  α ≠ [] ⊦ ¬ step(σ[0], α[0], σ[1]) → (frag(IOAut(start, step, ext))(σ, α) ↔ false)

• Proof step 47:

  (ls0, rs0) = psf(0), (ls, rs) = psf(1), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ⌜πrs(lstep, rstep, lren, rren, (λ n. psf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n0), paf.take(n0 + 1))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦ ⌜paf⌝ ≠ [] ∧ ¬ Π(lstep, rstep, lren, rren, lext, rext)(⌜psf⌝ [0], ⌜paf⌝ [0], ⌜psf⌝ [1])

Rule argument

Additional information

Used terms: Π(lext, rext, lren, rren), ⌜paf⌝ , Π(lstep, rstep, lren, rren, lext, rext), Π(lstart, rstart), ⌜psf⌝

Proof step 46 from proof pis-mon (previous step) (back to tree)

A spec-lemma

Proof step 47 from proof pis-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 48:

  (ls, rs) = psf(1), (ls0, rs0) = psf(0), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), Π(lstep, rstep, lren, rren, lext, rext)((ls0, rs0), paf(0), (ls, rs)), ⌜πrs(lstep, rstep, lren, rren, (λ n. psf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n0), paf.take(n0 + 1))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜nf⌝ [n] = nf(n); (s) ⊦ [] ≠ ⌜nf⌝ ; (s)

Proof step 48 from proof pis-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 49:

  ⊦ nf.take(n + 1) = nf(0) + (λ n. nf(n + 1)).take(n)

• Proof step 50:

  (ls0, rs0) = psf(0), (ls, rs) = psf(1), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), Π(lstep, rstep, lren, rren, lext, rext)((ls0, rs0), paf(0), (ls, rs)), ⌜πrs(lstep, rstep, lren, rren, (λ n. psf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n0), paf(0) + (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Used terms: paf, n0

Proof step 49 from proof pis-mon (previous step) (back to tree)

A spec-lemma

Proof step 50 from proof pis-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

  (ls, rs) = psf(1), (ls0, rs0) = psf(0), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), Π(lstep, rstep, lren, rren, lext, rext)((ls0, rs0), paf(0), (ls, rs)), ⌜πrs(lstep, rstep, lren, rren, (λ n. psf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ ⌜πrs(lstep, rstep, lren, rren, psf.take(2 + n0), paf(0) ' + (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s)

Proof step 51 from proof pis-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 52:

  ⊦ nf.take(n + 2) = nf(0) + (λ n. nf(n + 1)).take(n + 1)

• Proof step 53:

  (ls0, rs0) = psf(0), (ls, rs) = psf(1), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), Π(lstep, rstep, lren, rren, lext, rext)((ls0, rs0), paf(0), (ls, rs)), ⌜πrs(lstep, rstep, lren, rren, (λ n. psf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ ⌜πrs(lstep, rstep, lren, rren, psf(0) + (λ n. psf(n + 1)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic Used terms: psf, n0

Proof step 52 from proof pis-mon (previous step) (back to tree)

A spec-lemma

Proof step 53 from proof pis-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

  (ls, rs) = psf(1), (ls0, rs0) = psf(0), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), Π(lstep, rstep, lren, rren, lext, rext)((ls0, rs0), paf(0), (ls, rs)), ⌜πrs(lstep, rstep, lren, rren, (λ n. psf(n + 1)).take(n0 + 1), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (λ n. psf(n + 1)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s)

Proof step 54 from proof pis-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 55:

  ⊦ nf.take(n + 1) = nf(0) + (λ n. nf(n + 1)).take(n)

• Proof step 56:

  (ls0, rs0) = psf(0), (ls, rs) = psf(1), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), Π(lstep, rstep, lren, rren, lext, rext)((ls0, rs0), paf(0), (ls, rs)), ⌜πrs(lstep, rstep, lren, rren, psf(0 + 1) + (λ n. psf((n + 1) + 1)).take(n0), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (psf(0 + 1) + (λ n. psf((n + 1) + 1)).take(n0)), paf(0) ' + (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Used terms: λ n. psf(n + 1), n0

Proof step 55 from proof pis-mon (previous step) (back to tree)

A spec-lemma

Proof step 56 from proof pis-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 57:

  (ls, rs) = psf(1), (ls0, rs0) = psf(0), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), Π(lstep, rstep, lren, rren, lext, rext)((ls0, rs0), paf(0), (ls, rs)), ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0), paf(0) ' + (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a + x = a ' + x; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 57 from proof pis-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 58:

  ⊦ Π(lstep, rstep, lren, rren, lext, rext)((ls, rs), pa, (ls0, rs0)) ↔ rs = rs0 ∧ (∃ la. lstep(ls, la, ls0) ∧ pa = lren(la) ∧ ¬ cod(rren)(pa)) ∨ ls = ls0 ∧ (∃ ra. rstep(rs, ra, rs0) ∧ pa = rren(ra) ∧ ¬ cod(lren)(pa)) ∨ (∃ la, ra. lstep(ls, la, ls0) ∧ lext(la) ≠ None ∧ pa = lren(la) ∧ rstep(rs, ra, rs0) ∧ rext(ra) ≠ None ∧ pa = rren(ra))

• Proof step 59:

  (ls0, rs0) = psf(0), (ls, rs) = psf(1), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0), paf(0) ' + (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ , rs0 = rs ∧ (∃ la. lstep(ls0, la, ls) ∧ paf(0) = lren(la) ∧ ¬ cod(rren)(paf(0))) ∨ ls0 = ls ∧ (∃ ra. rstep(rs0, ra, rs) ∧ paf(0) = rren(ra) ∧ ¬ cod(lren)(paf(0))) ∨ (∃ la, ra. lstep(ls0, la, ls) ∧ lext(la) ≠ None ∧ paf(0) = lren(la) ∧ rstep(rs0, ra, rs) ∧ rext(ra) ≠ None ∧ paf(0) = rren(ra)) ⊦

Rule argument

Additional information

Used terms: rext, paf(0), rs0, rstep, lren, rren, rs, lstep, lext, ls0, ls

Proof step 58 from proof pis-mon (previous step) (back to tree)

A spec-lemma

Proof step 59 from proof pis-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 60:

  (ls, rs) = psf(1), (ls0, rs0) = psf(0), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0), paf(0) ' + (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ , rs0 = rs ∧ lstep(ls0, la, ls) ∧ paf(0) = lren(la) ∧ ¬ cod(rren)(paf(0)) ∨ ls0 = ls ∧ rstep(rs0, ra, rs) ∧ paf(0) = rren(ra) ∧ ¬ cod(lren)(paf(0)) ∨ lstep(ls0, la0, ls) ∧ lext(la0) ≠ None ∧ paf(0) = lren(la0) ∧ rstep(rs0, ra0, rs) ∧ rext(ra0) ≠ None ∧ paf(0) = rren(ra0) ⊦

Rule argument

Additional information

Proof step 60 from proof pis-mon (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 61:

  (ls0, rs0) = psf(0), (ls, rs) = psf(1), paf(0) = lren(la), rs0 = rs, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), lstep(ls0, la, ls), ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ cod(rren)(paf(0)), ¬ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0), paf(0) ' + (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

• Proof step 67:

  (ls0, rs0) = psf(0), (ls, rs) = psf(1), ls0 = ls, paf(0) = rren(ra), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), rstep(rs0, ra, rs), ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ cod(lren)(paf(0)), ¬ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0), paf(0) ' + (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

• Proof step 73:

  (ls0, rs0) = psf(0), (ls, rs) = psf(1), paf(0) = lren(la0), paf(0) = rren(ra0), lext(la0) ≠ None, rext(ra0) ≠ None, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), lstep(ls0, la0, ls), rstep(rs0, ra0, rs), ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0), paf(0) ' + (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), paf(0) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Proof step 61 from proof pis-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 62:

  (ls, rs) = psf(1), (ls0, rs) = psf(0), paf(0) = lren(la), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), lstep(ls0, la, ls), ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ cod(rren)(lren(la)), ¬ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0), lren(la) ' + (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), lren(la) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Proof step 62 from proof pis-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 63:

  ⊦ # psl = # pal ∧ lstep(ls, la, ls0) ∧ ¬ cod(rren)(lren(la)) → πrs(lstep, rstep, lren, rren, (ls, rs) ' + (ls0, rs) ' + psl, lren(la) ' + pal) = πrs(lstep, rstep, lren, rren, (ls0, rs) ' + psl, pal)

• Proof step 64:

  # (λ n. psf(2 + n)).take(n0) = # (λ n. paf(n + 1)).take(n0), (ls0, rs) = psf(0), (ls, rs) = psf(1), paf(0) = lren(la), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), lstep(ls0, la, ls), ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ cod(rren)(lren(la)), ¬ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), lren(la) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # nf.take(n) = n; (s) Used terms: (λ n. psf(2 + n)).take(n0), rs, (λ n. paf(n + 1)).take(n0), rstep, lren, rren, la, lstep, ls0, ls

Proof step 63 from proof pis-mon (previous step) (back to tree)

Lemma projstate-rec-skipL

Proof step 64 from proof pis-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 65:

  (ls, rs) = psf(1), (ls0, rs) = psf(0), paf(0) = lren(la), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), lstep(ls0, la, ls), ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ cod(rren)(lren(la)), ¬ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), lren(la) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # nf.take(n) = n; (s)

Proof step 65 from proof pis-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 66:

  ⊦ # psl = # pal ∧ lstep(ls, la, ls0) ∧ ¬ cod(rren)(lren(la)) → πrs(lstep, rstep, lren, rren, (ls, rs) ' + (ls0, rs) ' + psl, lren(la) ' + pal) = πrs(lstep, rstep, lren, rren, (ls0, rs) ' + psl, pal)

Rule argument

Additional information

Used simplifier rules: ⊦ # nf.take(n) = n; (s) ⊦ m + n = m + n0 ↔ n = n0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: (λ n. psf(2 + n)).take(n0 + 1), rs, (λ n. paf(n + 1)).take(n0 + 1), rstep, lren, rren, la, lstep, ls0, ls

Proof step 66 from proof pis-mon (previous step) (back to tree)

Lemma projstate-rec-skipL

Proof step 67 from proof pis-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 68:

  (ls, rs) = psf(1), (ls, rs0) = psf(0), paf(0) = rren(ra), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), rstep(rs0, ra, rs), ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ cod(lren)(rren(ra)), ¬ ⌜πrs(lstep, rstep, lren, rren, (ls, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0), rren(ra) ' + (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), rren(ra) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Proof step 68 from proof pis-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 69:

  ⊦ # psl = # pal ∧ rstep(rs, ra, rs0) ∧ ¬ cod(lren)(rren(ra)) → πrs(lstep, rstep, lren, rren, (ls, rs) ' + (ls, rs0) ' + psl, rren(ra) ' + pal) = rs ' + πrs(lstep, rstep, lren, rren, (ls, rs0) ' + psl, pal)

• Proof step 70:

  # (λ n. psf(2 + n)).take(n0) = # (λ n. paf(n + 1)).take(n0), (ls, rs0) = psf(0), (ls, rs) = psf(1), paf(0) = rren(ra), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), rstep(rs0, ra, rs), ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ cod(lren)(rren(ra)), ¬ ⌜rs0 ' + πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), rren(ra) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # nf.take(n) = n; (s) Used terms: (λ n. psf(2 + n)).take(n0), rs0, ra, (λ n. paf(n + 1)).take(n0), rstep, lren, rren, rs, lstep, ls

Proof step 69 from proof pis-mon (previous step) (back to tree)

Lemma projstate-rec-addR

Proof step 70 from proof pis-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 71:

  (ls, rs) = psf(1), (ls, rs0) = psf(0), paf(0) = rren(ra), fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), rstep(rs0, ra, rs), ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ cod(lren)(rren(ra)), ¬ ⌜rs0 '⌝ + ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), rren(ra) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s) ⊦ # nf.take(n) = n; (s)

Proof step 71 from proof pis-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 72:

  ⊦ # psl = # pal ∧ rstep(rs, ra, rs0) ∧ ¬ cod(lren)(rren(ra)) → πrs(lstep, rstep, lren, rren, (ls, rs) ' + (ls, rs0) ' + psl, rren(ra) ' + pal) = rs ' + πrs(lstep, rstep, lren, rren, (ls, rs0) ' + psl, pal)

Rule argument

Additional information

Used simplifier rules: ⊦ # nf.take(n) = n; (s) ⊦ m + n = m + n0 ↔ n = n0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ⌜x⌝ + σ1 ⊑ ⌜x⌝ + σ2 ↔ σ1 ⊑ σ2; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream Used terms: (λ n. psf(2 + n)).take(n0 + 1), rs0, ra, (λ n. paf(n + 1)).take(n0 + 1), rstep, lren, rren, rs, lstep, ls

Proof step 72 from proof pis-mon (previous step) (back to tree)

Lemma projstate-rec-addR

Proof step 73 from proof pis-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 74:

  (ls, rs) = psf(1), (ls0, rs0) = psf(0), lren(la0) = rren(ra0), paf(0) = rren(ra0), lext(la0) ≠ None, rext(ra0) ≠ None, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), lstep(ls0, la0, ls), rstep(rs0, ra0, rs), ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0), rren(ra0) ' + (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), rren(ra0) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Proof step 74 from proof pis-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 75:

  pa = lren(la) ⊦ # psl = # pal ∧ rstep(rs, ra, rs0) ∧ rren(ra) = lren(la) ∧ lstep(ls, la, ls0) → πrs(lstep, rstep, lren, rren, (ls, rs) ' + (ls0, rs0) ' + psl, pa ' + pal) = rs ' + πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + psl, pal)

• Proof step 76:

  # (λ n. psf(2 + n)).take(n0) = # (λ n. paf(n + 1)).take(n0), (ls0, rs0) = psf(0), (ls, rs) = psf(1), paf(0) = rren(ra0), rren(ra0) = lren(la0), lext(la0) ≠ None, rext(ra0) ≠ None, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), lstep(ls0, la0, ls), rstep(rs0, ra0, rs), ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ ⌜rs0 ' + πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), rren(ra0) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # nf.take(n) = n; (s) Used terms: rren(ra0), (λ n. psf(2 + n)).take(n0), rs0, ra0, (λ n. paf(n + 1)).take(n0), rstep, lren, rren, la0, rs, lstep, ls0, ls

Proof step 75 from proof pis-mon (previous step) (back to tree)

Lemma projstate-rec-addboth

Proof step 76 from proof pis-mon (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 77:

  (ls, rs) = psf(1), (ls0, rs0) = psf(0), paf(0) = lren(la0), rren(ra0) = lren(la0), lext(la0) ≠ None, rext(ra0) ≠ None, fragω(IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren)))(psf, paf), lstep(ls0, la0, ls), rstep(rs0, ra0, rs), ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), (λ n. paf(n + 1)).take(n0 + 1))⌝ , ¬ ⌜rs0 '⌝ + ⌜πrs(lstep, rstep, lren, rren, (ls, rs) ' + (λ n. psf(2 + n)).take(n0), (λ n. paf(n + 1)).take(n0))⌝ ⊑ ⌜πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + (ls, rs) ' + (λ n. psf(2 + n)).take(n0 + 1), lren(la0) ' + (λ n. paf(n + 1)).take(n0 + 1))⌝ ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s) ⊦ # nf.take(n) = n; (s)

Proof step 77 from proof pis-mon (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 78:

  pa = lren(la) ⊦ # psl = # pal ∧ rstep(rs, ra, rs0) ∧ rren(ra) = lren(la) ∧ lstep(ls, la, ls0) → πrs(lstep, rstep, lren, rren, (ls, rs) ' + (ls0, rs0) ' + psl, pa ' + pal) = rs ' + πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + psl, pal)

Rule argument

Additional information

Used simplifier rules: ⊦ # nf.take(n) = n; (s) ⊦ m + n = m + n0 ↔ n = n0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ⌜x⌝ + σ1 ⊑ ⌜x⌝ + σ2 ↔ σ1 ⊑ σ2; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream Used terms: lren(la0), (λ n. psf(2 + n)).take(n0 + 1), rs0, ra0, (λ n. paf(n + 1)).take(n0 + 1), rstep, lren, rren, la0, rs, lstep, ls0, ls

Proof step 78 from proof pis-mon (previous step) (back to tree)

Lemma projstate-rec-addboth