---

Step * 2 2 of Lemma countable-p-union_wf

.....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)))
BY
{ (BLemma `imax-list-lb`
   THEN Auto
   THEN Try (((RWO "length-map" 0 THENA Auto) THEN RWO "length_upto" 0 THEN Auto))
   THEN (BLemma `l_all_iff` THENA Auto)) }

1
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 ∈ ℤ)
⊢ ∀b:ℕ2. ((b ∈ map(λi@0.(A[i@0] <i, s>);upto(i))) ⇒ (b ≤ imax-list(map(λi.(A[i] <j, s>);upto(j)))))

---

Latex:


.....falsecase..... 
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))\} 
3.  s  :  \mBbbN{}  {}\mrightarrow{}  Outcome@i
4.  j  :  \mBbbN{}@i
5.  i  :  \mBbbN{}j@i
6.  \mneg{}(i  =  0)
7.  \mneg{}(j  =  0)
\mvdash{}  imax-list(map(\mlambda{}i@0.(A[i@0]  <i,  s>);upto(i)))  \mleq{}  imax-list(map(\mlambda{}i.(A[i]  <j,  s>);upto(j)))


By

(BLemma  `imax-list-lb`
  THEN  Auto
  THEN  Try  (((RWO  "length-map"  0  THENA  Auto)  THEN  RWO  "length\_upto"  0  THEN  Auto))
  THEN  (BLemma  `l\_all\_iff`  THENA  Auto))

---

Home Index