blist_coder : num ->
(α -> bool) # (β -> γ list) # (bool list -> (α # bool list) option) ->
(α list -> bool) # (β list -> γ list) # (bool list -> (α list # bool list) option)bnum_coder : num ->
(num -> bool) -> (num -> bool) # (num -> bool list) # (bool list -> (num # bool list) option)bool_coder : (bool -> bool) -> (bool -> bool) # (bool -> bool list) # (bool list -> (bool # bool list) option)decode : (α -> bool) -> (bool list -> (α # bool list) option) -> bool list -> αdecoder : (α -> bool) # (α -> bool list) # (bool list -> (α # bool list) option) -> bool list -> αdomain : (α -> bool) # (α -> bool list) # (bool list -> (α # bool list) option) -> α -> boolencoder : (α -> bool) # (α -> bool list) # (bool list -> (α # bool list) option) -> α -> bool listlist_coder : (α -> bool) # (β -> bool list) # (bool list -> (α # bool list) option) ->
(α list -> bool) # (β list -> bool list) # (bool list -> (α list # bool list) option)num_coder : (num -> bool) -> (num -> bool) # (num -> bool list) # (bool list -> (num # bool list) option)option_coder : (α -> bool) # (β -> bool list) # (bool list -> (α # bool list) option) ->
(α option -> bool) # (β option -> bool list) # (bool list -> (α option # bool list) option)prod_coder : (α -> bool) # (γ -> bool list) # (bool list -> (α # bool list) option) ->
(β -> bool) # (δ -> bool list) # (bool list -> (β # bool list) option) ->
(α # β -> bool) # (γ # δ -> bool list) # (bool list -> ((α # β) # bool list) option)sum_coder : (α -> bool) # (γ -> bool list) # (bool list -> (α # bool list) option) ->
(β -> bool) # (δ -> bool list) # (bool list -> (β # bool list) option) ->
(α + β -> bool) # (γ + δ -> bool list) # (bool list -> ((α + β) # bool list) option)tree_coder : (α -> bool) # (β -> bool list) # (bool list -> (α # bool list) option) ->
(α tree -> bool) # (β tree -> bool list) # (bool list -> (α tree # bool list) option)unit_coder : (unit -> bool) -> (unit -> bool) # (unit -> bool list) # (bool list -> (unit # bool list) option)wf_coder : (α -> bool) # (α -> bool list) # (bool list -> (α # bool list) option) -> bool⊢ ∀m p e d.
blist_coder m (p,e,d) =
(lift_blist m p,encode_blist m e,decode_blist (lift_blist m p) m d)
⊢ ∀m p. bnum_coder m p = (p,encode_bnum m,decode_bnum m p)
⊢ ∀p. bool_coder p = (p,encode_bool,decode_bool p)
⊢ ∀p d l. decode p d l = case d l of NONE => @x. p x | SOME (x,v2) => x
⊢ ∀p e d. decoder (p,e,d) = decode p d
⊢ ∀p e d. domain (p,e,d) = p
⊢ ∀p e d. encoder (p,e,d) = e
⊢ ∀p e d.
list_coder (p,e,d) = (EVERY p,encode_list e,decode_list (EVERY p) d)
⊢ ∀p. num_coder p = (p,encode_num,decode_num p)
⊢ ∀p e d.
option_coder (p,e,d) =
(lift_option p,encode_option e,decode_option (lift_option p) d)
⊢ ∀p1 e1 d1 p2 e2 d2.
prod_coder (p1,e1,d1) (p2,e2,d2) =
(lift_prod p1 p2,encode_prod e1 e2,decode_prod (lift_prod p1 p2) d1 d2)
⊢ ∀p1 e1 d1 p2 e2 d2.
sum_coder (p1,e1,d1) (p2,e2,d2) =
(lift_sum p1 p2,encode_sum e1 e2,decode_sum (lift_sum p1 p2) d1 d2)
⊢ ∀p e d.
tree_coder (p,e,d) =
(lift_tree p,encode_tree e,decode_tree (lift_tree p) d)
⊢ ∀p. unit_coder p = (p,encode_unit,decode_unit p)
⊢ ∀p e d. wf_coder (p,e,d) ⇔ wf_pred p ∧ wf_encoder p e ∧ d = enc2dec p e
⊢ ∀p e x. wf_encoder p e ∧ p x ⇒ decode p (enc2dec p e) (e x) = x
⊢ ∀c. wf_coder c ⇒ ∀x. domain c x ⇒ decoder c (encoder c x) = x
⊢ ∀m c. wf_coder c ⇒ wf_coder (blist_coder m c)
⊢ ∀m p. wf_pred_bnum m p ⇒ wf_coder (bnum_coder m p)
⊢ ∀p. wf_pred p ⇒ wf_coder (bool_coder p)
⊢ ∀c. wf_coder c ⇒ ∀l. domain c (decoder c l)
⊢ ∀c. wf_coder c ⇒ wf_coder (list_coder c)
⊢ ∀p. wf_pred p ⇒ wf_coder (num_coder p)
⊢ ∀p e f.
(∃x. p x) ∧ wf_encoder p e ∧ (∀x. p x ⇒ e x = f x) ⇒
wf_coder (p,e,enc2dec p f)
⊢ ∀c. wf_coder c ⇒ wf_coder (option_coder c)
⊢ ∀c1 c2. wf_coder c1 ∧ wf_coder c2 ⇒ wf_coder (prod_coder c1 c2)
⊢ ∀c1 c2. wf_coder c1 ∧ wf_coder c2 ⇒ wf_coder (sum_coder c1 c2)
⊢ ∀c. wf_coder c ⇒ wf_coder (tree_coder c)
⊢ ∀p. wf_pred p ⇒ wf_coder (unit_coder p)