---

Step * of Lemma fpf-union-compatible-property

∀[T,V:Type].
  ∀eq:EqDecider(T)
    ∀[X:T ─→ Type]
      ∀R:(V List) ─→ V ─→ 𝔹
        (∀A,B,C:t:T fp-> X[t] List.
           (fpf-union-compatible(T;V;t.X[t];eq;R;A;B)
           ⇒ fpf-union-compatible(T;V;t.X[t];eq;R;C;A)
           ⇒ fpf-union-compatible(T;V;t.X[t];eq;R;C;B)
           ⇒ fpf-union-compatible(T;V;t.X[t];eq;R;C;fpf-union-join(eq;R;A;B)))) supposing 
           ((∀L1,L2:V List. ∀x:V.  (↑(R (L1 @ L2) x)) supposing ((↑(R L2 x)) and (↑(R L1 x)))) and 
           (∀L1,L2:V List. ∀x:V.  (L1 ⊆ L2 ⇒ ↑(R L1 x) supposing ↑(R L2 x)))) 
      supposing ∀t:T. (X[t] ⊆r V)
BY
{ (Auto
   THEN All (Unfold `fpf-union-compatible`)
   THEN (D 0 THENA Auto)
   THEN (Assert X[t] ⊆r V BY
               Auto)
   THEN RepeatFor 2 (Auto)
   THEN Try ((DoSubsume THEN Auto))
   THEN MoveToConcl (-1)
   THEN (((RWO "fpf-union-join-dom" (-3) THENA Auto)
          THEN (RWO "fpf-union-join-ap" (0) THENA Auto)
          THEN RepUR ``fpf-cap fpf-union`` 0)
         THEN AutoBoolCase ⌈t ∈ dom(A)⌉⋅
         THEN AutoBoolCase ⌈t ∈ dom(B)⌉⋅
         THEN Try ((SplitOrHyps ⋅ THEN Complete (Auto)))
         THEN RepeatFor 2 (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 ∈ A(t) @ filter(R A(t);B(t))) ∧ (¬↑(R C(t) a))) ∨ ((a ∈ C(t)) ∧ (¬↑(R (A(t) @ filter(R A(t);B(t))) a)))@i
⊢ ∃a':X[t]. ((a' = a ∈ V) ∧ (a' ∈ C(t)) ∧ (a' ∈ A(t) @ filter(R A(t);B(t))))

---

Latex:


\mforall{}[T,V:Type].
    \mforall{}eq:EqDecider(T)
        \mforall{}[X:T  {}\mrightarrow{}  Type]
            \mforall{}R:(V  List)  {}\mrightarrow{}  V  {}\mrightarrow{}  \mBbbB{}
                (\mforall{}A,B,C:t:T  fp->  X[t]  List.
                      (fpf-union-compatible(T;V;t.X[t];eq;R;A;B)
                      {}\mRightarrow{}  fpf-union-compatible(T;V;t.X[t];eq;R;C;A)
                      {}\mRightarrow{}  fpf-union-compatible(T;V;t.X[t];eq;R;C;B)
                      {}\mRightarrow{}  fpf-union-compatible(T;V;t.X[t];eq;R;C;fpf-union-join(eq;R;A;B))))  supposing 
                      ((\mforall{}L1,L2:V  List.  \mforall{}x:V.    (\muparrow{}(R  (L1  @  L2)  x))  supposing  ((\muparrow{}(R  L2  x))  and  (\muparrow{}(R  L1  x))))  and 
                      (\mforall{}L1,L2:V  List.  \mforall{}x:V.    (L1  \msubseteq{}  L2  {}\mRightarrow{}  \muparrow{}(R  L1  x)  supposing  \muparrow{}(R  L2  x)))) 
            supposing  \mforall{}t:T.  (X[t]  \msubseteq{}r  V)


By

(Auto
  THEN  All  (Unfold  `fpf-union-compatible`)
  THEN  (D  0  THENA  Auto)
  THEN  (Assert  X[t]  \msubseteq{}r  V  BY
                          Auto)
  THEN  RepeatFor  2  (Auto)
  THEN  Try  ((DoSubsume  THEN  Auto))
  THEN  MoveToConcl  (-1)
  THEN  (((RWO  "fpf-union-join-dom"  (-3)  THENA  Auto)
                THEN  (RWO  "fpf-union-join-ap"  (0)  THENA  Auto)
                THEN  RepUR  ``fpf-cap  fpf-union``  0)
              THEN  AutoBoolCase  \mkleeneopen{}t  \mmember{}  dom(A)\mkleeneclose{}\mcdot{}
              THEN  AutoBoolCase  \mkleeneopen{}t  \mmember{}  dom(B)\mkleeneclose{}\mcdot{}
              THEN  Try  ((SplitOrHyps  \mcdot{}  THEN  Complete  (Auto)))
              THEN  RepeatFor  2  (Auto)\mcdot{})\mcdot{})

---

Home Index