---

Step * 1 of Lemma comparison-seq_wf


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)
∈ ℤ
BY
{ (((CallByValueReduce 0⋅ THENA Auto)
    THEN D 3
    THEN (InstHyp [⌜x⌝;⌜y⌝] 3⋅ THENA Auto)
    THEN HypSubst' (-1) 0
    THEN (Decide ⌜(c1 y x) = 0 ∈ ℤ⌝⋅ THENA Auto)
    THEN (OReduce 0 THENA Auto)
    THEN ((HypSubst' (-1) 0 THEN Reduce 0) ORELSE ((Assert ¬((-(c1 y x)) = 0 ∈ ℤ) BY Auto) THEN OReduce 0 THEN Auto)))
   THEN (GenConcl ⌜c2 = C ∈ comparison({b:T| (c1 x b) = 0 ∈ ℤ} )⌝⋅ THENA Auto)
   THEN D -2
   THEN D -2
   THEN BHyp -3
   THEN MemTypeCD
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  c1  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbZ{}
3.  (\mforall{}x,y:T.    ((c1  x  y)  =  (-(c1  y  x))))
\mwedge{}  (\mforall{}x,y:T.    (((c1  x  y)  =  0)  {}\mRightarrow{}  (\mforall{}z:T.  ((c1  x  z)  =  (c1  y  z)))))
\mwedge{}  (\mforall{}x,y,z:T.    ((0  \mleq{}  (c1  x  y))  {}\mRightarrow{}  (0  \mleq{}  (c1  y  z))  {}\mRightarrow{}  (0  \mleq{}  (c1  x  z))))
4.  c2  :  \mcap{}a:T.  comparison(\{b:T|  (c1  a  b)  =  0\}  )
5.  x  :  T
6.  y  :  T
\mvdash{}  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)


By

---

Latex:
(((CallByValueReduce  0\mcdot{}  THENA  Auto)
    THEN  D  3
    THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  3\mcdot{}  THENA  Auto)
    THEN  HypSubst'  (-1)  0
    THEN  (Decide  \mkleeneopen{}(c1  y  x)  =  0\mkleeneclose{}\mcdot{}  THENA  Auto)
    THEN  (OReduce  0  THENA  Auto)
    THEN  ((HypSubst'  (-1)  0  THEN  Reduce  0)
    ORELSE  ((Assert  \mneg{}((-(c1  y  x))  =  0)  BY  Auto)  THEN  OReduce  0  THEN  Auto)
    ))
  THEN  (GenConcl  \mkleeneopen{}c2  =  C\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  D  -2
  THEN  BHyp  -3
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index