bool_size : bool -> numfull_sum_size : (α -> num) -> (β -> num) -> α + β -> numitself_size : α itself -> nummin_pair_size : (α -> num) -> (β -> num) -> α # β -> numone_size : unit -> numoption_size : (α -> num) -> α option -> numpair_size : (α -> num) -> (β -> num) -> α # β -> numsum_size : (α -> num) -> (β -> num) -> α + β -> numbool_size_def⊢ ∀b. bool_size b = 0
full_sum_size_def⊢ ∀f g sum. full_sum_size f g sum = 1 + sum_size f g sum
itself_size_def⊢ ∀x. itself_size x = 0
min_pair_size_def⊢ ∀f g x y. min_pair_size f g (x,y) = f x + g y
one_size_def⊢ ∀x. one_size x = 0
option_size_def⊢ (∀f. option_size f NONE = 0) ∧ ∀f x. option_size f (SOME x) = 1 + f x
pair_size_def⊢ ∀f g x y. pair_size f g (x,y) = 1 + (f x + g y)
sum_size_def⊢ (∀f g x. sum_size f g (INL x) = f x) ∧ ∀f g y. sum_size f g (INR y) = g y
⊢ full_sum_size f g (INL x) = 1 + f x ∧ full_sum_size f g (INR y) = 1 + g y