---

Step * 3 2 of Lemma rational_set_blt


1. a4 : ℤ
2. a2 : ℤ
3. a3 : ℤ-o
4. ¬0 < a3
⊢ (((0 <z a2 + (((-1) * a4) * a3) ∧b ff) ∨b(a2 + (((-1) * a4) * a3) <z 0 ∧b tt)) ∨b(a4 * a3 =z a2))
  ∧b (¬b(((0 <z (a4 * a3) + ((-1) * a2) ∧b ff) ∨b((a4 * a3) + ((-1) * a2) <z 0 ∧b tt)) ∨b(a2 =z a4 * a3))) 
= a2 <z a3 * a4
BY
{ ((RWW "band_ff_simp band_tt_simp bor_ff_simp" 0 THENA Auto)
   THEN Reduce 0
   THEN (BLemma `iff_imp_equal_bool` THENM RW assert_pushdownC 0)
   THEN Auto) }

---

Latex:

---

Latex:

1.  a4  :  \mBbbZ{}
2.  a2  :  \mBbbZ{}
3.  a3  :  \mBbbZ{}\msupminus{}\msupzero{}
4.  \mneg{}0  <  a3
\mvdash{}  (((0  <z  a2  +  (((-1)  *  a4)  *  a3)  \mwedge{}\msubb{}  ff)  \mvee{}\msubb{}(a2  +  (((-1)  *  a4)  *  a3)  <z  0  \mwedge{}\msubb{}  tt))  \mvee{}\msubb{}(a4  *  a3  =\msubz{}  a2))
    \mwedge{}\msubb{}  (\mneg{}\msubb{}(((0  <z  (a4  *  a3)  +  ((-1)  *  a2)  \mwedge{}\msubb{}  ff)  \mvee{}\msubb{}((a4  *  a3)  +  ((-1)  *  a2)  <z  0  \mwedge{}\msubb{}  tt))
          \mvee{}\msubb{}(a2  =\msubz{}  a4  *  a3))) 
=  a2  <z  a3  *  a4


By

---

Latex:
((RWW  "band\_ff\_simp  band\_tt\_simp  bor\_ff\_simp"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (BLemma  `iff\_imp\_equal\_bool`  THENM  RW  assert\_pushdownC  0)
  THEN  Auto)

---

Home Index