---

Step * 1 1 of Lemma egyptian_wf


1. q : ℚ
2. v1 : ℤ
3. v2 : ℕ+ List
4. q = (v1 + Σ0 ≤ i < ||v2||. (1/v2[i])) ∈ ℚ
⊢ eval b' = norm-list(λx.x) v2 in
  <v1, b'> ∈ {p:ℤ × (ℕ+ List)| let x,L = p in q = (x + Σ0 ≤ i < ||L||. (1/L[i])) ∈ ℚ} 
BY
{ xxxSubst' (norm-list(λx.x) v2) = v2 ∈ (ℕ+ List) 0xxx }

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

2
1. q : ℚ
2. v1 : ℤ
3. v2 : ℕ+ List
4. q = (v1 + Σ0 ≤ i < ||v2||. (1/v2[i])) ∈ ℚ
⊢ eval b' = v2 in
  <v1, b'> ∈ {p:ℤ × (ℕ+ List)| let x,L = p in q = (x + Σ0 ≤ i < ||L||. (1/L[i])) ∈ ℚ} 

---

Latex:

---

Latex:

1.  q  :  \mBbbQ{}
2.  v1  :  \mBbbZ{}
3.  v2  :  \mBbbN{}\msupplus{}  List
4.  q  =  (v1  +  \mSigma{}0  \mleq{}  i  <  ||v2||.  (1/v2[i]))
\mvdash{}  eval  b'  =  norm-list(\mlambda{}x.x)  v2  in
    <v1,  b'>  \mmember{}  \{p:\mBbbZ{}  \mtimes{}  (\mBbbN{}\msupplus{}  List)|  let  x,L  =  p  in  q  =  (x  +  \mSigma{}0  \mleq{}  i  <  ||L||.  (1/L[i]))\} 


By

---

Latex:
xxxSubst'  (norm-list(\mlambda{}x.x)  v2)  =  v2  0xxx

---

Home Index