---

Step * 11 1 of Lemma assert-dlo_eq


1. x : Prog
2. x1 : Prop
3. ∀b:dl-Obj(). (↑dlo_eq(prog(x);b) ⇐⇒ prog(x) = b ∈ dl-Obj())
4. ∀b:dl-Obj(). (↑dlo_eq(prop(x1);b) ⇐⇒ prop(x1) = b ∈ dl-Obj())
5. x@0 : Prog
6. x1@0 : Prop
7. (↑dlo_eq(prop([x] x1);prog(x@0))) ⇒ (prop([x] x1) = prog(x@0) ∈ dl-Obj())
8. (↑dlo_eq(prop([x] x1);prog(x@0))) ⇐ prop([x] x1) = prog(x@0) ∈ dl-Obj()
9. (↑dlo_eq(prop([x] x1);prop(x1@0))) ⇒ (prop([x] x1) = prop(x1@0) ∈ dl-Obj())
10. (↑dlo_eq(prop([x] x1);prop(x1@0))) ⇐ prop([x] x1) = prop(x1@0) ∈ dl-Obj()
11. ↑(dlo_eq(prog(x);prog(x@0)) ∧b dlo_eq(prop(x1);prop(x1@0)))
⊢ prop([x] x1) = prop([x@0] x1@0) ∈ dl-Obj()
BY
{ ((RW assert_pushdownC (-1) THENA Auto)
   THEN D -1
   THEN ThinTrivial
   THEN (RWO "3 4" (-1) THENA Auto)
   THEN (RWO "3 4" (-2) THENA Auto)
   THEN EqCD
   THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  Prog
2.  x1  :  Prop
3.  \mforall{}b:dl-Obj().  (\muparrow{}dlo\_eq(prog(x);b)  \mLeftarrow{}{}\mRightarrow{}  prog(x)  =  b)
4.  \mforall{}b:dl-Obj().  (\muparrow{}dlo\_eq(prop(x1);b)  \mLeftarrow{}{}\mRightarrow{}  prop(x1)  =  b)
5.  x@0  :  Prog
6.  x1@0  :  Prop
7.  (\muparrow{}dlo\_eq(prop([x]  x1);prog(x@0)))  {}\mRightarrow{}  (prop([x]  x1)  =  prog(x@0))
8.  (\muparrow{}dlo\_eq(prop([x]  x1);prog(x@0)))  \mLeftarrow{}{}  prop([x]  x1)  =  prog(x@0)
9.  (\muparrow{}dlo\_eq(prop([x]  x1);prop(x1@0)))  {}\mRightarrow{}  (prop([x]  x1)  =  prop(x1@0))
10.  (\muparrow{}dlo\_eq(prop([x]  x1);prop(x1@0)))  \mLeftarrow{}{}  prop([x]  x1)  =  prop(x1@0)
11.  \muparrow{}(dlo\_eq(prog(x);prog(x@0))  \mwedge{}\msubb{}  dlo\_eq(prop(x1);prop(x1@0)))
\mvdash{}  prop([x]  x1)  =  prop([x@0]  x1@0)


By

---

Latex:
((RW  assert\_pushdownC  (-1)  THENA  Auto)
  THEN  D  -1
  THEN  ThinTrivial
  THEN  (RWO  "3  4"  (-1)  THENA  Auto)
  THEN  (RWO  "3  4"  (-2)  THENA  Auto)
  THEN  EqCD
  THEN  Auto)

---

Home Index