Step
*
1
2
1
of Lemma
fpf-union-compatible-property
1. [T] : Type
2. [V] : Type
3. eq : EqDecider(T)@i
4. [X] : T ─→ Type
5. ∀t:T. (X[t] ⊆r V)
6. R : (V List) ─→ V ─→ 𝔹@i
7. ∀L1,L2:V List. ∀x:V. (L1 ⊆ L2 ⇒ ↑(R L1 x) supposing ↑(R L2 x))
8. ∀L1,L2:V List. ∀x:V. (↑(R (L1 @ L2) x)) supposing ((↑(R L2 x)) and (↑(R L1 x)))
9. A : t:T fp-> X[t] List@i
10. B : t:T fp-> X[t] List@i
11. C : t:T fp-> X[t] List@i
12. ∀t:T
((↑t ∈ dom(B))
⇒ (↑t ∈ dom(A))
⇒ (∀a:V
((((a ∈ B(t)) ∧ (¬↑(R A(t) a))) ∨ ((a ∈ A(t)) ∧ (¬↑(R B(t) a))))
⇒ (∃a':X[t]. ((a' = a ∈ V) ∧ (a' ∈ A(t)) ∧ (a' ∈ B(t)))))))@i
13. ∀t:T
((↑t ∈ dom(A))
⇒ (↑t ∈ dom(C))
⇒ (∀a:V
((((a ∈ A(t)) ∧ (¬↑(R C(t) a))) ∨ ((a ∈ C(t)) ∧ (¬↑(R A(t) a))))
⇒ (∃a':X[t]. ((a' = a ∈ V) ∧ (a' ∈ C(t)) ∧ (a' ∈ A(t)))))))@i
14. ∀t:T
((↑t ∈ dom(B))
⇒ (↑t ∈ dom(C))
⇒ (∀a:V
((((a ∈ B(t)) ∧ (¬↑(R C(t) a))) ∨ ((a ∈ C(t)) ∧ (¬↑(R B(t) a))))
⇒ (∃a':X[t]. ((a' = a ∈ V) ∧ (a' ∈ C(t)) ∧ (a' ∈ B(t)))))))@i
15. t : T@i
16. X[t] ⊆r V
17. (↑t ∈ dom(A)) ∨ (↑t ∈ dom(B))
18. ↑t ∈ dom(C)@i
19. a : V@i
20. ↑t ∈ dom(A)
21. ↑t ∈ dom(B)
22. (a ∈ C(t))@i
23. ¬↑(R (A(t) @ filter(R A(t);B(t))) a)@i
24. ↑(R A(t) a)
⊢ ∃a':X[t]. ((a' = a ∈ V) ∧ (a' ∈ C(t)) ∧ (a' ∈ A(t) @ filter(R A(t);B(t))))
BY
{ (Decide ⌈↑(R B(t) a)⌉⋅ THENA Auto)⋅ }
1
1. [T] : Type
2. [V] : Type
3. eq : EqDecider(T)@i
4. [X] : T ─→ Type
5. ∀t:T. (X[t] ⊆r V)
6. R : (V List) ─→ V ─→ 𝔹@i
7. ∀L1,L2:V List. ∀x:V. (L1 ⊆ L2 ⇒ ↑(R L1 x) supposing ↑(R L2 x))
8. ∀L1,L2:V List. ∀x:V. (↑(R (L1 @ L2) x)) supposing ((↑(R L2 x)) and (↑(R L1 x)))
9. A : t:T fp-> X[t] List@i
10. B : t:T fp-> X[t] List@i
11. C : t:T fp-> X[t] List@i
12. ∀t:T
((↑t ∈ dom(B))
⇒ (↑t ∈ dom(A))
⇒ (∀a:V
((((a ∈ B(t)) ∧ (¬↑(R A(t) a))) ∨ ((a ∈ A(t)) ∧ (¬↑(R B(t) a))))
⇒ (∃a':X[t]. ((a' = a ∈ V) ∧ (a' ∈ A(t)) ∧ (a' ∈ B(t)))))))@i
13. ∀t:T
((↑t ∈ dom(A))
⇒ (↑t ∈ dom(C))
⇒ (∀a:V
((((a ∈ A(t)) ∧ (¬↑(R C(t) a))) ∨ ((a ∈ C(t)) ∧ (¬↑(R A(t) a))))
⇒ (∃a':X[t]. ((a' = a ∈ V) ∧ (a' ∈ C(t)) ∧ (a' ∈ A(t)))))))@i
14. ∀t:T
((↑t ∈ dom(B))
⇒ (↑t ∈ dom(C))
⇒ (∀a:V
((((a ∈ B(t)) ∧ (¬↑(R C(t) a))) ∨ ((a ∈ C(t)) ∧ (¬↑(R B(t) a))))
⇒ (∃a':X[t]. ((a' = a ∈ V) ∧ (a' ∈ C(t)) ∧ (a' ∈ B(t)))))))@i
15. t : T@i
16. X[t] ⊆r V
17. (↑t ∈ dom(A)) ∨ (↑t ∈ dom(B))
18. ↑t ∈ dom(C)@i
19. a : V@i
20. ↑t ∈ dom(A)
21. ↑t ∈ dom(B)
22. (a ∈ C(t))@i
23. ¬↑(R (A(t) @ filter(R A(t);B(t))) a)@i
24. ↑(R A(t) a)
25. ↑(R B(t) a)
⊢ ∃a':X[t]. ((a' = a ∈ V) ∧ (a' ∈ C(t)) ∧ (a' ∈ A(t) @ filter(R A(t);B(t))))
2
1. [T] : Type
2. [V] : Type
3. eq : EqDecider(T)@i
4. [X] : T ─→ Type
5. ∀t:T. (X[t] ⊆r V)
6. R : (V List) ─→ V ─→ 𝔹@i
7. ∀L1,L2:V List. ∀x:V. (L1 ⊆ L2 ⇒ ↑(R L1 x) supposing ↑(R L2 x))
8. ∀L1,L2:V List. ∀x:V. (↑(R (L1 @ L2) x)) supposing ((↑(R L2 x)) and (↑(R L1 x)))
9. A : t:T fp-> X[t] List@i
10. B : t:T fp-> X[t] List@i
11. C : t:T fp-> X[t] List@i
12. ∀t:T
((↑t ∈ dom(B))
⇒ (↑t ∈ dom(A))
⇒ (∀a:V
((((a ∈ B(t)) ∧ (¬↑(R A(t) a))) ∨ ((a ∈ A(t)) ∧ (¬↑(R B(t) a))))
⇒ (∃a':X[t]. ((a' = a ∈ V) ∧ (a' ∈ A(t)) ∧ (a' ∈ B(t)))))))@i
13. ∀t:T
((↑t ∈ dom(A))
⇒ (↑t ∈ dom(C))
⇒ (∀a:V
((((a ∈ A(t)) ∧ (¬↑(R C(t) a))) ∨ ((a ∈ C(t)) ∧ (¬↑(R A(t) a))))
⇒ (∃a':X[t]. ((a' = a ∈ V) ∧ (a' ∈ C(t)) ∧ (a' ∈ A(t)))))))@i
14. ∀t:T
((↑t ∈ dom(B))
⇒ (↑t ∈ dom(C))
⇒ (∀a:V
((((a ∈ B(t)) ∧ (¬↑(R C(t) a))) ∨ ((a ∈ C(t)) ∧ (¬↑(R B(t) a))))
⇒ (∃a':X[t]. ((a' = a ∈ V) ∧ (a' ∈ C(t)) ∧ (a' ∈ B(t)))))))@i
15. t : T@i
16. X[t] ⊆r V
17. (↑t ∈ dom(A)) ∨ (↑t ∈ dom(B))
18. ↑t ∈ dom(C)@i
19. a : V@i
20. ↑t ∈ dom(A)
21. ↑t ∈ dom(B)
22. (a ∈ C(t))@i
23. ¬↑(R (A(t) @ filter(R A(t);B(t))) a)@i
24. ↑(R A(t) a)
25. ¬↑(R B(t) a)
⊢ ∃a':X[t]. ((a' = a ∈ V) ∧ (a' ∈ C(t)) ∧ (a' ∈ A(t) @ filter(R A(t);B(t))))
Latex:
1. [T] : Type
2. [V] : Type
3. eq : EqDecider(T)@i
4. [X] : T {}\mrightarrow{} Type
5. \mforall{}t:T. (X[t] \msubseteq{}r V)
6. R : (V List) {}\mrightarrow{} V {}\mrightarrow{} \mBbbB{}@i
7. \mforall{}L1,L2:V List. \mforall{}x:V. (L1 \msubseteq{} L2 {}\mRightarrow{} \muparrow{}(R L1 x) supposing \muparrow{}(R L2 x))
8. \mforall{}L1,L2:V List. \mforall{}x:V. (\muparrow{}(R (L1 @ L2) x)) supposing ((\muparrow{}(R L2 x)) and (\muparrow{}(R L1 x)))
9. A : t:T fp-> X[t] List@i
10. B : t:T fp-> X[t] List@i
11. C : t:T fp-> X[t] List@i
12. \mforall{}t:T
((\muparrow{}t \mmember{} dom(B))
{}\mRightarrow{} (\muparrow{}t \mmember{} dom(A))
{}\mRightarrow{} (\mforall{}a:V
((((a \mmember{} B(t)) \mwedge{} (\mneg{}\muparrow{}(R A(t) a))) \mvee{} ((a \mmember{} A(t)) \mwedge{} (\mneg{}\muparrow{}(R B(t) a))))
{}\mRightarrow{} (\mexists{}a':X[t]. ((a' = a) \mwedge{} (a' \mmember{} A(t)) \mwedge{} (a' \mmember{} B(t)))))))@i
13. \mforall{}t:T
((\muparrow{}t \mmember{} dom(A))
{}\mRightarrow{} (\muparrow{}t \mmember{} dom(C))
{}\mRightarrow{} (\mforall{}a:V
((((a \mmember{} A(t)) \mwedge{} (\mneg{}\muparrow{}(R C(t) a))) \mvee{} ((a \mmember{} C(t)) \mwedge{} (\mneg{}\muparrow{}(R A(t) a))))
{}\mRightarrow{} (\mexists{}a':X[t]. ((a' = a) \mwedge{} (a' \mmember{} C(t)) \mwedge{} (a' \mmember{} A(t)))))))@i
14. \mforall{}t:T
((\muparrow{}t \mmember{} dom(B))
{}\mRightarrow{} (\muparrow{}t \mmember{} dom(C))
{}\mRightarrow{} (\mforall{}a:V
((((a \mmember{} B(t)) \mwedge{} (\mneg{}\muparrow{}(R C(t) a))) \mvee{} ((a \mmember{} C(t)) \mwedge{} (\mneg{}\muparrow{}(R B(t) a))))
{}\mRightarrow{} (\mexists{}a':X[t]. ((a' = a) \mwedge{} (a' \mmember{} C(t)) \mwedge{} (a' \mmember{} B(t)))))))@i
15. t : T@i
16. X[t] \msubseteq{}r V
17. (\muparrow{}t \mmember{} dom(A)) \mvee{} (\muparrow{}t \mmember{} dom(B))
18. \muparrow{}t \mmember{} dom(C)@i
19. a : V@i
20. \muparrow{}t \mmember{} dom(A)
21. \muparrow{}t \mmember{} dom(B)
22. (a \mmember{} C(t))@i
23. \mneg{}\muparrow{}(R (A(t) @ filter(R A(t);B(t))) a)@i
24. \muparrow{}(R A(t) a)
\mvdash{} \mexists{}a':X[t]. ((a' = a) \mwedge{} (a' \mmember{} C(t)) \mwedge{} (a' \mmember{} A(t) @ filter(R A(t);B(t))))
By
(Decide \mkleeneopen{}\muparrow{}(R B(t) a)\mkleeneclose{}\mcdot{} THENA Auto)\mcdot{}
Home
Index