Proof step 1 from proof repl-fin-size (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  # repls(step, cstep, cren, ren, aren, cext, aext, pcsl, pal, aσ, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, pcsl, pal, aσ, aα) + 1, frag(IOAut(astart, astep, aext))(aσ, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsl, pal), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(πra(step, cstep, ren, cren, ⌜pcsl⌝ , ⌜pal⌝ )) ⊑ aext !(aα) ⊦

Rule argument

Additional information

Proof step 2 from proof repl-fin-size (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ # psl = # pal + 1 → πra(lstep, rstep, lren, rren, ⌜psl⌝ , ⌜pal⌝ ) = ⌜πra(lstep, rstep, lren, rren, psl, pal)⌝

• Proof step 4:

  # pcsl = # pal + 1, # repls(step, cstep, cren, ren, aren, cext, aext, pcsl, pal, aσ, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, pcsl, pal, aσ, aα) + 1, frag(IOAut(astart, astep, aext))(aσ, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsl, pal), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(⌜πra(step, cstep, ren, cren, pcsl, pal)⌝ ) ⊑ aext !(aα) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ frag*(IOAut(start, step, ext))(sl, al) → (# sl = # al + 1 ↔ true); (ss) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: pcsl, cstep, pal, ren, cren, step

Proof step 3 from proof repl-fin-size (previous step) (back to tree)

A spec-lemma

Proof step 4 from proof repl-fin-size (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 5:

  #(pcs + pcsl0) = # pal + 1, # repls(step, cstep, cren, ren, aren, cext, aext, pcs + pcsl0, pal, aσ, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, pcs + pcsl0, pal, aσ, aα) + 1, frag(IOAut(astart, astep, aext))(aσ, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcs + pcsl0, pal), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), cext !(⌜πra(step, cstep, ren, cren, pcs + pcsl0, pal)⌝ ) ⊑ aext !(aα), ∀ pal, step, cstep, cren, ren, aren, cext, aext, aσ, aα, astart, astep, start, cstart, ext. ¬ ( # pcsl0 = # pal + 1 ∧ # repls(step, cstep, cren, ren, aren, cext, aext, pcsl0, pal, aσ, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, pcsl0, pal, aσ, aα) + 1 ∧ frag(IOAut(astart, astep, aext))(aσ, aα) ∧ frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcsl0, pal) ∧ nounsharedextR(cren, cext, ren) ∧ Πok(ext, cext, ren, cren) ∧ cext !(⌜πra(step, cstep, ren, cren, pcsl0, pal)⌝ ) ⊑ aext !(aα)) ⊦

Rule argument

Additional information

Used simplifier rules: List('a) freely generated by [], +;; ⊦ # [] = 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) ⊦ # x = 0 ↔ x = []; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 5 from proof repl-fin-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  # pcsl0 = # pal, # repls(step, cstep, cren, ren, aren, cext, aext, pcs ' + pcsl0, pal, aσ, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, pcs ' + pcsl0, pal, aσ, aα) + 1, frag(IOAut(astart, astep, aext))(aσ, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcs ' + pcsl0, pal), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), ⌜cext !(πra(step, cstep, ren, cren, pcs ' + pcsl0, pal))⌝ ⊑ aext !(aα), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, pcsl0, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, pcsl0, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))(pcsl0, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, pcsl0, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ frag*(IOAut(start, step, ext))(sl, al) → (# sl = # al + 1 ↔ true); (ss) ⊦ a + x = a ' + x; (s) ⊦ m + n = m + n0 ↔ n = n0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s)

Proof step 6 from proof repl-fin-size (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 7:

  # pcsl0 = # pal, pcs = (s, cs), # repls(step, cstep, cren, ren, aren, cext, aext, pcs ' + pcsl0, pal, aσ, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, pcs ' + pcsl0, pal, aσ, aα) + 1, frag(IOAut(astart, astep, aext))(aσ, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))(pcs ' + pcsl0, pal), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), ⌜cext !(πra(step, cstep, ren, cren, pcs ' + pcsl0, pal))⌝ ⊑ aext !(aα), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, pcsl0, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, pcsl0, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))(pcsl0, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, pcsl0, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

Proof step 7 from proof repl-fin-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  # pcsl0 = # pal, # repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsl0, pal, aσ, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsl0, pal, aσ, aα) + 1, frag(IOAut(astart, astep, aext))(aσ, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsl0, pal), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), ⌜cext !(πra(step, cstep, ren, cren, (s, cs) ' + pcsl0, pal))⌝ ⊑ aext !(aα), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, pcsl0, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, pcsl0, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))(pcsl0, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, pcsl0, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

Proof step 8 from proof repl-fin-size (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 9:

  ⊦ σ ≠ [] → (a = hd(σ) ∧ σ0 = tl(σ) ↔ σ = a + σ0)

• Proof step 10:

  # pcsl0 = # pal, # repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsl0, pal, aσ, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsl0, pal, aσ, aα) + 1, frag(IOAut(astart, astep, aext))(aσ, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsl0, pal), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), ⌜cext !(πra(step, cstep, ren, cren, (s, cs) ' + pcsl0, pal))⌝ ⊑ aext !(aα), aσ ≠ [] → (hd(aσ) = hd(aσ) ∧ tl(aσ) = tl(aσ) ↔ aσ = hd(aσ) + tl(aσ)), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, pcsl0, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, pcsl0, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))(pcsl0, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, pcsl0, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

Used terms: aσ, hd(aσ), tl(aσ)

Proof step 9 from proof repl-fin-size (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof repl-fin-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  # pcsl0 = # pal, aσ = ⌜hd(aσ) '⌝ + tl(aσ), # repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsl0, pal, aσ, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsl0, pal, aσ, aα) + 1, aσ ≠ [], frag(IOAut(astart, astep, aext))(aσ, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsl0, pal), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), ⌜cext !(πra(step, cstep, ren, cren, (s, cs) ' + pcsl0, pal))⌝ ⊑ aext !(aα), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, pcsl0, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, pcsl0, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))(pcsl0, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, pcsl0, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ frag(IOAut(start, step, ext))([], α); (s) ⊦ a + σ = ⌜a '⌝ + σ; (s)

Proof step 11 from proof repl-fin-size (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 12:

  # pcsl0 = # pal, aσ = ⌜as '⌝ + σ0, aσ = as + σ0, # repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsl0, pal, aσ, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsl0, pal, aσ, aα) + 1, aσ ≠ [], frag(IOAut(astart, astep, aext))(aσ, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsl0, pal), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), ⌜cext !(πra(step, cstep, ren, cren, (s, cs) ' + pcsl0, pal))⌝ ⊑ aext !(aα), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, pcsl0, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, pcsl0, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))(pcsl0, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, pcsl0, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ σ ≠ [] → (a = hd(σ) ∧ σ0 = tl(σ) ↔ σ = a + σ0); (elim) Used terms: aσ, as, σ0

Proof step 12 from proof repl-fin-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  # pcsl0 = # pal, # repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsl0, pal, ⌜as '⌝ + σ0, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsl0, pal, ⌜as '⌝ + σ0, aα) + 1, frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsl0, pal), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), ⌜cext !(πra(step, cstep, ren, cren, (s, cs) ' + pcsl0, pal))⌝ ⊑ aext !(aα), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, pcsl0, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, pcsl0, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))(pcsl0, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, pcsl0, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + σ = ⌜a '⌝ + σ; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ ⌜a '⌝ + σ ≠ []; (s) ⊦ # x = # y → (⌜x⌝ + σ = ⌜y⌝ + σ0 ↔ x = y ∧ σ = σ0); (s)

Proof step 13 from proof repl-fin-size (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 14:

  # pcsl0 = # pal, pcsl0 = pcs + pcsl, # repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsl0, pal, ⌜as '⌝ + σ0, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcsl0, pal, ⌜as '⌝ + σ0, aα) + 1, frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcsl0, pal), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), ⌜cext !(πra(step, cstep, ren, cren, (s, cs) ' + pcsl0, pal))⌝ ⊑ aext !(aα), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, pcsl0, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, pcsl0, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))(pcsl0, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, pcsl0, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

Used simplifier rules: repls-base: ⊦ repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ', [], ⌜as '⌝ + aσ, aα) = (s, as) '; repla-base: ⊦ repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ', [], ⌜as '⌝ + aσ, aα) = []; List('a) freely generated by [], +;; ⊦ # x = 0 ↔ x = []; (s) ⊦ x + [] = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ¬ frag*(IOAut(start, step, ext))([], al); (s) ⊦ # a ' = 0 +1; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ # [] = 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 14 from proof repl-fin-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  # pcsl + 1 = # pal, # repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcs ' + pcsl, pal, ⌜as '⌝ + σ0, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcs ' + pcsl, pal, ⌜as '⌝ + σ0, aα) + 1, frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcs ' + pcsl, pal), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), ⌜cext !(πra(step, cstep, ren, cren, (s, cs) ' + pcs ' + pcsl, pal))⌝ ⊑ aext !(aα), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, pcs ' + pcsl, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, pcs ' + pcsl, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))(pcs ' + pcsl, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, pcs ' + pcsl, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s)

Proof step 15 from proof repl-fin-size (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 16:

  # pcsl + 1 = # pal, pcs = (s0, cs0), # repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcs ' + pcsl, pal, ⌜as '⌝ + σ0, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + pcs ' + pcsl, pal, ⌜as '⌝ + σ0, aα) + 1, frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + pcs ' + pcsl, pal), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), ⌜cext !(πra(step, cstep, ren, cren, (s, cs) ' + pcs ' + pcsl, pal))⌝ ⊑ aext !(aα), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, pcs ' + pcsl, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, pcs ' + pcsl, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))(pcs ' + pcsl, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, pcs ' + pcsl, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

Proof step 16 from proof repl-fin-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  # pcsl + 1 = # pal, # repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, pal, ⌜as '⌝ + σ0, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, pal, ⌜as '⌝ + σ0, aα) + 1, frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + (s0, cs0) ' + pcsl, pal), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), ⌜cext !(πra(step, cstep, ren, cren, (s, cs) ' + (s0, cs0) ' + pcsl, pal))⌝ ⊑ aext !(aα), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsl, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, (s0, cs0) ' + pcsl, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

Proof step 17 from proof repl-fin-size (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 18:

  # pcsl + 1 = # pal, pal = pa + pal1, # repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, pal, ⌜as '⌝ + σ0, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, pal, ⌜as '⌝ + σ0, aα) + 1, frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + (s0, cs0) ' + pcsl, pal), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), ⌜cext !(πra(step, cstep, ren, cren, (s, cs) ' + (s0, cs0) ' + pcsl, pal))⌝ ⊑ aext !(aα), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsl, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, (s0, cs0) ' + pcsl, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

Used simplifier rules: List('a) freely generated by [], +;; ⊦ # [] = 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) ⊦ # x = 0 ↔ x = []; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 18 from proof repl-fin-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  # pcsl = # pal1, # repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, pa ' + pal1, ⌜as '⌝ + σ0, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, pa ' + pal1, ⌜as '⌝ + σ0, aα) + 1, frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s, cs) ' + (s0, cs0) ' + pcsl, pa ' + pal1), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), ⌜cext !(πra(step, cstep, ren, cren, (s, cs) ' + (s0, cs0) ' + pcsl, pa ' + pal1))⌝ ⊑ aext !(aα), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsl, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, (s0, cs0) ' + pcsl, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

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

Proof step 19 from proof repl-fin-size (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ frag*(IOAut(start, step, ext))(s ' + sl, a ' + al) ↔ step(s, a, sl.head) ∧ frag*(IOAut(start, step, ext))(sl, al)

• Proof step 21:

  # pcsl = # pal1, # repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, pa ' + pal1, ⌜as '⌝ + σ0, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, pa ' + pal1, ⌜as '⌝ + σ0, aα) + 1, frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), Π(step, cstep, ren, cren, ext, cext)((s, cs), pa, ((s0, cs0) ' + pcsl).head), Πok(ext, cext, ren, cren), ⌜cext !(πra(step, cstep, ren, cren, (s, cs) ' + (s0, cs0) ' + pcsl, pa ' + pal1))⌝ ⊑ aext !(aα), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsl, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, (s0, cs0) ' + pcsl, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: pal1, (s, cs), Π(ext, cext, ren, cren), (s0, cs0) ' + pcsl, pa, Π(start, cstart), Π(step, cstep, ren, cren, ext, cext)

Proof step 20 from proof repl-fin-size (previous step) (back to tree)

A spec-lemma

Proof step 21 from proof repl-fin-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  # pcsl = # pal1, # repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, pa ' + pal1, ⌜as '⌝ + σ0, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, pa ' + pal1, ⌜as '⌝ + σ0, aα) + 1, frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), Π(step, cstep, ren, cren, ext, cext)((s, cs), pa, (s0, cs0)), Πok(ext, cext, ren, cren), ⌜cext !(πra(step, cstep, ren, cren, (s, cs) ' + (s0, cs0) ' + pcsl, pa ' + pal1))⌝ ⊑ aext !(aα), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsl, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, (s0, cs0) ' + pcsl, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ (a ' + x).head = a; (s)

Proof step 22 from proof repl-fin-size (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 23:

  ⊦ Π(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 24:

  # pcsl = # pal1, # repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, pa ' + pal1, ⌜as '⌝ + σ0, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, pa ' + pal1, ⌜as '⌝ + σ0, aα) + 1, frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), ⌜cext !(πra(step, cstep, ren, cren, (s, cs) ' + (s0, cs0) ' + pcsl, pa ' + pal1))⌝ ⊑ aext !(aα), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsl, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, (s0, cs0) ' + pcsl, pal0))⌝ ⊑ aext0 !(aα0), cs = cs0 ∧ (∃ la. step(s, la, s0) ∧ pa = ren(la) ∧ ¬ cod(cren)(pa)) ∨ s = s0 ∧ (∃ ra. cstep(cs, ra, cs0) ∧ pa = cren(ra) ∧ ¬ cod(ren)(pa)) ∨ (∃ la, ra. step(s, la, s0) ∧ ext(la) ≠ None ∧ pa = ren(la) ∧ cstep(cs, ra, cs0) ∧ cext(ra) ≠ None ∧ pa = cren(ra)) ⊦

Rule argument

Additional information

Used terms: cext, pa, cs, cstep, ren, ext, cren, cs0, step, s, s0

Proof step 23 from proof repl-fin-size (previous step) (back to tree)

A spec-lemma

Proof step 24 from proof repl-fin-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  # pcsl = # pal1, # repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, pa ' + pal1, ⌜as '⌝ + σ0, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, pa ' + pal1, ⌜as '⌝ + σ0, aα) + 1, frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), ⌜cext !(πra(step, cstep, ren, cren, (s, cs) ' + (s0, cs0) ' + pcsl, pa ' + pal1))⌝ ⊑ aext !(aα), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsl, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, (s0, cs0) ' + pcsl, pal0))⌝ ⊑ aext0 !(aα0), cs = cs0 ∧ step(s, a, s0) ∧ pa = ren(a) ∧ ¬ cod(cren)(ren(a)) ∨ s = s0 ∧ cstep(cs, ca, cs0) ∧ pa = cren(ca) ∧ ¬ cod(ren)(cren(ca)) ∨ step(s, a0, s0) ∧ ext(a0) ≠ None ∧ cren(ca0) = ren(a0) ∧ cstep(cs, ca0, cs0) ∧ cext(ca0) ≠ None ∧ pa = cren(ca0) ⊦

Rule argument

Additional information

Proof step 25 from proof repl-fin-size (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 26:

  # pcsl = # pal1, cs = cs0, pa = ren(a), # repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, pa ' + pal1, ⌜as '⌝ + σ0, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, pa ' + pal1, ⌜as '⌝ + σ0, aα) + 1, frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), step(s, a, s0), Πok(ext, cext, ren, cren), ⌜cext !(πra(step, cstep, ren, cren, (s, cs) ' + (s0, cs0) ' + pcsl, pa ' + pal1))⌝ ⊑ aext !(aα), ¬ cod(cren)(ren(a)), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsl, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, (s0, cs0) ' + pcsl, pal0))⌝ ⊑ aext0 !(aα0) ⊦

• Proof step 28:

  # pcsl = # pal1, pa = cren(ca), s = s0, # repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, pa ' + pal1, ⌜as '⌝ + σ0, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, pa ' + pal1, ⌜as '⌝ + σ0, aα) + 1, cstep(cs, ca, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), ⌜cext !(πra(step, cstep, ren, cren, (s, cs) ' + (s0, cs0) ' + pcsl, pa ' + pal1))⌝ ⊑ aext !(aα), ¬ cod(ren)(cren(ca)), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsl, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, (s0, cs0) ' + pcsl, pal0))⌝ ⊑ aext0 !(aα0) ⊦

• Proof step 30:

  # pcsl = # pal1, cren(ca0) = ren(a0), pa = cren(ca0), # repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, pa ' + pal1, ⌜as '⌝ + σ0, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, pa ' + pal1, ⌜as '⌝ + σ0, aα) + 1, cext(ca0) ≠ None, ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ⌜cext !(πra(step, cstep, ren, cren, (s, cs) ' + (s0, cs0) ' + pcsl, pa ' + pal1))⌝ ⊑ aext !(aα), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsl, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, (s0, cs0) ' + pcsl, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

Proof step 26 from proof repl-fin-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  # pcsl = # pal1, # repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, ⌜as '⌝ + σ0, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, ⌜as '⌝ + σ0, aα) + 1, frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), step(s, a, s0), Πok(ext, cext, ren, cren), ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ ⊑ aext !(aα), ¬ cod(cren)(ren(a)), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsl, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, (s0, cs0) ' + pcsl, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

Used simplifier rules: repls-rec-addS: ⊦ step(s, a, s0) ∧ ¬ cod(cren)(ren(a)) → repls (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs) ' + pcsl, ren(a) ' + pal, ⌜as '⌝ + aσ, aα) = (s, as) ' + repls (step, cstep, cren, ren, aren, cext, aext, (s0, cs) ' + pcsl, pal, ⌜as '⌝ + aσ, aα); repla-rec-addS: ⊦ step(s, a, s0) ∧ ¬ cod(cren)(ren(a)) → repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs) ' + pcsl, ren(a) ' + pal, ⌜as '⌝ + aσ, aα) = ren(a) ' + repla (step, cstep, cren, ren, aren, cext, aext, (s0, cs) ' + pcsl, pal, ⌜as '⌝ + aσ, aα); a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ # psl = # pal ∧ lstep(ls, la, ls0) ∧ ¬ cod(rren)(lren(la)) → πra(lstep, rstep, lren, rren, (ls, rs) ' + (ls0, rs) ' + psl, lren(la) ' + pal) = πra(lstep, rstep, lren, rren, (ls0, rs) ' + psl, pal); (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic n < n0 ⊦ m + (* n) = m0 + (* n0) ↔ m = m0 + (n0 - n); (s) ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream

Proof step 27 from proof repl-fin-size (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: pal1, step, cstep, cren, ren, aren, cext, aext, ⌜as '⌝ + σ0, aα, astart, astep, start, cstart, ext

Proof step 28 from proof repl-fin-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  # pcsl = # pal1, # repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, ⌜as '⌝ + σ0, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, ⌜as '⌝ + σ0, aα) + 1, cstep(cs, ca, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), Πok(ext, cext, ren, cren), ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ ⊑ aext !(aα), ¬ cod(ren)(cren(ca)), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsl, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, (s0, cs0) ' + pcsl, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

Used simplifier rules: repls-rec-skip: ⊦ cstep(cs, ca, cs0) ∧ ¬ cod(ren)(cren(ca)) → repls (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s, cs0) ' + pcsl, cren(ca) ' + pal, ⌜as '⌝ + aσ, aα) = repls (step, cstep, cren, ren, aren, cext, aext, (s, cs0) ' + pcsl, pal, ⌜as '⌝ + aσ, aα); repla-rec-skip: ⊦ cstep(cs, ca, cs0) ∧ ¬ cod(ren)(cren(ca)) → repla (step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s, cs0) ' + pcsl, cren(ca) ' + pal, ⌜as '⌝ + aσ, aα) = repla (step, cstep, cren, ren, aren, cext, aext, (s, cs0) ' + pcsl, pal, ⌜as '⌝ + aσ, aα); nounsharedextR-notcodren: ⊦ ¬ cod(ren)(cren(ca)) ∧ nounsharedextR(cren, cext, ren) → cext !(ca ') = []; a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ [] + x = x; (s) ⊦ ext !(al + al0) = ext !(al) + ext !(al0); (s) ⊦ a + x = a ' + x; (s) ⊦ # psl = # pal ∧ rstep(rs, ra, rs0) ∧ ¬ cod(lren)(rren(ra)) → πra(lstep, rstep, lren, rren, (ls, rs) ' + (ls, rs0) ' + psl, rren(ra) ' + pal) = ra + πra(lstep, rstep, lren, rren, (ls, rs0) + psl, pal); (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream

Proof step 29 from proof repl-fin-size (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: pal1, step, cstep, cren, ren, aren, cext, aext, ⌜as '⌝ + σ0, aα, astart, astep, start, cstart, ext

Proof step 30 from proof repl-fin-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  # pcsl = # pal1, cren(ca0) = ren(a0), # repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, ren(a0) ' + pal1, ⌜as '⌝ + σ0, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, ren(a0) ' + pal1, ⌜as '⌝ + σ0, aα) + 1, cext(ca0) ≠ None, ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ⌜cext(ca0).get '⌝ + ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ ⊑ aext !(aα), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsl, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, (s0, cs0) ' + pcsl, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ ⌜x + y⌝ = ⌜x⌝ + ⌜y⌝ ; (s) ⊦ ext(a) ≠ None → ext !(a ' + al) = ext(a).get ' + ext !(al); (s) ⊦ a + x = a ' + x; (s) pa = lren(la) ⊦ # psl = # pal ∧ rstep(rs, ra, rs0) ∧ rren(ra) = lren(la) ∧ lstep(ls, la, ls0) → πra(lstep, rstep, lren, rren, (ls, rs) ' + (ls0, rs0) ' + psl, pa ' + pal) = ra + πra(lstep, rstep, lren, rren, (ls0, rs0) ' + psl, pal); (s)

Proof step 31 from proof repl-fin-size (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 32:

  # pcsl = # pal1, cext(ca0) = Some(e), cren(ca0) = ren(a0), # repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, ren(a0) ' + pal1, ⌜as '⌝ + σ0, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, ren(a0) ' + pal1, ⌜as '⌝ + σ0, aα) + 1, cext(ca0) ≠ None, ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ⌜e '⌝ + ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ ⊑ aext !(aα), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsl, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, (s0, cs0) ' + pcsl, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ opt ≠ None → (get = opt.get ↔ opt = Some(get)); (elim) Used terms: cext(ca0), e

Proof step 32 from proof repl-fin-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  # pcsl = # pal1, cext(ca0) = Some(e), cren(ca0) = ren(a0), # repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, ren(a0) ' + pal1, ⌜as '⌝ + σ0, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, ren(a0) ' + pal1, ⌜as '⌝ + σ0, aα) + 1, Some(e) ≠ None, ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ⌜e '⌝ + ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ ⊑ aext !(aα), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsl, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, (s0, cs0) ' + pcsl, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

Proof step 33 from proof repl-fin-size (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 34:

  ⊦ σ ⊑ σ0 ↔ (∃ σ1. σ + σ1 = σ0)

• Proof step 35:

  # pcsl = # pal1, cext(ca0) = Some(e), cren(ca0) = ren(a0), # repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, ren(a0) ' + pal1, ⌜as '⌝ + σ0, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, ren(a0) ' + pal1, ⌜as '⌝ + σ0, aα) + 1, Some(e) ≠ None, ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsl, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, (s0, cs0) ' + pcsl, pal0))⌝ ⊑ aext0 !(aα0), ∃ σ1. (⌜e '⌝ + ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ ) + σ1 = aext !(aα) ⊦

Rule argument

Additional information

Used terms: ⌜e '⌝ + ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ , aext !(aα)

Proof step 34 from proof repl-fin-size (previous step) (back to tree)

A spec-lemma

Proof step 35 from proof repl-fin-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  # pcsl = # pal1, (⌜e '⌝ + ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ ) + β = aext !(aα), cext(ca0) = Some(e), cren(ca0) = ren(a0), # repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, ren(a0) ' + pal1, ⌜as '⌝ + σ0, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, ren(a0) ' + pal1, ⌜as '⌝ + σ0, aα) + 1, Some(e) ≠ None, ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsl, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, (s0, cs0) ' + pcsl, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

Proof step 36 from proof repl-fin-size (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 37:

  ⊦ ext !(α) = ⌜e '⌝ + β ↔ (∃ al, a, α0. α = ⌜al⌝ + ⌜a '⌝ + α0 ∧ ext(a) = Some(e) ∧ ext !(⌜al⌝ ) = [] ∧ ext !(α0) = β)

• Proof step 38:

  # pcsl = # pal1, cext(ca0) = Some(e), cren(ca0) = ren(a0), # repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, ren(a0) ' + pal1, ⌜as '⌝ + σ0, aα) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, ren(a0) ' + pal1, ⌜as '⌝ + σ0, aα) + 1, Some(e) ≠ None, ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, aα), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsl, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, (s0, cs0) ' + pcsl, pal0))⌝ ⊑ aext0 !(aα0), ∃ al, aa, α0. aα = ⌜al⌝ + ⌜aa '⌝ + α0 ∧ aext(aa) = Some(e) ∧ aext !(⌜al⌝ ) = [] ∧ aext !(α0) = ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ + β ⊦

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream Used terms: aext, aα, e, ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ + β

Proof step 37 from proof repl-fin-size (previous step) (back to tree)

A spec-lemma

Proof step 38 from proof repl-fin-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 39:

  aext !(aα0) = ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ + β, aext !(aal) = [], # pcsl = # pal1, aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), # repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, ren(a0) ' + pal1, ⌜as '⌝ + σ0, ⌜aal⌝ + ⌜aa '⌝ + aα0) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, ren(a0) ' + pal1, ⌜as '⌝ + σ0, ⌜aal⌝ + ⌜aa '⌝ + aα0) + 1, Some(e) ≠ None, ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, ⌜aal⌝ + ⌜aa '⌝ + aα0), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsl, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, (s0, cs0) ' + pcsl, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ⌜x⌝ = [] ↔ x = []; (s) ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; (s)

Proof step 39 from proof repl-fin-size (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 40:

  ⊦ step(s, a, s0) ∧ cstep(cs, ca, cs0) ∧ aext !(⌜aal⌝ ) = [] ∧ cext(ca) = aext(aa) ∧ cren(ca) = ren(a) ∧ n = # aal → repls(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, ren(a) ' + pal, aσ, ⌜aal⌝ + ⌜aa '⌝ + aα) = lift(aσ.take(n), s) + (s, aσ[n]) ' + repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal, aσ.drop(n + 1), aα)

• Proof step 41:

  aext !(aal) = [], aext !(aα0) = ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ + β, aext !(⌜aal⌝ ) = [], # pcsl = # pal1, # aal = # aal, aext(aa) = Some(e), cext(ca0) = Some(e), cext(ca0) = aext(aa), cren(ca0) = ren(a0), # ( lift((⌜as '⌝ + σ0).take(# aal), s) + (s, (⌜as '⌝ + σ0)[# aal]) ' + repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, (⌜as '⌝ + σ0).drop(# aal + 1), aα0)) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, ren(a0) ' + pal1, ⌜as '⌝ + σ0, ⌜aal⌝ + ⌜aa '⌝ + aα0) + 1, Some(e) ≠ None, ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, ⌜aal⌝ + ⌜aa '⌝ + aα0), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsl, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, (s0, cs0) ' + pcsl, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; (s) ⊦ ⌜x⌝ = [] ↔ x = []; (s) Used terms: aren, ren, cstep, cext, aa, s, aext, aα0, ca0, a0, pal1, cren, aal, pcsl, cs0, s0, cs, # aal, ⌜as '⌝ + σ0, step

Proof step 40 from proof repl-fin-size (previous step) (back to tree)

Lemma repls-rec-addboth

Proof step 41 from proof repl-fin-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  aext !(aal) = [], aext !(aα0) = ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ + β, # pcsl = # pal1, aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), # (⌜as '⌝ + σ0).take(# aal) + # repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, ren(a0) ' + pal1, ⌜as '⌝ + σ0, ⌜aal⌝ + ⌜aa '⌝ + aα0), Some(e) ≠ None, ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, ⌜aal⌝ + ⌜aa '⌝ + aα0), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsl, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, (s0, cs0) ' + pcsl, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

Used simplifier rules: lift-size: ⊦ # lift(asl, s) = # asl; c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n = m + n0 ↔ n = n0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ #(x + y) = # x + # y; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ n + 0 = n; (s) ⊦ n ≠ 0 → (⌜a '⌝ + σ).drop((* n) + m) = σ.drop((n - 1) + m); (s) ⊦ ⌜x⌝ = [] ↔ x = []; (s) ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; (s)

Proof step 42 from proof repl-fin-size (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 43:

  ⊦ step(s, a, s0) ∧ cstep(cs, ca, cs0) ∧ cren(ca) = ren(a) ∧ aext !(⌜aal⌝ ) = [] ∧ cext(ca) = aext(aa) ∧ n = # aal → repla(step, cstep, cren, ren, aren, cext, aext, (s, cs) ' + (s0, cs0) ' + pcsl, ren(a) ' + pal, aσ, ⌜aal⌝ + ⌜aa '⌝ + aα) = aal.map(aren) + aren(aa) ' + repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal, aσ.drop(n + 1), aα)

• Proof step 44:

  aext !(aα0) = ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ + β, aext !(aal) = [], aext !(⌜aal⌝ ) = [], # pcsl = # pal1, # aal = # aal, aext(aa) = Some(e), cext(ca0) = Some(e), cext(ca0) = aext(aa), cren(ca0) = ren(a0), # (⌜as '⌝ + σ0).take(# aal) + # repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) ≠ # (aal.map(aren) + aren(aa) ' + repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, (⌜as '⌝ + σ0).drop(# aal + 1), aα0)), Some(e) ≠ None, ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, ⌜aal⌝ + ⌜aa '⌝ + aα0), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsl, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, (s0, cs0) ' + pcsl, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; (s) ⊦ ⌜x⌝ = [] ↔ x = []; (s) Used terms: aren, ren, cstep, cext, aa, s, aext, aα0, ca0, a0, pal1, cren, aal, pcsl, cs0, s0, cs, # aal, ⌜as '⌝ + σ0, step

Proof step 43 from proof repl-fin-size (previous step) (back to tree)

Lemma repla-rec-addboth

Proof step 44 from proof repl-fin-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 45:

  aext !(aα0) = ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ + β, aext !(aal) = [], # pcsl = # pal1, aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), # (⌜as '⌝ + σ0).take(# aal) + # repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) ≠ # aal + # repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) + 1, Some(e) ≠ None, ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, ⌜aal⌝ + ⌜aa '⌝ + aα0), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ∀ pal0, step0, cstep0, cren0, ren0, aren0, cext0, aext0, aσ0, aα0, astart0, astep0, start0, cstart0, ext0. # repls(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) = # repla(step0, cstep0, cren0, ren0, aren0, cext0, aext0, (s0, cs0) ' + pcsl, pal0, aσ0, aα0) + 1 ∨ ¬ frag(IOAut(astart0, astep0, aext0))(aσ0, aα0) ∨ ¬ frag*(IOAut(Π(start0, cstart0), Π(step0, cstep0, ren0, cren0, ext0, cext0), Π(ext0, cext0, ren0, cren0)))((s0, cs0) ' + pcsl, pal0) ∨ ¬ nounsharedextR(cren0, cext0, ren0) ∨ ¬ Πok(ext0, cext0, ren0, cren0) ∨ ¬ ⌜cext0 !(πra(step0, cstep0, ren0, cren0, (s0, cs0) ' + pcsl, pal0))⌝ ⊑ aext0 !(aα0) ⊦

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ # x.map(f) = # x; (s) ⊦ #(x + y) = # x + # y; (s) append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n + 0 = n; (s) ⊦ n ≠ 0 → (⌜a '⌝ + σ).drop((* n) + m) = σ.drop((n - 1) + m); (s) ⊦ ⌜x⌝ = [] ↔ x = []; (s) ⊦ ext !(⌜al⌝ ) = ⌜ext !(al)⌝ ; (s)

Proof step 45 from proof repl-fin-size (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 46:

  aext !(aal) = [], aext !(aα0) = ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ + β, # pcsl = # pal1, aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), # (⌜as '⌝ + σ0).take(# aal) + # repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) ≠ # aal + # repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) + 1, Some(e) ≠ None, ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, ⌜aal⌝ + ⌜aa '⌝ + aα0), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), # repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) = # repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) + 1 ∨ ¬ frag(IOAut(astart, astep, aext))(σ0.drop(# aal), aα0) ∨ ¬ frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1) ∨ ¬ nounsharedextR(cren, cext, ren) ∨ ¬ Πok(ext, cext, ren, cren) ∨ ¬ ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ ⊑ aext !(aα0) ⊦

Rule argument

Additional information

Used terms: pal1, step, cstep, cren, ren, aren, cext, aext, σ0.drop(# aal), aα0, astart, astep, start, cstart, ext

Proof step 46 from proof repl-fin-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 47:

  aext !(aα0) = ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ + β, aext !(aal) = [], # pcsl = # pal1, aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), # (⌜as '⌝ + σ0).take(# aal) + # repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) ≠ # aal + # repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) + 1, Some(e) ≠ None, ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, ⌜aal⌝ + ⌜aa '⌝ + aα0), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), # repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) = # repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) + 1 ∨ ¬ frag(IOAut(astart, astep, aext))(σ0.drop(# aal), aα0) ∨ ¬ ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ ⊑ aext !(aα0) ⊦

Rule argument

Additional information

Proof step 47 from proof repl-fin-size (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 48:

  ¬ # σ < ⌜n⌝ ⊦ # σ.take(n) = n

• Proof step 49:

  aext !(aal) = [], aext !(aα0) = ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ + β, # pcsl = # pal1, aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), # (⌜as '⌝ + σ0).take(# aal) + # repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) ≠ # aal + # repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) + 1, Some(e) ≠ None, ext(a0) ≠ None, #(⌜as '⌝ + σ0) < ⌜# aal⌝ , cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, ⌜aal⌝ + ⌜aa '⌝ + aα0), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), # repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) = # repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) + 1 ∨ ¬ frag(IOAut(astart, astep, aext))(σ0.drop(# aal), aα0) ∨ ¬ ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ ⊑ aext !(aα0) ⊦

• Proof step 54:

  aext !(aal) = [], aext !(aα0) = ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ + β, # pcsl = # pal1, aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), # aal + # repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) ≠ # aal + # repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) + 1, Some(e) ≠ None, ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, ⌜aal⌝ + ⌜aa '⌝ + aα0), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ¬ #(⌜as '⌝ + σ0) < ⌜# aal⌝ , # repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) = # repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) + 1 ∨ ¬ frag(IOAut(astart, astep, aext))(σ0.drop(# aal), aα0) ∨ ¬ ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ ⊑ aext !(aα0) ⊦

Rule argument

Additional information

Used terms: ⌜as '⌝ + σ0, # aal

Proof step 48 from proof repl-fin-size (previous step) (back to tree)

A spec-lemma

Proof step 49 from proof repl-fin-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 50:

  aext !(aα0) = ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ + β, aext !(aal) = [], # pcsl = # pal1, aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), # (⌜as '⌝ + σ0).take(# aal) + # repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) ≠ # aal + # repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) + 1, Some(e) ≠ None, ext(a0) ≠ None, ⌜1⌝ + # σ0 < ⌜# aal⌝ , cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, ⌜aal⌝ + ⌜aa '⌝ + aα0), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), # repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) = # repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) + 1 ∨ ¬ frag(IOAut(astart, astep, aext))(σ0.drop(# aal), aα0) ∨ ¬ ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ ⊑ aext !(aα0) ⊦

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ # a ' = 0 +1; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s)

Proof step 50 from proof repl-fin-size (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 51:

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

• Proof step 52:

  aext !(aal) = [], aext !(aα0) = ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ + β, #(⌜as '⌝ + σ0) = #(⌜aal⌝ + ⌜aa '⌝ + aα0) + ⌜1⌝ , # pcsl = # pal1, aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), # (⌜as '⌝ + σ0).take(# aal) + # repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) ≠ # aal + # repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) + 1, Some(e) ≠ None, ext(a0) ≠ None, ⌜1⌝ + # σ0 < ⌜# aal⌝ , cstep(cs, ca0, cs0), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ∀ n. ⌜n⌝ < #(⌜aal⌝ + ⌜aa '⌝ + aα0) → astep((⌜as '⌝ + σ0)[n], (⌜aal⌝ + ⌜aa '⌝ + aα0)[n], (⌜as '⌝ + σ0)[n +1]), # repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) = # repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) + 1 ∨ ¬ frag(IOAut(astart, astep, aext))(σ0.drop(# aal), aα0) ∨ ¬ ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ ⊑ aext !(aα0) ⊦

Rule argument

Additional information

Used terms: aext, ⌜aal⌝ + ⌜aa '⌝ + aα0, astart, ⌜as '⌝ + σ0, astep

Proof step 51 from proof repl-fin-size (previous step) (back to tree)

A spec-lemma

Proof step 52 from proof repl-fin-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 53:

  aext !(aα0) = ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ + β, aext !(aal) = [], # pcsl = # pal1, # σ0 = ⌜1⌝ + ⌜# aal⌝ + # aα0, aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), # (⌜as '⌝ + σ0).take(# aal) + # repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) ≠ # aal + # repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) + 1, Some(e) ≠ None, ext(a0) ≠ None, ⌜1⌝ + # σ0 < ⌜# aal⌝ , cstep(cs, ca0, cs0), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ∀ n. ¬ ⌜# aal⌝ + # aα0 < ⌜n⌝ → astep((⌜as '⌝ + σ0)[n], (⌜aal⌝ + ⌜aa '⌝ + aα0)[n], σ0[n]), # repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) = # repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) + 1 ∨ ¬ frag(IOAut(astart, astep, aext))(σ0.drop(# aal), aα0) ∨ ¬ ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ ⊑ aext !(aα0) ⊦

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ (⌜a '⌝ + σ)[n + 1] = σ[n]; (s) ⊦ m +1 = m + 1; (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 ⊦ ⌜n⌝ < ⌜1⌝ + n∞ ↔ ¬ n∞ < ⌜n⌝ ; (s) ⊦ # a ' = 0 +1; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s) ⊦ n < m → (⌜(* n)⌝ + n∞1 = ⌜(* m)⌝ + n∞2 ↔ n∞1 = ⌜m - n⌝ + n∞2); (s) ⊦ ⌜(* n)⌝ + ⌜(* m)⌝ = ⌜n + m⌝ ; (s)

Proof step 53 from proof repl-fin-size (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

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

Proof step 54 from proof repl-fin-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 55:

  aext !(aα0) = ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ + β, aext !(aal) = [], # pcsl = # pal1, aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), # repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) + 1, Some(e) ≠ None, ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, ⌜aal⌝ + ⌜aa '⌝ + aα0), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ¬ ⌜1⌝ + # σ0 < ⌜# aal⌝ , ¬ frag(IOAut(astart, astep, aext))(σ0.drop(# aal), aα0) ∨ ¬ ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ ⊑ aext !(aα0) ⊦

Rule argument

Additional information

Used simplifier rules: append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream ⊦ # a ' = 0 +1; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ #(σ + σ1) = # σ + # σ1; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n = m + n0 ↔ n = n0; (s)

Proof step 55 from proof repl-fin-size (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 56:

  aext !(aal) = [], aext !(aα0) = ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ + β, # pcsl = # pal1, aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), # repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) + 1, Some(e) ≠ None, ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, ⌜aal⌝ + ⌜aa '⌝ + aα0), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ¬ ⌜1⌝ + # σ0 < ⌜# aal⌝ , ¬ frag(IOAut(astart, astep, aext))(σ0.drop(# aal), aα0) ⊦

• Proof step 58:

  aext !(aal) = [], aext !(aα0) = ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ + β, # pcsl = # pal1, aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), # repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) + 1, Some(e) ≠ None, ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, ⌜aal⌝ + ⌜aa '⌝ + aα0), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ¬ ⌜1⌝ + # σ0 < ⌜# aal⌝ , ¬ ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ ⊑ aext !(aα0) ⊦

Rule argument

Additional information

Proof step 56 from proof repl-fin-size (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 57:

  ⊦ frag(IOAut(start, step, ext))(σ, α) ∧ ¬ # α < ⌜n⌝ → (frag(IOAut(start, step, ext))(σ.drop(n), α.drop(n)) ↔ true)

Rule argument

Additional information

Used simplifier rules: ⊦ #(σ + σ1) = # σ + # σ1; (s) ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ # a ' = 0 +1; (s) ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ ; (s) ⊦ m ≤ n → (⌜(* m)⌝ + n∞2 < ⌜(* n)⌝ + n∞1 ↔ n∞2 < ⌜n - m⌝ + n∞1); (s) ⊦ n∞ + ⌜0⌝ = n∞; (s) ⊦ ¬ n∞ + n∞1 < n∞1; (s) add-assoc: ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2; from specification nat-inf add-comm: ⊦ n∞1 + n∞2 = n∞2 + n∞1; from specification nat-inf ⊦ n ≠ 0 → (⌜a '⌝ + σ).drop((* n) + m) = σ.drop((n - 1) + m); (s) ⊦ n + 0 = n; (s) ⊦ (⌜x⌝ + σ).drop(m + # x) = σ.drop(m); (s) ⊦ (⌜a '⌝ + σ).drop(1) = σ; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; from specification stream Used terms: aext, ⌜aal⌝ + ⌜aa '⌝ + aα0, astart, ⌜as '⌝ + σ0, # aal + 1, astep

Proof step 57 from proof repl-fin-size (previous step) (back to tree)

A spec-lemma

Proof step 58 from proof repl-fin-size (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 59:

  ⊦ σ ⊑ σ0 ↔ (∃ σ1. σ + σ1 = σ0)

• Proof step 60:

  aext !(aα0) = ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ + β, aext !(aal) = [], # pcsl = # pal1, aext(aa) = Some(e), cext(ca0) = Some(e), cren(ca0) = ren(a0), # repls(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) ≠ # repla(step, cstep, cren, ren, aren, cext, aext, (s0, cs0) ' + pcsl, pal1, σ0.drop(# aal), aα0) + 1, Some(e) ≠ None, ext(a0) ≠ None, cstep(cs, ca0, cs0), frag(IOAut(astart, astep, aext))(⌜as '⌝ + σ0, ⌜aal⌝ + ⌜aa '⌝ + aα0), frag*(IOAut(Π(start, cstart), Π(step, cstep, ren, cren, ext, cext), Π(ext, cext, ren, cren)))((s0, cs0) ' + pcsl, pal1), nounsharedextR(cren, cext, ren), step(s, a0, s0), Πok(ext, cext, ren, cren), ¬ ⌜1⌝ + # σ0 < ⌜# aal⌝ , ∀ σ1. ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ + σ1 ≠ aext !(aα0) ⊦

Rule argument

Additional information

Used terms: ⌜cext !(πra(step, cstep, ren, cren, (s0, cs0) ' + pcsl, pal1))⌝ , aext !(aα0)

Proof step 59 from proof repl-fin-size (previous step) (back to tree)

A spec-lemma

Proof step 60 from proof repl-fin-size (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: β