---

Step * 2 of Lemma equipollent-two


1. b : ℕ2
⊢ ∃a:𝔹. (if a then 1 else 0 fi  = b ∈ ℕ2)
BY
{ (IntSegCases 1
   THEN (Complete ((With ⌜ff⌝ (D 0)⋅ THEN Reduce 0 THEN Auto))
        ORELSE Complete ((With ⌜tt⌝ (D 0)⋅ THEN Reduce 0 THEN Auto))
        )
   ) }

---

Latex:

---

Latex:

1.  b  :  \mBbbN{}2
\mvdash{}  \mexists{}a:\mBbbB{}.  (if  a  then  1  else  0  fi    =  b)


By

---

Latex:
(IntSegCases  1
  THEN  (Complete  ((With  \mkleeneopen{}ff\mkleeneclose{}  (D  0)\mcdot{}  THEN  Reduce  0  THEN  Auto))
            ORELSE  Complete  ((With  \mkleeneopen{}tt\mkleeneclose{}  (D  0)\mcdot{}  THEN  Reduce  0  THEN  Auto))
            )
  )

---

Home Index