---

Step * of Lemma comparison-seq_wf

∀[T:Type]. ∀[c1:comparison(T)]. ∀[c2:⋂a:T. comparison({b:T| (c1 a b) = 0 ∈ ℤ} )].  (comparison-seq(c1; c2) ∈ comparison(\000CT))
BY
{ (Auto
   THEN D -2
   THEN Unfold `comparison-seq` 0
   THEN MemTypeCD
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN SplitAndConcl
   THEN Try ((Auto
              THEN (Assert (c1 x x) = 0 ∈ ℤ BY
                          (InstHyp [⌜x⌝;⌜x⌝] 3⋅ THEN Auto'))
              THEN GenConcl ⌜c2 = C ∈ comparison({b:T| (c1 x b) = 0 ∈ ℤ} )⌝⋅
              THEN Complete (Auto)))
   THEN RepeatFor 2 ((D 0 THENA Auto))) }

1
1. T : Type
2. c1 : T ⟶ T ⟶ ℤ
3. (∀x,y:T.  ((c1 x y) = (-(c1 y x)) ∈ ℤ))
∧ (∀x,y:T.  (((c1 x y) = 0 ∈ ℤ) ⇒ (∀z:T. ((c1 x z) = (c1 y z) ∈ ℤ))))
∧ (∀x,y,z:T.  ((0 ≤ (c1 x y)) ⇒ (0 ≤ (c1 y z)) ⇒ (0 ≤ (c1 x z))))
4. c2 : ⋂a:T. comparison({b:T| (c1 a b) = 0 ∈ ℤ} )
5. x : T
6. y : T
⊢ eval answer1 = c1 x y in
  if answer1=0 then c2 x y else answer1
= (-eval answer1 = c1 y x in
    if answer1=0 then c2 y x else answer1)
∈ ℤ

2
1. T : Type
2. c1 : T ⟶ T ⟶ ℤ
3. (∀x,y:T.  ((c1 x y) = (-(c1 y x)) ∈ ℤ))
∧ (∀x,y:T.  (((c1 x y) = 0 ∈ ℤ) ⇒ (∀z:T. ((c1 x z) = (c1 y z) ∈ ℤ))))
∧ (∀x,y,z:T.  ((0 ≤ (c1 x y)) ⇒ (0 ≤ (c1 y z)) ⇒ (0 ≤ (c1 x z))))
4. c2 : ⋂a:T. comparison({b:T| (c1 a b) = 0 ∈ ℤ} )
5. x : T
6. y : T
⊢ (eval answer1 = c1 x y in if answer1=0 then c2 x y else answer1 = 0 ∈ ℤ)
⇒ (∀z:T
      (eval answer1 = c1 x z in
       if answer1=0 then c2 x z else answer1
      = eval answer1 = c1 y z in
        if answer1=0 then c2 y z else answer1
      ∈ ℤ))

3
1. T : Type
2. c1 : T ⟶ T ⟶ ℤ
3. (∀x,y:T.  ((c1 x y) = (-(c1 y x)) ∈ ℤ))
∧ (∀x,y:T.  (((c1 x y) = 0 ∈ ℤ) ⇒ (∀z:T. ((c1 x z) = (c1 y z) ∈ ℤ))))
∧ (∀x,y,z:T.  ((0 ≤ (c1 x y)) ⇒ (0 ≤ (c1 y z)) ⇒ (0 ≤ (c1 x z))))
4. c2 : ⋂a:T. comparison({b:T| (c1 a b) = 0 ∈ ℤ} )
5. x : T
6. y : T
⊢ ∀z:T
    ((0 ≤ eval answer1 = c1 x y in
          if answer1=0 then c2 x y else answer1)
    ⇒ (0 ≤ eval answer1 = c1 y z in
            if answer1=0 then c2 y z else answer1)
    ⇒ (0 ≤ eval answer1 = c1 x z in
            if answer1=0 then c2 x z else answer1))

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  D  -2
  THEN  Unfold  `comparison-seq`  0
  THEN  MemTypeCD
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  SplitAndConcl
  THEN  Try  ((Auto
                        THEN  (Assert  (c1  x  x)  =  0  BY
                                                (InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  3\mcdot{}  THEN  Auto'))
                        THEN  GenConcl  \mkleeneopen{}c2  =  C\mkleeneclose{}\mcdot{}
                        THEN  Complete  (Auto)))
  THEN  RepeatFor  2  ((D  0  THENA  Auto)))

---

Home Index