---

Step * of Lemma fpf-union-compatible-subtype

∀[A,C:Type]. ∀[B1,B2:A ─→ Type].
  (∀eq:EqDecider(A). ∀f,g:x:A fp-> B1[x] List. ∀R:(C List) ─→ C ─→ 𝔹.
     (fpf-union-compatible(A;C;x.B1[x];eq;R;f;g) ⇒ fpf-union-compatible(A;C;x.B2[x];eq;R;f;g))) supposing 
     ((∀x:A. (B1[x] ⊆r B2[x])) and 
     (∀a:A. (B2[a] ⊆r C)))
BY
{ (((Auto THEN All (Unfold `so_apply`))
    THEN Try (((D 0 THEN Auto) THEN (SubsumeC ⌈B2 x⌉⋅ THEN Auto) THEN DoSubsume THEN Auto))
    )
   THEN RepeatFor 5 (ParallelLast)
   THEN (D 0
         THENA (Auto
                THEN (DoSubsume
                      THEN Auto
                      THEN SubtypeReasoning
                      THEN Auto
                      THEN (D 0 THEN Auto)
                      THEN SubsumeC ⌈B2 x⌉⋅
                      THEN Auto
                      THEN DoSubsume
                      THEN Auto)⋅
                )
         )
   THEN D -2
   THEN Auto
   THEN ParallelLast
   THEN Auto
   THEN Try ((DoSubsume THEN Auto THEN SubtypeReasoning THEN Auto))) }

---

Latex:


\mforall{}[A,C:Type].  \mforall{}[B1,B2:A  {}\mrightarrow{}  Type].
    (\mforall{}eq:EqDecider(A).  \mforall{}f,g:x:A  fp->  B1[x]  List.  \mforall{}R:(C  List)  {}\mrightarrow{}  C  {}\mrightarrow{}  \mBbbB{}.
          (fpf-union-compatible(A;C;x.B1[x];eq;R;f;g)
          {}\mRightarrow{}  fpf-union-compatible(A;C;x.B2[x];eq;R;f;g)))  supposing 
          ((\mforall{}x:A.  (B1[x]  \msubseteq{}r  B2[x]))  and 
          (\mforall{}a:A.  (B2[a]  \msubseteq{}r  C)))


By

(((Auto  THEN  All  (Unfold  `so\_apply`))
    THEN  Try  (((D  0  THEN  Auto)  THEN  (SubsumeC  \mkleeneopen{}B2  x\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  DoSubsume  THEN  Auto))
    )
  THEN  RepeatFor  5  (ParallelLast)
  THEN  (D  0
              THENA  (Auto
                            THEN  (DoSubsume
                                        THEN  Auto
                                        THEN  SubtypeReasoning
                                        THEN  Auto
                                        THEN  (D  0  THEN  Auto)
                                        THEN  SubsumeC  \mkleeneopen{}B2  x\mkleeneclose{}\mcdot{}
                                        THEN  Auto
                                        THEN  DoSubsume
                                        THEN  Auto)\mcdot{}
                            )
              )
  THEN  D  -2
  THEN  Auto
  THEN  ParallelLast
  THEN  Auto
  THEN  Try  ((DoSubsume  THEN  Auto  THEN  SubtypeReasoning  THEN  Auto)))

---

Home Index