Proof step 2 from proof n2s-chars (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  char ∈ s→l(n→s(m)), ∀ m1, char. m1 < m → true → ¬ char ∈ '0' + '1' + '2' + '3' + '4' + '5' + '6' + '7' + ('8' + '9') → ¬ char ∈ s→l(n→s(m1)) ⊦ char = '0', char = '9', char = '8', char = '7', char = '6', char = '5', char = '4', char = '3', char = '2', char = '1'

Rule argument

Additional information

Used simplifier rules: ⊦ (chars + chars0) + chars1 = chars + chars0 + chars1;% ⊦ char ∈ char0 ' ↔ char = char0;% ⊦ char ∈ chars + chars0 ↔ ¬ ¬(char ∈ chars ∨ char ∈ chars0);% ⊦ ¬ char ∈ char0 ' + chars ↔ char ≠ char0 ∧ ¬ char ∈ chars;% ⊦ char + chars = char ' + chars;% ⊦ char + char0 = char ' + char0 ';