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;`
`           Leaf(lval)`` leaf[lval];`
`           Node(nval,left_subtree,right_subtree)`` rec1,rec2.node[nval;`
`                                                                  left_subtree;`
`                                                                  right_subtree;`
`                                                                  rec1;`
`                                                                  rec2])  ==`
`  fix((λl_tree_ind,v. let lbl,lval = v `
`                      in if lbl="leaf" then leaf[lval]`
`                         if lbl="node"`
`                           then let nval,v2 = lval `
`                                in let left_subtree,v3 = v2 `
`                                   in node[nval;`
`                                           left_subtree;`
`                                           v3;`
`                                           l_tree_ind left_subtree;`
`                                           l_tree_ind v3]`
`                         else Ax`
`                         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;`
`              Leaf(val)`` leaf[val];`
`              Node(val,left_subtree,right_subtree)`` rec1,rec2.node[val;left_subtree;right_subtree;rec1;rec2])  ∈ {x:A| `
`                                                                                                                   R[x;`
`                                                                                                                    v]} \000C)`

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;`
`              Leaf(val)`` leaf[val];`
`              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; Leaf(v)`` inr ⋅ ; 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?)`

Lemma: l_tree_ind_test
`max_l_tree(l_tree_leaf(3);λx.x) ~ inr ⋅ `

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; Leaf(v)`` inr ⋅ ; 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;`
`             Leaf(v)`` tt;`
`             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;`
`             Leaf(v)`` tt;`
`             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