Definition: equalf_from_lef
equalf_from_lef(lef;x;y) == if lef x y then lef y x else ff fi
Lemma: equalf_from_lef_wf
∀[y:Type]. ∀[lef:y ─→ y ─→ 𝔹]. ∀[x,y:y]. (equalf_from_lef(lef;x;y) ∈ 𝔹)
Definition: l_treeco
l_treeco(L;T) ==
corec(X.lbl:Atom × if lbl =a "leaf" then L
if lbl =a "node" then val:T × left_subtree:X × X
else Void
fi )
Lemma: l_treeco_wf
∀[L,T:Type]. (l_treeco(L;T) ∈ Type)
Lemma: l_treeco-ext
∀[L,T:Type].
l_treeco(L;T) ≡ lbl:Atom × if lbl =a "leaf" then L
if lbl =a "node" then val:T × left_subtree:l_treeco(L;T) × l_treeco(L;T)
else Void
fi
Definition: l_treeco_size
l_treeco_size(p) ==
fix((λsize,p. let lbl,x = p
in if lbl =a "leaf" then 0
if lbl =a "node" then let val,left_subtree,z = x in (1 + (size left_subtree)) + (size z)
else 0
fi ))
p
Lemma: l_treeco_size_wf
∀[L,T:Type]. ∀[p:l_treeco(L;T)]. (l_treeco_size(p) ∈ partial(ℕ))
Definition: l_tree
l_tree(L;T) == {p:l_treeco(L;T)| (l_treeco_size(p))↓}
Lemma: l_tree_wf
∀[L,T:Type]. (l_tree(L;T) ∈ Type)
Definition: l_tree_size
l_tree_size(p) ==
fix((λsize,p. let lbl,x = p
in if lbl =a "leaf" then 0
if lbl =a "node" then let val,left_subtree,z = x in (1 + (size left_subtree)) + (size z)
else 0
fi ))
p
Lemma: l_tree_size_wf
∀[L,T:Type]. ∀[p:l_tree(L;T)]. (l_tree_size(p) ∈ ℕ)
Lemma: l_tree-ext
∀[L,T:Type].
l_tree(L;T) ≡ lbl:Atom × if lbl =a "leaf" then L
if lbl =a "node" then val:T × left_subtree:l_tree(L;T) × l_tree(L;T)
else Void
fi
Definition: l_tree_leaf
l_tree_leaf(val) == <"leaf", val>
Lemma: l_tree_leaf_wf
∀[L,T:Type]. ∀[val:L]. (l_tree_leaf(val) ∈ l_tree(L;T))
Definition: l_tree_node
l_tree_node(val;left_subtree;right_subtree) == <"node", val, left_subtree, right_subtree>
Lemma: l_tree_node_wf
∀[L,T:Type]. ∀[val:T]. ∀[left_subtree,right_subtree:l_tree(L;T)].
(l_tree_node(val;left_subtree;right_subtree) ∈ l_tree(L;T))
Definition: l_tree_leaf?
l_tree_leaf?(v) == fst(v) =a "leaf"
Lemma: l_tree_leaf?_wf
∀[L,T:Type]. ∀[v:l_tree(L;T)]. (l_tree_leaf?(v) ∈ 𝔹)
Definition: l_tree_leaf-val
l_tree_leaf-val(v) == snd(v)
Lemma: l_tree_leaf-val_wf
∀[L,T:Type]. ∀[v:l_tree(L;T)]. l_tree_leaf-val(v) ∈ L supposing ↑l_tree_leaf?(v)
Definition: l_tree_node?
l_tree_node?(v) == fst(v) =a "node"
Lemma: l_tree_node?_wf
∀[L,T:Type]. ∀[v:l_tree(L;T)]. (l_tree_node?(v) ∈ 𝔹)
Definition: l_tree_node-val
l_tree_node-val(v) == fst(snd(v))
Lemma: l_tree_node-val_wf
∀[L,T:Type]. ∀[v:l_tree(L;T)]. l_tree_node-val(v) ∈ T supposing ↑l_tree_node?(v)
Definition: l_tree_node-left_subtree
l_tree_node-left_subtree(v) == fst(snd(snd(v)))
Lemma: l_tree_node-left_subtree_wf
∀[L,T:Type]. ∀[v:l_tree(L;T)]. l_tree_node-left_subtree(v) ∈ l_tree(L;T) supposing ↑l_tree_node?(v)
Definition: l_tree_node-right_subtree
l_tree_node-right_subtree(v) == snd(snd(snd(v)))
Lemma: l_tree_node-right_subtree_wf
∀[L,T:Type]. ∀[v:l_tree(L;T)]. l_tree_node-right_subtree(v) ∈ l_tree(L;T) supposing ↑l_tree_node?(v)
Lemma: l_tree-induction
∀[L,T:Type]. ∀[P:l_tree(L;T) ─→ ℙ].
((∀val:L. P[l_tree_leaf(val)])
⇒ (∀val:T. ∀left_subtree,right_subtree:l_tree(L;T).
(P[left_subtree] ⇒ P[right_subtree] ⇒ P[l_tree_node(val;left_subtree;right_subtree)]))
⇒ {∀v:l_tree(L;T). P[v]})
Lemma: l_tree-definition
∀[L,T,A:Type]. ∀[R:A ─→ l_tree(L;T) ─→ ℙ].
((∀val:L. {x:A| R[x;l_tree_leaf(val)]} )
⇒ (∀val:T. ∀left_subtree,right_subtree:l_tree(L;T).
({x:A| R[x;left_subtree]}
⇒ {x:A| R[x;right_subtree]}
⇒ {x:A| R[x;l_tree_node(val;left_subtree;right_subtree)]} ))
⇒ {∀v:l_tree(L;T). {x:A| R[x;v]} })
Definition: l_tree_ind
l_tree_ind(v;
l_tree_leaf(val)⇒ leaf[val];
l_tree_node(val,left_subtree,right_subtree)⇒ rec1,rec2.node[val; left_subtree; right_subtree; rec1;
rec2]) ==
fix((λl_tree_ind,v. let lbl,v1 = v
in if lbl="leaf" then leaf[v1]
if lbl="node"
then let val,v2 = v1
in let left_subtree,v3 = v2
in node[val; left_subtree; v3; l_tree_ind left_subtree; l_tree_ind v3]
else ⊥
fi ))
v
Lemma: l_tree_ind_wf
∀[L,T,A:Type]. ∀[R:A ─→ l_tree(L;T) ─→ ℙ]. ∀[v:l_tree(L;T)]. ∀[leaf:val:L ─→ {x:A| R[x;l_tree_leaf(val)]} ].
∀[node:val:T
─→ left_subtree:l_tree(L;T)
─→ right_subtree:l_tree(L;T)
─→ {x:A| R[x;left_subtree]}
─→ {x:A| R[x;right_subtree]}
─→ {x:A| R[x;l_tree_node(val;left_subtree;right_subtree)]} ].
(l_tree_ind(v;
l_tree_leaf(val)⇒ leaf[val];
l_tree_node(val,left_subtree,right_subtree)⇒ rec1,rec2.node[val;left_subtree;right_subtree;rec1;rec2])
∈ {x:A| R[x;v]} )
Lemma: l_tree_ind_wf_simple
∀[L,T,A:Type]. ∀[v:l_tree(L;T)]. ∀[leaf:val:L ─→ A]. ∀[node:val:T
─→ left_subtree:l_tree(L;T)
─→ right_subtree:l_tree(L;T)
─→ A
─→ A
─→ A].
(l_tree_ind(v;
l_tree_leaf(val)⇒ leaf[val];
l_tree_node(val,left_subtree,right_subtree)⇒ rec1,rec2.node[val;left_subtree;right_subtree;rec1;rec2])
∈ A)
Lemma: l_tree_covariant
∀[A,B,T:Type]. l_tree(A;T) ⊆r l_tree(B;T) supposing A ⊆r B
Definition: max_w_ord
max_w_ord(t1;t2;f) == if f[t1] <z f[t2] then t2 else t1 fi
Lemma: max_w_ord_wf
∀[T:Type]. ∀[t1,t2:T]. ∀[f:T ─→ ℤ]. (max_w_ord(t1;t2;f) ∈ T)
Definition: max_w_unit_l_tree
max_w_unit_l_tree(u1;u2;f) ==
case u1 of inl(val1) => case u2 of inl(val2) => inl max_w_ord(val1;val2;f) | inr(unitval2) => u1 | inr(unitval1) => u2
Lemma: max_w_unit_l_tree_wf
∀[T:Type]. ∀[u1,u2:T?]. ∀[f:T ─→ ℤ]. (max_w_unit_l_tree(u1;u2;f) ∈ T?)
Definition: max_l_tree
max_l_tree(t;f) ==
l_tree_ind(t;
l_tree_leaf(v)⇒ inr ⋅ ;
l_tree_node(v,ltr,rtr)⇒ ltrm,rtrm.max_w_unit_l_tree(inl v;rtrm;f))
Lemma: max_l_tree_wf
∀[L,T:Type]. ∀t:l_tree(L;T). ∀f:T ─→ ℤ. (max_l_tree(t;f) ∈ T?)
Definition: min_w_ord
min_w_ord(t1;t2;f) == if f[t1] <z f[t2] then t1 else t2 fi
Lemma: min_w_ord_wf
∀[T:Type]. ∀[t1,t2:T]. ∀[f:T ─→ ℤ]. (min_w_ord(t1;t2;f) ∈ T)
Definition: min_w_unit_l_tree
min_w_unit_l_tree(u1;u2;f) ==
case u1 of inl(val1) => case u2 of inl(val2) => inl min_w_ord(val1;val2;f) | inr(unitval2) => u1 | inr(unitval1) => u2
Lemma: min_w_unit_l_tree_wf
∀[T:Type]. ∀[u1,u2:T?]. ∀[f:T ─→ ℤ]. (min_w_unit_l_tree(u1;u2;f) ∈ T?)
Definition: min_l_tree
min_l_tree(t;f) ==
l_tree_ind(t;
l_tree_leaf(v)⇒ inr ⋅ ;
l_tree_node(v,ltr,rtr)⇒ ltrm,rtrm.min_w_unit_l_tree(inl v;ltrm;f))
Lemma: min_l_tree_wf
∀[L,T:Type]. ∀t:l_tree(L;T). ∀f:T ─→ ℤ. (min_l_tree(t;f) ∈ T?)
Definition: bs_l_tree
bs_l_tree(t;f) ==
l_tree_ind(t;
l_tree_leaf(v)⇒ tt;
l_tree_node(v,ltr,rtr)⇒ ltrp,rtrp.ltrp
∧b rtrp
∧b case max_l_tree(ltr;f) of inl(maxl) => f[maxl] <z f[v] | inr(ul) => tt
∧b case min_l_tree(rtr;f) of inl(minr) => f[v] <z f[minr] | inr(ur) => tt)
Lemma: bs_l_tree_wf
∀[L,T:Type]. ∀[t:l_tree(L;T)]. ∀[f:T ─→ ℤ]. (bs_l_tree(t;f) ∈ 𝔹)
Definition: bs_l_tree_member
bs_l_tree_member(x;t;f) ==
l_tree_ind(t;
l_tree_leaf(v)⇒ tt;
l_tree_node(v,ltr,rtr)⇒ ltrm,rtrm.(f[x] =z f[v]) ∨bif f[x] <z f[v] then ltrm else rtrm fi )
Lemma: bs_l_tree_member_wf
∀[L,T:Type]. ∀[t:l_tree(L;T)]. ∀[x:T]. ∀[f:T ─→ ℤ]. (bs_l_tree_member(x;t;f) ∈ 𝔹)
Home
Index