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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (st \ s) | s ≠ ∅ ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  (st \ s) \ ((dom st \ s) \ s) ≠ ∅ ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ disjoint(s, s0) → s \ s0 = s

• Proof step 5:

  (st \ s) \ (dom st \ s) ≠ ∅, disjoint(dom st \ s, s) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ disjoint(s0 \ s1, s1); (s) Used terms: dom st \ s, s

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  (st \ s) \ (dom st \ s) ≠ ∅ ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ disjoint(s0 \ s1, s1); (s)

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

User applied rule structural induction

And obtained the following new goals

• Proof step 7:

  (st0(a := d) \ s) \ (dom st0(a := d) \ s) ≠ ∅, ∀ s. (st0 \ s) \ (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 7 from proof restrict-diff (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  (st0(a := d) \ s) \ ((dom st0 ++ a) \ s) ≠ ∅, ∀ s. (st0 \ s) \ (dom st0 \ s) = ∅ ⊦

Rule argument

Additional information

Used simplifier rules: dom-ins: ⊦ dom st(a := d) = dom st ++ a;

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

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

• Proof step 10:

  (st0(a := d) \ s) \ ((dom st0 ++ a) \ s) ≠ ∅, a ∈ s, ∀ s. (st0 \ s) \ (dom st0 \ s) = ∅ ⊦

• Proof step 12:

  (st0 \ s)(a := d) \ ((dom st0 ++ a) \ s) ≠ ∅, ¬ a ∈ s, ∀ s. (st0 \ s) \ (dom st0 \ s) = ∅ ⊦

Rule argument

Additional information

Used terms: st0, a, d, s

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

Lemma rem-write

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

Used simplifier rules: rem-write-other: ⊦ a ∈ s → st(a := d) \ s = st \ s; 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)

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: s

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  ((st0 \ s) \ (dom st0 \ s)) -- a ≠ ∅, ¬ a ∈ s, ∀ s. (st0 \ s) \ (dom st0 \ s) = ∅ ⊦

Rule argument

Additional information

Used simplifier rules: Diff-mod: ⊦ st(a := d) \ (s ++ a) = st \ (s ++ a); Diff-rec: ⊦ st \ (s ++ a) = (st \ s) -- a; ⊦ ¬ a ∈ s1 → (s ++ a) \ s1 = (s \ s1) ++ a; (s)

Proof step 13 from proof restrict-diff (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ ∅ -- a = ∅; (s) Used terms: s