Proof step 1 from proof longest-common-prefix (conclusion) (back to tree)

Heuristic structural induction applied rule structural induction

And obtained the following new goals

• Proof step 2:

  ⊦ ∃ z, x0, y0. x = z + x0 ∧ [] = z + y0 ∧ (x0 ≠ [] ∧ y0 ≠ [] → x0.head ≠ y0.head)

• Proof step 3:

  ∀ x. ∃ z, x0, y1. x = z + x0 ∧ y0 = z + y1 ∧ (x0 ≠ [] ∧ y1 ≠ [] → x0.head ≠ y1.head) ⊦ ∃ z, x0, y1. x = z + x0 ∧ a + y0 = z + y1 ∧ (x0 ≠ [] ∧ y1 ≠ [] → x0.head ≠ y1.head)

Rule argument

Additional information

Used simplifier rules: list('a) freely generated by [], +;;

Proof step 2 from proof longest-common-prefix (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: Nil: ⊦ [] + x = x; a: ⊦ (x + y) + z = x + y + z; Used terms: [], x, []

Proof step 3 from proof longest-common-prefix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  ∀ x. ∃ z, x0, y1. x = z + x0 ∧ y0 = z + y1 ∧ (x0 ≠ [] ∧ y1 ≠ [] → x0.head ≠ y1.head) ⊦ ∃ z, x0, y1. x = z + x0 ∧ a ' + y0 = z + y1 ∧ (x0 ≠ [] ∧ y1 ≠ [] → x0.head ≠ y1.head)

Rule argument

Additional information

Used simplifier rules: c: ⊦ a + x = a ' + x;

Proof step 4 from proof longest-common-prefix (previous step) (back to tree)

User applied rule constructor cut

And obtained the following new goals

• Proof step 5:

  x = [], ∀ x. ∃ z, x0, y1. x = z + x0 ∧ y0 = z + y1 ∧ (x0 ≠ [] ∧ y1 ≠ [] → x0.head ≠ y1.head) ⊦ ∃ z, x0, y1. x = z + x0 ∧ a ' + y0 = z + y1 ∧ (x0 ≠ [] ∧ y1 ≠ [] → x0.head ≠ y1.head)

• Proof step 7:

  x = a0 + x1, ∀ x. ∃ z, x0, y1. x = z + x0 ∧ y0 = z + y1 ∧ (x0 ≠ [] ∧ y1 ≠ [] → x0.head ≠ y1.head) ⊦ ∃ z, x0, y1. x = z + x0 ∧ a ' + y0 = z + y1 ∧ (x0 ≠ [] ∧ y1 ≠ [] → x0.head ≠ y1.head)

Rule argument

Additional information

Used simplifier rules: list('a) freely generated by [], +;;

Proof step 5 from proof longest-common-prefix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  ∀ x. ∃ z, x0, y1. x = z + x0 ∧ y0 = z + y1 ∧ (x0 ≠ [] ∧ y1 ≠ [] → x0.head ≠ y1.head) ⊦ ∃ z, x0, y1. [] = z + x0 ∧ a ' + y0 = z + y1 ∧ (x0 ≠ [] ∧ y1 ≠ [] → x0.head ≠ y1.head)

Rule argument

Additional information

Proof step 6 from proof longest-common-prefix (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: c: ⊦ a + x = a ' + x; Nil: ⊦ [] + x = x; app-01: ⊦ x + y = x + z ↔ y = z; a: ⊦ (x + y) + z = x + y + z; Used terms: [], [], a + y0

Proof step 7 from proof longest-common-prefix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  ∀ x. ∃ z, x0, y1. x = z + x0 ∧ y0 = z + y1 ∧ (x0 ≠ [] ∧ y1 ≠ [] → x0.head ≠ y1.head) ⊦ ∃ z, x0, y1. a0 ' + x1 = z + x0 ∧ a ' + y0 = z + y1 ∧ (x0 ≠ [] ∧ y1 ≠ [] → x0.head ≠ y1.head)

Rule argument

Additional information

Used simplifier rules: c: ⊦ a + x = a ' + x;

Proof step 8 from proof longest-common-prefix (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 9:

  a = a0, ∀ x. ∃ z, x0, y1. x = z + x0 ∧ y0 = z + y1 ∧ (x0 ≠ [] ∧ y1 ≠ [] → x0.head ≠ y1.head) ⊦ ∃ z, x0, y1. a0 ' + x1 = z + x0 ∧ a ' + y0 = z + y1 ∧ (x0 ≠ [] ∧ y1 ≠ [] → x0.head ≠ y1.head)

• Proof step 13:

  a ≠ a0, ∀ x. ∃ z, x0, y1. x = z + x0 ∧ y0 = z + y1 ∧ (x0 ≠ [] ∧ y1 ≠ [] → x0.head ≠ y1.head) ⊦ ∃ z, x0, y1. a0 ' + x1 = z + x0 ∧ a ' + y0 = z + y1 ∧ (x0 ≠ [] ∧ y1 ≠ [] → x0.head ≠ y1.head)

Rule argument

Additional information

Used formulas: a = a0

Proof step 9 from proof longest-common-prefix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  ∀ x. ∃ z, x0, y1. x = z + x0 ∧ y0 = z + y1 ∧ (x0 ≠ [] ∧ y1 ≠ [] → x0.head ≠ y1.head) ⊦ ∃ z, x0, y1. a0 ' + x1 = z + x0 ∧ a0 ' + y0 = z + y1 ∧ (x0 ≠ [] ∧ y1 ≠ [] → x0.head ≠ y1.head)

Rule argument

Additional information

Proof step 10 from proof longest-common-prefix (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 11:

  ∃ z, x0, y1. x1 = z + x0 ∧ y0 = z + y1 ∧ (x0 ≠ [] ∧ y1 ≠ [] → x0.head ≠ y1.head) ⊦ ∃ z, x0, y1. a0 ' + x1 = z + x0 ∧ a0 ' + y0 = z + y1 ∧ (x0 ≠ [] ∧ y1 ≠ [] → x0.head ≠ y1.head)

Rule argument

Additional information

Used terms: x1

Proof step 11 from proof longest-common-prefix (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  x0 ≠ [] ∧ y1 ≠ [] → x0.head ≠ y1.head ⊦ ∃ z0, x, y. a0 ' + z + x0 = z0 + x ∧ a0 ' + z + y1 = z0 + y ∧ (x ≠ [] ∧ y ≠ [] → x.head ≠ y.head)

Rule argument

Additional information

Proof step 12 from proof longest-common-prefix (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: a: ⊦ (x + y) + z = x + y + z; Used terms: a0 ' + z, x0, y1

Proof step 13 from proof longest-common-prefix (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: Nil: ⊦ [] + x = x; app-01: ⊦ x + y = x + z ↔ y = z; e-01: ⊦ a ' + x ≠ []; c-08: ⊦ (a ' + x).head = a; a: ⊦ (x + y) + z = x + y + z; Used terms: [], a0 ' + x1, a ' + y0