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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ar0 ≤ ar1, ar1 ≤ ar2, ¬ ar0 ≤ ar2 ⊦

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  ar1 ≤ ar2, i + ar ≤ ar1, ¬ i + ar ≤ ar2, ∀ ar1, ar2. ¬(ar ≤ ar1 ∧ ar1 ≤ ar2 ∧ ¬ ar ≤ ar2) ⊦

Rule argument

Additional information

Used simplifier rules: lexicographic-base2: ⊦ [] ≤ ar2; array freely generated by [], +;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  ar1 ≤ ar2, i ' + ar ≤ ar1, ¬ i ' + ar ≤ ar2, ∀ ar0, ar3. ¬ ar ≤ ar0 ∨ ¬ ar0 ≤ ar3 ∨ ar ≤ ar3 ⊦

Rule argument

Additional information

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

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 5:

  ar1 = i0 + ar4, i ' + ar ≤ ar1, ar1 ≤ ar2, ¬ i ' + ar ≤ ar2, ∀ ar0, ar3. ¬ ar ≤ ar0 ∨ ¬ ar0 ≤ ar3 ∨ ar ≤ ar3 ⊦

Rule argument

Additional information

Used simplifier rules: lexicographic-base2: ⊦ [] ≤ ar2; lexicographic-base3: ⊦ ¬ ar1 ≤ []; array freely generated by [], +;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  i0 ' + ar4 ≤ ar2, ¬ i ' + ar ≤ ar2, (i = i0 ⊃ ar ≤ ar4;i < i0), ∀ ar0, ar3. ¬ ar ≤ ar0 ∨ ¬ ar0 ≤ ar3 ∨ ar ≤ ar3 ⊦

Rule argument

Additional information

Used simplifier rules: lexicographic-rec1: ⊦ n ' + ar1 ≤ m ' + ar2 ↔ (n = m ⊃ ar1 ≤ ar2;n ≤ m); a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] ⊦ m ≠ n → (m ≤ n ↔ m < n); (s) ⊦ a + x = a ' + x; (s)

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

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 7:

  i = i0, i0 ' + ar4 ≤ ar2, ar ≤ ar4, ¬ i ' + ar ≤ ar2, ∀ ar0, ar3. ¬ ar ≤ ar0 ∨ ¬ ar0 ≤ ar3 ∨ ar ≤ ar3 ⊦

• Proof step 13:

  i ≠ i0, i < i0, i0 ' + ar4 ≤ ar2, ¬ i ' + ar ≤ ar2, ∀ ar0, ar3. ¬ ar ≤ ar0 ∨ ¬ ar0 ≤ ar3 ∨ ar ≤ ar3 ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  ar ≤ ar4, i0 ' + ar4 ≤ ar2, ¬ i0 ' + ar ≤ ar2, ∀ ar0, ar3. ¬ ar ≤ ar0 ∨ ¬ ar0 ≤ ar3 ∨ ar ≤ ar3 ⊦

Rule argument

Additional information

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 9:

  ar2 = i + ar1, i0 ' + ar4 ≤ ar2, ar ≤ ar4, ¬ i0 ' + ar ≤ ar2, ∀ ar0, ar3. ¬ ar ≤ ar0 ∨ ¬ ar0 ≤ ar3 ∨ ar ≤ ar3 ⊦

Rule argument

Additional information

Used simplifier rules: lexicographic-base3: ⊦ ¬ ar1 ≤ []; array freely generated by [], +;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  ar ≤ ar4, (i0 = i ⊃ ar4 ≤ ar1;i0 < i), ∀ ar0, ar3. ¬ ar ≤ ar0 ∨ ¬ ar0 ≤ ar3 ∨ ar ≤ ar3 ⊦ (i0 = i ⊃ ar ≤ ar1;i0 < i)

Rule argument

Additional information

Used simplifier rules: lexicographic-rec1: ⊦ n ' + ar1 ≤ m ' + ar2 ↔ (n = m ⊃ ar1 ≤ ar2;n ≤ m); a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] ⊦ m ≠ n → (m ≤ n ↔ m < n); (s) ⊦ a + x = a ' + x; (s)

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

Heuristic nonsplitting cut applied rule cut formula

And obtained the following new goals

• Proof step 11:

  i0 = i, ar ≤ ar4, (i0 = i ⊃ ar4 ≤ ar1;i0 < i), ∀ ar0, ar3. ¬ ar ≤ ar0 ∨ ¬ ar0 ≤ ar3 ∨ ar ≤ ar3 ⊦ (i0 = i ⊃ ar ≤ ar1;i0 < i)

Rule argument

Additional information

Used formulas: i0 = i

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  ar ≤ ar4, ar4 ≤ ar1, ¬ ar ≤ ar1, ∀ ar0, ar3. ¬ ar ≤ ar0 ∨ ¬ ar0 ≤ ar3 ∨ ar ≤ ar3 ⊦

Rule argument

Additional information

Proof step 12 from proof array-le-trans (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: ar4, ar1

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

User applied rule constructor cut

And obtained the following new goals

• Proof step 14:

  ar2 = i1 + ar1, i ≠ i0, i < i0, i0 ' + ar4 ≤ ar2, ¬ i ' + ar ≤ ar2, ∀ ar0, ar3. ¬ ar ≤ ar0 ∨ ¬ ar0 ≤ ar3 ∨ ar ≤ ar3 ⊦

Rule argument

Additional information

Used simplifier rules: lexicographic-base3: ⊦ ¬ ar1 ≤ []; array freely generated by [], +;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  i ≠ i0, i < i0, (i0 = i1 ⊃ ar4 ≤ ar1;i0 < i1), ∀ ar0, ar3. ¬ ar ≤ ar0 ∨ ¬ ar0 ≤ ar3 ∨ ar ≤ ar3 ⊦ (i = i1 ⊃ ar ≤ ar1;i < i1)

Rule argument

Additional information

Used simplifier rules: lexicographic-rec1: ⊦ n ' + ar1 ≤ m ' + ar2 ↔ (n = m ⊃ ar1 ≤ ar2;n ≤ m); ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic a: ⊦ (x + y) + z = x + y + z; from specification list[natarray-oarray-sort] ⊦ m ≠ n → (m ≤ n ↔ m < n); (s) ⊦ a + x = a ' + x; (s)

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

Heuristic nonsplitting cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification oelem[natarray] lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic ⊦ m < n → n ≠ 0; (s) ⊦ m +1 = m + 1; (s) lel: ⊦ a < b ∧ a = c → c < b; (forward) from specification oelem[natarray] lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m + m0 < n → ¬ n + n0 < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used formulas: i0 = i1