Step * of Lemma comparison-seq_wf

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

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

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

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