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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ⊦ (∀ a0. a0 ∈ st → a0 ∈ st0(a := d) ∧ st(a0) = st0(a := d)(a0)) ↔ (∀ a. a ∈ st → a ∈ st0 ∧ st(a) = st0(a)) ∧ ¬ a ∈ st ∨ a ∈ st ∧ st(a) = d ∧ (∀ a0. a0 ∈ st -- a → a0 ∈ st0 -- a ∧ (st -- a)(a0) = (st0 -- a)(a0))

Rule argument

Additional information

Used simplifier rules: Subset: ⊦ st1 ⊆ st2 ↔ (∀ a. a ∈ st1 → a ∈ st2 ∧ st1(a) = st2(a));

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

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  ∀ a0. a0 ∈ st → a0 ∈ st0(a := d) ∧ st(a0) = st0(a := d)(a0) ⊦ (∀ a. a ∈ st → a ∈ st0 ∧ st(a) = st0(a)) ∧ ¬ a ∈ st, a ∈ st ∧ st(a) = d ∧ (∀ a0. a0 ∈ st -- a → a0 ∈ st0 -- a ∧ (st -- a)(a0) = (st0 -- a)(a0))

• Proof step 15:

  (∀ a. a ∈ st → a ∈ st0 ∧ st(a) = st0(a)) ∧ ¬ a ∈ st ∨ a ∈ st ∧ st(a) = d ∧ (∀ a0. a0 ∈ st -- a → a0 ∈ st0 -- a ∧ (st -- a)(a0) = (st0 -- a)(a0)) ⊦ ∀ a0. a0 ∈ st → a0 ∈ st0(a := d) ∧ st(a0) = st0(a := d)(a0)

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ∀ a0. a0 ∈ st → a0 ∈ st0(a := d) ∧ st(a0) = st0(a := d)(a0) ⊦ a ∈ st ∧ st(a) = d ∧ (a0 ∈ st -- a → a0 ∈ st0 -- a ∧ (st -- a)(a0) = (st0 -- a)(a0)), (a1 ∈ st → a1 ∈ st0 ∧ st(a1) = st0(a1)) ∧ ¬ a ∈ st

Rule argument

Additional information

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

User applied rule all left

And obtained the following new goals

• Proof step 6:

  a ∈ st → a ∈ st0(a := d) ∧ st(a) = st0(a := d)(a), ∀ a0. a0 ∈ st → a0 ∈ st0(a := d) ∧ st(a0) = st0(a := d)(a0) ⊦ (a1 ∈ st → a1 ∈ st0 ∧ st(a1) = st0(a1)) ∧ ¬ a ∈ st, a ∈ st ∧ st(a) = d ∧ (a0 ∈ st -- a → a0 ∈ st0 -- a ∧ (st -- a)(a0) = (st0 -- a)(a0))

Rule argument

Additional information

Used terms: a

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  a ∈ st → a ∈ st0(a := st(a)) ∧ st(a) = d, ∀ a0. a0 ∈ st → a0 ∈ st0(a := d) ∧ st(a0) = st0(a := d)(a0) ⊦ a ∈ st ∧ st(a) = d ∧ (a0 ∈ st -- a → a0 ∈ st0 -- a ∧ (st -- a)(a0) = (st0 -- a)(a0)), (a1 ∈ st → a1 ∈ st0 ∧ st(a1) = st0(a1)) ∧ ¬ a ∈ st

Rule argument

Additional information

Used simplifier rules: At-same: ⊦ st(a := d)(a) = d;

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

User applied rule all left

And obtained the following new goals

• Proof step 8:

  a ∈ st → a ∈ st0(a := st(a)) ∧ st(a) = d, a0 ∈ st → a0 ∈ st0(a := d) ∧ st(a0) = st0(a := d)(a0), ∀ a0. a0 ∈ st → a0 ∈ st0(a := d) ∧ st(a0) = st0(a := d)(a0) ⊦ (a1 ∈ st → a1 ∈ st0 ∧ st(a1) = st0(a1)) ∧ ¬ a ∈ st, a ∈ st ∧ st(a) = d ∧ (a0 ∈ st -- a → a0 ∈ st0 -- a ∧ (st -- a)(a0) = (st0 -- a)(a0))

Rule argument

Additional information

Used terms: a0

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 9:

  a0 = a, a0 ∈ st → a0 ∈ st0(a := d) ∧ st(a0) = st0(a := d)(a0), a ∈ st → a ∈ st0(a := st(a)) ∧ st(a) = d, ∀ a0. a0 ∈ st → a0 ∈ st0(a := d) ∧ st(a0) = st0(a := d)(a0) ⊦ a ∈ st ∧ st(a) = d ∧ (a0 ∈ st -- a → a0 ∈ st0 -- a ∧ (st -- a)(a0) = (st0 -- a)(a0)), (a1 ∈ st → a1 ∈ st0 ∧ st(a1) = st0(a1)) ∧ ¬ a ∈ st

• Proof step 12:

  a0 ≠ a, a0 ∈ st → a0 ∈ st0(a := d) ∧ st(a0) = st0(a := d)(a0), a ∈ st → a ∈ st0(a := st(a)) ∧ st(a) = d, ∀ a0. a0 ∈ st → a0 ∈ st0(a := d) ∧ st(a0) = st0(a := d)(a0) ⊦ a ∈ st ∧ st(a) = d ∧ (a0 ∈ st -- a → a0 ∈ st0 -- a ∧ (st -- a)(a0) = (st0 -- a)(a0)), (a1 ∈ st → a1 ∈ st0 ∧ st(a1) = st0(a1)) ∧ ¬ a ∈ st

Rule argument

Additional information

Used formulas: a0 = a

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  a ∈ st → a ∈ st0(a := st(a)) ∧ st(a) = d, ∀ a0. a0 ∈ st → a0 ∈ st0(a := d) ∧ st(a0) = st0(a := d)(a0) ⊦ (a1 ∈ st → a1 ∈ st0 ∧ st(a1) = st0(a1)) ∧ ¬ a ∈ st, a ∈ st ∧ st(a) = d ∧ (a ∈ st -- a → a ∈ st0 -- a ∧ (st -- a)(a) = (st0 -- a)(a))

Rule argument

Additional information

Used simplifier rules: At-same: ⊦ st(a := d)(a) = d;

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

User applied rule all left

And obtained the following new goals

• Proof step 11:

  a ∈ st → a ∈ st0(a := st(a)) ∧ st(a) = d, a1 ∈ st → a1 ∈ st0(a := d) ∧ st(a1) = st0(a := d)(a1), ∀ a0. a0 ∈ st → a0 ∈ st0(a := d) ∧ st(a0) = st0(a := d)(a0) ⊦ a ∈ st ∧ st(a) = d ∧ (a ∈ st -- a → a ∈ st0 -- a ∧ (st -- a)(a) = (st0 -- a)(a)), (a1 ∈ st → a1 ∈ st0 ∧ st(a1) = st0(a1)) ∧ ¬ a ∈ st

Rule argument

Additional information

Used terms: a1

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

Heuristic weak cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: Del-in: ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; in-neq: ⊦ a ≠ b → (a ∈ st(b := d) ↔ a ∈ st); At-other: ⊦ a ≠ b → st(b := d)(a) = st(a); Del-in: ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; Used formulas: a1 = a

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  a0 ≠ a, a ∈ st → a ∈ st0(a := st(a)) ∧ st(a) = d, a0 ∈ st → a0 ∈ st0 ∧ st(a0) = st0(a0), ∀ a0. a0 ∈ st → a0 ∈ st0(a := d) ∧ st(a0) = st0(a := d)(a0) ⊦ (a1 ∈ st → a1 ∈ st0 ∧ st(a1) = st0(a1)) ∧ ¬ a ∈ st, a ∈ st ∧ st(a) = d ∧ (a0 ∈ st -- a → a0 ∈ st0 -- a ∧ (st -- a)(a0) = (st0 -- a)(a0))

Rule argument

Additional information

Used simplifier rules: In-insert: ⊦ a ∈ st(b := d) ↔ a = b ∨ a ∈ st; At-other: ⊦ a ≠ b → st(b := d)(a) = st(a);

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

User applied rule all left

And obtained the following new goals

• Proof step 14:

  a0 ≠ a, a0 ∈ st → a0 ∈ st0 ∧ st(a0) = st0(a0), a ∈ st → a ∈ st0(a := st(a)) ∧ st(a) = d, a1 ∈ st → a1 ∈ st0(a := d) ∧ st(a1) = st0(a := d)(a1), ∀ a0. a0 ∈ st → a0 ∈ st0(a := d) ∧ st(a0) = st0(a := d)(a0) ⊦ a ∈ st ∧ st(a) = d ∧ (a0 ∈ st -- a → a0 ∈ st0 -- a ∧ (st -- a)(a0) = (st0 -- a)(a0)), (a1 ∈ st → a1 ∈ st0 ∧ st(a1) = st0(a1)) ∧ ¬ a ∈ st

Rule argument

Additional information

Used terms: a1

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

Heuristic weak cut applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: Del-at-strong: a ≠ b ⊦ (st -- b)(a) = st(a); Del-in: ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; in-neq: ⊦ a ≠ b → (a ∈ st(b := d) ↔ a ∈ st); At-other: ⊦ a ≠ b → st(b := d)(a) = st(a); Del-at-strong: a ≠ b ⊦ (st -- b)(a) = st(a); Del-in: ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; Used formulas: a1 = a

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  a0 ∈ st, (∀ a. a ∈ st → a ∈ st0 ∧ st(a) = st0(a)) ∧ ¬ a ∈ st ∨ a ∈ st ∧ st(a) = d ∧ (∀ a1. a1 ∈ st -- a → a1 ∈ st0 -- a ∧ st(a1) = st0(a1)) ⊦ a0 ∈ st0(a := d) ∧ st(a0) = st0(a := d)(a0)

Rule argument

Additional information

Used simplifier rules: Del-in: ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; Del-at-strong: a ≠ b ⊦ (st -- b)(a) = st(a);

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

Heuristic weak cut applied rule cut formula

And obtained the following new goals

• Proof step 17:

  a0 ≠ a, a0 ∈ st, (∀ a. a ∈ st → a ∈ st0 ∧ st(a) = st0(a)) ∧ ¬ a ∈ st ∨ a ∈ st ∧ st(a) = d ∧ (∀ a1. a1 ∈ st -- a → a1 ∈ st0 -- a ∧ st(a1) = st0(a1)) ⊦ a0 ∈ st0(a := d) ∧ st(a0) = st0(a := d)(a0)

Rule argument

Additional information

Used simplifier rules: At-same: ⊦ st(a := d)(a) = d; In-insert: ⊦ a ∈ st(b := d) ↔ a = b ∨ a ∈ st; Used formulas: a0 = a

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  a0 ≠ a, a0 ∈ st, (∀ a. a ∈ st → a ∈ st0 ∧ st(a) = st0(a)) ∧ ¬ a ∈ st ∨ a ∈ st ∧ st(a) = d ∧ (∀ a1. a1 ∈ st -- a → a1 ∈ st0 -- a ∧ st(a1) = st0(a1)) ⊦ a0 ∈ st0 ∧ st(a0) = st0(a0)

Rule argument

Additional information

Used simplifier rules: in-neq: ⊦ a ≠ b → (a ∈ st(b := d) ↔ a ∈ st); At-other: ⊦ a ≠ b → st(b := d)(a) = st(a);

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

User applied rule case distinction

And obtained the following new goals

• Proof step 19:

  a0 ≠ a, a0 ∈ st, ¬ a ∈ st, ∀ a. a ∈ st → a ∈ st0 ∧ st(a) = st0(a) ⊦ a0 ∈ st0 ∧ st(a0) = st0(a0)

• Proof step 21:

  st(a) = d, a0 ≠ a, a0 ∈ st, a ∈ st, ∀ a1. a1 ∈ st -- a → a1 ∈ st0 -- a ∧ st(a1) = st0(a1) ⊦ a0 ∈ st0 ∧ st(a0) = st0(a0)

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  a0 ≠ a, a0 ∈ st, ¬ a ∈ st, ∀ a. a ∈ st → a ∈ st0 ∧ st(a) = st0(a) ⊦ a0 ∈ st0 ∧ st(a0) = st0(a0)

Rule argument

Additional information

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

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  a0 ≠ a, a ∈ st, a0 ∈ st, ∀ a1. a1 ∈ st -- a → a1 ∈ st0 -- a ∧ st(a1) = st0(a1) ⊦ a0 ∈ st0 ∧ st(a0) = st0(a0)

Rule argument

Additional information

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

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: Del-in: ⊦ a ∈ st -- b ↔ a ≠ b ∧ a ∈ st; Used terms: a0