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