---

Step * of Lemma comparison-seq-zero

∀[T:Type]. ∀[c1:comparison(T)]. ∀[c2:⋂a:T. comparison({b:T| (c1 a b) = 0 ∈ ℤ} )]. ∀[x,y:T].
  uiff((comparison-seq(c1; c2) x y) = 0 ∈ ℤ;((c1 x y) = 0 ∈ ℤ) ∧ ((c2 x y) = 0 ∈ ℤ))
BY
{ (Intros
   THEN RepUR ``comparison-seq`` 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN (Unhide THENA Auto)
   THEN Try (((With ⌜x⌝ (D 3)⋅ THEN Auto)
              THEN (GenConcl ⌜c2 = X ∈ comparison({b:T| (c1 x b) = 0 ∈ ℤ} )⌝⋅ THEN Auto)
              THEN MemTypeCD
              THEN Auto
              THEN BLemma `comparison-reflexive`
              THEN Auto))) }

1
1. T : Type
2. c1 : comparison(T)
3. c2 : ⋂a:T. comparison({b:T| (c1 a b) = 0 ∈ ℤ} )
4. x : T
5. y : T
⊢ uiff(if c1 x y=0  then c2 x y  else (c1 x y) = 0 ∈ ℤ;((c1 x y) = 0 ∈ ℤ) ∧ ((c2 x y) = 0 ∈ ℤ))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[c1:comparison(T)].  \mforall{}[c2:\mcap{}a:T.  comparison(\{b:T|  (c1  a  b)  =  0\}  )].  \mforall{}[x,y:T].
    uiff((comparison-seq(c1;  c2)  x  y)  =  0;((c1  x  y)  =  0)  \mwedge{}  ((c2  x  y)  =  0))


By

---

Latex:
(Intros
  THEN  RepUR  ``comparison-seq``  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  (Unhide  THENA  Auto)
  THEN  Try  (((With  \mkleeneopen{}x\mkleeneclose{}  (D  3)\mcdot{}  THEN  Auto)
                        THEN  (GenConcl  \mkleeneopen{}c2  =  X\mkleeneclose{}\mcdot{}  THEN  Auto)
                        THEN  MemTypeCD
                        THEN  Auto
                        THEN  BLemma  `comparison-reflexive`
                        THEN  Auto)))

---

Home Index