Proof step 1 from proof len-app (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  #(str + str0) ≠ # str + # str0 ⊦

Rule argument

Additional information

Proof step 2 from proof len-app (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  #((char + str1) + str0) ≠ #(char + str1) + # str0, ∀ str0. #(str1 + str0) = # str1 + # str0 ⊦

Rule argument

Additional information

Used simplifier rules: string freely generated by "", +;; ⊦ "" + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[string] ⊦ # "" = 0; (s) ⊦ n + 0 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic

Proof step 3 from proof len-app (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  #(str1 + str0) ≠ # str1 + # str0, ∀ str0. #(str1 + str0) = # str1 + # str0 ⊦

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 ⊦ m + n = m + n0 ↔ n = n0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[string] ⊦ m +1 = m + 1; (s) ⊦ #(a ' + x) = (# x)+1; (s) ⊦ a + x = a ' + x; (s)

Proof step 4 from proof len-app (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: str0