---

Step * of Lemma bool-cmp_wf

bool-cmp() ∈ comparison(𝔹)
BY
{ (ProveWfLemma THEN MemTypeCD THEN Reduce 0 THEN Auto) }

1
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 
∈ ℤ

2
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 

---

Latex:

---

Latex:
bool-cmp()  \mmember{}  comparison(\mBbbB{})


By

---

Latex:
(ProveWfLemma  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto)

---

Home Index