Proof step 1 from proof val-total (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  str ≠ str2, ¬ str < str2, ¬ str2 < str ⊦

Rule argument

Additional information

Proof step 2 from proof val-total (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  str ≠ str2, ¬ str < str2, ¬ str2 < str ⊦

Rule argument

Additional information

Proof step 3 from proof val-total (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  char + str0 ≠ str2, ¬ char + str0 < str2, ¬ str2 < char + str0, ∀ str2. ¬(str0 ≠ str2 ∧ ¬ str0 < str2 ∧ ¬ str2 < str0) ⊦

Rule argument

Additional information

Used simplifier rules: less-empty: ⊦ "" < str ↔ str ≠ ""; string freely generated by "", +;;

Proof step 4 from proof val-total (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  char ' + str0 ≠ str2, ¬ char ' + str0 < str2, ¬ str2 < char ' + str0, ∀ str. str0 = str ∨ str0 < str ∨ str < str0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + x = a ' + x; (s)

Proof step 5 from proof val-total (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 6:

  char ' + str0 ≠ char0 + str, ¬ char ' + str0 < char0 + str, ¬ char0 + str < char ' + str0, ∀ str. str0 = str ∨ str0 < str ∨ str < str0, ∀ char, str0. ¬(char ' + str0 ≠ str ∧ ¬ char ' + str0 < str ∧ ¬ str < char ' + str0 ∧ (∀ str. str0 = str ∨ str0 < str ∨ str < str0)) ⊦

Rule argument

Additional information

Used simplifier rules: Less-empty: ⊦ "" < char ' + str; string freely generated by "", +;; ⊦ a ' + x ≠ ""; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[string]

Proof step 6 from proof val-total (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  char ' + str0 ≠ char0 ' + str, ¬ char < char0, ¬ char0 < char, ∀ str. str0 = str ∨ str0 < str ∨ str < str0, ∀ char1, str1. char1 ' + str1 = str ∨ char1 ' + str1 < str ∨ str < char1 ' + str1 ∨ ¬(∀ str. str1 = str ∨ str1 < str ∨ str < str1) ⊦ char = char0 ∧ str0 < str, char0 = char ∧ str < str0

Rule argument

Additional information

Used simplifier rules: Less-rec: ⊦ char1 ' + str1 < char2 ' + str2 ↔ char1 < char2 ∨ char1 = char2 ∧ str1 < str2; a: ⊦ (x + y) + z = x + y + z; from specification list[string] ⊦ a + x = a ' + x; (s)

Proof step 7 from proof val-total (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  y ≠ "" ⊦ a ' + x = y + z ↔ a = y.char1 ∧ x = y.rstring + z

• Proof step 9:

  char0 ' ≠ "", ¬ char < char0, ¬ char0 < char, ∀ char1, str1. char1 ' + str1 = str ∨ char1 ' + str1 < str ∨ str < char1 ' + str1 ∨ ¬(∀ str. str1 = str ∨ str1 < str ∨ str < str1), ∀ str. str0 = str ∨ str0 < str ∨ str < str0, char ≠ char0 '.char1 ∨ str0 ≠ char0 '.rstring + str ⊦ char0 = char ∧ str < str0, char = char0 ∧ str0 < str

Rule argument

Additional information

Used simplifier rules: ⊦ a ' ≠ ""; (s) Used terms: str, char0 ', str0, char

Proof step 8 from proof val-total (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof val-total (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  ¬ char < char0, ¬ char0 < char, ∀ str. str0 = str ∨ str0 < str ∨ str < str0, ∀ char1, str1. char1 ' + str1 = str ∨ char1 ' + str1 < str ∨ str < char1 ' + str1 ∨ ¬(∀ str. str1 = str ∨ str1 < str ∨ str < str1), char ≠ char0 ∨ str0 ≠ str ⊦ char = char0 ∧ str0 < str, char0 = char ∧ str < str0

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; from specification list[string] ⊦ "" + x = x; (s) ⊦ a '.rstring = ""; (s) ⊦ a '.char1 = a; (s) ⊦ a ' ≠ ""; (s)

Proof step 10 from proof val-total (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 11:

  ⊦ char1 < char2 ∨ char1 = char2 ∨ char2 < char1

• Proof step 12:

  ¬ char < char0, ¬ char0 < char, ∀ char1, str1. char1 ' + str1 = str ∨ char1 ' + str1 < str ∨ str < char1 ' + str1 ∨ ¬(∀ str. str1 = str ∨ str1 < str ∨ str < str1), ∀ str. str0 = str ∨ str0 < str ∨ str < str0, char ≠ char0 ∨ str0 ≠ str, char < char0 ∨ char = char0 ∨ char0 < char ⊦ char0 = char ∧ str < str0, char = char0 ∧ str0 < str

Rule argument

Additional information

Used terms: char, char0

Proof step 11 from proof val-total (previous step) (back to tree)

Lemma Char-total

Proof step 12 from proof val-total (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  str0 ≠ str, ¬ str < str0, ¬ str0 < str, ∀ char1, str1. char1 ' + str1 = str ∨ char1 ' + str1 < str ∨ str < char1 ' + str1 ∨ ¬(∀ str. str1 = str ∨ str1 < str ∨ str < str1), ∀ str. str0 = str ∨ str0 < str ∨ str < str0 ⊦

Rule argument

Additional information

Used simplifier rules: Char-irref: ⊦ ¬ char < char;

Proof step 13 from proof val-total (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: str