Proof step 1 from proof restrict-intersect-empty (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  dom st ∩ s = ∅, st \ s ≠ st ⊦

Rule argument

Additional information

Proof step 2 from proof restrict-intersect-empty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  dom st ∩ s = ∅, st \ s ≠ st ⊦

Rule argument

Additional information

Proof step 3 from proof restrict-intersect-empty (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ st1 = st2 ↔ (∀ a. (a ∈ st1 ↔ a ∈ st2) ∧ st1[a] = st2[a])

• Proof step 5:

  dom st ∩ s = ∅, ∃ a. ¬((a ∈ st \ s ↔ a ∈ st) ∧ (st \ s)[a] = st[a]) ⊦

Rule argument

Additional information

Used terms: st, st \ s

Proof step 4 from proof restrict-intersect-empty (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof restrict-intersect-empty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  dom st ∩ s = ∅ ⊦ (a ∈ st \ s ↔ a ∈ st) ∧ (st \ s)[a] = st[a]

Rule argument

Additional information

Proof step 6 from proof restrict-intersect-empty (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ ¬ a ∈ s → (st \ s)[a] = st[a]

• Proof step 8:

  dom st ∩ s = ∅, a ∈ s ⊦ (a ∈ st \ s ↔ a ∈ st) ∧ (st \ s)[a] = st[a]

Rule argument

Additional information

Used simplifier rules: Diff-ext: ⊦ a ∈ st \ s ↔ a ∈ st ∧ ¬ a ∈ s; Used terms: a, s, st

Proof step 7 from proof restrict-intersect-empty (previous step) (back to tree)

Lemma Diff-get

Proof step 8 from proof restrict-intersect-empty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  dom st ∩ s = ∅, # s ≠ 0, s ≠ ∅, a ∈ s ⊦ (a ∈ st \ s ↔ a ∈ st) ∧ ∅[a] = st[a]

Rule argument

Additional information

Used simplifier rules: Diff-mems-get: ⊦ a ∈ s → (st \ s)[a] = ∅[a]; size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic

Proof step 9 from proof restrict-intersect-empty (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ s1 = s2 ↔ (∀ a. a ∈ s1 ↔ a ∈ s2)

• Proof step 11:

  # s ≠ 0, s ≠ ∅, a ∈ s, ∀ a. a ∈ dom st ∩ s ↔ a ∈ ∅ ⊦ (a ∈ st \ s ↔ a ∈ st) ∧ ∅[a] = st[a]

Rule argument

Additional information

Used terms: ∅, dom st ∩ s

Proof step 10 from proof restrict-intersect-empty (previous step) (back to tree)

A spec-lemma

Proof step 11 from proof restrict-intersect-empty (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  # s ≠ 0, s ≠ ∅, a ∈ s, ∀ a0. ¬ a0 ∈ dom st ∩ s ⊦ (a ∈ st \ s ↔ a ∈ st) ∧ ∅[a] = st[a]

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ ∅; (s)

Proof step 12 from proof restrict-intersect-empty (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: Dom: ⊦ a ∈ dom st ↔ a ∈ st; Diff-ext: ⊦ a ∈ st \ s ↔ a ∈ st ∧ ¬ a ∈ s; ⊦ a ∈ s1 ∩ s2 ↔ a ∈ s1 ∧ a ∈ s2; (ws) int-a: ⊦ (s ∩ s0) ∩ s1 = s ∩ s0 ∩ s1; from specification set-union int-c: ⊦ s ∩ s0 = s0 ∩ s; from specification set-union ⊦ ¬ a ∈ st → st[a] = ∅[a]; (s) Used terms: a