---

Step * 2 of Lemma bool-cmp_wf


1. ∀x,y:𝔹.
     (if x then if y then 0 else 1 fi 
     if y then -1
     else 0
     fi 
     = (-if y then if x then 0 else 1 fi 
       if x then -1
       else 0
       fi )
     ∈ ℤ)
2. ∀x,y:𝔹.
     ((if x then if y then 0 else 1 fi  if y then -1 else 0 fi  = 0 ∈ ℤ)
     ⇒ (∀z:𝔹
           (if x then if z then 0 else 1 fi 
           if z then -1
           else 0
           fi 
           = if y then if z then 0 else 1 fi 
             if z then -1
             else 0
             fi 
           ∈ ℤ)))
3. x : 𝔹
4. y : 𝔹
5. z : 𝔹
6. 0 ≤ if x then if y then 0 else 1 fi 
   if y then -1
   else 0
   fi 
7. 0 ≤ if y then if z then 0 else 1 fi 
   if z then -1
   else 0
   fi 
⊢ 0 ≤ if x then if z then 0 else 1 fi 
  if z then -1
  else 0
  fi 
BY
{ (RepeatFor 3 (BoolInd' 3) THEN All Reduce THEN Auto) }

---

Latex:

---

Latex:

1.  \mforall{}x,y:\mBbbB{}.
          (if  x  then  if  y  then  0  else  1  fi 
          if  y  then  -1
          else  0
          fi 
          =  (-if  y  then  if  x  then  0  else  1  fi 
              if  x  then  -1
              else  0
              fi  ))
2.  \mforall{}x,y:\mBbbB{}.
          ((if  x  then  if  y  then  0  else  1  fi    if  y  then  -1  else  0  fi    =  0)
          {}\mRightarrow{}  (\mforall{}z:\mBbbB{}
                      (if  x  then  if  z  then  0  else  1  fi 
                      if  z  then  -1
                      else  0
                      fi 
                      =  if  y  then  if  z  then  0  else  1  fi 
                          if  z  then  -1
                          else  0
                          fi  )))
3.  x  :  \mBbbB{}
4.  y  :  \mBbbB{}
5.  z  :  \mBbbB{}
6.  0  \mleq{}  if  x  then  if  y  then  0  else  1  fi 
      if  y  then  -1
      else  0
      fi 
7.  0  \mleq{}  if  y  then  if  z  then  0  else  1  fi 
      if  z  then  -1
      else  0
      fi 
\mvdash{}  0  \mleq{}  if  x  then  if  z  then  0  else  1  fi 
    if  z  then  -1
    else  0
    fi 


By

---

Latex:
(RepeatFor  3  (BoolInd'  3)  THEN  All  Reduce  THEN  Auto)

---

Home Index