Proof step 1 from proof next-perm (conclusion) (back to tree)

User applied rule call right

And obtained the following new goals

• Proof step 2:

  ar = ar0 ⊦ ⟨let ghostar = ar in if # ar = 0 then hasNext := false else let i = (# ar)-1 in {while i > 0 ∧ ar[i -1] ≥ ar[i] do {/* next-perm: invariant i < # ar wfbound i */; i := i -1}; if i ≤ 0 then hasNext := false else {let j = (# ar)-1 in {while ar[j] ≤ ar[i -1] do {/* next-perm: invariant j < # ar ∧ i ≤ j ∧ i ≠ 0 wfbound j */; j := j -1}; let temp = ar[i -1] in {ar[i -1] := ar[j]; ar[j] := temp; let ghost_j = j in {j := (# ar)-1; while i < j do {/* next-perm: invariant perm(ar`, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar wfbound j */; temp := ar[i]; ar[i] := ar[j]; ar[j] := temp; i := i +1; j := j -1}}}}; hasNext := true}}⟩ perm(ar, ar0)

Rule argument

Additional information

Used simplifier rules: next: ⊦ ;

Proof step 2 from proof next-perm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ar = ar0 ⊦ ⟨let ghostar = ar in if ar = [] then hasNext := false else let i = (# ar)-1 in {while i ≠ 0 ∧ ar[i -1] ≥ ar[i] do {/* next-perm: invariant i < # ar wfbound i */; i := i -1}; if i = 0 then hasNext := false else {let j = (# ar)-1 in {while ar[j] ≤ ar[i -1] do {/* next-perm: invariant j < # ar ∧ i ≤ j ∧ i ≠ 0 wfbound j */; j := j -1}; let temp = ar[i -1] in {ar[i -1] := ar[j]; ar[j] := temp; let ghost_j = j in {j := (# ar)-1; while i < j do {/* next-perm: invariant perm(ar`, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar wfbound j */; temp := ar[i]; ar[i] := ar[j]; ar[j] := temp; i := i + 1; j := j -1}}}}; hasNext := true}}⟩ perm(ar, ar0)

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s) ⊦ m ≤ 0 ↔ m = 0; (s) ⊦ m +1 = m + 1; (s) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ m > n ↔ n < m; (s)

Proof step 3 from proof next-perm (previous step) (back to tree)

User applied rule let right

And obtained the following new goals

• Proof step 4:

  ar = ar0, ghostar = ar ⊦ ⟨if ar = [] then hasNext := false else let i = (# ar)-1 in {while i ≠ 0 ∧ ar[i -1] ≥ ar[i] do {/* next-perm: invariant i < # ar wfbound i */; i := i -1}; if i = 0 then hasNext := false else {let j = (# ar)-1 in {while ar[j] ≤ ar[i -1] do {/* next-perm: invariant j < # ar ∧ i ≤ j ∧ i ≠ 0 wfbound j */; j := j -1}; let temp = ar[i -1] in {ar[i -1] := ar[j]; ar[j] := temp; let ghost_j = j in {j := (# ar)-1; while i < j do {/* next-perm: invariant perm(ar`, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar wfbound j */; temp := ar[i]; ar[i] := ar[j]; ar[j] := temp; i := i + 1; j := j -1}}}}; hasNext := true}}⟩ perm(ar, ar0)

Rule argument

Additional information

Proof step 4 from proof next-perm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ar = ar0 ⊦ ⟨if ar0 = [] then hasNext := false else let i = (# ar)-1 in {while i ≠ 0 ∧ ar[i -1] ≥ ar[i] do {/* next-perm: invariant i < # ar wfbound i */; i := i -1}; if i = 0 then hasNext := false else {let j = (# ar)-1 in {while ar[j] ≤ ar[i -1] do {/* next-perm: invariant j < # ar ∧ i ≤ j ∧ i ≠ 0 wfbound j */; j := j -1}; let temp = ar[i -1] in {ar[i -1] := ar[j]; ar[j] := temp; let ghost_j = j in {j := (# ar)-1; while i < j do {/* next-perm: invariant perm(ar`, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar wfbound j */; temp := ar[i]; ar[i] := ar[j]; ar[j] := temp; i := i + 1; j := j -1}}}}; hasNext := true}}⟩ perm(ar, ar0)

Rule argument

Additional information

Proof step 5 from proof next-perm (previous step) (back to tree)

User applied rule if right

And obtained the following new goals

• Proof step 6:

  ar = ar0, ar0 = [] ⊦ ⟨hasNext := false⟩ perm(ar, ar0)

• Proof step 7:

  ar = ar0, ar0 ≠ [] ⊦ ⟨let i = (# ar)-1 in {while i ≠ 0 ∧ ar[i -1] ≥ ar[i] do {/* next-perm: invariant i < # ar wfbound i */; i := i -1}; if i = 0 then hasNext := false else {let j = (# ar)-1 in {while ar[j] ≤ ar[i -1] do {/* next-perm: invariant j < # ar ∧ i ≤ j ∧ i ≠ 0 wfbound j */; j := j -1}; let temp = ar[i -1] in {ar[i -1] := ar[j]; ar[j] := temp; let ghost_j = j in {j := (# ar)-1; while i < j do {/* next-perm: invariant perm(ar`, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar wfbound j */; temp := ar[i]; ar[i] := ar[j]; ar[j] := temp; i := i + 1; j := j -1}}}}; hasNext := true}}⟩ perm(ar, ar0)

Rule argument

Additional information

Proof step 6 from proof next-perm (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ perm([], []); (s)

Proof step 7 from proof next-perm (previous step) (back to tree)

Heuristic symbolic execution applied rule let right

And obtained the following new goals

• Proof step 8:

  ar = ar0, i = (# ar)-1, # ar ≠ 0, ar0 ≠ [] ⊦ ⟨while i ≠ 0 ∧ ar[i -1] ≥ ar[i] do {/* next-perm: invariant i < # ar wfbound i */; i := i -1}; if i = 0 then hasNext := false else {let j = (# ar)-1 in {while ar[j] ≤ ar[i -1] do {/* next-perm: invariant j < # ar ∧ i ≤ j ∧ i ≠ 0 wfbound j */; j := j -1}; let temp = ar[i -1] in {ar[i -1] := ar[j]; ar[j] := temp; let ghost_j = j in {j := (# ar)-1; while i < j do {/* next-perm: invariant perm(ar`, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar wfbound j */; temp := ar[i]; ar[i] := ar[j]; ar[j] := temp; i := i + 1; j := j -1}}}}; hasNext := true}⟩ perm(ar, ar0)

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s)

Proof step 8 from proof next-perm (previous step) (back to tree)

Heuristic annotation applied rule annotation right

And obtained the following new goals

• Proof step 9:

  ar = ar0, i = i0, i1 = (# ar)-1, # ar ≠ 0, ar0 ≠ [], i ≠ 0, i < # ar, ar[i -1] ≥ ar[i], i ≠ 0 → (i -1 < # ar ∧ i ≠ 0) ∧ i < # ar ⊦ ⟨i := i -1⟩ (i < # ar ∧ i < i0)

• Proof step 10:

  ar = ar0, i1 = (# ar)-1, # ar ≠ 0, ar0 ≠ [], i < # ar, i ≠ 0 → (i -1 < # ar ∧ i ≠ 0) ∧ i < # ar ⊦ ⟨if i = 0 then hasNext := false else {let j = (# ar)-1 in {while ar[j] ≤ ar[i -1] do {/* next-perm: invariant j < # ar ∧ i ≤ j ∧ i ≠ 0 wfbound j */; j := j -1}; let temp = ar[i -1] in {ar[i -1] := ar[j]; ar[j] := temp; let ghost_j = j in {j := (# ar)-1; while i < j do {/* next-perm: invariant perm(ar`, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar wfbound j */; temp := ar[i]; ar[i] := ar[j]; ar[j] := temp; i := i + 1; j := j -1}}}}; hasNext := true}⟩ perm(ar, ar0), i ≠ 0 ∧ ar[i -1] ≥ ar[i]

Rule argument

Additional information

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

Proof step 9 from proof next-perm (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And closed the goal!

Rule argument

Additional information

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

Proof step 10 from proof next-perm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  ar = ar0, ar0 ≠ [], i < # ar0 ⊦ ⟨if i = 0 then hasNext := false else {let j = (# ar)-1 in {while ar[j] ≤ ar[i -1] do {/* next-perm: invariant j < # ar ∧ i ≤ j ∧ i ≠ 0 wfbound j */; j := j -1}; let temp = ar[i -1] in {ar[i -1] := ar[j]; ar[j] := temp; let ghost_j = j in {j := (# ar)-1; while i < j do {/* next-perm: invariant perm(ar`, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar wfbound j */; temp := ar[i]; ar[i] := ar[j]; ar[j] := temp; i := i + 1; j := j -1}}}}; hasNext := true}⟩ perm(ar, ar0), i ≠ 0 ∧ ar0[i] ≤ ar0[i - 1]

Rule argument

Additional information

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

Proof step 11 from proof next-perm (previous step) (back to tree)

Heuristic conditional right split applied rule if right

And obtained the following new goals

• Proof step 12:

  ar = ar0, i = 0, ar0 ≠ [], i < # ar0 ⊦ ⟨hasNext := false⟩ perm(ar, ar0), i ≠ 0 ∧ ar0[i] ≤ ar0[i - 1]

• Proof step 13:

  ar = ar0, ar0 ≠ [], i ≠ 0, i < # ar0 ⊦ ⟨let j = (# ar)-1 in {while ar[j] ≤ ar[i -1] do {/* next-perm: invariant j < # ar ∧ i ≤ j ∧ i ≠ 0 wfbound j */; j := j -1}; let temp = ar[i -1] in {ar[i -1] := ar[j]; ar[j] := temp; let ghost_j = j in {j := (# ar)-1; while i < j do {/* next-perm: invariant perm(ar`, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar wfbound j */; temp := ar[i]; ar[i] := ar[j]; ar[j] := temp; i := i + 1; j := j -1}}}}; hasNext := true⟩ perm(ar, ar0), i ≠ 0 ∧ ar0[i] ≤ ar0[i - 1]

Rule argument

Additional information

Proof step 12 from proof next-perm (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ perm(x, x); (s)

Proof step 13 from proof next-perm (previous step) (back to tree)

Heuristic symbolic execution applied rule let right

And obtained the following new goals

• Proof step 14:

  ar = ar0, j = (# ar)-1, # ar ≠ 0, ar0 ≠ [], i ≠ 0, i < # ar0 ⊦ ⟨while ar[j] ≤ ar[i -1] do {/* next-perm: invariant j < # ar ∧ i ≤ j ∧ i ≠ 0 wfbound j */; j := j -1}; let temp = ar[i -1] in {ar[i -1] := ar[j]; ar[j] := temp; let ghost_j = j in {j := (# ar)-1; while i < j do {/* next-perm: invariant perm(ar`, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar wfbound j */; temp := ar[i]; ar[i] := ar[j]; ar[j] := temp; i := i + 1; j := j -1}}}; hasNext := true⟩ perm(ar, ar0), i ≠ 0 ∧ ar0[i] ≤ ar0[i - 1]

Rule argument

Additional information

Used simplifier rules: ⊦ # x = 0 ↔ x = []; (s)

Proof step 14 from proof next-perm (previous step) (back to tree)

Heuristic annotation applied rule annotation right

And obtained the following new goals

• Proof step 15:

  ar = ar0, j = j0, j1 = (# ar)-1, # ar ≠ 0, ar0 ≠ [], i ≠ 0, i < # ar0, j < # ar, i -1 < # ar, i ≤ j, ar[j] ≤ ar[i -1] ⊦ ⟨j := j -1⟩ ((j < # ar ∧ i ≤ j ∧ i ≠ 0) ∧ j < j0), i ≠ 0 ∧ ar0[i] ≤ ar0[i - 1]

• Proof step 16:

  ar = ar0, j1 = (# ar)-1, # ar ≠ 0, ar0 ≠ [], i ≠ 0, i < # ar0, j < # ar, i -1 < # ar, i ≤ j, ¬ ar[j] ≤ ar[i -1] ⊦ ⟨let temp = ar[i -1] in {ar[i -1] := ar[j]; ar[j] := temp; let ghost_j = j in {j := (# ar)-1; while i < j do {/* next-perm: invariant perm(ar`, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar wfbound j */; temp := ar[i]; ar[i] := ar[j]; ar[j] := temp; i := i + 1; j := j -1}}}; hasNext := true⟩ perm(ar, ar0), i ≠ 0 ∧ ar0[i] ≤ ar0[i - 1]

Rule argument

Additional information

Used simplifier rules: ⊦ n -1 = n - 1; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < 1 ↔ m = 0; (s) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat 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 fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n → n ≠ 0; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ m < n → ¬ n < m; (s) ⊦ ¬ a < a; (s) n0 ≤ n ⊦ m ≤ n - n0 ↔ m + n0 ≤ n; (s) ⊦ m + 1 ≤ n ↔ m < n; (s) Used formulas: j < # ar ∧ i ≤ j ∧ i ≠ 0, j = j

Proof step 15 from proof next-perm (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And closed the goal!

Rule argument

Additional information

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

Proof step 16 from proof next-perm (previous step) (back to tree)

Heuristic symbolic execution applied rule let right

And obtained the following new goals

• Proof step 17:

  ar = ar0, j1 = (# ar)-1, temp = ar[i -1], # ar ≠ 0, ar0 ≠ [], i ≠ 0, i -1 < # ar, j < # ar, i < # ar0, i ≤ j, ¬ ar[j] ≤ ar[i -1] ⊦ ⟨ar[i -1] := ar[j]; ar[j] := temp; let ghost_j = j in {j := (# ar)-1; while i < j do {/* next-perm: invariant perm(ar`, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar wfbound j */; temp := ar[i]; ar[i] := ar[j]; ar[j] := temp; i := i + 1; j := j -1}}; hasNext := true⟩ perm(ar, ar0), i ≠ 0 ∧ ar0[i] ≤ ar0[i - 1]

Rule argument

Additional information

Proof step 17 from proof next-perm (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 18:

  ar = ar1[i -1, ar1[j]], ar1 = ar0, j1 = (# ar1)-1, temp = ar1[i -1], # ar1 ≠ 0, ar0 ≠ [], i ≠ 0, i < # ar0, i -1 < # ar1, j < # ar1, i ≤ j, ¬ ar1[j] ≤ ar1[i -1] ⊦ ⟨ar[j] := temp; let ghost_j = j in {j := (# ar)-1; while i < j do {/* next-perm: invariant perm(ar`, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar wfbound j */; temp := ar[i]; ar[i] := ar[j]; ar[j] := temp; i := i + 1; j := j -1}}; hasNext := true⟩ perm(ar, ar0), i ≠ 0 ∧ ar0[i] ≤ ar0[i - 1]

Rule argument

Additional information

Proof step 18 from proof next-perm (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 19:

  ar = ar2[j, temp], ar1 = ar0, ar2 = ar1[i -1, ar1[j]], j1 = (# ar1)-1, temp = ar1[i -1], # ar1 ≠ 0, ar0 ≠ [], i ≠ 0, j < # ar1, i -1 < # ar1, i < # ar0, j < # ar2, i ≤ j, ¬ ar1[j] ≤ ar1[i -1] ⊦ ⟨let ghost_j = j in {j := (# ar)-1; while i < j do {/* next-perm: invariant perm(ar`, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar wfbound j */; temp := ar[i]; ar[i] := ar[j]; ar[j] := temp; i := i + 1; j := j -1}}; hasNext := true⟩ perm(ar, ar0), i ≠ 0 ∧ ar0[i] ≤ ar0[i - 1]

Rule argument

Additional information

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

Proof step 19 from proof next-perm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  ar = ar0[i - 1, ar0[j]][j, ar0[i - 1]], ar0 ≠ [], i ≠ 0, ar0[i - 1] < ar0[i], ar0[i - 1] < ar0[j], j < # ar0, i < # ar0, i ≤ j ⊦ ⟨let ghost_j = j in {j := (# ar)-1; while i < j do {/* next-perm: invariant perm(ar`, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar wfbound j */; temp := ar[i]; ar[i] := ar[j]; ar[j] := temp; i := i + 1; j := j -1}}; hasNext := true⟩ perm(ar, ar0)

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ n -1 = n - 1; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ a < b → (b < a ↔ false); (ss) ⊦ m < n + 1 ↔ ¬ n < m; (s) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ # ar[n, a] = # ar; (s) ⊦ # x = 0 ↔ x = []; (s)

Proof step 20 from proof next-perm (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 21:

  ar = ar0[m, ar0[j]][j, ar0[m]], i = m + 1, ar0 ≠ [], i ≠ 0, i < # ar0, j < # ar0, ar0[m] < ar0[j], ar0[m] < ar0[i], i ≤ j ⊦ ⟨let ghost_j = j in {j := (# ar)-1; while i < j do {/* next-perm: invariant perm(ar`, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar wfbound j */; temp := ar[i]; ar[i] := ar[j]; ar[j] := temp; i := i + 1; j := j -1}}; hasNext := true⟩ perm(ar, ar0)

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: i, m

Proof step 21 from proof next-perm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  ar = ar0[m, ar0[j]][j, ar0[m]], i = m + 1, ar0 ≠ [], ar0[m] < ar0[m + 1], ar0[m] < ar0[j], j < # ar0, m + 1 < # ar0, m < j, m < # ar0 ⊦ ⟨let ghost_j = j in {j := (# ar)-1; while i < j do {/* next-perm: invariant perm(ar`, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar wfbound j */; temp := ar[i]; ar[i] := ar[j]; ar[j] := temp; i := i + 1; j := j -1}}; hasNext := true⟩ perm(ar, ar0)

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) eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat ⊦ m +1 = m + 1; (s) ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification oelem[natarray] ⊦ m + 1 ≠ 0; (s)

Proof step 22 from proof next-perm (previous step) (back to tree)

Heuristic symbolic execution applied rule let right

And obtained the following new goals

• Proof step 23:

  ar = ar0[m, ar0[j]][j, ar0[m]], ghost_j = j, i = m + 1, ar0 ≠ [], m < # ar0, m < j, m + 1 < # ar0, j < # ar0, ar0[m] < ar0[j], ar0[m] < ar0[m + 1] ⊦ ⟨j := (# ar)-1; while i < j do {/* next-perm: invariant perm(ar`, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar wfbound j */; temp := ar[i]; ar[i] := ar[j]; ar[j] := temp; i := i + 1; j := j -1}; hasNext := true⟩ perm(ar, ar0)

Rule argument

Additional information

Proof step 23 from proof next-perm (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 24:

  ar = ar0[m, ar0[j0]][j0, ar0[m]], ghost_j = j0, i = m + 1, j = (# ar)-1, # ar ≠ 0, ar0 ≠ [], ar0[m] < ar0[m + 1], ar0[m] < ar0[j0], j0 < # ar0, m + 1 < # ar0, m < j0, m < # ar0 ⊦ ⟨while i < j do {/* next-perm: invariant perm(ar`, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar wfbound j */; temp := ar[i]; ar[i] := ar[j]; ar[j] := temp; i := i + 1; j := j -1}; hasNext := true⟩ perm(ar, ar0)

Rule argument

Additional information

Used simplifier rules: ⊦ # ar[n, a] = # ar; (s) ⊦ n < # x → # x[n, a] = # x; (s) ⊦ # x = 0 ↔ x = []; (s)

Proof step 24 from proof next-perm (previous step) (back to tree)

Heuristic annotation applied rule annotation right

And obtained the following new goals

• Proof step 25:

  ar = ar0[m, ar0[j0]][j0, ar0[m]], ghost_j = j0, i = m + 1, j = (# ar)-1, # ar ≠ 0, ar0 ≠ [], m < # ar0, m < j0, m + 1 < # ar0, j0 < # ar0, ar0[m] < ar0[j0], ar0[m] < ar0[m + 1] ⊦ perm(ar, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar

• Proof step 28:

  ar1 = ar0[m, ar0[j0]][j0, ar0[m]], ghost_j = j0, i0 = m + 1, j = j1, j2 = (# ar1)-1, # ar1 ≠ 0, ar0 ≠ [], i ≠ 0, m < # ar0, m < j0, m + 1 < # ar0, j0 < # ar0, ar0[m] < ar0[j0], ar0[m] < ar0[m + 1], i < # ar, j < # ar, i < j, perm(ar1, ar) ⊦ ⟨temp := ar[i]; ar[i] := ar[j]; ar[j] := temp; i := i + 1; j := j -1⟩ ((perm(ar1, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar) ∧ j < j1)

• Proof step 36:

  ar1 = ar0[m, ar0[j0]][j0, ar0[m]], ghost_j = j0, i0 = m + 1, j2 = (# ar1)-1, # ar1 ≠ 0, ar0 ≠ [], i ≠ 0, m < # ar0, m < j0, m + 1 < # ar0, j0 < # ar0, ar0[m] < ar0[j0], ar0[m] < ar0[m + 1], i < # ar, j < # ar, perm(ar1, ar), ¬ i < j ⊦ ⟨hasNext := true⟩ perm(ar, ar0)

Rule argument

Additional information

Used formulas: perm(ar`, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar, j = j

Proof step 25 from proof next-perm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  ar0 ≠ [], m < # ar0, m < j0, m + 1 < # ar0, j0 < # ar0, ar0[m] < ar0[j0], ar0[m] < ar0[m + 1], ¬ perm(ar0, ar0[m, ar0[j0]][j0, ar0[m]]) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ¬ a < a; (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) ⊦ n < # x → # x[n, a] = # x; (s) ⊦ # ar[n, a] = # ar; (s) ⊦ n -1 = n - 1; (s) ⊦ m + 1 ≠ 0; (s) m < # x, n < # x ⊦ perm(x[n, x[m]][m, x[n]], y) ↔ perm(x, y); (s)

Proof step 26 from proof next-perm (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

  ⊦ m < # y ∧ n < # y ∧ a = y[n] ∧ b = y[m] → (perm(x, y[m, a][n, b]) ↔ perm(x, y))

Rule argument

Additional information

Used simplifier rules: ⊦ perm(x, x); (s) Used terms: ar0, j0, m, ar0, ar0[j0], ar0[m]

Proof step 27 from proof next-perm (previous step) (back to tree)

A spec-lemma

Proof step 28 from proof next-perm (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 29:

  ar1 = ar0[m, ar0[j0]][j0, ar0[m]], ghost_j = j0, i0 = m + 1, j = j1, j2 = (# ar1)-1, temp = ar[i], # ar1 ≠ 0, ar0 ≠ [], i ≠ 0, i < j, j < # ar, ar0[m] < ar0[m + 1], ar0[m] < ar0[j0], j0 < # ar0, m + 1 < # ar0, m < j0, m < # ar0, i < # ar, perm(ar1, ar) ⊦ ⟨ar[i] := ar[j]; ar[j] := temp; i := i + 1; j := j -1⟩ ((perm(ar1, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar) ∧ j < j1)

Rule argument

Additional information

Proof step 29 from proof next-perm (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 30:

  ar = ar2[i, ar2[j]], ar1 = ar0[m, ar0[j0]][j0, ar0[m]], ghost_j = j0, i0 = m + 1, j = j1, j2 = (# ar1)-1, temp = ar2[i], # ar1 ≠ 0, ar0 ≠ [], i ≠ 0, m < # ar0, m < j0, m + 1 < # ar0, j0 < # ar0, ar0[m] < ar0[j0], ar0[m] < ar0[m + 1], i < j, i < # ar2, j < # ar2, perm(ar1, ar2) ⊦ ⟨ar[j] := temp; i := i + 1; j := j -1⟩ ((perm(ar1, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar) ∧ j < j1)

Rule argument

Additional information

Proof step 30 from proof next-perm (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 31:

  ar = ar3[j, temp], ar1 = ar0[m, ar0[j0]][j0, ar0[m]], ar3 = ar2[i, ar2[j]], ghost_j = j0, i0 = m + 1, j = j1, j2 = (# ar1)-1, temp = ar2[i], # ar1 ≠ 0, ar0 ≠ [], i ≠ 0, j < # ar2, i < # ar2, i < j, ar0[m] < ar0[m + 1], ar0[m] < ar0[j0], j0 < # ar0, m + 1 < # ar0, m < j0, m < # ar0, j < # ar3, perm(ar1, ar2) ⊦ ⟨i := i + 1; j := j -1⟩ ((perm(ar1, ar) ∧ i ≠ 0 ∧ i < # ar ∧ j < # ar) ∧ j < j1)

Rule argument

Additional information

Used simplifier rules: ⊦ # ar[n, a] = # ar; (s) ⊦ # x = 0 ↔ x = []; (s) m < # x, n < # x ⊦ perm(x[n, x[m]][m, x[n]], y) ↔ perm(x, y); (s) ⊦ n < # x → # x[n, a] = # x; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s)

Proof step 31 from proof next-perm (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 32:

  ar = ar3[j, temp], ar1 = ar0[m, ar0[j0]][j0, ar0[m]], ar3 = ar2[i, ar2[j]], ghost_j = j0, i0 = m + 1, j = j1, j2 = (# ar1)-1, temp = ar2[i], # ar1 ≠ 0, ar0 ≠ [], i ≠ 0, j < # ar3, m < # ar0, m < j0, m + 1 < # ar0, j0 < # ar0, ar0[m] < ar0[j0], ar0[m] < ar0[m + 1], i < j, i < # ar2, j < # ar2, perm(ar1, ar2) ⊦ ⟨j := j -1⟩ ((perm(ar1, ar) ∧ i + 1 ≠ 0 ∧ i + 1 < # ar ∧ j < # ar) ∧ j < j1)

Rule argument

Additional information

Proof step 32 from proof next-perm (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 33:

  ar = ar3[j, temp], ar1 = ar0[m, ar0[j0]][j0, ar0[m]], ar3 = ar2[i, ar2[j]], ghost_j = j0, i0 = m + 1, j = j1, j2 = (# ar1)-1, temp = ar2[i], # ar1 ≠ 0, ar0 ≠ [], i ≠ 0, j ≠ 0, j < # ar2, i < # ar2, i < j, ar0[m] < ar0[m + 1], ar0[m] < ar0[j0], j0 < # ar0, m + 1 < # ar0, m < j0, m < # ar0, j < # ar3, perm(ar1, ar2) ⊦ (perm(ar1, ar) ∧ i + 1 ≠ 0 ∧ i + 1 < # ar ∧ j -1 < # ar) ∧ j -1 < j1

Rule argument

Additional information

Used simplifier rules: ⊦ # ar[n, a] = # ar; (s) m < # x, n < # x ⊦ perm(x[n, x[m]][m, x[n]], y) ↔ perm(x, y); (s) ⊦ n < # x → # x[n, a] = # x; (s) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ # x = 0 ↔ x = []; (s) ⊦ x ≠ [] → x[0] = x.first; (s) ⊦ ¬ n < 0; (s)

Proof step 33 from proof next-perm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  ar0 ≠ [], ar2 ≠ [], i ≠ 0, j1 < # ar2, i < j1, ar0[m] < ar0[m + 1], ar0[m] < ar0[j0], j0 < # ar0, m + 1 < # ar0, m < j0, m < # ar0, i < # ar2, i + 1 < # ar2, perm(ar0, ar2), ¬ perm(ar0, ar2[i, ar2[j1]][j1, ar2[i]]) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s) ⊦ m < n → n ≠ 0; (s) ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic transitivity: ⊦ a < b ∧ b < c → a < c; (forward) from specification oelem[natarray] c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ¬ a < a; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ n -1 = n - 1; (s) ⊦ m < n → ¬ n < m; (s) ⊦ n < # x → # x[n, a] = # x; (s) ⊦ # ar[n, a] = # ar; (s) ⊦ m + 1 ≠ 0; (s) m < # x, n < # x ⊦ perm(x[n, x[m]][m, x[n]], y) ↔ perm(x, y); (s)

Proof step 34 from proof next-perm (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

  ⊦ m < # y ∧ n < # y ∧ a = y[n] ∧ b = y[m] → (perm(x, y[m, a][n, b]) ↔ perm(x, y))

Rule argument

Additional information

Used terms: ar2, j1, i, ar0, ar2[j1], ar2[i]

Proof step 35 from proof next-perm (previous step) (back to tree)

A spec-lemma

Proof step 36 from proof next-perm (previous step) (back to tree)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 37:

  ar1 = ar0[m, ar0[j0]][j0, ar0[m]], ghost_j = j0, i0 = m + 1, j2 = (# ar1)-1, # ar1 ≠ 0, ar0 ≠ [], i ≠ 0, j < # ar, i < # ar, ar0[m] < ar0[m + 1], ar0[m] < ar0[j0], j0 < # ar0, m + 1 < # ar0, m < j0, m < # ar0, perm(ar1, ar), ¬ i < j, ¬ perm(ar, ar0) ⊦

Rule argument

Additional information

Proof step 37 from proof next-perm (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 38:

  ar ≠ [], ar0 ≠ [], i ≠ 0, j < # ar, i < # ar, ar0[m] < ar0[m + 1], ar0[m] < ar0[j0], j0 < # ar0, m + 1 < # ar0, m < j0, m < # ar0, perm(ar0, ar), j ≤ i, ¬ perm(ar, ar0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) ⊦ # x = 0 ↔ x = []; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss) m < # x, n < # x ⊦ perm(x[n, x[m]][m, x[n]], y) ↔ perm(x, y); (s) ⊦ n < # x → # x[n, a] = # x; (s) ⊦ # ar[n, a] = # ar; (s)

Proof step 38 from proof next-perm (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 39:

  ⊦ perm(x, y) ↔ perm(y, x)

Rule argument

Additional information

Used terms: ar, ar0

Proof step 39 from proof next-perm (previous step) (back to tree)

A spec-lemma