Proof step 1 from proof put-put-get-ls (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ar[n0, a][n1, b][n1] ≠ b, n1 < n0, n0 < # ar ⊦

Rule argument

Additional information

Proof step 2 from proof put-put-get-ls (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

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