---

Step * 2 of Lemma countable-p-union_wf

.....set predicate..... 
1. p : FinProbSpace
2. A : ℕ ─→ {C:(n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2| ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} 
⊢ ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.
    (((λp.if (fst(p) =z 0) then 0 else imax-list(map(λi.(A[i] p);upto(fst(p)))) fi ) <i, s>) ≤ ((λp.if (fst(p) =z 0) the\000Cn 0 else imax-list(map(λi.(A[i] p);upto(fst(p)))) fi ) <j, s>))
BY
{ (Reduce 0 THEN Auto THEN RepeatFor 2 ((SplitOnConclITE THENA Auto)) THEN Auto') }

1
.....falsecase..... 
1. p : FinProbSpace
2. A : ℕ ─→ {C:(n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2| ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} 
3. s : ℕ ─→ Outcome@i
4. j : ℕ@i
5. i : ℕj@i
6. i = 0 ∈ ℤ
7. ¬(j = 0 ∈ ℤ)
⊢ 0 ≤ imax-list(map(λi.(A[i] <j, s>);upto(j)))

2
.....falsecase..... 
1. p : FinProbSpace
2. A : ℕ ─→ {C:(n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2| ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} 
3. s : ℕ ─→ Outcome@i
4. j : ℕ@i
5. i : ℕj@i
6. ¬(i = 0 ∈ ℤ)
7. ¬(j = 0 ∈ ℤ)
⊢ imax-list(map(λi@0.(A[i@0] <i, s>);upto(i))) ≤ imax-list(map(λi.(A[i] <j, s>);upto(j)))

---

Latex:


.....set  predicate..... 
1.  p  :  FinProbSpace
2.  A  :  \mBbbN{}  {}\mrightarrow{}  \{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>\000C))\} 
\mvdash{}  \mforall{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  \mforall{}j:\mBbbN{}.  \mforall{}i:\mBbbN{}j.
        (((\mlambda{}p.if  (fst(p)  =\msubz{}  0)  then  0  else  imax-list(map(\mlambda{}i.(A[i]  p);upto(fst(p))))  fi  )  <i,  s>)  \mleq{}  ((\mlambda{}p.\000Cif  (fst(p)  =\msubz{}  0)  then  0  else  imax-list(map(\mlambda{}i.(A[i]  p);upto(fst(p))))  fi  ) 
                                  <j,  s>))


By

(Reduce  0  THEN  Auto  THEN  RepeatFor  2  ((SplitOnConclITE  THENA  Auto))  THEN  Auto')

---

Home Index