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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  str < str2, str2 < str3, ¬ str < str3 ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  str2 < str3, str < str2, ¬ str < str3 ⊦

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

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

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  str2 < str3, char ' + str0 < str2, ¬ char ' + str0 < str3, ∀ str, str1. ¬ str < str1 ∨ ¬ str0 < str ∨ str0 < str1 ⊦

Rule argument

Additional information

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

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

User applied rule structural induction

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  char0 ' + str < str3, char ' + str0 < char0 ' + str, ¬ char ' + str0 < str3, ∀ str, str1. ¬ str < str1 ∨ ¬ str0 < str ∨ str0 < str1, ∀ str1, char1, str2. ¬ str < str1 ∨ ¬ char1 ' + str2 < str ∨ char1 ' + str2 < str1 ∨ ¬(∀ str, str1. ¬ str < str1 ∨ ¬ str2 < str ∨ str2 < str1) ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ char1 ' + str1 < char2 ' + str2 ↔ char1 < char2 ∨ char1 = char2 ∧ str1 < str2

• Proof step 9:

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

Rule argument

Additional information

Used terms: str, char0, str0, char

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

Lemma Less-rec

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

User applied rule case distinction

And obtained the following new goals

• Proof step 10:

  char0 ' + str < str3, char < char0, ¬ char ' + str0 < str3, ∀ str, str1. ¬ str < str1 ∨ ¬ str0 < str ∨ str0 < str1, ∀ str1, char1, str2. ¬ str < str1 ∨ ¬ char1 ' + str2 < str ∨ char1 ' + str2 < str1 ∨ ¬(∀ str, str1. ¬ str < str1 ∨ ¬ str2 < str ∨ str2 < str1) ⊦

• Proof step 14:

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

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

Used simplifier rules: Less-notempty: ⊦ ¬ str < ""; string freely generated by "", +;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  char < char0, char0 ' + str < char1 ' + str1, ¬ char < char1, ∀ str, str1. ¬ str < str1 ∨ ¬ str0 < str ∨ str0 < str1, ∀ str1, char1, str2. ¬ str < str1 ∨ ¬ char1 ' + str2 < str ∨ char1 ' + str2 < str1 ∨ ¬(∀ str, str1. ¬ str < str1 ∨ ¬ str2 < str ∨ str2 < str1), ∀ char2, str2, char3, str3. ¬ char2 ' + str2 < str1 ∨ ¬ char3 < char2 ∨ char3 ' + str3 < str1 ∨ ¬(∀ str, str1. ¬ str < str1 ∨ ¬ str3 < str ∨ str3 < str1) ∨ ¬ (∀ str1, char1, str0. ¬ str2 < str1 ∨ ¬ char1 ' + str0 < str2 ∨ char1 ' + str0 < str1 ∨ ¬(∀ str, str1. ¬ str < str1 ∨ ¬ str0 < str ∨ str0 < str1)) ⊦ char = char1 ∧ str0 < str1

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 12 from proof val-trans (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ char1 ' + str1 < char2 ' + str2 ↔ char1 < char2 ∨ char1 = char2 ∧ str1 < str2

Rule argument

Additional information

Used simplifier rules: val-trans-01: ⊦ char < char2 ∧ char2 < char3 → char < char3; Used terms: str1, char1, str, char0

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

Lemma Less-rec

Proof step 14 from proof val-trans (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  str0 < str, char0 ' + str < str3, ¬ char0 ' + str0 < str3, ∀ str1, char1, str2. ¬ str < str1 ∨ ¬ char1 ' + str2 < str ∨ char1 ' + str2 < str1 ∨ ¬(∀ str, str1. ¬ str < str1 ∨ ¬ str2 < str ∨ str2 < str1), ∀ str, str1. ¬ str < str1 ∨ ¬ str0 < str ∨ str0 < str1 ⊦

Rule argument

Additional information

Proof step 15 from proof val-trans (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 16:

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

Rule argument

Additional information

Used simplifier rules: Less-notempty: ⊦ ¬ str < ""; string freely generated by "", +;;

Proof step 16 from proof val-trans (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  str < str1, str0 < str, ¬ str0 < str1, ∀ str2, str3, char1. ¬ str2 < str3 ∨ ¬ char1 ' + str3 < str1 ∨ char1 ' + str2 < str1 ∨ ¬ (∀ str1, char1, str2. ¬ str3 < str1 ∨ ¬ char1 ' + str2 < str3 ∨ char1 ' + str2 < str1 ∨ ¬(∀ str, str1. ¬ str < str1 ∨ ¬ str2 < str ∨ str2 < str1)) ∨ ¬(∀ str, str1. ¬ str < str1 ∨ ¬ str2 < str ∨ str2 < str1), ∀ str, str1. ¬ str < str1 ∨ ¬ str0 < str ∨ str0 < str1, ∀ str1, char1, str2. ¬ str < str1 ∨ ¬ char1 ' + str2 < str ∨ char1 ' + str2 < str1 ∨ ¬(∀ str, str1. ¬ str < str1 ∨ ¬ str2 < str ∨ str2 < str1) ⊦

Rule argument

Additional information

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

Proof step 17 from proof val-trans (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: str, str1