---

Step * of Lemma base-disjoint-classrel

∀A,B:Type. ∀f:Name ⟶ Type. ∀es:EO+(Message(f)). ∀hdr1,hdr2:Name.
  ((¬(hdr1 = hdr2 ∈ Name)) ⇒ hdr1 encodes A ⇒ hdr2 encodes B ⇒ disjoint-classrel(es;A;Base(hdr1);B;Base(hdr2)))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `disjoint-classrel` 0
   THEN Auto
   THEN (Assert ⌜Dec(header(e) = hdr1 ∈ Name)⌝⋅ THENA Auto)
   THEN D (-1)
   THEN Try (Complete (((OrRight THEN Auto) THEN (D 0 THENA Auto) THEN MaUseClassRel (-1))))
   THEN (OrLeft THEN Auto)
   THEN (D 0 THENA Auto)
   THEN MaUseClassRel (-1)
   THEN HypSubst' (-3) (-5)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}A,B:Type.  \mforall{}f:Name  {}\mrightarrow{}  Type.  \mforall{}es:EO+(Message(f)).  \mforall{}hdr1,hdr2:Name.
    ((\mneg{}(hdr1  =  hdr2))
    {}\mRightarrow{}  hdr1  encodes  A
    {}\mRightarrow{}  hdr2  encodes  B
    {}\mRightarrow{}  disjoint-classrel(es;A;Base(hdr1);B;Base(hdr2)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `disjoint-classrel`  0
  THEN  Auto
  THEN  (Assert  \mkleeneopen{}Dec(header(e)  =  hdr1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  Try  (Complete  (((OrRight  THEN  Auto)  THEN  (D  0  THENA  Auto)  THEN  MaUseClassRel  (-1))))
  THEN  (OrLeft  THEN  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  MaUseClassRel  (-1)
  THEN  HypSubst'  (-3)  (-5)
  THEN  Auto)

---

Home Index