---

Step * 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 ∈ A(t)) ∨ ((a ∈ B(t)) ∧ (↑(R A(t) a)))
23. ¬↑(R C(t) a)@i
⊢ ∃a':X[t]. ((a' = a ∈ V) ∧ (a' ∈ C(t)) ∧ (a' ∈ A(t) @ filter(R A(t);B(t))))
BY
{ ((D (-2))
   THEN AllHyps h.((InstHyp [⌈t⌉; ⌈a⌉] h)⋅ THENA Complete (Auto)) 
   THEN ParallelLast
   THEN Auto
   THEN skip{(((RWO "member_append" (0)) THENM (RWO "member_filter" (0)))
              THEN Auto
              THEN OrRight
              THEN Auto
              THEN (HypSubst (-3) 0)
              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{}  A(t))  \mvee{}  ((a  \mmember{}  B(t))  \mwedge{}  (\muparrow{}(R  A(t)  a)))
23.  \mneg{}\muparrow{}(R  C(t)  a)@i
\mvdash{}  \mexists{}a':X[t].  ((a'  =  a)  \mwedge{}  (a'  \mmember{}  C(t))  \mwedge{}  (a'  \mmember{}  A(t)  @  filter(R  A(t);B(t))))


By

((D  (-2))
  THEN  AllHyps  h.((InstHyp  [\mkleeneopen{}t\mkleeneclose{};  \mkleeneopen{}a\mkleeneclose{}]  h)\mcdot{}  THENA  Complete  (Auto)) 
  THEN  ParallelLast
  THEN  Auto
  THEN  skip\{(((RWO  "member\_append"  (0))  THENM  (RWO  "member\_filter"  (0)))
                        THEN  Auto
                        THEN  OrRight
                        THEN  Auto
                        THEN  (HypSubst  (-3)  0)
                        THEN  Auto)\})

---

Home Index