---

Step * 1 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 : 𝔹
3. y : 𝔹
4. if x then if y then 0 else 1 fi  if y then -1 else 0 fi  = 0 ∈ ℤ
5. 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 
∈ ℤ
BY
{ (RepeatFor 2 (BoolInd' 2) 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.  x  :  \mBbbB{}
3.  y  :  \mBbbB{}
4.  if  x  then  if  y  then  0  else  1  fi    if  y  then  -1  else  0  fi    =  0
5.  z  :  \mBbbB{}
\mvdash{}  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 


By

---

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

---

Home Index