---

Step * 1 of Lemma member-p-union


1. p : FinProbSpace@i
2. A : {C:(n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2| ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} @i
3. B : {C:(n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2| ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} @i
4. s : ℕ ─→ Outcome@i
5. ∃n:ℕ. (((λp.if (A p =z 1) then 1 else B p fi ) <n, s>) = 1 ∈ ℤ)@i
⊢ (∃n:ℕ. ((A <n, s>) = 1 ∈ ℤ)) ∨ (∃n:ℕ. ((B <n, s>) = 1 ∈ ℤ))
BY
{ (ExRepD THEN (Reduce (-1)) THEN (SplitOnHypITE -1  THENA Auto)) }

1
.....truecase..... 
1. p : FinProbSpace@i
2. A : {C:(n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2| ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} @i
3. B : {C:(n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2| ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} @i
4. s : ℕ ─→ Outcome@i
5. n : ℕ@i
6. 1 = 1 ∈ ℤ@i
7. (A <n, s>) = 1 ∈ ℤ
⊢ (∃n:ℕ. ((A <n, s>) = 1 ∈ ℤ)) ∨ (∃n:ℕ. ((B <n, s>) = 1 ∈ ℤ))

2
.....falsecase..... 
1. p : FinProbSpace@i
2. A : {C:(n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2| ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} @i
3. B : {C:(n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2| ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} @i
4. s : ℕ ─→ Outcome@i
5. n : ℕ@i
6. (B <n, s>) = 1 ∈ ℤ@i
7. ¬((A <n, s>) = 1 ∈ ℤ)
⊢ (∃n:ℕ. ((A <n, s>) = 1 ∈ ℤ)) ∨ (∃n:ℕ. ((B <n, s>) = 1 ∈ ℤ))

---

Latex:



1.  p  :  FinProbSpace@i
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>))\}  @\000Ci
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>))\}  @\000Ci
4.  s  :  \mBbbN{}  {}\mrightarrow{}  Outcome@i
5.  \mexists{}n:\mBbbN{}.  (((\mlambda{}p.if  (A  p  =\msubz{}  1)  then  1  else  B  p  fi  )  <n,  s>)  =  1)@i
\mvdash{}  (\mexists{}n:\mBbbN{}.  ((A  <n,  s>)  =  1))  \mvee{}  (\mexists{}n:\mBbbN{}.  ((B  <n,  s>)  =  1))


By

(ExRepD  THEN  (Reduce  (-1))  THEN  (SplitOnHypITE  -1    THENA  Auto))

---

Home Index