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:

  str < str2, str2 < str3, ¬ 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. ¬(str0 < str2 ∧ str2 < str3 ∧ ¬ 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:

  char ' + str0 < str2, str2 < str3, ¬ char ' + str0 < str3, ∀ str, str1. ¬ str0 < str ∨ ¬ str < str1 ∨ 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, ∀ char, str0, str3. ¬(char ' + str0 < str ∧ str < str3 ∧ ¬ char ' + str0 < str3 ∧ (∀ str, str1. ¬ str0 < str ∨ ¬ str < str1 ∨ str0 < str1)), ∀ str, str1. ¬ str0 < str ∨ ¬ str < str1 ∨ str0 < str1 ⊦

Rule argument

Additional information

Used simplifier rules: 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:

  char ' + str0 < char0 ' + str, char0 ' + str < str3, ¬ char ' + str0 < str3, ∀ char1, str1, str2. ¬ char1 ' + str1 < str ∨ ¬ str < str2 ∨ char1 ' + str1 < str2 ∨ ¬(∀ str, str2. ¬ str1 < str ∨ ¬ str < str2 ∨ str1 < str2), ∀ str, str1. ¬ str0 < str ∨ ¬ str < str1 ∨ str0 < 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, char < char0 ∨ char = char0 ∧ str0 < str, ∀ char1, str1, str2. ¬ char1 ' + str1 < str ∨ ¬ str < str2 ∨ char1 ' + str1 < str2 ∨ ¬(∀ str, str2. ¬ str1 < str ∨ ¬ str < str2 ∨ str1 < str2), ∀ str, str1. ¬ str0 < str ∨ ¬ str < str1 ∨ str0 < str1 ⊦

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:

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

• Proof step 14:

  char = char0, char0 ' + str < str3, str0 < str, ¬ char ' + str0 < str3, ∀ char1, str1, str2. ¬ char1 ' + str1 < str ∨ ¬ str < str2 ∨ char1 ' + str1 < str2 ∨ ¬(∀ str, str2. ¬ str1 < str ∨ ¬ str < str2 ∨ str1 < str2), ∀ str, str1. ¬ str0 < str ∨ ¬ str < str1 ∨ str0 < 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, ∀ char, char0, str, str0. ¬ ( char < char0 ∧ char0 ' + str < str1 ∧ ¬ char ' + str0 < str1 ∧ (∀ char1, str1, str2. ¬ char1 ' + str1 < str ∨ ¬ str < str2 ∨ char1 ' + str1 < str2 ∨ ¬(∀ str, str2. ¬ str1 < str ∨ ¬ str < str2 ∨ str1 < str2)) ∧ (∀ str, str1. ¬ str0 < str ∨ ¬ str < str1 ∨ str0 < str1)), ∀ char1, str1, str2. ¬ char1 ' + str1 < str ∨ ¬ str < str2 ∨ char1 ' + str1 < str2 ∨ ¬(∀ str, str2. ¬ str1 < str ∨ ¬ str < str2 ∨ str1 < str2), ∀ str, str1. ¬ str0 < str ∨ ¬ str < str1 ∨ str0 < 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, ∀ char1, str1, str2. ¬ char1 ' + str1 < str ∨ ¬ str < str2 ∨ char1 ' + str1 < str2 ∨ ¬(∀ str, str2. ¬ str1 < str ∨ ¬ str < str2 ∨ str1 < str2), ∀ char2, char3, str2, str3. ¬ char2 < char3 ∨ ¬ char3 ' + str2 < str1 ∨ char2 ' + str3 < str1 ∨ ¬ (∀ char1, str1, str0. ¬ char1 ' + str1 < str2 ∨ ¬ str2 < str0 ∨ char1 ' + str1 < str0 ∨ ¬(∀ str, str2. ¬ str1 < str ∨ ¬ str < str2 ∨ str1 < str2)) ∨ ¬(∀ str, str1. ¬ str3 < str ∨ ¬ str < str1 ∨ str3 < str1), ∀ str, str1. ¬ str0 < str ∨ ¬ str < str1 ∨ 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:

  char0 ' + str < str3, str0 < str, ¬ char0 ' + str0 < str3, ∀ char1, str1, str2. ¬ char1 ' + str1 < str ∨ ¬ str < str2 ∨ char1 ' + str1 < str2 ∨ ¬(∀ str, str2. ¬ str1 < str ∨ ¬ str < str2 ∨ str1 < str2), ∀ str, str1. ¬ str0 < str ∨ ¬ str < str1 ∨ 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, ∀ char0, str, str0. ¬ ( char0 ' + str < str1 ∧ str0 < str ∧ ¬ char0 ' + str0 < str1 ∧ (∀ char1, str1, str2. ¬ char1 ' + str1 < str ∨ ¬ str < str2 ∨ char1 ' + str1 < str2 ∨ ¬(∀ str, str2. ¬ str1 < str ∨ ¬ str < str2 ∨ str1 < str2)) ∧ (∀ str, str1. ¬ str0 < str ∨ ¬ str < str1 ∨ str0 < str1)), ∀ char1, str1, str2. ¬ char1 ' + str1 < str ∨ ¬ str < str2 ∨ char1 ' + str1 < str2 ∨ ¬(∀ str, str2. ¬ str1 < str ∨ ¬ str < str2 ∨ str1 < str2), ∀ str, str1. ¬ str0 < str ∨ ¬ str < str1 ∨ 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, ∀ char1, str2, str3. ¬ char1 ' + str2 < str1 ∨ ¬ str3 < str2 ∨ char1 ' + str3 < str1 ∨ ¬ (∀ char1, str1, str0. ¬ char1 ' + str1 < str2 ∨ ¬ str2 < str0 ∨ char1 ' + str1 < str0 ∨ ¬(∀ str, str2. ¬ str1 < str ∨ ¬ str < str2 ∨ str1 < str2)) ∨ ¬(∀ str, str1. ¬ str3 < str ∨ ¬ str < str1 ∨ str3 < str1), ∀ char1, str1, str2. ¬ char1 ' + str1 < str ∨ ¬ str < str2 ∨ char1 ' + str1 < str2 ∨ ¬(∀ str, str2. ¬ str1 < str ∨ ¬ str < str2 ∨ str1 < str2), ∀ str, str1. ¬ str0 < str ∨ ¬ str < str1 ∨ str0 < 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