Proof step 1 from proof toone-cons (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ⌜a '⌝ + σ to 1 ≠ a ' ⊦

Rule argument

Additional information

Proof step 2 from proof toone-cons (previous step) (back to tree)

User applied rule structural induction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: to-appfin: ⊦ ⌜x⌝ + ⌜y⌝ to n = x + y to n; toone-cons-fin: ⊦ a ' + y to 1 = a '; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; append-empty-01: ⊦ σ0 + σ1 = [] ↔ σ0 = [] ∧ σ1 = []; fin-empty: ⊦ ⌜x⌝ = [] ↔ x = []; toone-equal: σ ≠ [] ⊦ σ to 1 = a ' ↔ σ[0] = a; get-cons-zero: ⊦ (⌜a '⌝ + σ)[0] = a; append-assoc: ⊦ (σ + σ1) + σ2 = σ + σ1 + σ2; stream('a) freely generated by ⌜ ⌝, ⌜ ⌝;; ⊦ a ' ≠ []; (s) a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ a ' = a0 ' ↔ a = a0; (s)