---

Step * of Lemma comparison-seq-zero-simple

∀[T:Type]. ∀[c1,c2:comparison(T)]. ∀[x,y:T].
  uiff((comparison-seq(c1; c2) x y) = 0 ∈ ℤ;((c1 x y) = 0 ∈ ℤ) ∧ ((c2 x y) = 0 ∈ ℤ))
BY
{ (InstLemma `comparison-seq-zero` [] THEN RepeatFor 3 (ParallelLast)) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `comparison-seq-zero`  []  THEN  RepeatFor  3  (ParallelLast))

---

Home Index