---

Step * 2 1 of Lemma bl-exists-filter


1. Q : Base
2. L : Base
3. P : Base
4. x : Base
5. y : Base
6. r1 : Base
7. r2 : Base
8. r1 ≤ (∃x∈r2.Q[x])_b
9. ∀z:Top + Top. ((z ∧b Q[x]) ∨br1 ≤ (∃x∈if z then [x / r2] else r2 fi .Q[x])_b)
⊢ ((P x) ∧b Q[x]) ∨br1 ≤ (∃x∈if P x then [x / r2] else r2 fi .Q[x])_b
BY
{ AssumeHasValue }

1
1. Q : Base
2. L : Base
3. P : Base
4. x : Base
5. y : Base
6. r1 : Base
7. r2 : Base
8. r1 ≤ (∃x∈r2.Q[x])_b
9. ∀z:Top + Top. ((z ∧b Q[x]) ∨br1 ≤ (∃x∈if z then [x / r2] else r2 fi .Q[x])_b)
10. (((P x) ∧b Q[x]) ∨br1)↓
⊢ ((P x) ∧b Q[x]) ∨br1 ≤ (∃x∈if P x then [x / r2] else r2 fi .Q[x])_b

2
1. Q : Base
2. L : Base
3. P : Base
4. x : Base
5. y : Base
6. r1 : Base
7. r2 : Base
8. r1 ≤ (∃x∈r2.Q[x])_b
9. ∀z:Top + Top. ((z ∧b Q[x]) ∨br1 ≤ (∃x∈if z then [x / r2] else r2 fi .Q[x])_b)
10. is-exception(((P x) ∧b Q[x]) ∨br1)
⊢ ((P x) ∧b Q[x]) ∨br1 ≤ (∃x∈if P x then [x / r2] else r2 fi .Q[x])_b

---

Latex:

---

Latex:

1.  Q  :  Base
2.  L  :  Base
3.  P  :  Base
4.  x  :  Base
5.  y  :  Base
6.  r1  :  Base
7.  r2  :  Base
8.  r1  \mleq{}  (\mexists{}x\mmember{}r2.Q[x])\_b
9.  \mforall{}z:Top  +  Top.  ((z  \mwedge{}\msubb{}  Q[x])  \mvee{}\msubb{}r1  \mleq{}  (\mexists{}x\mmember{}if  z  then  [x  /  r2]  else  r2  fi  .Q[x])\_b)
\mvdash{}  ((P  x)  \mwedge{}\msubb{}  Q[x])  \mvee{}\msubb{}r1  \mleq{}  (\mexists{}x\mmember{}if  P  x  then  [x  /  r2]  else  r2  fi  .Q[x])\_b


By

---

Latex:
AssumeHasValue

---

Home Index