---

Step * 1 1 1 of Lemma egyptian_wf

.....equality..... 
1. q : ℚ
2. v1 : ℤ
3. v2 : ℕ+ List
4. q = (v1 + Σ0 ≤ i < ||v2||. (1/v2[i])) ∈ ℚ
⊢ (norm-list(λx.x) v2) = v2 ∈ (ℕ+ List)
BY
{ xxx(GenConclAtAddrType ⌜id-fun(ℕ+ List)⌝ [2;1]⋅ THEN Auto)xxx }

1
1. q : ℚ
2. v1 : ℤ
3. v2 : ℕ+ List
4. q = (v1 + Σ0 ≤ i < ||v2||. (1/v2[i])) ∈ ℚ
5. v : id-fun(ℕ+ List)
6. norm-list(λx.x) = v ∈ id-fun(ℕ+ List)
⊢ (v v2) = v2 ∈ (ℕ+ List)

---

Latex:

---

Latex:
.....equality..... 
1.  q  :  \mBbbQ{}
2.  v1  :  \mBbbZ{}
3.  v2  :  \mBbbN{}\msupplus{}  List
4.  q  =  (v1  +  \mSigma{}0  \mleq{}  i  <  ||v2||.  (1/v2[i]))
\mvdash{}  (norm-list(\mlambda{}x.x)  v2)  =  v2


By

---

Latex:
xxx(GenConclAtAddrType  \mkleeneopen{}id-fun(\mBbbN{}\msupplus{}  List)\mkleeneclose{}  [2;1]\mcdot{}  THEN  Auto)xxx

---

Home Index