---

Step * 2 1 of Lemma rational_set_blt


1. a3 : ℤ
2. a4 : ℤ-o
3. a1 : ℤ
4. 0 < a4
⊢ (((0 <z (a1 * a4) + ((-1) * a3) ∧b tt) ∨b((a1 * a4) + ((-1) * a3) <z 0 ∧b ff)) ∨b(a3 =z a1 * a4))
  ∧b (¬b(((0 <z a3 + (((-1) * a1) * a4) ∧b tt) ∨b(a3 + (((-1) * a1) * a4) <z 0 ∧b ff)) ∨b(a1 * a4 =z a3))) 
= a3 <z a4 * a1
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.  a3  :  \mBbbZ{}
2.  a4  :  \mBbbZ{}\msupminus{}\msupzero{}
3.  a1  :  \mBbbZ{}
4.  0  <  a4
\mvdash{}  (((0  <z  (a1  *  a4)  +  ((-1)  *  a3)  \mwedge{}\msubb{}  tt)  \mvee{}\msubb{}((a1  *  a4)  +  ((-1)  *  a3)  <z  0  \mwedge{}\msubb{}  ff))  \mvee{}\msubb{}(a3  =\msubz{}  a1  *  a4))
    \mwedge{}\msubb{}  (\mneg{}\msubb{}(((0  <z  a3  +  (((-1)  *  a1)  *  a4)  \mwedge{}\msubb{}  tt)  \mvee{}\msubb{}(a3  +  (((-1)  *  a1)  *  a4)  <z  0  \mwedge{}\msubb{}  ff))
          \mvee{}\msubb{}(a1  *  a4  =\msubz{}  a3))) 
=  a3  <z  a4  *  a1


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