Definition: fpf
a:A fp-> B[a] == d:A List × (a:{a:A| (a ∈ d)} ⟶ B[a])
Lemma: fpf_wf
∀[A:Type]. ∀[B:A ⟶ Type]. (a:A fp-> B[a] ∈ Type)
Lemma: subtype-fpf-general
∀[A:Type]. ∀[P:A ⟶ ℙ]. ∀[B:A ⟶ 𝕌{j}]. (a:{a:A| P[a]} fp-> B[a] ⊆r a:A fp-> B[a])
Lemma: subtype-fpf
∀[A:Type]. ∀[P:A ⟶ ℙ]. ∀[B:A ⟶ Type]. (a:{a:A| P[a]} fp-> B[a] ⊆r a:A fp-> B[a])
Lemma: subtype-fpf-variant
∀[A:Type]. ∀[P:A ⟶ ℙ]. ∀[B:A ⟶ 𝕌']. (a:{a:A| P[a]} fp-> B[a] ⊆r a:A fp-> B[a])
Lemma: subtype-fpf2
∀[A:Type]. ∀[B1,B2:A ⟶ Type]. a:A fp-> B1[a] ⊆r a:A fp-> B2[a] supposing ∀a:A. (B1[a] ⊆r B2[a])
Lemma: subtype-fpf3
∀[A1,A2:Type]. ∀[B1:A1 ⟶ Type]. ∀[B2:A2 ⟶ Type].
(a:A1 fp-> B1[a] ⊆r a:A2 fp-> B2[a]) supposing ((∀a:A1. (B1[a] ⊆r B2[a])) and strong-subtype(A1;A2))
Lemma: subtype-fpf-void
∀[A:Type]. ∀[B1:Top]. ∀[B2:A ⟶ Type]. (a:Void fp-> B1[a] ⊆r a:A fp-> B2[a])
Definition: fpf-dom
x ∈ dom(f) == x ∈b fst(f)
Lemma: fpf-dom_wf
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[f:a:A fp-> Top]. ∀[x:A]. (x ∈ dom(f) ∈ 𝔹)
Definition: fpf-domain
fpf-domain(f) == fst(f)
Lemma: fpf-domain_wf2
∀[A,B:Type]. ∀[f:a:A fp-> B]. (fpf-domain(f) ∈ A List)
Lemma: fpf-domain_wf
∀[A:Type]. ∀[f:a:A fp-> Top]. (fpf-domain(f) ∈ A List)
Lemma: member-fpf-domain
∀[A:Type]. ∀f:a:A fp-> Top. ∀eq:EqDecider(A). ∀x:A. (↑x ∈ dom(f) ⇐⇒ (x ∈ fpf-domain(f)))
Lemma: member-fpf-domain-variant
∀[A,V:Type]. ∀f:a:A fp-> V × Top. ∀eq:EqDecider(A). ∀x:A. (↑x ∈ dom(f) ⇐⇒ (x ∈ fpf-domain(f)))
Lemma: fpf-trivial-subtype-set
∀[A:Type]. ∀[P:A ⟶ ℙ]. ∀[f:a:{a:A| P[a]} fp-> Type × Top]. (f ∈ a:A fp-> Type × Top)
Lemma: fpf-trivial-subtype-top
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[f:a:A fp-> B[a]]. (f ∈ a:A fp-> Top)
Lemma: fpf-type
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[f:a:A fp-> B[a]]. (f ∈ a:{a:A| (a ∈ fpf-domain(f))} fp-> B[a])
Lemma: fpf-dom_functionality
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq1,eq2:EqDecider(A)]. ∀[f:a:A fp-> B[a]]. ∀[x:A]. x ∈ dom(f) = x ∈ dom(f)
Lemma: fpf-dom_functionality2
∀[A:Type]. ∀[eq1,eq2:EqDecider(A)]. ∀[f:a:A fp-> Top]. ∀[x:A]. {↑x ∈ dom(f) supposing ↑x ∈ dom(f)}
Lemma: fpf-dom-type
∀[X,Y:Type]. ∀[eq:EqDecider(Y)]. ∀[f:x:X fp-> Top]. ∀[x:Y]. (x ∈ X) supposing ((↑x ∈ dom(f)) and strong-subtype(X;Y))
Lemma: fpf-dom-type2
∀[X,Y:Type]. ∀[eq:EqDecider(Y)]. ∀[f:x:X fp-> Top]. ∀[x:Y]. {x ∈ X supposing ↑x ∈ dom(f)} supposing strong-subtype(X;Y)
Definition: fpf-empty
⊗ == <[], λx.⋅>
Lemma: fpf-empty_wf
∀[A:Type]. ∀[B:A ⟶ Type]. (⊗ ∈ x:A fp-> B[x])
Definition: fpf-is-empty
fpf-is-empty(f) == (||fst(f)|| =z 0)
Lemma: fpf-is-empty_wf
∀[A:Type]. ∀[f:x:A fp-> Top]. (fpf-is-empty(f) ∈ 𝔹)
Lemma: assert-fpf-is-empty
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[f:x:A fp-> B[x]]. uiff(↑fpf-is-empty(f);f = ⊗ ∈ x:A fp-> B[x])
Lemma: fpf-null-domain
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[f:Void ⟶ Top]. (<[], f> = ⊗ ∈ x:A fp-> B[x])
Definition: fpf-ap
f(x) == (snd(f)) x
Lemma: fpf-ap_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[f:a:A fp-> B[a]]. ∀[eq:EqDecider(A)]. ∀[x:A]. f(x) ∈ B[x] supposing ↑x ∈ dom(f)
Lemma: fpf_ap_pair_lemma
∀x,eq,f,d:Top. (<d, f>(x) ~ f x)
Lemma: fpf-ap_functionality
∀[eq1,eq2,f,x:Top]. (f(x) ~ f(x))
Definition: fpf-cap
f(x)?z == if x ∈ dom(f) then f(x) else z fi
Lemma: fpf-cap-wf-univ
∀[A:Type]. ∀[f:a:A fp-> Type]. ∀[eq:EqDecider(A)]. ∀[x:A]. ∀[z:Type]. (f(x)?z ∈ Type)
Lemma: fpf-cap_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[f:a:A fp-> B[a]]. ∀[eq:EqDecider(A)]. ∀[x:A]. ∀[z:B[x]]. (f(x)?z ∈ B[x])
Lemma: alist-domain-first
∀[A:Type]
∀d:A List. ∀f1:a:{a:A| (a ∈ d)} ⟶ Top. ∀x:A. ∀eq:EqDecider(A).
((x ∈ d)
⇒ (∃i:ℕ||d||. ((∀j:ℕi. (¬((fst(map(λx.<x, f1 x>;d)[j])) = x ∈ A))) ∧ ((fst(map(λx.<x, f1 x>;d)[i])) = x ∈ A))))
Lemma: fpf-as-apply-alist
∀[A,B:Type]. ∀[f:a:A fp-> B]. ∀[eq:EqDecider(A)].
(f = <fpf-domain(f), λx.outl(apply-alist(eq;map(λx.<x, f(x)>;fpf-domain(f));x))> ∈ a:A fp-> B)
Definition: fpf-union
fpf-union(f;g;eq;R;x) == if x ∈ dom(f) ∧b x ∈ dom(g) then f(x) @ filter(R f(x);g(x)) else f(x)?g(x)?[] fi
Lemma: fpf-union_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f,g:x:A fp-> B[x] List]. ∀[x:A]. ∀[R:⋂a:A. ((B[a] List) ⟶ B[a] ⟶ 𝔹)].
(fpf-union(f;g;eq;R;x) ∈ B[x] List)
Lemma: fpf-union-contains
∀[A:Type]. ∀[B:A ⟶ Type].
∀eq:EqDecider(A). ∀f,g:x:A fp-> B[x] List. ∀x:A. ∀R:⋂a:A. ((B[a] List) ⟶ B[a] ⟶ 𝔹). f(x)?[] ⊆ fpf-union(f;g;eq;R;x)
Definition: fpf-union-compatible
fpf-union-compatible(A;C;x.B[x];eq;R;f;g) ==
∀x:A
((↑x ∈ dom(g))
⇒ (↑x ∈ dom(f))
⇒ (∀a:C
((((a ∈ g(x)) ∧ (¬↑(R f(x) a))) ∨ ((a ∈ f(x)) ∧ (¬↑(R g(x) a))))
⇒ (∃a':B[x]. ((a' = a ∈ C) ∧ (a' ∈ f(x)) ∧ (a' ∈ g(x)))))))
Lemma: fpf-union-compatible_wf
∀[A,C:Type]. ∀[B:A ⟶ Type].
∀[eq:EqDecider(A)]. ∀[f,g:x:A fp-> B[x] List]. ∀[R:(C List) ⟶ C ⟶ 𝔹].
(fpf-union-compatible(A;C;x.B[x];eq;R;f;g) ∈ ℙ)
supposing ∀x:A. (B[x] ⊆r C)
Lemma: fpf-union-compatible_symmetry
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[C:Type].
∀eq:EqDecider(A). ∀f,g:x:A fp-> B[x] List. ∀R:(C List) ⟶ C ⟶ 𝔹.
(fpf-union-compatible(A;C;x.B[x];eq;R;f;g) ⇒ fpf-union-compatible(A;C;x.B[x];eq;R;g;f))
supposing ∀a:A. (B[a] ⊆r C)
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)))
Lemma: fpf-union-compatible-self
∀[A,C:Type]. ∀[B:A ⟶ Type].
∀eq:EqDecider(A). ∀f:x:A fp-> B[x] List. ∀R:(C List) ⟶ C ⟶ 𝔹. fpf-union-compatible(A;C;x.B[x];eq;R;f;f)
supposing ∀a:A. (B[a] ⊆r C)
Definition: fpf-single-valued
fpf-single-valued(A;eq;x.B[x];V;g) ==
∀x:A. ((↑x ∈ dom(g)) ⇒ (∀b1,b2:B[x]. ((b1 ∈ g(x)) ⇒ (b2 ∈ g(x)) ⇒ (b1 = b2 ∈ V) ⇒ (b1 = b2 ∈ B[x]))))
Lemma: fpf-single-valued_wf
∀[A,V:Type]. ∀[B:A ⟶ Type].
∀[eq:EqDecider(A)]. ∀[g:x:A fp-> B[x] List]. (fpf-single-valued(A;eq;x.B[x];V;g) ∈ ℙ) supposing ∀a:A. (B[a] ⊆r V)
Lemma: fpf-union-contains2
∀[A,V:Type]. ∀[B:A ⟶ Type].
∀eq:EqDecider(A). ∀f,g:x:A fp-> B[x] List.
∀x:A. ∀R:(V List) ⟶ V ⟶ 𝔹. (fpf-union-compatible(A;V;x.B[x];eq;R;f;g) ⇒ g(x)?[] ⊆ fpf-union(f;g;eq;R;x))
supposing fpf-single-valued(A;eq;x.B[x];V;g)
supposing ∀a:A. (B[a] ⊆r V)
Definition: fpf-val
z != f(x) ==> P[a; z] == (↑x ∈ dom(f)) ⇒ P[x; f(x)]
Lemma: fpf-val_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[f:a:A fp-> B[a]]. ∀[eq:EqDecider(A)]. ∀[x:A]. ∀[P:a:{a:A| ↑a ∈ dom(f)} ⟶ B[a] ⟶ ℙ].
(z != f(x) ==> P[x;z] ∈ ℙ)
Definition: fpf-sub
f ⊆ g == ∀x:A. ((↑x ∈ dom(f)) ⇒ ((↑x ∈ dom(g)) c∧ (f(x) = g(x) ∈ B[x])))
Lemma: fpf-sub_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> B[a]]. (f ⊆ g ∈ ℙ)
Lemma: fpf-sub_witness
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> B[a]]. (f ⊆ g ⇒ (λx,y. <Ax, Ax> ∈ f ⊆ g))
Lemma: fpf-sub-set
∀[A:Type]. ∀[P:A ⟶ ℙ]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:{a:A| P[a]} fp-> B[a]]. f ⊆ g supposing f ⊆ g
Lemma: sq_stable__fpf-sub
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> B[a]]. SqStable(f ⊆ g)
Lemma: fpf-empty-sub
∀[A:Type]. ∀[B,eq,g:Top]. ⊗ ⊆ g
Lemma: fpf-sub-functionality
∀[A,A':Type].
∀[B:A ⟶ Type]. ∀[C:A' ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[eq':EqDecider(A')]. ∀[f,g:a:A fp-> B[a]].
(f ⊆ g) supposing (f ⊆ g and (∀a:A. (B[a] ⊆r C[a])))
supposing strong-subtype(A;A')
Lemma: fpf-sub-functionality2
∀[A,A':Type].
∀[B:A ⟶ Type]. ∀[C:A' ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[eq':EqDecider(A')]. ∀[f,g:a:A fp-> B[a]].
(f ⊆ g) supposing (f ⊆ g and (∀a:A. (B[a] ⊆r C[a])))
supposing strong-subtype(A;A')
Lemma: fpf-sub_functionality
∀[A,A':Type].
∀[B:A ⟶ Type]. ∀[C:A' ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[eq':EqDecider(A')]. ∀[f,g:a:A fp-> B[a]].
{f ⊆ g supposing f ⊆ g} supposing ∀a:A. (B[a] ⊆r C[a])
supposing strong-subtype(A;A')
Lemma: fpf-sub_functionality2
∀[A,A':Type].
∀[B:A ⟶ Type]. ∀[C:A' ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[eq':EqDecider(A')]. ∀[f,g:a:A fp-> B[a]].
{f ⊆ g supposing f ⊆ g} supposing ∀a:A. (B[a] ⊆r C[a])
supposing strong-subtype(A;A')
Lemma: fpf-sub_transitivity
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f,g,h:a:A fp-> B[a]]. (f ⊆ h) supposing (g ⊆ h and f ⊆ g)
Lemma: fpf-sub_weakening
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> B[a]]. f ⊆ g supposing f = g ∈ a:A fp-> B[a]
Definition: fpf-contains
f ⊆⊆ g == ∀x:A. ((↑x ∈ dom(f)) ⇒ ((↑x ∈ dom(g)) c∧ f(x) ⊆ g(x)))
Lemma: fpf-contains_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> B[a] List]. (f ⊆⊆ g ∈ ℙ)
Lemma: fpf-contains_self
∀[A:Type]. ∀[B:A ⟶ Type]. ∀eq:EqDecider(A). ∀f:a:A fp-> B[a] List. f ⊆⊆ f
Lemma: subtype-fpf-cap
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[f,g:x:X fp-> Type]. {∀[x:X]. (f(x)?Top ⊆r g(x)?Top)} supposing g ⊆ f
Lemma: subtype-fpf-cap-top
∀[T,X:Type]. ∀[eq:EqDecider(X)]. ∀[f,g:x:X fp-> Type]. ∀[x:X]. f(x)?T ⊆r g(x)?Top supposing g ⊆ f
Lemma: subtype-fpf-cap-top2
∀[X,T:Type]. ∀[eq:EqDecider(X)]. ∀[g:x:X fp-> Type]. ∀[x:X]. T ⊆r g(x)?Top supposing (↑x ∈ dom(g)) ⇒ (T ⊆r g(x))
Lemma: fpf-cap-void-subtype
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[ds:x:A fp-> Type]. ∀[x:A]. (ds(x)?Void ⊆r ds(x)?Top)
Lemma: subtype-fpf-cap-void
∀[T,X:Type]. ∀[eq:EqDecider(X)]. ∀[f,g:x:X fp-> Type]. ∀[x:X]. f(x)?Void ⊆r g(x)?T supposing f ⊆ g
Lemma: fpf-cap_functionality
∀[A:Type]. ∀[d1,d2:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[f:a:A fp-> B[a]]. ∀[x:A]. ∀[z:B[x]]. (f(x)?z = f(x)?z ∈ B[x])
Lemma: fpf-cap-subtype_functionality
∀[A:Type]. ∀[d1,d2:EqDecider(A)]. ∀[f:a:A fp-> Type]. ∀[x:A]. ∀[z:Type]. (f(x)?z ⊆r f(x)?z)
Lemma: fpf-cap_functionality_wrt_sub
∀[A:Type]. ∀[d1,d2,d3,d4:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[f,g:a:A fp-> B[a]]. ∀[x:A]. ∀[z:B[x]].
(f(x)?z = g(x)?z ∈ B[x]) supposing ((↑x ∈ dom(f)) and f ⊆ g)
Lemma: fpf-cap-subtype_functionality_wrt_sub
∀[A:Type]. ∀[d1,d2,d4:EqDecider(A)]. ∀[f,g:a:A fp-> Type]. ∀[x:A]. {g(x)?Top ⊆r f(x)?Top supposing f ⊆ g}
Lemma: fpf-cap-subtype_functionality_wrt_sub2
∀[A1,A2,A3:Type]. ∀[d,d':EqDecider(A3)]. ∀[d2:EqDecider(A2)]. ∀[f:a:A1 fp-> Type]. ∀[g:a:A2 fp-> Type]. ∀[x:A3].
({g(x)?Top ⊆r f(x)?Top supposing f ⊆ g}) supposing (strong-subtype(A2;A3) and strong-subtype(A1;A2))
Definition: fpf-compatible
f || g == ∀x:A. (((↑x ∈ dom(f)) ∧ (↑x ∈ dom(g))) ⇒ (f(x) = g(x) ∈ B[x]))
Lemma: fpf-compatible_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> B[a]]. (f || g ∈ ℙ)
Lemma: fpf-compatible-wf2
∀[A:Type]. ∀[B,C:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f:a:A fp-> B[a]]. ∀[g:a:A fp-> C[a]].
f || g ∈ ℙ supposing ∀x:A. ((↑x ∈ dom(f)) ⇒ (↑x ∈ dom(g)) ⇒ (B[x] ⊆r C[x]))
Lemma: fpf-compatible_monotonic
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f1,g1,f2,g2:a:A fp-> B[a]].
(f1 || g1) supposing (f2 || g2 and g1 ⊆ g2 and f1 ⊆ f2)
Lemma: fpf-compatible_monotonic-guard
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f1,g1,f2,g2:a:A fp-> B[a]].
({f1 || g1 supposing f2 || g2}) supposing (g1 ⊆ g2 and f1 ⊆ f2)
Definition: fpf-compatible-mod
fpf-compatible-mod(A;a.B[a];eq;
R;f;g) ==
∀x:A. (((↑x ∈ dom(f)) ∧ (↑x ∈ dom(g))) ⇒ (¬↑(R f(x) g(x))) ⇒ (f(x) = g(x) ∈ B[x]))
Lemma: fpf-compatible-mod_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> B[a]]. ∀[R:⋂a:A. (B[a] ⟶ B[a] ⟶ 𝔹)].
(fpf-compatible-mod(A;a.B[a];eq;
R;f;g) ∈ ℙ)
Lemma: fpf-sub-compatible-left
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> B[a]]. f || g supposing f ⊆ g
Lemma: fpf-sub-compatible-right
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> B[a]]. f || g supposing g ⊆ f
Lemma: subtype-fpf-cap5
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[f,g:x:X fp-> Type]. ∀[x:X]. f(x)?Void ⊆r g(x)?Top supposing f || g
Lemma: subtype-fpf-cap-void2
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[f,g:x:X fp-> Type]. ∀[x:X]. ∀[z:g(x)?Void]. f(x)?Void ⊆r g(x)?Void supposing f || g
Lemma: subtype-fpf-cap-void-list
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[f,g:x:X fp-> Type]. ∀[x:X]. (f(x)?Void List) ⊆r (g(x)?Void List) supposing f ⊆ g
Lemma: fpf-cap-compatible
∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[f,g:x:X fp-> Type]. ∀[x:X].
(f(x)?Void = g(x)?Void ∈ Type) supposing (g(x)?Void and f(x)?Void and f || g)
Definition: fpf-join
f ⊕ g == <(fst(f)) @ filter(λa.(¬ba ∈ dom(f));fst(g)), λa.f(a)?g(a)>
Lemma: fpf-join_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[f,g:a:A fp-> B[a]]. ∀[eq:EqDecider(A)]. (f ⊕ g ∈ a:A fp-> B[a])
Lemma: fpf-join-wf
∀[A:Type]. ∀[B,C,D:A ⟶ Type]. ∀[f:a:A fp-> B[a]]. ∀[g:a:A fp-> C[a]]. ∀[eq:EqDecider(A)].
(f ⊕ g ∈ a:A fp-> D[a]) supposing
((∀a:A. ((↑a ∈ dom(g)) ⇒ (C[a] ⊆r D[a]))) and
(∀a:A. ((↑a ∈ dom(f)) ⇒ (B[a] ⊆r D[a]))))
Lemma: fpf-join-empty
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[f:a:A fp-> B[a]]. ∀[eq:EqDecider(A)]. (⊗ ⊕ f = f ∈ a:A fp-> B[a])
Lemma: fpf-empty-join
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[f:a:A fp-> B[a]]. ∀[eq:EqDecider(A)]. (f ⊕ ⊗ = f ∈ a:A fp-> B[a])
Lemma: fpf-join-empty-sq
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[f:a:A fp-> B[a]]. ∀[eq:EqDecider(A)]. (⊗ ⊕ f ~ <fst(f), λa.((snd(f)) a)>)
Lemma: fpf-join-idempotent
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[f:a:A fp-> B[a]]. ∀[eq:EqDecider(A)]. (f ⊕ f = f ∈ a:A fp-> B[a])
Lemma: fpf-join-assoc
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f,g,h:a:A fp-> B[a]]. (f ⊕ g ⊕ h = f ⊕ g ⊕ h ∈ a:A fp-> B[a])
Lemma: fpf-join-dom
∀[A:Type]. ∀[B:A ⟶ Type].
∀eq:EqDecider(A). ∀f,g:a:A fp-> B[a]. ∀x:A. (↑x ∈ dom(f ⊕ g) ⇐⇒ (↑x ∈ dom(f)) ∨ (↑x ∈ dom(g)))
Lemma: fpf-join-dom2
∀[A:Type]. ∀eq:EqDecider(A). ∀f,g:a:A fp-> Top. ∀x:A. (↑x ∈ dom(f ⊕ g) ⇐⇒ (↑x ∈ dom(f)) ∨ (↑x ∈ dom(g)))
Lemma: fpf-join-dom-sq
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> Top]. ∀[x:A]. (x ∈ dom(f ⊕ g) ~ x ∈ dom(f) ∨bx ∈ dom(g))
Lemma: fpf-domain-join
∀[A:Type]
∀f,g:a:A fp-> Top. ∀eq:EqDecider(A). ∀x:A. ((x ∈ fpf-domain(f ⊕ g)) ⇐⇒ (x ∈ fpf-domain(f)) ∨ (x ∈ fpf-domain(g)))
Lemma: fpf-join-domain
∀[A:Type]. ∀f,g:a:A fp-> Top. ∀eq:EqDecider(A). fpf-domain(f ⊕ g) ⊆ fpf-domain(f) @ fpf-domain(g)
Lemma: fpf-join-is-empty
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[f,g:x:A fp-> Top]. (fpf-is-empty(f ⊕ g) ~ fpf-is-empty(f) ∧b fpf-is-empty(g))
Lemma: fpf-join-ap
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> B[a]]. ∀[x:A].
f ⊕ g(x) = if x ∈ dom(f) then f(x) else g(x) fi ∈ B[x] supposing ↑x ∈ dom(f ⊕ g)
Lemma: fpf-join-ap-left
∀[A:Type]. ∀[B,C:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f:a:A fp-> B[a]]. ∀[g:a:A fp-> C[a]]. ∀[x:A].
f ⊕ g(x) = f(x) ∈ B[x] supposing ↑x ∈ dom(f)
Lemma: fpf-join-ap-sq
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[f:a:A fp-> Top]. ∀[g:Top]. ∀[x:A]. (f ⊕ g(x) ~ if x ∈ dom(f) then f(x) else g(x) fi )
Lemma: fpf-join-cap-sq
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> Top]. ∀[x:A]. ∀[z:Top].
(f ⊕ g(x)?z ~ if x ∈ dom(f) then f(x)?z else g(x)?z fi )
Lemma: fpf-join-cap
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> Top]. ∀[x:A]. ∀[z:Top]. (f ⊕ g(x)?z ~ f(x)?g(x)?z)
Lemma: fpf-join-range
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[df:x:A fp-> Type]. ∀[f:x:A fp-> df(x)?Top]. ∀[dg:x:A fp-> Type].
∀[g:x:A fp-> dg(x)?Top].
(f ⊕ g ∈ x:A fp-> df ⊕ dg(x)?Top) supposing
((∀x:A. ((↑x ∈ dom(g)) ⇒ (↑x ∈ dom(dg)))) and
(∀x:A. ((↑x ∈ dom(f)) ⇒ (↑x ∈ dom(df)))) and
df || dg)
Lemma: fpf-sub-join-left
∀[A:Type]. ∀[B1,B2:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f:a:A fp-> B1[a]]. ∀[g:a:A fp-> Top]. f ⊆ f ⊕ g
Lemma: fpf-sub-join-left2
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f,h,g:a:A fp-> B[a]]. h ⊆ f ⊕ g supposing h ⊆ f
Lemma: fpf-sub-join-right
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> B[a]]. g ⊆ f ⊕ g supposing f || g
Lemma: fpf-sub-join-right2
∀[A:Type]. ∀[B,C:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f:a:A fp-> B[a]]. ∀[g:a:A fp-> C[a]].
g ⊆ f ⊕ g supposing ∀x:A. (((↑x ∈ dom(f)) ∧ (↑x ∈ dom(g))) ⇒ ((B[x] ⊆r C[x]) c∧ (f(x) = g(x) ∈ C[x])))
Lemma: fpf-sub-join
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> B[a]]. {f ⊆ f ⊕ g ∧ g ⊆ f ⊕ g} supposing f || g
Lemma: fpf-join-sub
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f1,g1,f2,g2:a:A fp-> B[a]].
(f1 ⊕ f2 ⊆ g1 ⊕ g2) supposing (f2 ⊆ g2 and f1 ⊆ g1 and f2 || g1)
Lemma: fpf-join-sub2
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f1,g,f2:a:A fp-> B[a]]. (f1 ⊕ f2 ⊆ g) supposing (f2 ⊆ g and f1 ⊆ g)
Definition: fpf-join-list
⊕(L) == reduce(λf,g. f ⊕ g;⊗;L)
Lemma: fpf-join-list_wf
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[L:a:A fp-> B[a] List]. (⊕(L) ∈ a:A fp-> B[a])
Lemma: fpf-join-list-dom
∀[A:Type]. ∀eq:EqDecider(A). ∀[B:A ⟶ Type]. ∀L:a:A fp-> B[a] List. ∀x:A. (↑x ∈ dom(⊕(L)) ⇐⇒ (∃f∈L. ↑x ∈ dom(f)))
Lemma: fpf-join-list-dom2
∀[A:Type]. ∀eq:EqDecider(A). ∀L:a:A fp-> Top List. ∀x:A. (↑x ∈ dom(⊕(L)) ⇐⇒ (∃f∈L. ↑x ∈ dom(f)))
Lemma: fpf-join-list-domain
∀[A:Type]
∀eq:EqDecider(A)
∀[B:A ⟶ Type]. ∀L:a:A fp-> B[a] List. ∀x:A. ((x ∈ fpf-domain(⊕(L))) ⇐⇒ (∃f∈L. (x ∈ fpf-domain(f))))
Lemma: fpf-join-list-domain2
∀[A:Type]. ∀eq:EqDecider(A). ∀L:a:A fp-> Top List. ∀x:A. ((x ∈ fpf-domain(⊕(L))) ⇐⇒ (∃f∈L. (x ∈ fpf-domain(f))))
Lemma: fpf-join-list-ap
∀[A:Type]
∀eq:EqDecider(A)
∀[B:A ⟶ Type]
∀L:a:A fp-> B[a] List. ∀x:A. (∃f∈L. (↑x ∈ dom(f)) ∧ (⊕(L)(x) = f(x) ∈ B[x])) supposing ↑x ∈ dom(⊕(L))
Lemma: fpf-join-list-ap2
∀[A:Type]
∀eq:EqDecider(A)
∀[B:A ⟶ Type]
∀L:a:A fp-> B[a] List. ∀x:A. ((x ∈ fpf-domain(⊕(L))) ⇒ (∃f∈L. (↑x ∈ dom(f)) ∧ (⊕(L)(x) = f(x) ∈ B[x])))
Lemma: fpf-join-list-ap-disjoint
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[L:a:A fp-> B[a] List]. ∀[x:A].
(∀[f:a:A fp-> B[a]]. (⊕(L)(x) = f(x) ∈ B[x]) supposing ((↑x ∈ dom(f)) and (f ∈ L))) supposing
((∀f,g∈L. ∀x:A. (¬((↑x ∈ dom(f)) ∧ (↑x ∈ dom(g))))) and
(↑x ∈ dom(⊕(L))))
Lemma: fpf_join_cons_lemma
∀v,u,eq:Top. (⊕([u / v]) ~ u ⊕ ⊕(v))
Lemma: fpf_join_nil_lemma
∀eq:Top. (⊕([]) ~ ⊗)
Lemma: fpf-sub-join-symmetry
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> B[a]]. f ⊕ g ⊆ g ⊕ f supposing f || g
Definition: fpf-union-join
fpf-union-join(eq;R;f;g) == <(fst(f)) @ filter(λa.(¬ba ∈ dom(f));fst(g)), λa.fpf-union(f;g;eq;R;a)>
Lemma: fpf-union-join_wf
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[f,g:a:A fp-> B[a] List]. ∀[R:⋂a:A. ((B[a] List) ⟶ B[a] ⟶ 𝔹)].
(fpf-union-join(eq;R;f;g) ∈ a:A fp-> B[a] List)
Lemma: fpf-union-join-dom
∀[A:Type]
∀eq:EqDecider(A). ∀f,g:a:A fp-> Top. ∀x:A. ∀R:Top.
(↑x ∈ dom(fpf-union-join(eq;R;f;g)) ⇐⇒ (↑x ∈ dom(f)) ∨ (↑x ∈ dom(g)))
Lemma: fpf-domain-union-join
∀[A:Type]
∀f:a:A fp-> Top List. ∀g:a:A fp-> Top. ∀eq:EqDecider(A). ∀x:A. ∀R:Top.
((x ∈ fpf-domain(fpf-union-join(eq;R;f;g))) ⇐⇒ (x ∈ fpf-domain(f)) ∨ (x ∈ fpf-domain(g)))
Lemma: fpf-union-join-ap
∀[f,g,eq,x,R:Top]. (fpf-union-join(eq;R;f;g)(x) ~ fpf-union(f;g;eq;R;x))
Lemma: fpf-union-join-member
∀[A:Type]
∀eq:EqDecider(A)
∀[B:A ⟶ Type]
∀f,g:a:A fp-> B[a] List. ∀R:⋂a:A. ((B[a] List) ⟶ B[a] ⟶ 𝔹). ∀a:A.
∀x:B[a]. ((x ∈ fpf-union-join(eq;R;f;g)(a)) ⇒ (((↑a ∈ dom(f)) ∧ (x ∈ f(a))) ∨ ((↑a ∈ dom(g)) ∧ (x ∈ g(a)))))
supposing ↑a ∈ dom(fpf-union-join(eq;R;f;g))
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)
Lemma: fpf-contains-union-join-left2
∀[A:Type]. ∀[B:A ⟶ Type].
∀eq:EqDecider(A). ∀f,h,g:a:A fp-> B[a] List. ∀R:⋂a:A. ((B[a] List) ⟶ B[a] ⟶ 𝔹).
(h ⊆⊆ f ⇒ h ⊆⊆ fpf-union-join(eq;R;f;g))
Lemma: fpf-contains-union-join-right2
∀[A,V:Type]. ∀[B:A ⟶ Type].
∀eq:EqDecider(A). ∀f,h,g:a:A fp-> B[a] List. ∀R:(V List) ⟶ V ⟶ 𝔹.
fpf-union-compatible(A;V;x.B[x];eq;R;f;g) ⇒ h ⊆⊆ g ⇒ h ⊆⊆ fpf-union-join(eq;R;f;g)
supposing fpf-single-valued(A;eq;x.B[x];V;g)
supposing ∀a:A. (B[a] ⊆r V)
Lemma: fpf-sub-val
∀[A:Type]. ∀[B:A ⟶ Type].
∀eq:EqDecider(A). ∀f,g:a:A fp-> B[a]. ∀x:A.
∀[P:a:A ⟶ B[a] ⟶ ℙ]. z != f(x) ==> P[x;z] ⇒ z != g(x) ==> P[x;z] supposing g ⊆ f
Lemma: fpf-sub-val2
∀[A,A':Type].
∀[B:A ⟶ Type]
∀eq:EqDecider(A'). ∀f,g:a:A fp-> B[a]. ∀x:A'.
∀[P,Q:a:A ⟶ B[a] ⟶ ℙ].
((∀x:A. ∀z:B[x]. (P[x;z] ⇒ Q[x;z])) ⇒ z != f(x) ==> P[x;z] ⇒ z != g(x) ==> Q[x;z] supposing g ⊆ f)
supposing strong-subtype(A;A')
Lemma: fpf-sub-val3
∀[A:Type]. ∀[B,C:A ⟶ Type].
∀eq:EqDecider(A). ∀f:a:A fp-> B[a]. ∀g:a:A fp-> C[a]. ∀x:A.
∀[P:a:A ⟶ B[a] ⟶ ℙ]. ∀[Q:a:A ⟶ C[a] ⟶ ℙ].
((∀x:A. ((C[x] ⊆r B[x]) c∧ (P[x;g(x)] ⇒ Q[x;g(x)])) supposing ((↑x ∈ dom(f)) and (↑x ∈ dom(g))))
⇒ {z != f(x) ==> P[y;z] ⇒ z != g(x) ==> Q[y;z] supposing g ⊆ f})
Definition: fpf-const
L |-fpf-> v == <L, λx.v>
Lemma: fpf-const_wf
∀[A,B:Type]. ∀[L:A List]. ∀[v:B]. (L |-fpf-> v ∈ a:A fp-> B)
Lemma: fpf-const-dom
∀[A:Type]. ∀eq:EqDecider(A). ∀L:A List. ∀v:Top. ∀x:A. (↑x ∈ dom(L |-fpf-> v) ⇐⇒ (x ∈ L))
Definition: fpf-single
x : v == <[x], λx.v>
Lemma: fpf-single_wf
∀[A:𝕌{j}]. ∀[B:A ⟶ Type]. ∀[x:A]. ∀[v:B[x]]. (x : v ∈ x:A fp-> B[x])
Lemma: fpf-single_wf2
∀[A,B:Type]. ∀[x:A]. ∀[v:B]. ∀[eqa:EqDecider(A)]. (x : v ∈ a:A fp-> x : B(a)?Top)
Lemma: fpf-single_wf3
∀[A,B:Type]. ∀[x:A]. (x : B ∈ a:A fp-> Type)
Definition: mk_fpf
mk_fpf(L;f) == <L, f>
Lemma: mk_fpf_wf
∀[A:Type]. ∀[L:A List]. ∀[B:A ⟶ Type]. ∀[f:a:{a:A| (a ∈ L)} ⟶ B[a]]. (mk_fpf(L;f) ∈ a:A fp-> B[a])
Lemma: mk_fpf_dom_lemma
∀f,L:Top. (fpf-domain(mk_fpf(L;f)) ~ L)
Lemma: mk_fpf_ap_lemma
∀x,eq,f,L:Top. (mk_fpf(L;f)(x) ~ f x)
Lemma: fpf-single-sub-reflexive
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[x:A]. ∀[v:B[x]]. ∀[eqa:EqDecider(A)]. x : v ⊆ x : v
Lemma: fpf-cap-single1
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[x:A]. ∀[v,z:Top]. (x : v(x)?z ~ v)
Lemma: fpf-split
∀[A:Type]
∀eq:EqDecider(A)
∀[B:A ⟶ Type]
∀f:a:A fp-> B[a]
∀[P:A ⟶ ℙ]
((∀a:A. Dec(P[a]))
⇒ (∃fp,fnp:a:A fp-> B[a]
((f ⊆ fp ⊕ fnp ∧ fp ⊕ fnp ⊆ f)
∧ ((∀a:A. P[a] supposing ↑a ∈ dom(fp)) ∧ (∀a:A. ¬P[a] supposing ↑a ∈ dom(fnp)))
∧ fpf-domain(fp) ⊆ fpf-domain(f)
∧ fpf-domain(fnp) ⊆ fpf-domain(f))))
Lemma: fpf-cap-single-join
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[x:A]. ∀[v,z,f:Top]. (x : v ⊕ f(x)?z ~ v)
Lemma: fpf_ap_single_lemma
∀y,eq,v,x:Top. (x : v(y) ~ v)
Lemma: fpf-ap-single
∀[eq,x,v,y:Top]. (x : v(y) ~ v)
Lemma: fpf-cap-single
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[x,y:A]. ∀[v,z:Top]. (x : v(y)?z ~ if eq x y then v else z fi )
Lemma: fpf-conversion-test
4 : 2 ⊕ 6 : 2 ⊕ 7 : 5 = <[4; 6; 7], λx.if x ∈b [4; 6] then 2 else 5 fi > ∈ i:ℤ fp-> ℤ
Lemma: fpf-val-single1
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[x:A]. ∀[v,P:Top]. (z != x : v(x) ==> P[a;z] ~ True ⇒ P[x;v])
Definition: fpf-add-single
fx : v == f ⊕ x : v
Lemma: fpf-add-single_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[x:A]. ∀[v:B[x]]. ∀[eq:EqDecider(A)]. ∀[f:x:A fp-> B[x]]. (fx : v ∈ x:A fp-> B[x])
Definition: fpf-vals
fpf-vals(eq;P;f) == let L = filter(P;remove-repeats(eq;fst(f))) in zip(L;map(snd(f);L))
Lemma: fpf-vals_wf
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[P:A ⟶ 𝔹]. ∀[f:x:A fp-> B[x]]. (fpf-vals(eq;P;f) ∈ (x:{a:A| ↑(P a)} ×\000C B[x]) List)
Lemma: member-fpf-vals
∀[A:Type]
∀eq:EqDecider(A)
∀[B:A ⟶ Type]
∀P:A ⟶ 𝔹. ∀f:x:A fp-> B[x]. ∀x:A. ∀v:B[x].
((<x, v> ∈ fpf-vals(eq;P;f)) ⇐⇒ {((↑x ∈ dom(f)) ∧ (↑(P x))) ∧ (v = f(x) ∈ B[x])})
Lemma: member-fpf-vals2
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[P:A ⟶ 𝔹]. ∀[f:x:A fp-> B[x]]. ∀[x:{a:A| ↑(P a)} ]. ∀[v:B[x]].
{(↑x ∈ dom(f)) ∧ (v = f(x) ∈ B[x])} supposing (<x, v> ∈ fpf-vals(eq;P;f))
Lemma: filter-fpf-vals
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[P,Q:A ⟶ 𝔹]. ∀[f:x:A fp-> B[x]].
(filter(λpL.Q[fst(pL)];fpf-vals(eq;P;f)) ~ fpf-vals(eq;λa.((P a) ∧b (Q a));f))
Lemma: fpf-vals-singleton
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[P:A ⟶ 𝔹]. ∀[f:x:A fp-> B[x]]. ∀[a:A].
(fpf-vals(eq;P;f) = [<a, f(a)>] ∈ ((x:A × B[x]) List)) supposing ((∀b:A. (↑(P b) ⇐⇒ b = a ∈ A)) and (↑a ∈ dom(f)))
Lemma: fpf-vals-nil
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[P:A ⟶ 𝔹]. ∀[f:x:A fp-> B[x]]. ∀[a:A].
(fpf-vals(eq;P;f) ~ []) supposing ((∀b:A. (↑(P b) ⇐⇒ b = a ∈ A)) and (¬↑a ∈ dom(f)))
Definition: fpf-all
∀x∈dom(f). v=f(x) ⇒ P[x; v] == ∀x:A. ((↑x ∈ dom(f)) ⇒ P[x; f(x)])
Lemma: fpf-all_wf
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[f:x:A fp-> B[x]]. ∀[P:x:{x:A| ↑x ∈ dom(f)} ⟶ B[x] ⟶ ℙ].
(∀x∈dom(f). v=f(x) ⇒ P[x;v] ∈ ℙ)
Definition: fpf-map
fpf-map(a,v.f[a; v];x) == map(λa.f[a; (snd(x)) a];fst(x))
Lemma: fpf-map_wf
∀[A,C:Type]. ∀[B:A ⟶ Type]. ∀[x:a:A fp-> B[a]]. ∀[f:a:{a:A| (a ∈ fpf-domain(x))} ⟶ B[a] ⟶ C].
(fpf-map(a,v.f[a;v];x) ∈ C List)
Definition: fpf-accum
fpf-accum(z,a,v.f[z;
a;
v];y;x) ==
accumulate (with value z and list item a):
f[z;
a;
(snd(x)) a]
over list:
fst(x)
with starting value:
y)
Lemma: fpf-accum_wf
∀[A,C:Type]. ∀[B:A ⟶ Type]. ∀[x:a:A fp-> B[a]]. ∀[y:C]. ∀[f:C ⟶ a:A ⟶ B[a] ⟶ C].
(fpf-accum(z,a,v.f[z;a;v];y;x) ∈ C)
Definition: fpf-rename
rename(r;f) == <map(r;fst(f)), λx.((snd(f)) hd(filter(λy.(eq (r y) x);fst(f))))>
Lemma: fpf-rename_wf
∀[A,C:Type]. ∀[B:A ⟶ Type]. ∀[D:C ⟶ Type]. ∀[eq:EqDecider(C)]. ∀[r:A ⟶ C]. ∀[f:a:A fp-> B[a]].
rename(r;f) ∈ c:C fp-> D[c] supposing ∀a:A. (D[r a] = B[a] ∈ Type)
Lemma: fpf-rename-dom
∀[A,C:Type]. ∀[B:A ⟶ Type].
∀eqa:EqDecider(A). ∀eqc:EqDecider(C). ∀r:A ⟶ C. ∀f:a:A fp-> B[a]. ∀c:C.
(↑c ∈ dom(rename(r;f)) ⇐⇒ ∃a:A. ((↑a ∈ dom(f)) c∧ (c = (r a) ∈ C)))
Lemma: fpf-rename-dom2
∀[A,C:Type]. ∀[eqa:EqDecider(A)]. ∀[eqc:EqDecider(C)]. ∀[eqc':Top]. ∀[r:A ⟶ C]. ∀[f:a:A fp-> Top]. ∀[a:A].
{↑r a ∈ dom(rename(r;f)) supposing ↑a ∈ dom(f)}
Lemma: fpf-rename-ap
∀[A,C:Type]. ∀[B:A ⟶ Type]. ∀[eqa:EqDecider(A)]. ∀[eqc:EqDecider(C)]. ∀[r:A ⟶ C]. ∀[f:a:A fp-> B[a]]. ∀[a:A].
(rename(r;f)(r a) = f(a) ∈ B[a]) supposing ((↑a ∈ dom(f)) and Inj(A;C;r))
Lemma: fpf-rename-ap2
∀[A,C:Type]. ∀[B:A ⟶ Type]. ∀[eqa:EqDecider(A)]. ∀[eqc,eqc':EqDecider(C)]. ∀[r:A ⟶ C]. ∀[f:a:A fp-> B[a]]. ∀[a:A].
(rename(r;f)(r a) = f(a) ∈ B[a]) supposing ((↑a ∈ dom(f)) and Inj(A;C;r))
Lemma: fpf-rename-cap
∀[A,C,B:Type]. ∀[eqa:EqDecider(A)]. ∀[eqc:EqDecider(C)]. ∀[r:A ⟶ C]. ∀[f:a:A fp-> B]. ∀[a:A]. ∀[z:B].
rename(r;f)(r a)?z = f(a)?z ∈ B supposing Inj(A;C;r)
Lemma: fpf-rename-cap2
∀[A,C,B:Type]. ∀[eqa:EqDecider(A)]. ∀[eqc,eqc':EqDecider(C)]. ∀[r:A ⟶ C]. ∀[f:a:A fp-> B]. ∀[a:A]. ∀[z:B].
rename(r;f)(r a)?z = f(a)?z ∈ B supposing Inj(A;C;r)
Lemma: fpf-rename-cap3
∀[A,C,B:Type]. ∀[eqa:EqDecider(A)]. ∀[eqc,eqc':EqDecider(C)]. ∀[r:A ⟶ C]. ∀[f:a:A fp-> B]. ∀[a:A]. ∀[z:B]. ∀[c:C].
(rename(r;f)(c)?z = f(a)?z ∈ B) supposing ((c = (r a) ∈ C) and Inj(A;C;r))
Definition: fpf-inv-rename
fpf-inv-rename(r;rinv;f) == <mapfilter(λx.outl(rinv x);λx.isl(rinv x);fst(f)), (snd(f)) o r>
Lemma: fpf-inv-rename_wf
∀[A,C:Type]. ∀[B:A ⟶ Type]. ∀[D:C ⟶ Type]. ∀[rinv:C ⟶ (A?)]. ∀[r:A ⟶ C]. ∀[f:c:C fp-> D[c]].
(fpf-inv-rename(r;rinv;f) ∈ a:A fp-> B[a]) supposing ((∀a:A. (D[r a] = B[a] ∈ Type)) and inv-rel(A;C;r;rinv))
Definition: fpf-compose
g o f == <fst(f), g o (snd(f))>
Lemma: fpf-compose_wf
∀[A:Type]. ∀[B,C:A ⟶ Type]. ∀[f:a:A fp-> B[a]]. ∀[g:⋂a:A. (B[a] ⟶ C[a])]. (g o f ∈ a:A fp-> C[a])
Lemma: fpf_dom_compose_lemma
∀f,g,x,eq:Top. (x ∈ dom(g o f) ~ x ∈ dom(f))
Lemma: fpf_ap_compose_lemma
∀x,eq,f,g:Top. (g o f(x) ~ g f(x))
Lemma: fpf-dom-compose
∀[x:Top]. ∀[f:a:Top fp-> Top]. ∀[g,eq:Top]. (x ∈ dom(g o f) ~ x ∈ dom(f))
Lemma: fpf-ap-compose
∀[x:Top]. ∀[f:a:Top fp-> Top]. ∀[g,eq:Top]. (g o f(x) ~ g f(x))
Definition: compose-fpf
compose-fpf(a;b;f) == <mapfilter(λx.outl(a x);λx.isl(a x);fpf-domain(f)), (snd(f)) o b>
Lemma: compose-fpf_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[f:x:A fp-> B[x]]. ∀[C:Type]. ∀[a:A ⟶ (C?)]. ∀[b:C ⟶ A].
compose-fpf(a;b;f) ∈ y:C fp-> B[b y] supposing ∀y:A. ((↑isl(a y)) ⇒ ((b outl(a y)) = y ∈ A))
Lemma: compose-fpf-dom
∀[A:Type]. ∀[B:A ⟶ Type].
∀f:x:A fp-> B[x]
∀[C:Type]
∀a:A ⟶ (C?). ∀b:C ⟶ A. ∀y:C.
((y ∈ fpf-domain(compose-fpf(a;b;f))) ⇐⇒ ∃x:A. ((x ∈ fpf-domain(f)) ∧ ((↑isl(a x)) c∧ (y = outl(a x) ∈ C))))
Lemma: fpf-sub-reflexive
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f:a:A fp-> B[a]]. f ⊆ f
Definition: mkfpf
mkfpf(a;b) == <a, b>
Lemma: mkfpf_wf
∀[A:Type]. ∀[a:A List]. ∀[b:a:{a@0:A| (a@0 ∈ a)} ⟶ Top]. (mkfpf(a;b) ∈ a:A fp-> Top)
Lemma: fpf-join-compatible-left
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B,C,D,E,F,G:A ⟶ Type]. ∀[f:a:A fp-> B[a]]. ∀[g:a:A fp-> C[a]]. ∀[h:a:A fp-> D[a]].
({(f ⊕ g || h) supposing (g || h and f || h)}) supposing
((∀a:A. (E[a] ⊆r G[a])) and
(∀a:A. (F[a] ⊆r G[a])) and
(∀a:A. (D[a] ⊆r F[a])) and
(∀a:A. (D[a] ⊆r E[a])) and
(∀a:A. (C[a] ⊆r F[a])) and
(∀a:A. (B[a] ⊆r E[a])))
Lemma: fpf-join-compatible-right
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B,C,D,E,F,G:A ⟶ Type]. ∀[f:a:A fp-> B[a]]. ∀[g:a:A fp-> C[a]]. ∀[h:a:A fp-> D[a]].
({(h || f ⊕ g) supposing (h || g and h || f)}) supposing
((∀a:A. (E[a] ⊆r G[a])) and
(∀a:A. (F[a] ⊆r G[a])) and
(∀a:A. (D[a] ⊆r F[a])) and
(∀a:A. (D[a] ⊆r E[a])) and
(∀a:A. (C[a] ⊆r F[a])) and
(∀a:A. (B[a] ⊆r E[a])))
Lemma: fpf-compatible-self
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[f:a:A fp-> B[a]]. f || f
Lemma: fpf-compatible-join
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[f,g,h:a:A fp-> B[a]]. (h || f ⊕ g) supposing (h || g and h || f)
Lemma: fpf-compatible-join-iff
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[f,g,h:a:A fp-> B[a]].
uiff(h || f ⊕ g;h || f ∧ h || g) supposing f || g
Lemma: fpf-compatible-symmetry
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[f,g:a:A fp-> B[a]]. g || f supposing f || g
Lemma: fpf-disjoint-compatible
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[f,g:a:A fp-> B[a]]. f || g supposing l_disjoint(A;fst(f);fst(g))
Lemma: fpf-compatible-update
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[f,g:a:A fp-> B[a]]. f ⊕ g || f
Lemma: fpf-compatible-update2
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[f,g:a:A fp-> B[a]]. f || f ⊕ g
Lemma: fpf-compatible-update3
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[f,g,h:a:A fp-> B[a]]. h ⊕ f || h ⊕ g supposing f || g
Lemma: fpf-compatible-join2
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[f,g,h:a:A fp-> B[a]]. (f ⊕ g || h) supposing (g || h and f || h)
Lemma: fpf-compatible-singles
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[x,y:A]. ∀[v:B[x]]. ∀[u:B[y]].
x : v || y : u supposing (x = y ∈ A) ⇒ (v = u ∈ B[x])
Lemma: fpf-compatible-singles-trivial
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:Top]. ∀[x,y:A]. ∀[v,u:Top]. x : v || y : u supposing ¬(x = y ∈ A)
Lemma: fpf-single-dom
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[x,y:A]. ∀[v:Top]. uiff(↑x ∈ dom(y : v);x = y ∈ A)
Lemma: fpf-single-dom-sq
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[x,y:A]. ∀[v:Top]. (x ∈ dom(y : v) ~ eq y x)
Lemma: fpf-join-single-property
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[f:a:A fp-> B[a]]. ∀[a:A]. ∀[v:B[a]]. ∀[eq:EqDecider(A)]. ∀[b:A].
({(↑b ∈ dom(f)) ∧ (f ⊕ a : v(b) = f(b) ∈ B[b])}) supposing ((↑b ∈ dom(f ⊕ a : v)) and (¬(b = a ∈ A)))
Lemma: fpf-compatible-single
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[f:a:A fp-> B[a]]. ∀[x:A]. ∀[v:B[x]]. f || x : v supposing ¬↑x ∈ dom(f)
Lemma: fpf-compatible-single-iff
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[f:a:A fp-> B[a]]. ∀[x:A]. ∀[v:B[x]].
uiff(f || x : v;v = f(x) ∈ B[x] supposing ↑x ∈ dom(f))
Lemma: fpf-compatible-single2
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[f:a:A fp-> B[a]]. ∀[x:A]. ∀[v:B[x]]. x : v || f supposing ¬↑x ∈ dom(f)
Lemma: fpf-compatible-singles-iff
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[x,y:A]. ∀[v:B[x]]. ∀[u:B[y]].
uiff(x : v || y : u;v = u ∈ B[x] supposing x = y ∈ A)
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)||
Lemma: fpf-compatible-join-cap
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[f,g:a:A fp-> B[a]]. ∀[x:A]. ∀[z:B[x]].
f ⊕ g(x)?z = g(x)?f(x)?z ∈ B[x] supposing f || g
Lemma: fpf-ap-equal
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[f:a:A fp-> B[a]]. ∀[x:A]. ∀[v:B[x]].
(f(x) = v ∈ B[x]) supposing ((↑x ∈ dom(f)) and f || x : v)
Lemma: fpf-join-dom-decl
∀f,g:x:Id fp-> Type. ∀x:Id. (↑x ∈ dom(f ⊕ g) ⇐⇒ (↑x ∈ dom(f)) ∨ (↑x ∈ dom(g)))
Lemma: fpf-cap-join-subtype
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> Type]. ∀[a:A]. (f ⊕ g(a)?Top ⊆r f(a)?Top)
Lemma: fpf-cap-join-subtype2
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> Type]. ∀[a:A]. f ⊕ g(a)?Top ⊆r g(a)?Top supposing f || g
Lemma: fpf-all-empty
∀[A:Type]. ∀eq,P:Top. (∀y∈dom(⊗). w=⊗(y) ⇒ P[y;w] ⇐⇒ True)
Lemma: fpf-all-single
∀[A:Type]
∀eq:EqDecider(A)
∀[B:A ⟶ Type]. ∀[P:x:A ⟶ B[x] ⟶ ℙ]. ∀x:A. ∀v:B[x]. (∀y∈dom(x : v). w=x : v(y) ⇒ P[y;w] ⇐⇒ P[x;v])
Lemma: fpf-all-single-decl
∀[A:Type]. ∀eq:EqDecider(A). ∀[P:x:A ⟶ Type ⟶ ℙ]. ∀x:A. ∀[v:Type]. (∀y∈dom(x : v). w=x : v(y) ⇒ P[y;w] ⇐⇒ P[x;v])
Lemma: fpf-all-join-decl
∀[A:Type]
∀eq:EqDecider(A)
∀[P:x:A ⟶ Type ⟶ ℙ]
∀f,g:x:A fp-> Type.
(∀y∈dom(f). w=f(y) ⇒ P[y;w] ⇒ ∀y∈dom(g). w=g(y) ⇒ P[y;w] ⇒ ∀y∈dom(f ⊕ g). w=f ⊕ g(y) ⇒ P[y;w])
Definition: non-void-decl
non-void(d) == ∀x∈dom(d). A=d(x) ⇒ A
Lemma: non-void-decl_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[d:a:T fp-> Type]. (non-void(d) ∈ ℙ')
Lemma: non-void-decl-join
∀[T:Type]. ∀eq:EqDecider(T). ∀d1,d2:a:T fp-> Type. (non-void(d1) ⇒ non-void(d2) ⇒ non-void(d1 ⊕ d2))
Lemma: non-void-decl-single
∀[T,A:Type]. ∀x:T. ∀eq:EqDecider(T). (A ⇒ non-void(x : A))
Definition: atom-free-decl
AtomFree(d) == ∀x∈dom(d). A=d(x) ⇒ atom-free{1:n}(Type; A)
Lemma: fpf-empty-compatible-right
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:Top]. ∀[f:a:A fp-> Top]. f || ⊗
Lemma: fpf-empty-compatible-left
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:Top]. ∀[f:a:A fp-> Top]. ⊗ || f
Lemma: fpf-compatible-triple
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[f,g,h:x:T fp-> Type].
({(g ⊆ h ⊕ f ⊕ g ∧ f ⊆ h ⊕ f ⊕ g) ∧ h ⊕ g ⊆ h ⊕ f ⊕ g ∧ h ⊕ f ⊆ h ⊕ f ⊕ g}) supposing (h || g and h || f and f || g)
Definition: fpf-dom-list
fpf-dom-list(f) == fst(f)
Lemma: fpf-dom-list_wf
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[f:a:A fp-> Top]. (fpf-dom-list(f) ∈ {a:A| ↑a ∈ dom(f)} List)
Lemma: member-fpf-dom
∀[A:Type]. ∀eq:EqDecider(A). ∀f:a:A fp-> Top. ∀x:A. (↑x ∈ dom(f) ⇐⇒ (x ∈ fst(f)))
Definition: fpf-restrict
fpf-restrict(f;P) == mk_fpf(filter(P;fpf-domain(f));snd(f))
Lemma: fpf-restrict_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[f:x:A fp-> B[x]]. ∀[P:A ⟶ 𝔹]. (fpf-restrict(f;P) ∈ x:{x:A| ↑(P x)} fp-> B[x])
Lemma: fpf-restrict_wf2
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[f:x:A fp-> B[x]]. ∀[P:A ⟶ 𝔹]. (fpf-restrict(f;P) ∈ x:A fp-> B[x])
Lemma: domain_fpf_restrict_lemma
∀P,f:Top. (fpf-domain(fpf-restrict(f;P)) ~ filter(P;fpf-domain(f)))
Lemma: ap_fpf_restrict_lemma
∀x,eq,P,f:Top. (fpf-restrict(f;P)(x) ~ f(x))
Lemma: fpf-restrict-domain
∀[f,P:Top]. (fpf-domain(fpf-restrict(f;P)) ~ filter(P;fpf-domain(f)))
Lemma: fpf-restrict-dom
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[f:x:A fp-> B[x]]. ∀[P:A ⟶ 𝔹]. ∀[x:A].
uiff(↑x ∈ dom(fpf-restrict(f;P));{(↑x ∈ dom(f)) ∧ (↑(P x))})
Lemma: fpf-restrict-ap
∀[f,P,eq,x:Top]. (fpf-restrict(f;P)(x) ~ f(x))
Lemma: fpf-restrict-cap
∀[A:Type]. ∀[P:A ⟶ 𝔹]. ∀[x:A].
∀[f:x:A fp-> Top]. ∀[eq:EqDecider(A)]. ∀[z:Top]. (fpf-restrict(f;P)(x)?z ~ f(x)?z) supposing ↑(P x)
Lemma: fpf-restrict-compatible
∀[A:Type]. ∀[P:A ⟶ 𝔹]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[f,g:x:A fp-> B[x]].
fpf-restrict(f;P) || g supposing f || g
Lemma: fpf-restrict-compatible2
∀[A:Type]. ∀[P:A ⟶ 𝔹]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[f,g:x:A fp-> B[x]].
f || fpf-restrict(g;P) supposing f || g
Lemma: l_disjoint-fpf-dom
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[f:a:A fp-> Top]. ∀[L:A List].
uiff(l_disjoint(A;fst(f);L);∀[a:A]. ¬(a ∈ L) supposing ↑a ∈ dom(f))
Lemma: l_disjoint-fpf-join-dom
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> Top]. ∀[L:A List].
uiff(l_disjoint(A;fst(f ⊕ g);L);l_disjoint(A;fst(f);L) ∧ l_disjoint(A;fst(g);L))
Definition: pairs-fpf
fpf(L) ==
<remove-repeats(eq1;map(λp.(fst(p));L)), λx.reduce(λp,l. if eqof(eq1) (fst(p)) x then insert(snd(p);l) else l fi ;[];L\000C)>
Lemma: pairs-fpf_wf
∀[A,B:Type]. ∀[eq1:EqDecider(A)]. ∀[eq2:EqDecider(B)]. ∀[L:(A × B) List]. (fpf(L) ∈ a:A fp-> B List)
Lemma: pairs-fpf_property
∀[A,B:Type].
∀eq1:EqDecider(A). ∀eq2:EqDecider(B). ∀L:(A × B) List.
(no_repeats(A;fpf-domain(fpf(L)))
∧ (∀a:A. ((a ∈ fpf-domain(fpf(L))) ⇐⇒ ∃b:B. (<a, b> ∈ L)))
∧ ∀a∈dom(fpf(L)). l=fpf(L)(a) ⇒ no_repeats(B;l) ∧ (∀b:B. ((b ∈ l) ⇐⇒ (<a, b> ∈ L))))
Lemma: no_repeats-pairs-fpf
∀[A,B:Type]. ∀[eq1:EqDecider(A)]. ∀[eq2:EqDecider(B)]. ∀[L:(A × B) List]. no_repeats(A;fpf-domain(fpf(L)))
Definition: fpf-normalize
fpf-normalize(eq;g) == reduce(λx,f. x : (snd(g)) x ⊕ f;⊗;fst(g))
Lemma: fpf-normalize_wf
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[g:x:A fp-> B[x]]. (fpf-normalize(eq;g) ∈ x:A fp-> B[x])
Lemma: fpf-normalize-dom
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[g:x:A fp-> B[x]]. ∀[x:A]. (x ∈ dom(fpf-normalize(eq;g)) ~ x ∈ dom(g))
Lemma: fpf-normalize-ap
∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[g:x:A fp-> B[x]]. ∀[x:A].
fpf-normalize(eq;g)(x) = g(x) ∈ B[x] supposing ↑x ∈ dom(g)
Lemma: free-from-atom-fpf-ap
∀[a:Atom1]. ∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ 𝕌']. ∀[f:x:A fp-> B[x]].
∀[x:A]. (a#f(x):B[x]) supposing ((↑x ∈ dom(f)) and a#x:A) supposing a#f:x:A fp-> B[x]
Home
Index