---

Step * 1 of Lemma p-union_wf


1. p : FinProbSpace
2. A : {C:(n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2| ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} 
3. B : {C:(n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2| ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} 
⊢ λp.if (A p =z 1) then 1 else B p fi  ∈ {C:(n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2| 
                                          ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} 
BY
{ (DVar `A' THEN DVar `B' THEN MemTypeCD THEN Reduce 0 THEN Auto) }

1
1. p : FinProbSpace
2. A : (n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2
3. ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((A <i, s>) ≤ (A <j, s>))
4. B : (n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2
5. ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((B <i, s>) ≤ (B <j, s>))
6. s : ℕ ─→ Outcome@i
7. j : ℕ@i
8. i : ℕj@i
⊢ if (A <i, s> =z 1) then 1 else B <i, s> fi  ≤ if (A <j, s> =z 1) then 1 else B <j, s> fi 

---

Latex:



1.  p  :  FinProbSpace
2.  A  :  \{C:(n:\mBbbN{}  \mtimes{}  (\mBbbN{}n  {}\mrightarrow{}  Outcome))  {}\mrightarrow{}  \mBbbN{}2|  \mforall{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  \mforall{}j:\mBbbN{}.  \mforall{}i:\mBbbN{}j.    ((C  <i,  s>)  \mleq{}  (C  <j,  s>))\} 
3.  B  :  \{C:(n:\mBbbN{}  \mtimes{}  (\mBbbN{}n  {}\mrightarrow{}  Outcome))  {}\mrightarrow{}  \mBbbN{}2|  \mforall{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  \mforall{}j:\mBbbN{}.  \mforall{}i:\mBbbN{}j.    ((C  <i,  s>)  \mleq{}  (C  <j,  s>))\} 
\mvdash{}  \mlambda{}p.if  (A  p  =\msubz{}  1)  then  1  else  B  p  fi    \mmember{}  \{C:(n:\mBbbN{}  \mtimes{}  (\mBbbN{}n  {}\mrightarrow{}  Outcome))  {}\mrightarrow{}  \mBbbN{}2| 
                                                                                    \mforall{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  \mforall{}j:\mBbbN{}.  \mforall{}i:\mBbbN{}j.    ((C  <i,  s>)  \mleq{}  (C  <j,  s>))\} 


By

(DVar  `A'  THEN  DVar  `B'  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto)

---

Home Index