---

Step * of Lemma egyptian_wf

∀q:ℚ. (egyptian(q) ∈ {p:ℤ × (ℕ+ List)| let x,L = p in q = (x + Σ0 ≤ i < ||L||. (1/L[i])) ∈ ℚ} )
BY
{ (Auto THEN Unfold `egyptian` 0 THEN (GenConclAtAddr [2;2] THENA (Auto THEN Auto'))) }

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

---

Latex:

---

Latex:
\mforall{}q:\mBbbQ{}.  (egyptian(q)  \mmember{}  \{p:\mBbbZ{}  \mtimes{}  (\mBbbN{}\msupplus{}  List)|  let  x,L  =  p  in  q  =  (x  +  \mSigma{}0  \mleq{}  i  <  ||L||.  (1/L[i]))\}  )


By

---

Latex:
(Auto  THEN  Unfold  `egyptian`  0  THEN  (GenConclAtAddr  [2;2]  THENA  (Auto  THEN  Auto')))

---

Home Index