Proof step 29 from proof inject-n2s (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 30:

  ⊦ m < # chars ∧ n < # chars ∧ ¬ dups(chars) → (chars[m] ' = chars[n] ' ↔ m = n)

Rule argument

Additional information

Used simplifier rules: ⊦ #(chars + chars0) = # chars + # chars0;% ⊦ # char ' = 0 +1;% ⊦ (chars + chars0) + chars1 = chars + chars0 + chars1;% ⊦ dups(char ' + chars) ↔ ¬ ¬(char ∈ chars ∨ dups(chars));% ⊦ char ∈ chars + chars0 ↔ ¬ ¬(char ∈ chars ∨ char ∈ chars0);% ⊦ char ∈ char0 ' ↔ char = char0;% ⊦ ¬ dups(char '); Used terms: n, m, '0' ' + '1' ' + '2' ' + '3' ' + '4' ' + '5' ' + '6' ' + '7' ' + '8' ' + '9' '