---

Step * 1 1 of Lemma p-union_wf


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
7. j : ℕ
8. i : ℕj
⊢ 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 
BY
{ xxx(RepeatFor 2 ((SplitOnConclITE THENA Auto)) THEN Auto')xxx }

1
.....falsecase..... 
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
7. j : ℕ
8. i : ℕj
9. (A <i, s>) = 1 ∈ ℤ
10. ¬((A <j, s>) = 1 ∈ ℤ)
⊢ 1 ≤ (B <j, s>)

---

Latex:

---

Latex:

1.  p  :  FinProbSpace
2.  A  :  (n:\mBbbN{}  \mtimes{}  (\mBbbN{}n  {}\mrightarrow{}  Outcome))  {}\mrightarrow{}  \mBbbN{}2
3.  \mforall{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  \mforall{}j:\mBbbN{}.  \mforall{}i:\mBbbN{}j.    ((A  <i,  s>)  \mleq{}  (A  <j,  s>))
4.  B  :  (n:\mBbbN{}  \mtimes{}  (\mBbbN{}n  {}\mrightarrow{}  Outcome))  {}\mrightarrow{}  \mBbbN{}2
5.  \mforall{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  \mforall{}j:\mBbbN{}.  \mforall{}i:\mBbbN{}j.    ((B  <i,  s>)  \mleq{}  (B  <j,  s>))
6.  s  :  \mBbbN{}  {}\mrightarrow{}  Outcome
7.  j  :  \mBbbN{}
8.  i  :  \mBbbN{}j
\mvdash{}  if  (A  <i,  s>  =\msubz{}  1)  then  1  else  B  <i,  s>  fi    \mleq{}  if  (A  <j,  s>  =\msubz{}  1)  then  1  else  B  <j,  s>  fi 


By

---

Latex:
xxx(RepeatFor  2  ((SplitOnConclITE  THENA  Auto))  THEN  Auto')xxx

---

Home Index