Proof step 1 from proof postfix-split-stronger (conclusion) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  x ⊒ y + z, ¬ x ⊒ z ⊦ ∃ x0. x0 + z = x ∧ x0 ⊒ y

Rule argument

Additional information

Proof step 2 from proof postfix-split-stronger (previous step) (back to tree)

User applied rule induction

And obtained the following new goals

• Proof step 3:

  x ⊒ y + z, ¬ x ⊒ z, ∀ x0, y, z. # x0 < # x → x0 ⊒ y + z ∧ ¬ x0 ⊒ z → (∃ x1. x1 + z = x0 ∧ x1 ⊒ y) ⊦ ∃ x0. x0 + z = x ∧ x0 ⊒ y

Rule argument

Additional information

Used simplifier rules: <; (wellfounded) Used terms: # x

Proof step 3 from proof postfix-split-stronger (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  x ⊒ y + z, ¬ x ⊒ z, ∀ x0, y, z. # x0 < # x → x0 ⊒ y + z ∧ ¬ x0 ⊒ z → (∃ x1. x1 + z = x0 ∧ x1 ⊒ y) ⊦ ∃ x0. x0 + z = x ∧ x0 ⊒ y

Rule argument

Additional information

Proof step 4 from proof postfix-split-stronger (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ x ≠ [] ∧ y ≠ [] → (x ⊒ y ↔ x.last = y.last ∧ x.butlast ⊒ y.butlast)

• Proof step 6:

  x.last = (y + z).last, y + z ≠ [], x ≠ [], x.butlast ⊒ (y + z).butlast, ¬ x ⊒ z, ∀ x0, y, z. # x0 < # x → x0 ⊒ y + z ∧ ¬ x0 ⊒ z → (∃ x1. x1 + z = x0 ∧ x1 ⊒ y) ⊦ ∃ x0. x0 + z = x ∧ x0 ⊒ y

Rule argument

Additional information

Used simplifier rules: postfix-empty: ⊦ [] ⊒ x; postfix-empty-03: ⊦ x ⊒ [] ↔ x = []; ⊦ x + y = [] ↔ x = [] ∧ y = []; (as) ⊦ [] + x = x; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: y + z, x

Proof step 5 from proof postfix-split-stronger (previous step) (back to tree)

Lemma postfix-rec

Proof step 6 from proof postfix-split-stronger (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  x.last = (y + z).last, y + z ≠ [], x ≠ [], x.butlast ⊒ (y + z).butlast, ¬ x ⊒ z, ∀ x0, y, z. # x0 < # x → x0 ⊒ y + z ∧ ¬ x0 ⊒ z → (∃ x1. x1 + z = x0 ∧ x1 ⊒ y) ⊦ ∃ x0. x0 + z = x ∧ x0 ⊒ y

Rule argument

Additional information

Proof step 7 from proof postfix-split-stronger (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ x ≠ [] ∧ y ≠ [] → (x ⊒ y ↔ x.last = y.last ∧ x.butlast ⊒ y.butlast)

• Proof step 9:

  x.last = (y + z).last, y + z ≠ [], x ≠ [], x.butlast ⊒ (y + z).butlast, ¬ x ⊒ z, ∀ x0, y, z. # x0 < # x → x0 ⊒ y + z ∧ ¬ x0 ⊒ z → (∃ x1. x1 + z = x0 ∧ x1 ⊒ y) ⊦ ∃ x0. x0 + z = x ∧ x0 ⊒ y, x ≠ [] ∧ z ≠ []

• Proof step 12:

  x.last = (y + z).last, y + z ≠ [], x ≠ [], z ≠ [], x.butlast ⊒ (y + z).butlast, x.last ≠ z.last ∨ ¬ x.butlast ⊒ z.butlast, ∀ x0, y, z. # x0 < # x → x0 ⊒ y + z ∧ ¬ x0 ⊒ z → (∃ x1. x1 + z = x0 ∧ x1 ⊒ y) ⊦ ∃ x0. x0 + z = x ∧ x0 ⊒ y

Rule argument

Additional information

Used terms: z, x

Proof step 8 from proof postfix-split-stronger (previous step) (back to tree)

Lemma postfix-rec

Proof step 9 from proof postfix-split-stronger (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  x.last = y.last, x ≠ [], y ≠ [], x.butlast ⊒ y.butlast, ¬ x ⊒ y, ∀ x0, y, z. # x0 < # x → x0 ⊒ y + z ∧ ¬ x0 ⊒ z → (∃ x1. x1 + z = x0 ∧ x1 ⊒ y) ⊦

Rule argument

Additional information

Used simplifier rules: postfix-empty-03: ⊦ x ⊒ [] ↔ x = []; a: ⊦ (x + y) + z = x + y + z; from specification list ⊦ x + [] = x; (s)

Proof step 10 from proof postfix-split-stronger (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ x ≠ [] ∧ y ≠ [] → (x ⊒ y ↔ x.last = y.last ∧ x.butlast ⊒ y.butlast)

Rule argument

Additional information

Used terms: y, x

Proof step 11 from proof postfix-split-stronger (previous step) (back to tree)

Lemma postfix-rec

Proof step 12 from proof postfix-split-stronger (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  x.last = z.last, y + z ≠ [], x ≠ [], z ≠ [], x.butlast ⊒ y + z.butlast, ¬ x.butlast ⊒ z.butlast, ∀ x0, y, z. # x0 < # x → x0 ⊒ y + z ∧ ¬ x0 ⊒ z → (∃ x1. x1 + z = x0 ∧ x1 ⊒ y) ⊦ ∃ x0. x0 + z = x ∧ x0 ⊒ y

Rule argument

Additional information

Used simplifier rules: lapp: ⊦ y ≠ [] → (x + y).last = y.last; bapp: ⊦ y ≠ [] → (x + y).butlast = x + y.butlast; a: ⊦ (x + y) + z = x + y + z; from specification list

Proof step 13 from proof postfix-split-stronger (previous step) (back to tree)

User applied rule apply induction

And obtained the following new goals

• Proof step 14:

  x.last = z.last, y + z ≠ [], x ≠ [], z ≠ [], x.butlast ⊒ y + z.butlast, ¬ # x.butlast < # x, ¬ x.butlast ⊒ z.butlast, ∀ x0, y, z. # x0 < # x → x0 ⊒ y + z ∧ ¬ x0 ⊒ z → (∃ x1. x1 + z = x0 ∧ x1 ⊒ y) ⊦ ∃ x0. x0 + z = x ∧ x0 ⊒ y

Rule argument

Additional information

Used simplifier rules: blapp: ⊦ x ≠ [] → (x.butlast = y ↔ x = y + x.last '); lapp: ⊦ y ≠ [] → (x + y).last = y.last; lin-01: ⊦ x.last ∈ x ↔ x ≠ []; postfix-app-02: ⊦ y + x ⊒ z + x ↔ y ⊒ z; bapp: ⊦ y ≠ [] → (x + y).butlast = x + y.butlast; butlast-last: x ≠ [] ⊦ x.butlast + x.last ' = x; in-15: ⊦ x + a ' = y → a ∈ y; (forward) from specification list ⊦ a ∈ x + y ↔ a ∈ x ∨ a ∈ y; (s) ⊦ x + y = z + y ↔ x = z; (s) a: ⊦ (x + y) + z = x + y + z; from specification list Used terms: x.butlast, y, z.butlast

Proof step 14 from proof postfix-split-stronger (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: lb: ⊦ x ≠ [] → # x.butlast = # x - 1; c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ¬ n < n; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss)