Proof step 1 from proof insorted (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(pos(char, sortedchars) < # sortedchars ↔ true) ⊦

Rule argument

Additional information

Proof step 2 from proof insorted (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  # sortedchars ≤ pos(char, sortedchars) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 3 from proof insorted (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ sortedchars = " !#$%&()*+-./0123456789:<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[]^_abcdefghijklmnopqrstuvwxyz|~"

• Proof step 5:

  # " !#$%&()*+-./0123456789:<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[]^_abcdefghijklmnopqrstuvwxyz|~" ≤ pos(char, " !#$%&()*+-./0123456789:<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[]^_abcdefghijklmnopqrstuvwxyz|~") ⊦

Rule argument

Additional information

Used terms:

Proof step 4 from proof insorted (previous step) (back to tree)

Lemma Sortedchars

Proof step 5 from proof insorted (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  pos(char, " !#$%&()*+-./0123456789:<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[]^_abcdefghijklmnopqrstuvwxyz|~") ≠ 0, 87 ≤ pos(char, " !#$%&()*+-./0123456789:<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[]^_abcdefghijklmnopqrstuvwxyz|~") ⊦

Rule argument

Additional information

Used simplifier rules: len-str-01: str ≠ "" ⊦ # (* str) = # str.rstring + 1; not-zero: 0 < n ⊦ (* n) ≤ m → m ≠ 0; (forward) from specification nat c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ # "" = 0; (s)

Proof step 6 from proof insorted (previous step) (back to tree)

User applied rule structural induction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-02: str ≠ "", char ≠ str.char1 ⊦ pos((* char), (* str)) = pos(char, str.rstring) + 1; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; pos-str-03: str ≠ "", char = str.char1 ⊦ pos((* char), (* str)) = 0; char generated by `a`, `b`, `c`, `d`, `e`, `f`, `g`, `h`, `i`, `j`, `k`, `l`, `m`, `n`, `o`, `p`, `q`, `r`, `s`, `t`, `u`, `v`, `w`, `x`, `y`, `z`, `A`, `B`, `C`, `D`, `E`, `F`, `G`, `H`, `I`, `J`, `K`, `L`, `M`, `N`, `O`, `P`, `Q`, `R`, `S`, `T`, `U`, `V`, `W`, `X`, `Y`, `Z`, `!`, `@`, `#`, `$`, `%`, `^`, `&`, `*`, `_`, `-`, `+`, `=`, `~`, `<`, `>`, `?`, `.`, `:`, `/`, `|`, `0`, `1`, `2`, `3`, `4`, `5`, `6`, `7`, `8`, `9`, `(`, `)`, `[`, `]`, ` ` ;; a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic