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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  st | s ≠ st, dom st ⊆ s ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  st \ (dom st \ s) ≠ st, dom st ⊆ s ⊦

Rule argument

Additional information

Used simplifier rules: restrict: ⊦ st | s = st \ (dom st \ s);

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

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  st0(a := d) \ (dom st0(a := d) \ s) ≠ st0(a := d), dom st0(a := d) ⊆ s, ∀ s. ¬(st0 \ (dom st0 \ s) ≠ st0 ∧ dom st0 ⊆ s) ⊦

Rule argument

Additional information

Used simplifier rules: dom-emp: ⊦ dom ∅ = ∅; Diff-empty: ⊦ ∅ \ s = ∅; Map[A, B] generated by ∅, . ( . := . ); ⊦ ∅ \ s = ∅; (s)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  # s ≠ 0, s ≠ ∅, st0(a := d) \ (dom st0 \ s) ≠ st0(a := d), a ∈ s, dom st0 ⊆ s, ∀ s0. st0 \ (dom st0 \ s0) = st0 ∨ ¬ dom st0 ⊆ s0 ⊦

Rule argument

Additional information

Used simplifier rules: dom-ins: ⊦ dom st(a := d) = dom st ++ a; size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic ⊦ a ∈ s1 → (s ++ a) \ s1 = s \ s1; (s) ⊦ s ++ a ⊆ s0 ↔ s ⊆ s0 ∧ a ∈ s0; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ ¬ a ∈ s → st(a := d) \ s = (st \ s)(a := d)

• Proof step 7:

  # s ≠ 0, s ≠ ∅, (st0 \ (dom st0 \ s))(a := d) ≠ st0(a := d), a ∈ s, dom st0 ⊆ s, ¬ a ∈ dom st0 \ s, ∀ s0. st0 \ (dom st0 \ s0) = st0 ∨ ¬ dom st0 ⊆ s0 ⊦

Rule argument

Additional information

Used simplifier rules: rem-write-other: ⊦ a ∈ s → st(a := d) \ s = st \ s; Dom: ⊦ a ∈ dom st ↔ a ∈ st; ⊦ a ∈ s1 \ s2 ↔ a ∈ s1 ∧ ¬ a ∈ s2; (s) Used terms: st0, a, d, dom st0 \ s

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

Lemma rem-write

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  # s ≠ 0, s ≠ ∅, (st0 \ (dom st0 \ s))(a := d) ≠ st0(a := d), a ∈ s, dom st0 ⊆ s, ∀ s0. st0 \ (dom st0 \ s0) = st0 ∨ ¬ dom st0 ⊆ s0 ⊦

Rule argument

Additional information

Used simplifier rules: Dom: ⊦ a ∈ dom st ↔ a ∈ st; ⊦ a ∈ s1 \ s2 ↔ a ∈ s1 ∧ ¬ a ∈ s2; (s)

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

User applied rule reduce equation

And obtained the following new goals

• Proof step 9:

  # s ≠ 0, s ≠ ∅, st0 \ (dom st0 \ s) ≠ st0, a ∈ s, dom st0 ⊆ s, ∀ s0. st0 \ (dom st0 \ s0) = st0 ∨ ¬ dom st0 ⊆ s0 ⊦

Rule argument

Additional information

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: s