---

Step * 1 1 2 2 of Lemma fpf-decompose


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)
⊢ hd(fpf-domain(f)) : f(hd(fpf-domain(f))) ⊆ fnp
BY
{ OnMaybeHyp 9 (\h. (Unfold `fpf-sub` h
                     THEN ((InstHyp [⌜hd(fpf-domain(f))⌝] h)⋅ THENA Complete ((Using [`A',⌜A⌝] Auto)⋅))
                     THEN D -1
                     THEN (((RWO "fpf-join-ap-sq" (-1)) THENM SplitOnHypITE -1 ) THENA Auto)
                     THEN Try ((All (Unfold `eqof`)
                                THEN ((InstHyp [⌜hd(fpf-domain(f))⌝] 11)⋅ THENM (RW assert_pushdownC (-1)) THENM D -1)
                                THEN Complete (Auto))))) }

1
.....falsecase..... 
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. ∀x:A. ((↑x ∈ dom(f)) ⇒ ((↑x ∈ dom(fp ⊕ fnp)) c∧ (f(x) = fp ⊕ fnp(x) ∈ B[x])))
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)
16. ↑hd(fpf-domain(f)) ∈ dom(fp ⊕ fnp)
17. f(hd(fpf-domain(f))) = fnp(hd(fpf-domain(f))) ∈ B[hd(fpf-domain(f))]
18. ¬↑hd(fpf-domain(f)) ∈ dom(fp)
⊢ hd(fpf-domain(f)) : f(hd(fpf-domain(f))) ⊆ fnp

---

Latex:

---

Latex:

1.  A  :  Type
2.  eq  :  EqDecider(A)@i
3.  B  :  A  {}\mrightarrow{}  Type
4.  f  :  a:A  fp->  B[a]@i
5.  ||fpf-domain(f)||  \mgeq{}  1 
6.  0  <  ||fpf-domain(f)||
7.  fp  :  a:A  fp->  B[a]
8.  fnp  :  a:A  fp->  B[a]
9.  f  \msubseteq{}  fp  \moplus{}  fnp
10.  fp  \moplus{}  fnp  \msubseteq{}  f
11.  \mforall{}a:A.  \muparrow{}\mneg{}\msubb{}(eqof(eq)  a  hd(fpf-domain(f)))  supposing  \muparrow{}a  \mmember{}  dom(fp)
12.  \mforall{}a:A.  \mneg{}\muparrow{}\mneg{}\msubb{}(eqof(eq)  a  hd(fpf-domain(f)))  supposing  \muparrow{}a  \mmember{}  dom(fnp)
13.  fpf-domain(fp)  \msubseteq{}  fpf-domain(f)
14.  fpf-domain(fnp)  \msubseteq{}  fpf-domain(f)
15.  \muparrow{}hd(fpf-domain(f))  \mmember{}  dom(f)
\mvdash{}  hd(fpf-domain(f))  :  f(hd(fpf-domain(f)))  \msubseteq{}  fnp


By

---

Latex:
OnMaybeHyp  9  (\mbackslash{}h.  (Unfold  `fpf-sub`  h
                                      THEN  ((InstHyp  [\mkleeneopen{}hd(fpf-domain(f))\mkleeneclose{}]  h)\mcdot{}
                                                  THENA  Complete  ((Using  [`A',\mkleeneopen{}A\mkleeneclose{}]  Auto)\mcdot{})
                                                  )
                                      THEN  D  -1
                                      THEN  (((RWO  "fpf-join-ap-sq"  (-1))  THENM  SplitOnHypITE  -1  )  THENA  Auto)
                                      THEN  Try  ((All  (Unfold  `eqof`)
                                                            THEN  ((InstHyp  [\mkleeneopen{}hd(fpf-domain(f))\mkleeneclose{}]  11)\mcdot{}
                                                                        THENM  (RW  assert\_pushdownC  (-1))
                                                                        THENM  D  -1)
                                                            THEN  Complete  (Auto)))))

---

Home Index