Proof step 1 from proof ex3-shift-01 (conclusion) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 2:

  ⊦ (∃ oa. (oaR(oa.obj, oa.aux) * hR)[rs, λ r. f(r) ×× g(r)]__) ↔ (∃ o, a. (oaR(o, a) * hR)[rs, λ r. f(r) ×× g(r)]__)

Rule argument

Additional information

Used simplifier rules: ex3-01: ⊦ _∃ oaR = __∃(λ oa. oaR(oa.obj, oa.aux)); modifysep-def: ⊦ hP[rs, f, g] ↔ hP[rs, λ r. f(r) ×× g(r)]__; sep-com: ⊦ hP0 * hP1 = hP1 * hP0; from specification heap-sep[heap-aux-inst] sep-ass: ⊦ (hP0 * hP1) * hP2 = hP0 * hP1 * hP2; from specification heap-sep[heap-aux-inst] ⊦ (__∃ oP * hP)[rs, f]__ ↔ (∃ o. (oP(o) * hP)[rs, f]__); (s)

Proof step 2 from proof ex3-shift-01 (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 3:

  ∃ oa. (oaR(oa.obj, oa.aux) * hR)[rs, λ r. f(r) ×× g(r)]__ ⊦ ∃ o, a. (oaR(o, a) * hR)[rs, λ r. f(r) ×× g(r)]__

• Proof step 7:

  ∃ o, a. (oaR(o, a) * hR)[rs, λ r. f(r) ×× g(r)]__ ⊦ ∃ oa. (oaR(oa.obj, oa.aux) * hR)[rs, λ r. f(r) ×× g(r)]__

Rule argument

Additional information

Proof step 3 from proof ex3-shift-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  (oaR(oa.obj, oa.aux) * hR)[rs, λ r. f(r) ×× g(r)]__ ⊦ ∃ o, a. (oaR(o, a) * hR)[rs, λ r. f(r) ×× g(r)]__

Rule argument

Additional information

Proof step 4 from proof ex3-shift-01 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 5:

  oa = o0 ×× a0, (oaR(o0, a0) * hR)[rs, λ r. f(r) ×× g(r)]__ ⊦ ∃ o, a. (oaR(o, a) * hR)[rs, λ r. f(r) ×× g(r)]__

Rule argument

Additional information

Used simplifier rules: ⊦ obj = oa.obj ∧ aux = oa.aux ↔ oa = obj ×× aux; (elim) Used terms: oa, obj, aux

Proof step 5 from proof ex3-shift-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  (oaR(o0, a0) * hR)[rs, λ r. f(r) ×× g(r)]__ ⊦ ∃ o, a. (oaR(o, a) * hR)[rs, λ r. f(r) ×× g(r)]__

Rule argument

Additional information

Proof step 6 from proof ex3-shift-01 (previous step) (back to tree)

Heuristic quantifier closing applied rule exists right

And closed the goal!

Rule argument

Additional information

Used terms: o0, a0

Proof step 7 from proof ex3-shift-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  (oaR(o, a) * hR)[rs, λ r. f(r) ×× g(r)]__ ⊦ ∃ oa. (oaR(oa.obj, oa.aux) * hR)[rs, λ r. f(r) ×× g(r)]__

Rule argument

Additional information

Proof step 8 from proof ex3-shift-01 (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (obj ×× aux).obj = obj; (s) ⊦ (obj ×× aux).aux = aux; (s) Used terms: o ×× a