---

Step * 1 of Lemma egyptian_wf


1. q : ℚ
2. v : ∃p:ℤ × (ℕ+ List) [let x,L = p 
                         in q = (x + Σ0 ≤ i < ||L||. (1/L[i])) ∈ ℚ]
3. (TERMOF{egyptian-number:o, 1:l} q) = v ∈ (∃p:ℤ × (ℕ+ List) [let x,L = p in q = (x + Σ0 ≤ i < ||L||. (1/L[i])) ∈ ℚ])
⊢ norm-pair(λx.x;norm-list(λx.x)) v ∈ {p:ℤ × (ℕ+ List)| let x,L = p in q = (x + Σ0 ≤ i < ||L||. (1/L[i])) ∈ ℚ} 
BY
{ xxx(Thin (-1)
      THEN D -1
      THEN D -2
      THEN Reduce (-1)
      THEN Unfold `norm-pair` 0
      THEN Reduce 0
      THEN (CallByValueReduce 0 THENA Auto))xxx }

1
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])) ∈ ℚ} 

---

Latex:

---

Latex:

1.  q  :  \mBbbQ{}
2.  v  :  \mexists{}p:\mBbbZ{}  \mtimes{}  (\mBbbN{}\msupplus{}  List)  [let  x,L  =  p 
                                                  in  q  =  (x  +  \mSigma{}0  \mleq{}  i  <  ||L||.  (1/L[i]))]
3.  (TERMOF\{egyptian-number:o,  1:l\}  q)  =  v
\mvdash{}  norm-pair(\mlambda{}x.x;norm-list(\mlambda{}x.x))  v  \mmember{}  \{p:\mBbbZ{}  \mtimes{}  (\mBbbN{}\msupplus{}  List)| 
                                                                              let  x,L  =  p 
                                                                              in  q  =  (x  +  \mSigma{}0  \mleq{}  i  <  ||L||.  (1/L[i]))\} 


By

---

Latex:
xxx(Thin  (-1)
        THEN  D  -1
        THEN  D  -2
        THEN  Reduce  (-1)
        THEN  Unfold  `norm-pair`  0
        THEN  Reduce  0
        THEN  (CallByValueReduce  0  THENA  Auto))xxx

---

Home Index