---

Step * 9 1 of Lemma assert-dlo_eq


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