Lines Matching refs:g2
109 prove(``!f1 g1 f2 g2.
110 ((sum_retrieve g1 g2)o h) o ((sum_map f1 f2)o h) =
111 ((sum_retrieve (g1 o f1) (g2 o f2)) o h)``
119 val sum_inj_pair_thm = prove(``!f1 g1 f2 g2.
121 (inj_pair f2 g2) ==>
122 (inj_pair (sum_map f1 f2) (sum_retrieve g1 g2))``,
130 val sum_retrieve_map_thm = prove(``!f1 g1 f2 g2.
131 (sum_retrieve g1 g2) o (sum_map f1 f2) =
132 (sum_retrieve (g1 o f1) (g2 o f2))
178 val prod_inj_pair_thm = prove(``!f1 g1 f2 g2.
180 (inj_pair f2 g2) ==>
181 (inj_pair (f1 ## f2) (prod_retrieve g1 g2))``,
192 val prod_retrieve_map_thm = prove(``!f1 g1 f2 g2.
193 (prod_retrieve g1 g2) o (f1 ## f2) =
194 (prod_retrieve (g1 o f1) (g2 o f2))
277 val prod_retrieve_map_thm = prove(``!f1 g1 f2 g2.
278 (prod_retrieve g1 g2) o (f1 ## f2) =
279 (prod_retrieve (g1 o f1) (g2 o f2))