---

Step * of Lemma ranked-eo-eq-E

∀[L,rk:Top]. ∀[a,b:Top × ℤ].  (a = b ~ fst(a) = fst(b) ∧b (snd(a) =z snd(b)))
BY
{ (Auto
   THEN RepUR ``es-eq-E es-eq es-locless`` 0
   THEN (RWO "ranked-eo-loc" 0 THENA Auto)
   THEN RepUR ``ranked-eo mk-extended-eo mk-eo mk-eo-record`` 0
   THEN DProds
   THEN Reduce 0) }

1
1. L : Top
2. rk : Top
3. a1 : Top
4. a2 : ℤ
5. b1 : Top
6. b2 : ℤ
⊢ a1 = b1 ∧b (¬ba2 <z b2) ∧b (¬bb2 <z a2) ~ a1 = b1 ∧b (a2 =z b2)

---

Latex:

---

Latex:
\mforall{}[L,rk:Top].  \mforall{}[a,b:Top  \mtimes{}  \mBbbZ{}].    (a  =  b  \msim{}  fst(a)  =  fst(b)  \mwedge{}\msubb{}  (snd(a)  =\msubz{}  snd(b)))


By

---

Latex:
(Auto
  THEN  RepUR  ``es-eq-E  es-eq  es-locless``  0
  THEN  (RWO  "ranked-eo-loc"  0  THENA  Auto)
  THEN  RepUR  ``ranked-eo  mk-extended-eo  mk-eo  mk-eo-record``  0
  THEN  DProds
  THEN  Reduce  0)

---

Home Index