Proof step 1 from proof map-putrev (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬((r.==>(o0, a0) * hR)[rs, f(r := o1), g(r := a1)] ↔ (o0 = o1 ∧ a0 = a1) ∧ (r.=>_ * hR)[rs, f, g]), r ∈ rs ⊦

Rule argument

Additional information

Proof step 2 from proof map-putrev (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  # rs ≠ 0, ¬((r => (o0, a0) * hR)[rs, λ r0. ((r = r0 ⊃ o1;f(r0)), (r = r0 ⊃ a1;g(r0)))] ↔ o0 = o1 ∧ a0 = a1 ∧ (r.=>_ * hR)[rs, λ r. (f(r), g(r))]), rs ≠ ∅, r ∈ rs ⊦

Rule argument

Additional information

Used simplifier rules: maplet-def: ⊦ r.==>(o, a) = r => (o, a); modifysep-def: ⊦ hP[rs, f, g] ↔ hP[rs, λ r. (f(r), g(r))]; size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic

Proof step 3 from proof map-putrev (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

  r ∈ rs ⊦ (r => o0 * hP)[rs, f(r := o1)] ↔ o0 = o1 ∧ (r.=>_ * hP)[rs, f]

• Proof step 5:

  (r => (o0, a0) * hR)[rs, (λ r. (f(r), g(r)))(r := (o1, a1))] ↔ (o0, a0) = (o1, a1) ∧ (r.=>_ * hR)[rs, λ r. (f(r), g(r))], # rs ≠ 0, ¬((r => (o0, a0) * hR)[rs, λ r0. ((r = r0 ⊃ o1;f(r0)), (r = r0 ⊃ a1;g(r0)))] ↔ o0 = o1 ∧ a0 = a1 ∧ (r.=>_ * hR)[rs, λ r. (f(r), g(r))]), rs ≠ ∅, r ∈ rs ⊦

Rule argument

Additional information

Used terms: rs, r, hR, (o1, a1), (o0, a0), λ r. (f(r), g(r))

Proof step 4 from proof map-putrev (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof map-putrev (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  (r => (o0, a0) * hR)[rs, λ r0. (r0 = r ⊃ (o1, a1);(f(r0), g(r0)))] ↔ (o0, a0) = (o1, a1) ∧ (r.=>_ * hR)[rs, λ r. (f(r), g(r))], # rs ≠ 0, ¬((r => (o0, a0) * hR)[rs, λ r0. ((r = r0 ⊃ o1;f(r0)), (r = r0 ⊃ a1;g(r0)))] ↔ o0 = o1 ∧ a0 = a1 ∧ (r.=>_ * hR)[rs, λ r. (f(r), g(r))]), rs ≠ ∅, r ∈ rs ⊦

Rule argument

Additional information

Proof step 6 from proof map-putrev (previous step) (back to tree)

User applied rule expand tuple

And obtained the following new goals

• Proof step 7:

  (r => (o0, a0) * hR)[rs, λ r0. (r0 = r ⊃ (o1, a1);(f(r0), g(r0)))] ↔ (o0 = o1 ∧ a0 = a1) ∧ (r.=>_ * hR)[rs, λ r. (f(r), g(r))], # rs ≠ 0, ¬((r => (o0, a0) * hR)[rs, λ r0. ((r = r0 ⊃ o1;f(r0)), (r = r0 ⊃ a1;g(r0)))] ↔ o0 = o1 ∧ a0 = a1 ∧ (r.=>_ * hR)[rs, λ r. (f(r), g(r))]), rs ≠ ∅, r ∈ rs ⊦

Rule argument

Additional information

Proof step 7 from proof map-putrev (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  (r => (o0, a0) * hR)[rs, λ r0. (r0 = r ⊃ (o1, a1);(f(r0), g(r0)))] ↔ o0 = o1 ∧ a0 = a1 ∧ (r.=>_ * hR)[rs, λ r. (f(r), g(r))], # rs ≠ 0, ¬ ((r => (o0, a0) * hR)[rs, λ r0. ((r = r0 ⊃ o1;f(r0)), (r = r0 ⊃ a1;g(r0)))] ↔ (r => (o0, a0) * hR)[rs, λ r0. (r0 = r ⊃ (o1, a1);(f(r0), g(r0)))]), rs ≠ ∅, r ∈ rs ⊦

Rule argument

Additional information

Proof step 8 from proof map-putrev (previous step) (back to tree)

User applied rule reduce equation

And obtained the following new goals

• Proof step 9:

  (r => (o0, a0) * hR)[rs, λ r0. (r0 = r ⊃ (o1, a1);(f(r0), g(r0)))] ↔ o0 = o1 ∧ a0 = a1 ∧ (r.=>_ * hR)[rs, λ r. (f(r), g(r))], # rs ≠ 0, (λ r0. ((r = r0 ⊃ o1;f(r0)), (r = r0 ⊃ a1;g(r0)))) ≠ (λ r0. (r0 = r ⊃ (o1, a1);(f(r0), g(r0)))), rs ≠ ∅, r ∈ rs ⊦

Rule argument

Additional information

Proof step 9 from proof map-putrev (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  (r => (o0, a0) * hR)[rs, λ r0. (r0 = r ⊃ (o1, a1);(f(r0), g(r0)))] ↔ o0 = o1 ∧ a0 = a1 ∧ (r.=>_ * hR)[rs, λ r. (f(r), g(r))], # rs ≠ 0, ((r = r0 ⊃ o1;f(r0)), (r = r0 ⊃ a1;g(r0))) ≠ (r0 = r ⊃ (o1, a1);(f(r0), g(r0))), rs ≠ ∅, r ∈ rs ⊦

Rule argument

Additional information

Proof step 10 from proof map-putrev (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information