---

Step * 2 1 1 1 2 1 of Lemma equipollent-exp

.....truecase..... 
1. n : ℤ
2. 0 < n
3. ∀b:ℕ. ℕn - 1 ⟶ ℕb ~ ℕb^(n - 1)
4. 1 ≤ n
5. b : ℕ
6. b1 : ℕb
7. b2 : ℕn - 1 ⟶ ℕb
8. (n - 1) = (n - 1) ∈ ℤ
⊢ <b1, λx.if (x =z n - 1) then b1 else b2 x fi > = <b1, b2> ∈ (ℕb × (ℕn - 1 ⟶ ℕb))
BY
{ (EqCD THEN Auto)⋅ }

---

Latex:

---

Latex:
.....truecase..... 
1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}b:\mBbbN{}.  \mBbbN{}n  -  1  {}\mrightarrow{}  \mBbbN{}b  \msim{}  \mBbbN{}b\^{}(n  -  1)
4.  1  \mleq{}  n
5.  b  :  \mBbbN{}
6.  b1  :  \mBbbN{}b
7.  b2  :  \mBbbN{}n  -  1  {}\mrightarrow{}  \mBbbN{}b
8.  (n  -  1)  =  (n  -  1)
\mvdash{}  <b1,  \mlambda{}x.if  (x  =\msubz{}  n  -  1)  then  b1  else  b2  x  fi  >  =  <b1,  b2>


By

---

Latex:
(EqCD  THEN  Auto)\mcdot{}

---

Home Index