---

Step * 2 1 of Lemma assert-dlo_eq


1. x : Prog
2. x1 : Prog
3. ∀b:dl-Obj(). (↑dlo_eq(prog(x);b) ⇐⇒ prog(x) = b ∈ dl-Obj())
4. ∀b:dl-Obj(). (↑dlo_eq(prog(x1);b) ⇐⇒ prog(x1) = b ∈ dl-Obj())
5. x@0 : Prog
6. x1@0 : Prog
7. (↑dlo_eq(prog((x;x1));prog(x@0))) ⇒ (prog((x;x1)) = prog(x@0) ∈ dl-Obj())
8. (↑dlo_eq(prog((x;x1));prog(x@0))) ⇐ prog((x;x1)) = prog(x@0) ∈ dl-Obj()
9. (↑dlo_eq(prog((x;x1));prog(x1@0))) ⇒ (prog((x;x1)) = prog(x1@0) ∈ dl-Obj())
10. (↑dlo_eq(prog((x;x1));prog(x1@0))) ⇐ prog((x;x1)) = prog(x1@0) ∈ dl-Obj()
11. ↑(dlo_eq(prog(x);prog(x@0)) ∧b dlo_eq(prog(x1);prog(x1@0)))
⊢ prog((x;x1)) = prog((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  :  Prog
3.  \mforall{}b:dl-Obj().  (\muparrow{}dlo\_eq(prog(x);b)  \mLeftarrow{}{}\mRightarrow{}  prog(x)  =  b)
4.  \mforall{}b:dl-Obj().  (\muparrow{}dlo\_eq(prog(x1);b)  \mLeftarrow{}{}\mRightarrow{}  prog(x1)  =  b)
5.  x@0  :  Prog
6.  x1@0  :  Prog
7.  (\muparrow{}dlo\_eq(prog((x;x1));prog(x@0)))  {}\mRightarrow{}  (prog((x;x1))  =  prog(x@0))
8.  (\muparrow{}dlo\_eq(prog((x;x1));prog(x@0)))  \mLeftarrow{}{}  prog((x;x1))  =  prog(x@0)
9.  (\muparrow{}dlo\_eq(prog((x;x1));prog(x1@0)))  {}\mRightarrow{}  (prog((x;x1))  =  prog(x1@0))
10.  (\muparrow{}dlo\_eq(prog((x;x1));prog(x1@0)))  \mLeftarrow{}{}  prog((x;x1))  =  prog(x1@0)
11.  \muparrow{}(dlo\_eq(prog(x);prog(x@0))  \mwedge{}\msubb{}  dlo\_eq(prog(x1);prog(x1@0)))
\mvdash{}  prog((x;x1))  =  prog((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