Proof step 1 from proof eqpos (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(pos(char1, str) = pos(char2, str) ↔ char1 = char2), pos(char1, str) < # str ⊦

Rule argument

Additional information

Proof step 2 from proof eqpos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  pos(char1, str) = pos(char2, str), char1 ≠ char2, str ≠ "", pos(char2, str) < # str ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = ""; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 3 from proof eqpos (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  pos(char1, char + str0) = pos(char2, char + str0), char + str0 ≠ "", char1 ≠ char2, pos(char2, char + str0) < #(char + str0), ∀ char1, char2. ¬(pos(char1, str0) = pos(char2, str0) ∧ char1 ≠ char2 ∧ str0 ≠ "" ∧ pos(char2, str0) < # str0) ⊦

Rule argument

Additional information

Used simplifier rules: string freely generated by "", +;;

Proof step 4 from proof eqpos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  pos(char1, char ' + str0) = pos(char2, char ' + str0), char1 ≠ char2, pos(char2, char ' + str0) ≤ # str0, ∀ char0, char3. pos(char0, str0) ≠ pos(char3, str0) ∨ char0 = char3 ∨ str0 = "" ∨ ¬ pos(char3, str0) < # str0 ⊦

Rule argument

Additional information

Used simplifier rules: len-app: ⊦ #(str + str0) = # str + # str0; length-one: ⊦ # char ' = 1; ⊦ m < n ↔ ¬ n ≤ m; (ss) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m < n + 1 ↔ ¬ n < m; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[string] ⊦ a + x = a ' + x; (s) ⊦ a ' + x ≠ ""; (s)

Proof step 5 from proof eqpos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ a ≠ b → pos(a, b ' + x) = pos(a, x) + 1

• Proof step 7:

  pos(char1, str0) + 1 = pos(char2, char ' + str0), char1 ≠ char, char1 ≠ char2, pos(char2, char ' + str0) ≤ # str0, ∀ char0, char3. pos(char0, str0) ≠ pos(char3, str0) ∨ char0 = char3 ∨ str0 = "" ∨ ¬ pos(char3, str0) < # str0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ pos(a, a ' + x) = 0; (s) ⊦ a ≠ b → pos(a, b ' + x) = pos(a, x) + 1; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[string] ⊦ m + 1 ≠ 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: str0, char, char1

Proof step 6 from proof eqpos (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof eqpos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  pos(char1, str0) + 1 = pos(char2, char ' + str0), char1 ≠ char2, char1 ≠ char, str0 ≠ "", pos(char1, str0) < # str0, ∀ char0, char3. pos(char0, str0) ≠ pos(char3, str0) ∨ char0 = char3 ∨ ¬ pos(char3, str0) < # str0 ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ # x = 0 ↔ x = ""; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat

Proof step 8 from proof eqpos (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ a ≠ b → pos(a, b ' + x) = pos(a, x) + 1

• Proof step 10:

  pos(char1, str0) + 1 = pos(char2, str0) + 1, char1 ≠ char2, char1 ≠ char, char2 ≠ char, str0 ≠ "", pos(char1, str0) < # str0, ∀ char0, char3. pos(char0, str0) ≠ pos(char3, str0) ∨ char0 = char3 ∨ ¬ pos(char3, str0) < # str0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ pos(a, a ' + x) = 0; (s) a: ⊦ (x + y) + z = x + y + z; from specification list[string] ⊦ m + 1 ≠ 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: str0, char, char2

Proof step 9 from proof eqpos (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof eqpos (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  pos(char1, str0) = pos(char2, str0), char1 ≠ char2, char1 ≠ char, char2 ≠ char, str0 ≠ "", pos(char2, str0) < # str0, ∀ char0, char3. pos(char0, str0) ≠ pos(char3, str0) ∨ char0 = char3 ∨ ¬ pos(char3, str0) < # str0 ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n = m + n0 ↔ n = n0; (s)

Proof step 11 from proof eqpos (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: char1, char2