---

Step * 1 2 1 1 1 1 1 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) a)
24. ↑(R B(t) a)
25. (X[t] List) ⊆r (V List)
26. X1 : V List@i
27. A(t) = X1 ∈ (V List)@i
28. Z : V List@i
29. B(t) = Z ∈ (V List)@i
⊢ X1 @ filter(R X1;Z) ⊆ X1 @ Z
BY
{ ((Unfold `l_contains` 0 THEN (BLemma `l_all_iff` THENA Auto))
   THEN (RWW "member_append" 0 THENA Auto)
   THEN RWW "member_filter" 0
   THEN Auto
   THEN ParallelLast
   THEN Auto) }

---

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.  \muparrow{}(R  A(t)  a)
24.  \muparrow{}(R  B(t)  a)
25.  (X[t]  List)  \msubseteq{}r  (V  List)
26.  X1  :  V  List@i
27.  A(t)  =  X1@i
28.  Z  :  V  List@i
29.  B(t)  =  Z@i
\mvdash{}  X1  @  filter(R  X1;Z)  \msubseteq{}  X1  @  Z


By

((Unfold  `l\_contains`  0  THEN  (BLemma  `l\_all\_iff`  THENA  Auto))
  THEN  (RWW  "member\_append"  0  THENA  Auto)
  THEN  RWW  "member\_filter"  0
  THEN  Auto
  THEN  ParallelLast
  THEN  Auto)

---

Home Index