Step * 2 1 of Lemma equipollent-add


1. : ℕ@i
2. : ℕ@i
3. b@0 : ℕb@i
4. b@0 < a
⊢ ∃a@0:ℕ+ ℕb. (case a@0 of inl(x) => inr(y) => b@0 ∈ ℕb)
BY
((InstConcl [⌜inl b@0⌝]⋅ THEN Reduce 0) THEN Auto') }


Latex:


Latex:

1.  a  :  \mBbbN{}@i
2.  b  :  \mBbbN{}@i
3.  b@0  :  \mBbbN{}a  +  b@i
4.  b@0  <  a
\mvdash{}  \mexists{}a@0:\mBbbN{}a  +  \mBbbN{}b.  (case  a@0  of  inl(x)  =>  x  |  inr(y)  =>  a  +  y  =  b@0)


By


Latex:
((InstConcl  [\mkleeneopen{}inl  b@0\mkleeneclose{}]\mcdot{}  THEN  Reduce  0)  THEN  Auto')




Home Index