Proof step 1 from proof subset-size (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  # st0 < # st, st ⊆ st0 ⊦

Rule argument

Additional information

Proof step 2 from proof subset-size (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  # st0 < # st1(a := d), st1(a := d) ⊆ st0, ∀ st0. ¬(# st0 < # st1 ∧ st1 ⊆ st0) ⊦

Rule argument

Additional information

Used simplifier rules: gen: ⊦ ; subset-empty: ⊦ ∅ ⊆ st; Size-empty: ⊦ # ∅ = 0; ⊦ ¬ n < 0; (s)

Proof step 3 from proof subset-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  st1(a := d) ≠ ∅, # st0 < # st1(a := d), st1(a := d) ⊆ st0, ∀ st. ¬ # st < # st1 ∨ ¬ st1 ⊆ st ⊦

Rule argument

Additional information

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

Proof step 4 from proof subset-size (previous step) (back to tree)

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 5:

  st1(a := d) ≠ ∅, # st0 < # st1(a := d), a ∈ st1, st1(a := d) ⊆ st0, ∀ st. ¬ # st < # st1 ∨ ¬ st1 ⊆ st ⊦

• Proof step 18:

  st1(a := d) ≠ ∅, # st0 < # st1(a := d), st1(a := d) ⊆ st0, ¬ a ∈ st1, ∀ st. ¬ # st < # st1 ∨ ¬ st1 ⊆ st ⊦

Rule argument

Additional information

Used formulas: a ∈ st1

Proof step 5 from proof subset-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  st1(a := d) ≠ ∅, st1 ≠ ∅, # st0 < # st1, a ∈ st1, st1(a := d) ⊆ st0, ∀ st. ¬ # st < # st1 ∨ ¬ st1 ⊆ st ⊦

Rule argument

Additional information

Used simplifier rules: size-in: ⊦ a ∈ st → # st(a := d) = # st; empty: ⊦ # st = 0 ↔ st = ∅; f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 6 from proof subset-size (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ st(a) = d ∧ a ∈ st → st(a := d) = st

• Proof step 8:

  st1(a := d) ≠ ∅, st1 ≠ ∅, # st0 < # st1, a ∈ st1, st1(a := d) ⊆ st0, ∀ st. ¬ # st < # st1 ∨ ¬ st1 ⊆ st ⊦ st1(a) = d ∧ a ∈ st1

• Proof step 16:

  st1(a) = d, st1 ≠ ∅, # st0 < # st1, a ∈ st1, st1 ⊆ st0, ∀ st. ¬ # st < # st1 ∨ ¬ st1 ⊆ st ⊦

Rule argument

Additional information

Used terms: d, a, st1

Proof step 7 from proof subset-size (previous step) (back to tree)

Lemma ins

Proof step 8 from proof subset-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  st1(a := d) ≠ ∅, st1 ≠ ∅, st1(a) ≠ d, # st0 < # st1, a ∈ st1, st1(a := d) ⊆ st0, ∀ st. ¬ # st < # st1 ∨ ¬ st1 ⊆ st ⊦

Rule argument

Additional information

Proof step 9 from proof subset-size (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ st(a := d) ⊆ st0 ↔ st -- a ⊆ st0 -- a ∧ a ∈ st0 ∧ st0(a) = d

• Proof step 11:

  st0(a) = d, st1(a := d) ≠ ∅, st1 ≠ ∅, st1(a) ≠ d, # st0 < # st1, a ∈ st0, a ∈ st1, st1 -- a ⊆ st0 -- a, ∀ st. ¬ # st < # st1 ∨ ¬ st1 ⊆ st ⊦

Rule argument

Additional information

Used terms: st0, d, a, st1

Proof step 10 from proof subset-size (previous step) (back to tree)

Lemma subset-put-02

Proof step 11 from proof subset-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  st1(a := st0(a)) ≠ ∅, st1 ≠ ∅, st1(a) ≠ st0(a), # st0 < # st1, a ∈ st1, a ∈ st0, st1 -- a ⊆ st0 -- a, ∀ st. ¬ # st < # st1 ∨ ¬ st1 ⊆ st ⊦

Rule argument

Additional information

Proof step 12 from proof subset-size (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 13:

  st1(a := st0(a)) ≠ ∅, st1 ≠ ∅, st1(a) ≠ st0(a), # st0 < # st1, a ∈ st0, a ∈ st1, st1 -- a ⊆ st0 -- a, ¬ # st0(a := st1(a)) < # st1 ∨ ¬ st1 ⊆ st0(a := st1(a)), ∀ st. ¬ # st < # st1 ∨ ¬ st1 ⊆ st ⊦

Rule argument

Additional information

Used terms: st0(a := st1(a))

Proof step 13 from proof subset-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  st1(a := st0(a)) ≠ ∅, st1 ≠ ∅, st1(a) ≠ st0(a), # st0 < # st1, a ∈ st1, a ∈ st0, st1 -- a ⊆ st0 -- a, ¬ st1 ⊆ st0(a := st1(a)), ∀ st. ¬ # st < # st1 ∨ ¬ st1 ⊆ st ⊦

Rule argument

Additional information

Used simplifier rules: size-in: ⊦ a ∈ st → # st(a := d) = # st;

Proof step 14 from proof subset-size (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ st ⊆ st0(a := d) ↔ st ⊆ st0 ∧ ¬ a ∈ st ∨ a ∈ st ∧ st(a) = d ∧ st -- a ⊆ st0 -- a

Rule argument

Additional information

Used terms: st1(a), a, st0, st1

Proof step 15 from proof subset-size (previous step) (back to tree)

Lemma subset-put-01

Proof step 16 from proof subset-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  st1 ≠ ∅, # st0 < # st1, a ∈ st1, st1 ⊆ st0, ∀ st. ¬ # st < # st1 ∨ ¬ st1 ⊆ st ⊦

Rule argument

Additional information

Proof step 17 from proof subset-size (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: st0

Proof step 18 from proof subset-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 19:

  st1(a := d) ≠ ∅, # st0 ≤ # st1, st1(a := d) ⊆ st0, ¬ a ∈ st1, ∀ st. ¬ # st < # st1 ∨ ¬ st1 ⊆ st ⊦

Rule argument

Additional information

Used simplifier rules: Size-insert: ⊦ ¬ a ∈ st → # st(a := d) = # st + 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)

Proof step 19 from proof subset-size (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ st(a := d) ⊆ st0 ↔ st -- a ⊆ st0 -- a ∧ a ∈ st0 ∧ st0(a) = d

• Proof step 21:

  st0(a) = d, st1(a := d) ≠ ∅, # st0 ≤ # st1, a ∈ st0, st1 -- a ⊆ st0 -- a, ¬ a ∈ st1, ∀ st. ¬ # st < # st1 ∨ ¬ st1 ⊆ st ⊦

Rule argument

Additional information

Used terms: st0, d, a, st1

Proof step 20 from proof subset-size (previous step) (back to tree)

Lemma subset-put-02

Proof step 21 from proof subset-size (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  st1(a := st0(a)) ≠ ∅, # st0 ≤ # st1, a ∈ st0, st1 ⊆ st0 -- a, ¬ a ∈ st1, ∀ st. ¬ # st < # st1 ∨ ¬ st1 ⊆ st ⊦

Rule argument

Additional information

Used simplifier rules: notin-del-notin: ⊦ ¬ a ∈ st → st -- a = st;

Proof step 22 from proof subset-size (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: size: ⊦ a ∈ st → #(st -- a) = (# st).-1; empty: ⊦ # st = 0 ↔ st = ∅; Del-empty: ⊦ ∅ -- a = ∅; subset-empty-01: ⊦ st ⊆ ∅ ↔ st = ∅; In-empty: ⊦ ¬ a ∈ ∅; ⊦ 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 ↔ false); (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: st0 -- a