Step
*
1
2
2
2
of Lemma
fpf-split
1. [A] : Type
2. eq : EqDecider(A)@i
3. [B] : A ─→ Type
4. d : A List@i
5. f1 : a:{a:A| (a ∈ d)} ─→ B[a]@i
6. [P] : A ─→ ℙ
7. dec : ∀a:A. Dec(P[a])@i
8. <d, f1> ∈ a:A fp-> B[a]
9. <filter(λa.[dec a]b;d), f1> ∈ a:A fp-> B[a]
10. <filter(λa.(¬b[dec a]b);d), f1> ∈ a:A fp-> B[a]
⊢ ∃fp,fnp:a:A fp-> B[a]
((<d, f1> ⊆ fp ⊕ fnp ∧ fp ⊕ fnp ⊆ <d, f1>)
∧ ((∀a:A. P[a] supposing ↑a ∈ dom(fp)) ∧ (∀a:A. ¬P[a] supposing ↑a ∈ dom(fnp)))
∧ fpf-domain(fp) ⊆ fpf-domain(<d, f1>)
∧ fpf-domain(fnp) ⊆ fpf-domain(<d, f1>))
BY
{ (InstConcl [⌈<filter(λa.[dec a]b;d), f1>⌉;⌈<filter(λa.(¬b[dec a]b);d), f1>⌉]⋅ THEN Auto) }
1
1. [A] : Type
2. eq : EqDecider(A)@i
3. [B] : A ─→ Type
4. d : A List@i
5. f1 : a:{a:A| (a ∈ d)} ─→ B[a]@i
6. [P] : A ─→ ℙ
7. dec : ∀a:A. Dec(P[a])@i
8. <d, f1> ∈ a:A fp-> B[a]
9. <filter(λa.[dec a]b;d), f1> ∈ a:A fp-> B[a]
10. <filter(λa.(¬b[dec a]b);d), f1> ∈ a:A fp-> B[a]
⊢ <d, f1> ⊆ <filter(λa.[dec a]b;d), f1> ⊕ <filter(λa.(¬b[dec a]b);d), f1>
2
1. [A] : Type
2. eq : EqDecider(A)@i
3. [B] : A ─→ Type
4. d : A List@i
5. f1 : a:{a:A| (a ∈ d)} ─→ B[a]@i
6. [P] : A ─→ ℙ
7. dec : ∀a:A. Dec(P[a])@i
8. <d, f1> ∈ a:A fp-> B[a]
9. <filter(λa.[dec a]b;d), f1> ∈ a:A fp-> B[a]
10. <filter(λa.(¬b[dec a]b);d), f1> ∈ a:A fp-> B[a]
11. <d, f1> ⊆ <filter(λa.[dec a]b;d), f1> ⊕ <filter(λa.(¬b[dec a]b);d), f1>
⊢ <filter(λa.[dec a]b;d), f1> ⊕ <filter(λa.(¬b[dec a]b);d), f1> ⊆ <d, f1>
3
1. [A] : Type
2. eq : EqDecider(A)@i
3. [B] : A ─→ Type
4. d : A List@i
5. f1 : a:{a:A| (a ∈ d)} ─→ B[a]@i
6. [P] : A ─→ ℙ
7. dec : ∀a:A. Dec(P[a])@i
8. <d, f1> ∈ a:A fp-> B[a]
9. <filter(λa.[dec a]b;d), f1> ∈ a:A fp-> B[a]
10. <filter(λa.(¬b[dec a]b);d), f1> ∈ a:A fp-> B[a]
11. <d, f1> ⊆ <filter(λa.[dec a]b;d), f1> ⊕ <filter(λa.(¬b[dec a]b);d), f1>
12. <filter(λa.[dec a]b;d), f1> ⊕ <filter(λa.(¬b[dec a]b);d), f1> ⊆ <d, f1>
13. a : A@i
14. ↑a ∈ dom(<filter(λa.[dec a]b;d), f1>)
⊢ P[a]
4
1. A : Type
2. eq : EqDecider(A)@i
3. B : A ─→ Type
4. d : A List@i
5. f1 : a:{a:A| (a ∈ d)} ─→ B[a]@i
6. P : A ─→ ℙ
7. dec : ∀a:A. Dec(P[a])@i
8. <d, f1> ∈ a:A fp-> B[a]
9. <filter(λa.[dec a]b;d), f1> ∈ a:A fp-> B[a]
10. <filter(λa.(¬b[dec a]b);d), f1> ∈ a:A fp-> B[a]
11. <d, f1> ⊆ <filter(λa.[dec a]b;d), f1> ⊕ <filter(λa.(¬b[dec a]b);d), f1>
12. <filter(λa.[dec a]b;d), f1> ⊕ <filter(λa.(¬b[dec a]b);d), f1> ⊆ <d, f1>
13. ∀a:A. P[a] supposing ↑a ∈ dom(<filter(λa.[dec a]b;d), f1>)
14. a : A@i
15. ↑a ∈ dom(<filter(λa.(¬b[dec a]b);d), f1>)
⊢ ¬P[a]
5
1. [A] : Type
2. eq : EqDecider(A)@i
3. [B] : A ─→ Type
4. d : A List@i
5. f1 : a:{a:A| (a ∈ d)} ─→ B[a]@i
6. [P] : A ─→ ℙ
7. dec : ∀a:A. Dec(P[a])@i
8. <d, f1> ∈ a:A fp-> B[a]
9. <filter(λa.[dec a]b;d), f1> ∈ a:A fp-> B[a]
10. <filter(λa.(¬b[dec a]b);d), f1> ∈ a:A fp-> B[a]
11. <d, f1> ⊆ <filter(λa.[dec a]b;d), f1> ⊕ <filter(λa.(¬b[dec a]b);d), f1>
12. <filter(λa.[dec a]b;d), f1> ⊕ <filter(λa.(¬b[dec a]b);d), f1> ⊆ <d, f1>
13. ∀a:A. P[a] supposing ↑a ∈ dom(<filter(λa.[dec a]b;d), f1>)
14. ∀a:A. ¬P[a] supposing ↑a ∈ dom(<filter(λa.(¬b[dec a]b);d), f1>)
⊢ fpf-domain(<filter(λa.[dec a]b;d), f1>) ⊆ fpf-domain(<d, f1>)
6
1. [A] : Type
2. eq : EqDecider(A)@i
3. [B] : A ─→ Type
4. d : A List@i
5. f1 : a:{a:A| (a ∈ d)} ─→ B[a]@i
6. [P] : A ─→ ℙ
7. dec : ∀a:A. Dec(P[a])@i
8. <d, f1> ∈ a:A fp-> B[a]
9. <filter(λa.[dec a]b;d), f1> ∈ a:A fp-> B[a]
10. <filter(λa.(¬b[dec a]b);d), f1> ∈ a:A fp-> B[a]
11. <d, f1> ⊆ <filter(λa.[dec a]b;d), f1> ⊕ <filter(λa.(¬b[dec a]b);d), f1>
12. <filter(λa.[dec a]b;d), f1> ⊕ <filter(λa.(¬b[dec a]b);d), f1> ⊆ <d, f1>
13. ∀a:A. P[a] supposing ↑a ∈ dom(<filter(λa.[dec a]b;d), f1>)
14. ∀a:A. ¬P[a] supposing ↑a ∈ dom(<filter(λa.(¬b[dec a]b);d), f1>)
15. fpf-domain(<filter(λa.[dec a]b;d), f1>) ⊆ fpf-domain(<d, f1>)
⊢ fpf-domain(<filter(λa.(¬b[dec a]b);d), f1>) ⊆ fpf-domain(<d, f1>)
Latex:
1. [A] : Type
2. eq : EqDecider(A)@i
3. [B] : A {}\mrightarrow{} Type
4. d : A List@i
5. f1 : a:\{a:A| (a \mmember{} d)\} {}\mrightarrow{} B[a]@i
6. [P] : A {}\mrightarrow{} \mBbbP{}
7. dec : \mforall{}a:A. Dec(P[a])@i
8. <d, f1> \mmember{} a:A fp-> B[a]
9. <filter(\mlambda{}a.[dec a]\msubb{};d), f1> \mmember{} a:A fp-> B[a]
10. <filter(\mlambda{}a.(\mneg{}\msubb{}[dec a]\msubb{});d), f1> \mmember{} a:A fp-> B[a]
\mvdash{} \mexists{}fp,fnp:a:A fp-> B[a]
((<d, f1> \msubseteq{} fp \moplus{} fnp \mwedge{} fp \moplus{} fnp \msubseteq{} <d, f1>)
\mwedge{} ((\mforall{}a:A. P[a] supposing \muparrow{}a \mmember{} dom(fp)) \mwedge{} (\mforall{}a:A. \mneg{}P[a] supposing \muparrow{}a \mmember{} dom(fnp)))
\mwedge{} fpf-domain(fp) \msubseteq{} fpf-domain(<d, f1>)
\mwedge{} fpf-domain(fnp) \msubseteq{} fpf-domain(<d, f1>))
By
(InstConcl [\mkleeneopen{}<filter(\mlambda{}a.[dec a]\msubb{};d), f1>\mkleeneclose{};\mkleeneopen{}<filter(\mlambda{}a.(\mneg{}\msubb{}[dec a]\msubb{});d), f1>\mkleeneclose{}]\mcdot{} THEN Auto)
Home
Index