---

Step * 1 1 1 3 1 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)
16. hd(fpf-domain(f)) ∈ A
⊢ fnp ⊆ hd(fpf-domain(f)) : f(hd(fpf-domain(f)))
BY
{ ((Assert ∀x,y:A.  Dec(x = y ∈ A) BY
          Auto)
   THEN D 0
   THEN Auto
   THEN (Assert hd(fpf-domain(f)) = x ∈ A BY
               OnMaybeHyp 12 (\h. (((InstHyp [⌜x⌝] h)⋅ THENA Auto)
                                   THEN Unfold `eqof` -1
                                   THEN ((RW assert_pushdownC (-1)) THENA Auto)
                                   THEN SupposeNot⋅
                                   THEN D -2
                                   THEN ParallelLast)))
   THEN Reduce 0) }

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)
16. hd(fpf-domain(f)) ∈ A
17. ∀x,y:A.  Dec(x = y ∈ A)
18. x : A@i
19. ↑x ∈ dom(fnp)@i
20. hd(fpf-domain(f)) = x ∈ A
⊢ x = hd(fpf-domain(f)) ∈ A

2
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)
16. hd(fpf-domain(f)) ∈ A
17. ∀x,y:A.  Dec(x = y ∈ A)
18. x : A@i
19. ↑x ∈ dom(fnp)@i
20. ↑x ∈ dom(hd(fpf-domain(f)) : f(hd(fpf-domain(f))))
21. hd(fpf-domain(f)) = x ∈ A
⊢ fnp(x) = f(hd(fpf-domain(f))) ∈ B[x]

---

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)
16.  hd(fpf-domain(f))  \mmember{}  A
\mvdash{}  fnp  \msubseteq{}  hd(fpf-domain(f))  :  f(hd(fpf-domain(f)))


By

---

Latex:
((Assert  \mforall{}x,y:A.    Dec(x  =  y)  BY
                Auto)
  THEN  D  0
  THEN  Auto
  THEN  (Assert  hd(fpf-domain(f))  =  x  BY
                          OnMaybeHyp  12  (\mbackslash{}h.  (((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  h)\mcdot{}  THENA  Auto)
                                                                  THEN  Unfold  `eqof`  -1
                                                                  THEN  ((RW  assert\_pushdownC  (-1))  THENA  Auto)
                                                                  THEN  SupposeNot\mcdot{}
                                                                  THEN  D  -2
                                                                  THEN  ParallelLast)))
  THEN  Reduce  0)

---

Home Index