---

Step * of Lemma rational_set_blt

No Annotations
∀[r,s:ℚ].
  (r <b s ~ if isint(r)
  then if isint(s) then r <z s else let i,j = s in if 0 <z j then j * r <z i else i <z j * r fi  fi 
  else let p,q = r 
       in if isint(s)
          then if 0 <z q then p <z q * s else q * s <z p fi 
          else let i,j = s 
               in if 0 <z q * j then j * p <z q * i else q * i <z j * p fi 
          fi 
  fi )
BY
{ (Intros
   THEN Assert ⌜r <b s 
                = if isint(r)
                  then if isint(s) then r <z s else let i,j = s in if 0 <z j then j * r <z i else i <z j * r fi  fi 
                  else let p,q = r 
                       in if isint(s)
                          then if 0 <z q then p <z q * s else q * s <z p fi 
                          else let i,j = s 
                               in if 0 <z q * j then j * p <z q * i else q * i <z j * p fi 
                          fi 
                  fi ⌝⋅
   THEN Try ((TACTIC:UseWitness ⌜Ax⌝⋅ THEN RevHypSubst' (-1) 0 THEN Auto))
   THEN (DVar `r' THEN Try (QuickAuto))
   THEN DVar `s'
   THEN Try (QuickAuto)
   THEN Subst' r <b s ~ r1 <b s1 0
   THEN Try (Try (Complete ((TACTIC:(Assert r = r1 ∈ ℚ BY
                                           (EqTypeCD THEN Auto))
                             THEN TACTIC:((Assert s = s1 ∈ ℚ BY (EqTypeCD THEN Auto)) THEN Auto)
                             ))))
   THEN GenConclTerms Auto [⌜r1⌝;⌜s1⌝]⋅
   THEN All Thin
   THEN All D_rational_form⋅
   THEN Reduce 0
   THEN Auto
   THEN RepUR ``q_less grp_lt set_lt set_blt q_le`` 0
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN (RWO "qeq-elim" 0 THENA Auto)
   THEN (Reduce 0 THENA Auto)
   THEN (RWO "qpositive-elim" 0 THENA Auto)
   THEN Reduce 0
   THEN RepUR ``qsub`` 0
   THEN (RWO "qadd-elim" 0 THENA Auto)
   THEN (Reduce 0 THENA Auto)
   THEN (RWO "qmul-elim" 0 THENA Auto)
   THEN (Reduce 0 THENA Auto)
   THEN Repeat (((RW (LowerC (LemmaC `isint-int`)) 0 THENA Complete (Auto)) THEN Reduce 0))) }

1
1. a2 : ℤ
2. a1 : ℤ
⊢ (0 <z a1 + ((-1) * a2) ∨b(a2 =z a1)) ∧b (¬b(0 <z a2 + ((-1) * a1) ∨b(a1 =z a2))) = a2 <z a1

2
1. a3 : ℤ
2. a4 : ℤ-o
3. a1 : ℤ
⊢ (((0 <z (a1 * a4) + ((-1) * a3) ∧b 0 <z a4) ∨b((a1 * a4) + ((-1) * a3) <z 0 ∧b a4 <z 0)) ∨b(a3 =z a1 * a4))
  ∧b (¬b(((0 <z a3 + (((-1) * a1) * a4) ∧b 0 <z a4) ∨b(a3 + (((-1) * a1) * a4) <z 0 ∧b a4 <z 0)) ∨b(a1 * a4 =z a3))) 
= if 0 <z a4 then a3 <z a4 * a1 else a4 * a1 <z a3 fi 

3
1. a4 : ℤ
2. a2 : ℤ
3. a3 : ℤ-o
⊢ (((0 <z a2 + (((-1) * a4) * a3) ∧b 0 <z a3) ∨b(a2 + (((-1) * a4) * a3) <z 0 ∧b a3 <z 0)) ∨b(a4 * a3 =z a2))
  ∧b (¬b(((0 <z (a4 * a3) + ((-1) * a2) ∧b 0 <z a3) ∨b((a4 * a3) + ((-1) * a2) <z 0 ∧b a3 <z 0)) ∨b(a2 =z a4 * a3))) 
= if 0 <z a3 then a3 * a4 <z a2 else a2 <z a3 * a4 fi 

4
1. a5 : ℤ
2. a6 : ℤ-o
3. a2 : ℤ
4. a3 : ℤ-o
⊢ (((0 <z (a2 * a6) + (((-1) * a5) * a3) ∧b 0 <z a3 * a6) ∨b((a2 * a6) + (((-1) * a5) * a3) <z 0 ∧b a3 * a6 <z 0))
  ∨b(a5 * a3 =z a2 * a6))
  ∧b (¬b(((0 <z (a5 * a3) + (((-1) * a2) * a6) ∧b 0 <z a6 * a3) ∨b((a5 * a3) + (((-1) * a2) * a6) <z 0 ∧b a6 * a3 <z 0))
     ∨b(a2 * a6 =z a5 * a3))) 
= if 0 <z a6 * a3 then a3 * a5 <z a6 * a2 else a6 * a2 <z a3 * a5 fi 

---

Latex:

---

Latex:
No  Annotations
\mforall{}[r,s:\mBbbQ{}].
    (r  <\msubb{}  s  \msim{}  if  isint(r)
    then  if  isint(s)  then  r  <z  s  else  let  i,j  =  s  in  if  0  <z  j  then  j  *  r  <z  i  else  i  <z  j  *  r  fi    fi 
    else  let  p,q  =  r 
              in  if  isint(s)
                    then  if  0  <z  q  then  p  <z  q  *  s  else  q  *  s  <z  p  fi 
                    else  let  i,j  =  s 
                              in  if  0  <z  q  *  j  then  j  *  p  <z  q  *  i  else  q  *  i  <z  j  *  p  fi 
                    fi 
    fi  )


By

---

Latex:
(Intros
  THEN  Assert  \mkleeneopen{}r  <\msubb{}  s 
                            =  if  isint(r)
                                then  if  isint(s)
                                          then  r  <z  s
                                          else  let  i,j  =  s 
                                                    in  if  0  <z  j  then  j  *  r  <z  i  else  i  <z  j  *  r  fi 
                                          fi 
                                else  let  p,q  =  r 
                                          in  if  isint(s)
                                                then  if  0  <z  q  then  p  <z  q  *  s  else  q  *  s  <z  p  fi 
                                                else  let  i,j  =  s 
                                                          in  if  0  <z  q  *  j  then  j  *  p  <z  q  *  i  else  q  *  i  <z  j  *  p  fi 
                                                fi 
                                fi  \mkleeneclose{}\mcdot{}
  THEN  Try  ((TACTIC:UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}  THEN  RevHypSubst'  (-1)  0  THEN  Auto))
  THEN  (DVar  `r'  THEN  Try  (QuickAuto))
  THEN  DVar  `s'
  THEN  Try  (QuickAuto)
  THEN  Subst'  r  <\msubb{}  s  \msim{}  r1  <\msubb{}  s1  0
  THEN  Try  (Try  (Complete  ((TACTIC:(Assert  r  =  r1  BY
                                                                                  (EqTypeCD  THEN  Auto))
                                                      THEN  TACTIC:((Assert  s  =  s1  BY  (EqTypeCD  THEN  Auto))  THEN  Auto)
                                                      ))))
  THEN  GenConclTerms  Auto  [\mkleeneopen{}r1\mkleeneclose{};\mkleeneopen{}s1\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  All  D\_rational\_form\mcdot{}
  THEN  Reduce  0
  THEN  Auto
  THEN  RepUR  ``q\_less  grp\_lt  set\_lt  set\_blt  q\_le``  0
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  (RWO  "qeq-elim"  0  THENA  Auto)
  THEN  (Reduce  0  THENA  Auto)
  THEN  (RWO  "qpositive-elim"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  RepUR  ``qsub``  0
  THEN  (RWO  "qadd-elim"  0  THENA  Auto)
  THEN  (Reduce  0  THENA  Auto)
  THEN  (RWO  "qmul-elim"  0  THENA  Auto)
  THEN  (Reduce  0  THENA  Auto)
  THEN  Repeat  (((RW  (LowerC  (LemmaC  `isint-int`))  0  THENA  Complete  (Auto))  THEN  Reduce  0)))

---

Home Index