---

Step * of Lemma fpf-decompose

∀[A:Type]
  ∀eq:EqDecider(A)
    ∀[B:A ⟶ Type]
      ∀f:a:A fp-> B[a]
        ∃g:a:A fp-> B[a]
         ∃a:A
          ∃b:B[a]
           ((f ⊆ g ⊕ a : b ∧ g ⊕ a : b ⊆ f)
           ∧ (∀a':A. ¬(a' = a ∈ A) supposing ↑a' ∈ dom(g))
           ∧ ||fpf-domain(g)|| < ||fpf-domain(f)||) 
        supposing 0 < ||fpf-domain(f)||
BY
{ ((Using [`A',⌜A⌝] Auto)⋅
   THEN ((InstLemma `fpf-split` [⌜A⌝; ⌜eq⌝; ⌜B⌝; ⌜f⌝; ⌜λ2a.↑¬b(eqof(eq) a hd(fpf-domain(f)))⌝])⋅
         THENA (Using [`A',⌜A⌝] Auto)⋅
         )
   THEN ExRepD
   THEN (Assert ⌜||fpf-domain(f)|| ≥ 1 ⌝ BY
               (MoveToConcl 5 THEN GenConcl ⌜fpf-domain(f) = L ∈ (A List)⌝⋅ THEN All Thin THEN Auto))
   THEN PromoteHyp (-1) 5
   THEN (Assert ↑hd(fpf-domain(f)) ∈ dom(f) BY
               (DVar `f'
                THEN DVar `d'
                THEN (All (RepUR ``fpf-domain fpf-dom eqof``))
                THEN Auto'
                THEN RW assert_pushdownC 0
                THEN Auto
                THEN OrLeft
                THEN Auto))⋅
   THEN (ExRepD
         THEN ((InstConcl [⌜fp⌝; ⌜hd(fpf-domain(f))⌝; ⌜f(hd(fpf-domain(f)))⌝])⋅ THENA (Using [`A',⌜A⌝] Auto)⋅)
         THEN Try (Complete (Auto)))⋅) }

1
1. [A] : Type
2. eq : EqDecider(A)@i
3. [B] : A ⟶ Type
4. f : a:A fp-> B[a]@i
5. ||fpf-domain(f)|| ≥ 1 
6. 0 < ||fpf-domain(f)||
7. fp : a:A fp-> B[a]
8. fnp : a:A fp-> B[a]
9. f ⊆ fp ⊕ fnp
10. fp ⊕ fnp ⊆ f
11. ∀a:A. ↑¬b(eqof(eq) a hd(fpf-domain(f))) supposing ↑a ∈ dom(fp)
12. ∀a:A. ¬↑¬b(eqof(eq) a hd(fpf-domain(f))) supposing ↑a ∈ dom(fnp)
13. fpf-domain(fp) ⊆ fpf-domain(f)
14. fpf-domain(fnp) ⊆ fpf-domain(f)
15. ↑hd(fpf-domain(f)) ∈ dom(f)
⊢ (f ⊆ fp ⊕ hd(fpf-domain(f)) : f(hd(fpf-domain(f))) ∧ fp ⊕ hd(fpf-domain(f)) : f(hd(fpf-domain(f))) ⊆ f)
∧ (∀a':A. ¬(a' = hd(fpf-domain(f)) ∈ A) supposing ↑a' ∈ dom(fp))
∧ ||fpf-domain(fp)|| < ||fpf-domain(f)||

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}eq:EqDecider(A)
        \mforall{}[B:A  {}\mrightarrow{}  Type]
            \mforall{}f:a:A  fp->  B[a]
                \mexists{}g:a:A  fp->  B[a]
                  \mexists{}a:A
                    \mexists{}b:B[a]
                      ((f  \msubseteq{}  g  \moplus{}  a  :  b  \mwedge{}  g  \moplus{}  a  :  b  \msubseteq{}  f)
                      \mwedge{}  (\mforall{}a':A.  \mneg{}(a'  =  a)  supposing  \muparrow{}a'  \mmember{}  dom(g))
                      \mwedge{}  ||fpf-domain(g)||  <  ||fpf-domain(f)||) 
                supposing  0  <  ||fpf-domain(f)||


By

---

Latex:
((Using  [`A',\mkleeneopen{}A\mkleeneclose{}]  Auto)\mcdot{}
  THEN  ((InstLemma  `fpf-split`  [\mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}eq\mkleeneclose{};  \mkleeneopen{}B\mkleeneclose{};  \mkleeneopen{}f\mkleeneclose{};  \mkleeneopen{}\mlambda{}\msubtwo{}a.\muparrow{}\mneg{}\msubb{}(eqof(eq)  a  hd(fpf-domain(f)))\mkleeneclose{}])\mcdot{}
              THENA  (Using  [`A',\mkleeneopen{}A\mkleeneclose{}]  Auto)\mcdot{}
              )
  THEN  ExRepD
  THEN  (Assert  \mkleeneopen{}||fpf-domain(f)||  \mgeq{}  1  \mkleeneclose{}  BY
                          (MoveToConcl  5  THEN  GenConcl  \mkleeneopen{}fpf-domain(f)  =  L\mkleeneclose{}\mcdot{}  THEN  All  Thin  THEN  Auto))
  THEN  PromoteHyp  (-1)  5
  THEN  (Assert  \muparrow{}hd(fpf-domain(f))  \mmember{}  dom(f)  BY
                          (DVar  `f'
                            THEN  DVar  `d'
                            THEN  (All  (RepUR  ``fpf-domain  fpf-dom  eqof``))
                            THEN  Auto'
                            THEN  RW  assert\_pushdownC  0
                            THEN  Auto
                            THEN  OrLeft
                            THEN  Auto))\mcdot{}
  THEN  (ExRepD
              THEN  ((InstConcl  [\mkleeneopen{}fp\mkleeneclose{};  \mkleeneopen{}hd(fpf-domain(f))\mkleeneclose{};  \mkleeneopen{}f(hd(fpf-domain(f)))\mkleeneclose{}])\mcdot{}
                          THENA  (Using  [`A',\mkleeneopen{}A\mkleeneclose{}]  Auto)\mcdot{}
                          )
              THEN  Try  (Complete  (Auto)))\mcdot{})

---

Home Index