Proof step 1 from proof fragfin-size-ls-02 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(# sl < # al ↔ false), frag*(IOAut(start, step, ext))(s ' + sl, al) ⊦

Rule argument

Additional information

Proof step 2 from proof fragfin-size-ls-02 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

Used simplifier rules: ⊦ #(σ + σ1) = # σ + # σ1; (s) ⊦ # a ' = 0 +1; (s) ⊦ m ≤ n → (⌜(* n)⌝ + n∞1 = ⌜(* m)⌝ + n∞2 ↔ ⌜n - m⌝ + n∞1 = n∞2); (s) ⊦ n∞ + ⌜0⌝ = n∞; (s) ⊦ ⌜n⌝ = ⌜n0⌝ ↔ n = n0; (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 ⊦ # ⌜x⌝ = ⌜# x⌝ ; (s) ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n; (s) ⊦ (⌜x⌝ + ⌜x0⌝ )[m] = (x + x0)[m]; (s) ⊦ m +1 = m + 1; (s) ⊦ (⌜a '⌝ + σ)[n + 1] = σ[n]; (s) ⊦ ⌜x⌝ [n] = x[n]; (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 f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ # x = 0 ↔ x = []; (s) ⊦ m < n → ¬ n < m; (s) Used terms: ext, ⌜al⌝ , step, start, ⌜s '⌝ + ⌜sl⌝

Proof step 3 from proof fragfin-size-ls-02 (previous step) (back to tree)

Lemma frag