---

Step * 2 2 1 2 1 1 2 1 of Lemma countable-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. s : ℕ ⟶ Outcome
4. j : ℕ
5. i : ℕj
6. ¬(i = 0 ∈ ℤ)
7. ¬(j = 0 ∈ ℤ)
8. b : ℕ2
9. y : ℕi
10. (y ∈ upto(i))
11. b = (A[y] <i, s>) ∈ ℕ2
12. ¬(b = 0 ∈ ℤ)
⊢ (A[y] <i, s>) = (A[y] <j, s>) ∈ ℕ2
BY
{ xxx(Assert (A[y] <i, s>) ≤ (A[y] <j, s>) BY
            Auto)xxx }

1
.....assertion..... 
1. p : FinProbSpace
2. A : ℕ ⟶ {C:(n:ℕ × (ℕn ⟶ Outcome)) ⟶ ℕ2| ∀s:ℕ ⟶ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} 
3. s : ℕ ⟶ Outcome
4. j : ℕ
5. i : ℕj
6. ¬(i = 0 ∈ ℤ)
7. ¬(j = 0 ∈ ℤ)
8. b : ℕ2
9. y : ℕi
10. (y ∈ upto(i))
11. b = (A[y] <i, s>) ∈ ℕ2
12. ¬(b = 0 ∈ ℤ)
⊢ (A[y] <i, s>) ≤ (A[y] <j, s>)

2
1. p : FinProbSpace
2. A : ℕ ⟶ {C:(n:ℕ × (ℕn ⟶ Outcome)) ⟶ ℕ2| ∀s:ℕ ⟶ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} 
3. s : ℕ ⟶ Outcome
4. j : ℕ
5. i : ℕj
6. ¬(i = 0 ∈ ℤ)
7. ¬(j = 0 ∈ ℤ)
8. b : ℕ2
9. y : ℕi
10. (y ∈ upto(i))
11. b = (A[y] <i, s>) ∈ ℕ2
12. ¬(b = 0 ∈ ℤ)
13. (A[y] <i, s>) ≤ (A[y] <j, s>)
⊢ (A[y] <i, s>) = (A[y] <j, s>) ∈ ℕ2

---

Latex:

---

Latex:

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
4.  j  :  \mBbbN{}
5.  i  :  \mBbbN{}j
6.  \mneg{}(i  =  0)
7.  \mneg{}(j  =  0)
8.  b  :  \mBbbN{}2
9.  y  :  \mBbbN{}i
10.  (y  \mmember{}  upto(i))
11.  b  =  (A[y]  <i,  s>)
12.  \mneg{}(b  =  0)
\mvdash{}  (A[y]  <i,  s>)  =  (A[y]  <j,  s>)


By

---

Latex:
xxx(Assert  (A[y]  <i,  s>)  \mleq{}  (A[y]  <j,  s>)  BY
                    Auto)xxx

---

Home Index