Proof step 1 from proof htok-add (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ar[n] = ⊥, e ≠ ⊥, allslotsfull(ar, get_hash(e, # ar), n, e, false), htok(ar), ¬ htok(ar[n := e]) ⊦

Rule argument

Additional information

Proof step 2 from proof htok-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ar[n] = ⊥, (ar[n := e])[n0] ≠ ⊥, e ≠ ⊥, n0 < # ar, m < # ar, (n0 < get_hash((ar[n := e])[n0], # ar) ⊃ m < n0 ∨ get_hash((ar[n := e])[n0], # ar) ≤ m ;get_hash((ar[n := e])[n0], # ar) ≤ m ∧ m < n0 ), ∀ m. (n < get_hash(e, # ar) ⊃ m < n ∨ get_hash(e, # ar) ≤ m;get_hash(e, # ar) ≤ m ∧ m < n) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥, ∀ n0. n0 < # ar ∧ ar[n0] ≠ ⊥ → (∀ m. (n0 < get_hash(ar[n0], # ar) ⊃ m < n0 ∨ get_hash(ar[n0], # ar) ≤ m;get_hash(ar[n0], # ar) ≤ m ∧ m < n0) ∧ m < # ar → ar[m] ≠ ar[n0] ∧ ar[m] ≠ ⊥) ⊦ (ar[n := e])[m] ≠ (ar[n := e])[n0] ∧ (ar[n := e])[m] ≠ ⊥

Rule argument

Additional information

Used simplifier rules: htok-def: ⊦ htok(ar) ↔ (∀ n. n < # ar ∧ ar[n] ≠ ⊥ → allslotsfull(ar, get_hash(ar[n], # ar), n, ar[n], false)); allslotsfull-def: ⊦ allslotsfull(ar, n0, n, e, b) ↔ (∀ m. between(n0, m, n, b) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥); between-def: ⊦ between(n0, m, n, b) ↔ n0 = n ∧ b ∨ (n < n0 ⊃ m < n ∨ n0 ≤ m;n0 ≤ m ∧ m < n); ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ # ar[n := a] = # ar; (s)

Proof step 3 from proof htok-add (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 4:

  ar[n] = ⊥, (ar[n := e])[n0] ≠ ⊥, e ≠ ⊥, m < # ar, n0 < # ar, n0 < # ar ∧ ar[n0] ≠ ⊥ → (∀ m. (n0 < get_hash(ar[n0], # ar) ⊃ m < n0 ∨ get_hash(ar[n0], # ar) ≤ m;get_hash(ar[n0], # ar) ≤ m ∧ m < n0) ∧ m < # ar → ar[m] ≠ ar[n0] ∧ ar[m] ≠ ⊥), (n0 < get_hash((ar[n := e])[n0], # ar) ⊃ m < n0 ∨ get_hash((ar[n := e])[n0], # ar) ≤ m ;get_hash((ar[n := e])[n0], # ar) ≤ m ∧ m < n0 ), ∀ n0. n0 < # ar ∧ ar[n0] ≠ ⊥ → (∀ m. (n0 < get_hash(ar[n0], # ar) ⊃ m < n0 ∨ get_hash(ar[n0], # ar) ≤ m;get_hash(ar[n0], # ar) ≤ m ∧ m < n0) ∧ m < # ar → ar[m] ≠ ar[n0] ∧ ar[m] ≠ ⊥), ∀ m. (n < get_hash(e, # ar) ⊃ m < n ∨ get_hash(e, # ar) ≤ m;get_hash(e, # ar) ≤ m ∧ m < n) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ (ar[n := e])[m] ≠ (ar[n := e])[n0] ∧ (ar[n := e])[m] ≠ ⊥

Rule argument

Additional information

Used terms: n0

Proof step 4 from proof htok-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ar[n] = ⊥, (ar[n := e])[n0] ≠ ⊥, e ≠ ⊥, n0 < # ar, m < # ar, ar[n0] ≠ ⊥ → (∀ m. (n0 < get_hash(ar[n0], # ar) ⊃ m < n0 ∨ get_hash(ar[n0], # ar) ≤ m;get_hash(ar[n0], # ar) ≤ m ∧ m < n0) ∧ m < # ar → ar[m] ≠ ar[n0] ∧ ar[m] ≠ ⊥), (n0 < get_hash((ar[n := e])[n0], # ar) ⊃ m < n0 ∨ get_hash((ar[n := e])[n0], # ar) ≤ m ;get_hash((ar[n := e])[n0], # ar) ≤ m ∧ m < n0 ), ∀ m. (n < get_hash(e, # ar) ⊃ m < n ∨ get_hash(e, # ar) ≤ m;get_hash(e, # ar) ≤ m ∧ m < n) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥, ∀ n0. n0 < # ar ∧ ar[n0] ≠ ⊥ → (∀ m. (n0 < get_hash(ar[n0], # ar) ⊃ m < n0 ∨ get_hash(ar[n0], # ar) ≤ m;get_hash(ar[n0], # ar) ≤ m ∧ m < n0) ∧ m < # ar → ar[m] ≠ ar[n0] ∧ ar[m] ≠ ⊥) ⊦ (ar[n := e])[m] ≠ (ar[n := e])[n0] ∧ (ar[n := e])[m] ≠ ⊥

Rule argument

Additional information

Proof step 5 from proof htok-add (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 6:

  ar[n] = ⊥, (ar[n := e])[n0] ≠ ⊥, e ≠ ⊥, m < # ar, n0 < # ar, ar[n0] ≠ ⊥ → (∀ m. (n0 < get_hash(ar[n0], # ar) ⊃ m < n0 ∨ get_hash(ar[n0], # ar) ≤ m;get_hash(ar[n0], # ar) ≤ m ∧ m < n0) ∧ m < # ar → ar[m] ≠ ar[n0] ∧ ar[m] ≠ ⊥), (n < get_hash(e, # ar) ⊃ m < n ∨ get_hash(e, # ar) ≤ m;get_hash(e, # ar) ≤ m ∧ m < n) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥, (n0 < get_hash((ar[n := e])[n0], # ar) ⊃ m < n0 ∨ get_hash((ar[n := e])[n0], # ar) ≤ m ;get_hash((ar[n := e])[n0], # ar) ≤ m ∧ m < n0 ), ∀ n0. n0 < # ar ∧ ar[n0] ≠ ⊥ → (∀ m. (n0 < get_hash(ar[n0], # ar) ⊃ m < n0 ∨ get_hash(ar[n0], # ar) ≤ m;get_hash(ar[n0], # ar) ≤ m ∧ m < n0) ∧ m < # ar → ar[m] ≠ ar[n0] ∧ ar[m] ≠ ⊥), ∀ m. (n < get_hash(e, # ar) ⊃ m < n ∨ get_hash(e, # ar) ≤ m;get_hash(e, # ar) ≤ m ∧ m < n) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ (ar[n := e])[m] ≠ (ar[n := e])[n0] ∧ (ar[n := e])[m] ≠ ⊥

Rule argument

Additional information

Used terms: m

Proof step 6 from proof htok-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ar[n] = ⊥, (ar[n := e])[n0] ≠ ⊥, e ≠ ⊥, n0 < # ar, m < # ar, ar[n0] ≠ ⊥ → (∀ m. (n0 < get_hash(ar[n0], # ar) ⊃ m < n0 ∨ get_hash(ar[n0], # ar) ≤ m;get_hash(ar[n0], # ar) ≤ m ∧ m < n0) ∧ m < # ar → ar[m] ≠ ar[n0] ∧ ar[m] ≠ ⊥), (n < get_hash(e, # ar) ⊃ m < n ∨ get_hash(e, # ar) ≤ m;get_hash(e, # ar) ≤ m ∧ m < n) → ar[m] ≠ e ∧ ar[m] ≠ ⊥, (n0 < get_hash((ar[n := e])[n0], # ar) ⊃ m < n0 ∨ get_hash((ar[n := e])[n0], # ar) ≤ m ;get_hash((ar[n := e])[n0], # ar) ≤ m ∧ m < n0 ), ∀ m. (n < get_hash(e, # ar) ⊃ m < n ∨ get_hash(e, # ar) ≤ m;get_hash(e, # ar) ≤ m ∧ m < n) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥, ∀ n0. n0 < # ar ∧ ar[n0] ≠ ⊥ → (∀ m. (n0 < get_hash(ar[n0], # ar) ⊃ m < n0 ∨ get_hash(ar[n0], # ar) ≤ m;get_hash(ar[n0], # ar) ≤ m ∧ m < n0) ∧ m < # ar → ar[m] ≠ ar[n0] ∧ ar[m] ≠ ⊥) ⊦ (ar[n := e])[m] ≠ (ar[n := e])[n0] ∧ (ar[n := e])[m] ≠ ⊥

Rule argument

Additional information

Proof step 7 from proof htok-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ m ≠ n → (ar[n := a])[m] = ar[m]

• Proof step 9:

  ar[n] = ⊥, n0 = n, (ar[n := e])[n0] ≠ ⊥, e ≠ ⊥, m < # ar, n0 < # ar, (n < get_hash(e, # ar) ⊃ m < n ∨ get_hash(e, # ar) ≤ m;get_hash(e, # ar) ≤ m ∧ m < n) → ar[m] ≠ e ∧ ar[m] ≠ ⊥, ar[n0] ≠ ⊥ → (∀ m. (n0 < get_hash(ar[n0], # ar) ⊃ m < n0 ∨ get_hash(ar[n0], # ar) ≤ m;get_hash(ar[n0], # ar) ≤ m ∧ m < n0) ∧ m < # ar → ar[m] ≠ ar[n0] ∧ ar[m] ≠ ⊥), (n0 < get_hash((ar[n := e])[n0], # ar) ⊃ m < n0 ∨ get_hash((ar[n := e])[n0], # ar) ≤ m ;get_hash((ar[n := e])[n0], # ar) ≤ m ∧ m < n0 ), ∀ n0. n0 < # ar ∧ ar[n0] ≠ ⊥ → (∀ m. (n0 < get_hash(ar[n0], # ar) ⊃ m < n0 ∨ get_hash(ar[n0], # ar) ≤ m;get_hash(ar[n0], # ar) ≤ m ∧ m < n0) ∧ m < # ar → ar[m] ≠ ar[n0] ∧ ar[m] ≠ ⊥), ∀ m. (n < get_hash(e, # ar) ⊃ m < n ∨ get_hash(e, # ar) ≤ m;get_hash(e, # ar) ≤ m ∧ m < n) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ (ar[n := e])[m] ≠ (ar[n := e])[n0] ∧ (ar[n := e])[m] ≠ ⊥

• Proof step 12:

  ar[n] = ⊥, ar[n0] ≠ ⊥, e ≠ ⊥, n0 ≠ n, m < # ar, n0 < # ar, (n < get_hash(e, # ar) ⊃ m < n ∨ get_hash(e, # ar) ≤ m;get_hash(e, # ar) ≤ m ∧ m < n) → ar[m] ≠ e ∧ ar[m] ≠ ⊥, ar[n0] ≠ ⊥ → (∀ m. (n0 < get_hash(ar[n0], # ar) ⊃ m < n0 ∨ get_hash(ar[n0], # ar) ≤ m;get_hash(ar[n0], # ar) ≤ m ∧ m < n0) ∧ m < # ar → ar[m] ≠ ar[n0] ∧ ar[m] ≠ ⊥), (n0 < get_hash(ar[n0], # ar) ⊃ m < n0 ∨ get_hash(ar[n0], # ar) ≤ m;get_hash(ar[n0], # ar) ≤ m ∧ m < n0), ∀ n0. n0 < # ar ∧ ar[n0] ≠ ⊥ → (∀ m. (n0 < get_hash(ar[n0], # ar) ⊃ m < n0 ∨ get_hash(ar[n0], # ar) ≤ m;get_hash(ar[n0], # ar) ≤ m ∧ m < n0) ∧ m < # ar → ar[m] ≠ ar[n0] ∧ ar[m] ≠ ⊥), ∀ m. (n < get_hash(e, # ar) ⊃ m < n ∨ get_hash(e, # ar) ≤ m;get_hash(e, # ar) ≤ m ∧ m < n) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ (ar[n := e])[m] ≠ ar[n0] ∧ (ar[n := e])[m] ≠ ⊥

Rule argument

Additional information

Used terms: ar, n, e, n0

Proof step 8 from proof htok-add (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof htok-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  ar[n] = ⊥, ar[m] ≠ ⊥, ar[m] ≠ e, e ≠ ⊥, n < # ar, m < # ar, (n < get_hash(e, # ar) ⊃ m < n ∨ get_hash(e, # ar) ≤ m;get_hash(e, # ar) ≤ m ∧ m < n), ∀ m. (n < get_hash(e, # ar) ⊃ m < n ∨ get_hash(e, # ar) ≤ m;get_hash(e, # ar) ≤ m ∧ m < n) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥, ∀ n0. n0 < # ar ∧ ar[n0] ≠ ⊥ → (∀ m. (n0 < get_hash(ar[n0], # ar) ⊃ m < n0 ∨ get_hash(ar[n0], # ar) ≤ m;get_hash(ar[n0], # ar) ≤ m ∧ m < n0) ∧ m < # ar → ar[m] ≠ ar[n0] ∧ ar[m] ≠ ⊥) ⊦ (ar[n := e])[m] ≠ e ∧ (ar[n := e])[m] ≠ ⊥

Rule argument

Additional information

Used simplifier rules: ⊦ m < # ar → (ar[m := a])[m] = a; (s)

Proof step 10 from proof htok-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ m ≠ n → (ar[n := a])[m] = ar[m]

Rule argument

Additional information

Used terms: ar, n, e, m

Proof step 11 from proof htok-add (previous step) (back to tree)

A spec-lemma

Proof step 12 from proof htok-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  ar[n] = ⊥, ar[n0] ≠ ⊥, e ≠ ⊥, n0 ≠ n, n0 < # ar, m < # ar, (n < get_hash(e, # ar) ⊃ m < n ∨ get_hash(e, # ar) ≤ m;get_hash(e, # ar) ≤ m ∧ m < n) → ar[m] ≠ e ∧ ar[m] ≠ ⊥, (n0 < get_hash(ar[n0], # ar) ⊃ m < n0 ∨ get_hash(ar[n0], # ar) ≤ m;get_hash(ar[n0], # ar) ≤ m ∧ m < n0), ∀ m. (n < get_hash(e, # ar) ⊃ m < n ∨ get_hash(e, # ar) ≤ m;get_hash(e, # ar) ≤ m ∧ m < n) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥, ∀ n0. n0 < # ar ∧ ar[n0] ≠ ⊥ → (∀ m. (n0 < get_hash(ar[n0], # ar) ⊃ m < n0 ∨ get_hash(ar[n0], # ar) ≤ m;get_hash(ar[n0], # ar) ≤ m ∧ m < n0) ∧ m < # ar → ar[m] ≠ ar[n0] ∧ ar[m] ≠ ⊥), ∀ m. (n0 < get_hash(ar[n0], # ar) ⊃ m < n0 ∨ get_hash(ar[n0], # ar) ≤ m;get_hash(ar[n0], # ar) ≤ m ∧ m < n0) ∧ m < # ar → ar[m] ≠ ar[n0] ∧ ar[m] ≠ ⊥ ⊦ (ar[n := e])[m] ≠ ar[n0] ∧ (ar[n := e])[m] ≠ ⊥

Rule argument

Additional information

Proof step 13 from proof htok-add (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 14:

  ar[n] = ⊥, ar[n0] ≠ ⊥, e ≠ ⊥, n0 ≠ n, m < # ar, n0 < # ar, (n < get_hash(e, # ar) ⊃ m < n ∨ get_hash(e, # ar) ≤ m;get_hash(e, # ar) ≤ m ∧ m < n) → ar[m] ≠ e ∧ ar[m] ≠ ⊥, (n0 < get_hash(ar[n0], # ar) ⊃ m < n0 ∨ get_hash(ar[n0], # ar) ≤ m;get_hash(ar[n0], # ar) ≤ m ∧ m < n0) ∧ m < # ar → ar[m] ≠ ar[n0] ∧ ar[m] ≠ ⊥, (n0 < get_hash(ar[n0], # ar) ⊃ m < n0 ∨ get_hash(ar[n0], # ar) ≤ m;get_hash(ar[n0], # ar) ≤ m ∧ m < n0), ∀ m. (n0 < get_hash(ar[n0], # ar) ⊃ m < n0 ∨ get_hash(ar[n0], # ar) ≤ m;get_hash(ar[n0], # ar) ≤ m ∧ m < n0) ∧ m < # ar → ar[m] ≠ ar[n0] ∧ ar[m] ≠ ⊥, ∀ n0. n0 < # ar ∧ ar[n0] ≠ ⊥ → (∀ m. (n0 < get_hash(ar[n0], # ar) ⊃ m < n0 ∨ get_hash(ar[n0], # ar) ≤ m;get_hash(ar[n0], # ar) ≤ m ∧ m < n0) ∧ m < # ar → ar[m] ≠ ar[n0] ∧ ar[m] ≠ ⊥), ∀ m. (n < get_hash(e, # ar) ⊃ m < n ∨ get_hash(e, # ar) ≤ m;get_hash(e, # ar) ≤ m ∧ m < n) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ (ar[n := e])[m] ≠ ar[n0] ∧ (ar[n := e])[m] ≠ ⊥

Rule argument

Additional information

Used terms: m

Proof step 14 from proof htok-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  ar[n] = ⊥, ar[n0] ≠ ⊥, ar[m] ≠ ⊥, ar[m] ≠ ar[n0], e ≠ ⊥, n0 ≠ n, n0 < # ar, m < # ar, (n < get_hash(ar[m], # ar) ⊃ m < n ∨ get_hash(ar[m], # ar) ≤ m;get_hash(ar[m], # ar) ≤ m ∧ m < n) → ar[m] ≠ e, (n0 < get_hash(ar[n0], # ar) ⊃ m < n0 ∨ get_hash(ar[n0], # ar) ≤ m;get_hash(ar[n0], # ar) ≤ m ∧ m < n0), ∀ m. (n < get_hash(e, # ar) ⊃ m < n ∨ get_hash(e, # ar) ≤ m;get_hash(e, # ar) ≤ m ∧ m < n) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥, ∀ n0. n0 < # ar ∧ ar[n0] ≠ ⊥ → (∀ m. (n0 < get_hash(ar[n0], # ar) ⊃ m < n0 ∨ get_hash(ar[n0], # ar) ≤ m;get_hash(ar[n0], # ar) ≤ m ∧ m < n0) ∧ m < # ar → ar[m] ≠ ar[n0] ∧ ar[m] ≠ ⊥), ∀ m. (n0 < get_hash(ar[n0], # ar) ⊃ m < n0 ∨ get_hash(ar[n0], # ar) ≤ m;get_hash(ar[n0], # ar) ≤ m ∧ m < n0) ∧ m < # ar → ar[m] ≠ ar[n0] ∧ ar[m] ≠ ⊥ ⊦ (ar[n := e])[m] ≠ ar[n0] ∧ (ar[n := e])[m] ≠ ⊥

Rule argument

Additional information

Proof step 15 from proof htok-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ m ≠ n → (ar[n := a])[m] = ar[m]

Rule argument

Additional information

Used terms: ar, n, e, m

Proof step 16 from proof htok-add (previous step) (back to tree)

A spec-lemma