---

Step * 1 1 of Lemma fpf-union-compatible-property


1. [T] : Type
2. [V] : Type
3. eq : EqDecider(T)
4. [X] : T ⟶ Type
5. ∀t:T. (X[t] ⊆r V)
6. R : (V List) ⟶ V ⟶ 𝔹
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
10. B : t:T fp-> X[t] List
11. C : t:T fp-> X[t] List
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)))))))
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)))))))
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)))))))
15. t : T
16. X[t] ⊆r V
17. (↑t ∈ dom(A)) ∨ (↑t ∈ dom(B))
18. ↑t ∈ dom(C)
19. a : V
20. ↑t ∈ dom(A)
21. ↑t ∈ dom(B)
22. (a ∈ A(t) @ filter(R A(t);B(t)))
23. ¬↑(R C(t) a)
⊢ ∃a':X[t]. ((a' = a ∈ V) ∧ (a' ∈ C(t)) ∧ (a' ∈ A(t) @ filter(R A(t);B(t))))
BY
{ ((RWO "member_append" (-2) THENM RWO "member_filter" (-2)) THENA Auto) }

1
1. [T] : Type
2. [V] : Type
3. eq : EqDecider(T)
4. [X] : T ⟶ Type
5. ∀t:T. (X[t] ⊆r V)
6. R : (V List) ⟶ V ⟶ 𝔹
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
10. B : t:T fp-> X[t] List
11. C : t:T fp-> X[t] List
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)))))))
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)))))))
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)))))))
15. t : T
16. X[t] ⊆r V
17. (↑t ∈ dom(A)) ∨ (↑t ∈ dom(B))
18. ↑t ∈ dom(C)
19. a : V
20. ↑t ∈ dom(A)
21. ↑t ∈ dom(B)
22. (a ∈ A(t)) ∨ ((a ∈ B(t)) ∧ (↑(R A(t) a)))
23. ¬↑(R C(t) a)
⊢ ∃a':X[t]. ((a' = a ∈ V) ∧ (a' ∈ C(t)) ∧ (a' ∈ A(t) @ filter(R A(t);B(t))))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [V]  :  Type
3.  eq  :  EqDecider(T)
4.  [X]  :  T  {}\mrightarrow{}  Type
5.  \mforall{}t:T.  (X[t]  \msubseteq{}r  V)
6.  R  :  (V  List)  {}\mrightarrow{}  V  {}\mrightarrow{}  \mBbbB{}
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
10.  B  :  t:T  fp->  X[t]  List
11.  C  :  t:T  fp->  X[t]  List
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)))))))
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)))))))
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)))))))
15.  t  :  T
16.  X[t]  \msubseteq{}r  V
17.  (\muparrow{}t  \mmember{}  dom(A))  \mvee{}  (\muparrow{}t  \mmember{}  dom(B))
18.  \muparrow{}t  \mmember{}  dom(C)
19.  a  :  V
20.  \muparrow{}t  \mmember{}  dom(A)
21.  \muparrow{}t  \mmember{}  dom(B)
22.  (a  \mmember{}  A(t)  @  filter(R  A(t);B(t)))
23.  \mneg{}\muparrow{}(R  C(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

---

Latex:
((RWO  "member\_append"  (-2)  THENM  RWO  "member\_filter"  (-2))  THENA  Auto)

---

Home Index