signature TNet_LIBinterfaceTheory = sig type thm = Thm.thm (* Definitions *) val LIB_interface_TY_DEF : thm val LIB_interface_case_def : thm val LIB_interface_repfns : thm val LIB_interface_size_def : thm val MODULE_interface_TY_DEF : thm val MODULE_interface_case_def : thm val MODULE_interface_repfns : thm val MODULE_interface_size_def : thm val STORE_interface_TY_DEF : thm val STORE_interface_case_def : thm val STORE_interface_repfns : thm val STORE_interface_size_def : thm val STget : thm val STnew : thm val STset : thm val TNet_LIBinterface0_def : thm val TNet_LIBinterface10_def : thm val TNet_LIBinterface11_def : thm val TNet_LIBinterface12_def : thm val TNet_LIBinterface13_def : thm val TNet_LIBinterface14_def : thm val TNet_LIBinterface15_def : thm val TNet_LIBinterface16_def : thm val TNet_LIBinterface17_def : thm val TNet_LIBinterface18_def : thm val TNet_LIBinterface19_def : thm val TNet_LIBinterface1_def : thm val TNet_LIBinterface20_def : thm val TNet_LIBinterface21_def : thm val TNet_LIBinterface22_def : thm val TNet_LIBinterface23_def : thm val TNet_LIBinterface24_def : thm val TNet_LIBinterface25_def : thm val TNet_LIBinterface2_def : thm val TNet_LIBinterface3_def : thm val TNet_LIBinterface4_def : thm val TNet_LIBinterface5_def : thm val TNet_LIBinterface6_def : thm val TNet_LIBinterface7_def : thm val TNet_LIBinterface8_def : thm val TNet_LIBinterface9_def : thm val bind : thm val close : thm val connect : thm val create : thm val delay : thm val disconnect : thm val exit : thm val get_status : thm val geterr : thm val getifaddrs : thm val getpeername : thm val getsockname : thm val getsockopt : thm val ip_of_string : thm val port_of_int : thm val print_endline_flush : thm val recvfrom : thm val retTypeM_def : thm val retTypeST_primitive_def : thm val retType_def : thm val select : thm val sendto : thm val setsockopt : thm val socket : thm val start_heartbeat_a : thm val start_heartbeat_b : thm (* Theorems *) val LIB_interface_11 : thm val LIB_interface_Axiom : thm val LIB_interface_case_cong : thm val LIB_interface_distinct : thm val LIB_interface_induction : thm val LIB_interface_nchotomy : thm val MODULE_interface_11 : thm val MODULE_interface_Axiom : thm val MODULE_interface_case_cong : thm val MODULE_interface_distinct : thm val MODULE_interface_induction : thm val MODULE_interface_nchotomy : thm val STORE_interface_11 : thm val STORE_interface_Axiom : thm val STORE_interface_case_cong : thm val STORE_interface_distinct : thm val STORE_interface_induction : thm val STORE_interface_nchotomy : thm val retTypeST_def : thm val retTypeST_ind : thm val TNet_LIBinterface_grammars : parse_type.grammar * term_grammar.grammar (* [TNet_types] Parent theory of "TNet_LIBinterface" [LIB_interface_TY_DEF] Definition |- ?rep'. TYPE_DEFINITION (\a0. !'LIB_interface'. (!a0. (?a. a0 = (\a. CONSTR 0 (a,(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC 0) ((@v. T),a,(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC 0)) ((@v. T),(@v. T),a,(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC 0))) ((@v. T),(@v. T),(@v. T),a,(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC 0)))) ((@v. T),(@v. T),(@v. T),a,(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC 0))))) ((@v. T),(@v. T),(@v. T),a,(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC 0)))))) ((@v. T),(@v. T),(@v. T),(@v. T),a,(@v. T), (@v. T),(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),a, (@v. T),(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))) ((@v. T),(@v. T),(@v. T),a,(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), a,(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),a,(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))))) ((@v. T),(@v. T),(@v. T),a,(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),a,(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))))))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))))))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),(@v. T),a) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))))))))))) (a,(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))))))))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),(@v. T),a) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))))))))))))) (a,(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))))))))))))) (a,(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) ==> 'LIB_interface' a0) ==> 'LIB_interface' a0) rep' [LIB_interface_case_def] Definition |- (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 a. case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 (socket a) = f a) /\ (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 a. case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 (bind a) = f1 a) /\ (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 a. case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 (connect a) = f2 a) /\ (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 a. case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 (disconnect a) = f3 a) /\ (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 a. case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 (getsockname a) = f4 a) /\ (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 a. case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 (getpeername a) = f5 a) /\ (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 a. case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 (sendto a) = f6 a) /\ (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 a. case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 (recvfrom a) = f7 a) /\ (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 a. case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 (geterr a) = f8 a) /\ (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 a. case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 (getsockopt a) = f9 a) /\ (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 a. case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 (setsockopt a) = f10 a) /\ (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 a. case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 (close a) = f11 a) /\ (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 a. case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 (select a) = f12 a) /\ (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 a. case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 (delay a) = f13 a) /\ (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 a. case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 (port_of_int a) = f14 a) /\ (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 a. case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 (ip_of_string a) = f15 a) /\ (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 a. case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 (getifaddrs a) = f16 a) /\ (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 a. case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 (print_endline_flush a) = f17 a) /\ (!f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 a. case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 (create a) = f18 a) /\ !f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 a. case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 (exit a) = f19 a [LIB_interface_repfns] Definition |- (!a. mk_LIB_interface (dest_LIB_interface a) = a) /\ !r. (\a0. !'LIB_interface'. (!a0. (?a. a0 = (\a. CONSTR 0 (a,(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC 0) ((@v. T),a,(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC 0)) ((@v. T),(@v. T),a,(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC 0))) ((@v. T),(@v. T),(@v. T),a,(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC 0)))) ((@v. T),(@v. T),(@v. T),a,(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC 0))))) ((@v. T),(@v. T),(@v. T),a,(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC 0)))))) ((@v. T),(@v. T),(@v. T),(@v. T),a,(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),a,(@v. T), (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))) ((@v. T),(@v. T),(@v. T),a,(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),a, (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),a,(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))))) ((@v. T),(@v. T),(@v. T),a,(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),a,(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))))))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))))))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),(@v. T),a) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))))))))))) (a,(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))))))))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),(@v. T),a) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))))))))))))) (a,(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))))))))))))) (a,(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) ==> 'LIB_interface' a0) ==> 'LIB_interface' a0) r = (dest_LIB_interface (mk_LIB_interface r) = r) [LIB_interface_size_def] Definition |- (!a. LIB_interface_size (socket a) = 1) /\ (!a. LIB_interface_size (bind a) = 1 + (\(x,y). fd_size x + (\(x,y). (case x of NONE -> 0 || SOME x -> SUC (ip_size x)) + case y of NONE -> 0 || SOME x -> SUC (port_size x)) y) a) /\ (!a. LIB_interface_size (connect a) = 1 + (\(x,y). fd_size x + (\(x,y). ip_size x + case y of NONE -> 0 || SOME x -> SUC (port_size x)) y) a) /\ (!a. LIB_interface_size (disconnect a) = 1 + fd_size a) /\ (!a. LIB_interface_size (getsockname a) = 1 + fd_size a) /\ (!a. LIB_interface_size (getpeername a) = 1 + fd_size a) /\ (!a. LIB_interface_size (sendto a) = 1 + (\(x,y). fd_size x + (\(x,y). (case x of NONE -> 0 || SOME x -> SUC ((\(x,y). ip_size x + port_size y) x)) + (\(x,y). string_size x + case y of T -> 0 || F -> 0) y) y) a) /\ (!a. LIB_interface_size (recvfrom a) = 1 + (\(x,y). fd_size x + case y of T -> 0 || F -> 0) a) /\ (!a. LIB_interface_size (geterr a) = 1 + fd_size a) /\ (!a. LIB_interface_size (getsockopt a) = 1 + (\(x,y). fd_size x + sockopt_size y) a) /\ (!a. LIB_interface_size (setsockopt a) = 1 + (\(x,y). fd_size x + (\(x,y). sockopt_size x + case y of T -> 0 || F -> 0) y) a) /\ (!a. LIB_interface_size (close a) = 1 + fd_size a) /\ (!a. LIB_interface_size (select a) = 1 + (\(x,y). list_size fd_size x + (\(x,y). list_size fd_size x + case y of NONE -> 0 || SOME x -> SUC ((\v. 0) x)) y) a) /\ (!a. LIB_interface_size (delay a) = 1) /\ (!a. LIB_interface_size (port_of_int a) = 1) /\ (!a. LIB_interface_size (ip_of_string a) = 1 + string_size a) /\ (!a. LIB_interface_size (getifaddrs a) = 1) /\ (!a. LIB_interface_size (print_endline_flush a) = 1 + string_size a) /\ (!a. LIB_interface_size (create a) = 1) /\ !a. LIB_interface_size (exit a) = 1 [MODULE_interface_TY_DEF] Definition |- ?rep'. TYPE_DEFINITION (\a0. !'MODULE_interface'. (!a0. (?a. a0 = (\a. CONSTR 0 (a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC 0) ((@v. T),a) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC 0)) (a,@v. T) (\n. BOTTOM)) a) ==> 'MODULE_interface' a0) ==> 'MODULE_interface' a0) rep' [MODULE_interface_case_def] Definition |- (!f f1 f2 a. case f f1 f2 (start_heartbeat_a a) = f a) /\ (!f f1 f2 a. case f f1 f2 (get_status a) = f1 a) /\ !f f1 f2 a. case f f1 f2 (start_heartbeat_b a) = f2 a [MODULE_interface_repfns] Definition |- (!a. mk_MODULE_interface (dest_MODULE_interface a) = a) /\ !r. (\a0. !'MODULE_interface'. (!a0. (?a. a0 = (\a. CONSTR 0 (a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC 0) ((@v. T),a) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC 0)) (a,@v. T) (\n. BOTTOM)) a) ==> 'MODULE_interface' a0) ==> 'MODULE_interface' a0) r = (dest_MODULE_interface (mk_MODULE_interface r) = r) [MODULE_interface_size_def] Definition |- (!a. MODULE_interface_size (start_heartbeat_a a) = 1) /\ (!a. MODULE_interface_size (get_status a) = 1 + location_size a) /\ !a. MODULE_interface_size (start_heartbeat_b a) = 1 [STORE_interface_TY_DEF] Definition |- ?rep'. TYPE_DEFINITION (\a0. !'STORE_interface'. (!a0. (?a. a0 = (\a. CONSTR 0 (a,(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC 0) ((@v. T),a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC 0)) ((@v. T),(@v. T),a) (\n. BOTTOM)) a) ==> 'STORE_interface' a0) ==> 'STORE_interface' a0) rep' [STORE_interface_case_def] Definition |- (!f f1 f2 a. case f f1 f2 (STnew a) = f a) /\ (!f f1 f2 a. case f f1 f2 (STset a) = f1 a) /\ !f f1 f2 a. case f f1 f2 (STget a) = f2 a [STORE_interface_repfns] Definition |- (!a. mk_STORE_interface (dest_STORE_interface a) = a) /\ !r. (\a0. !'STORE_interface'. (!a0. (?a. a0 = (\a. CONSTR 0 (a,(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC 0) ((@v. T),a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC 0)) ((@v. T),(@v. T),a) (\n. BOTTOM)) a) ==> 'STORE_interface' a0) ==> 'STORE_interface' a0) r = (dest_STORE_interface (mk_STORE_interface r) = r) [STORE_interface_size_def] Definition |- (!a. STORE_interface_size (STnew a) = 1 + (\(x,y). TLang_type_size x + TLang_size y) a) /\ (!a. STORE_interface_size (STset a) = 1 + (\(x,y). TLang_type_size x + (\(x,y). location_size x + TLang_size y) y) a) /\ !a. STORE_interface_size (STget a) = 1 + (\(x,y). TLang_type_size x + location_size y) a [STget] Definition |- STget = TNet_LIBinterface22 [STnew] Definition |- STnew = TNet_LIBinterface20 [STset] Definition |- STset = TNet_LIBinterface21 [TNet_LIBinterface0_def] Definition |- TNet_LIBinterface0 = (\a. mk_LIB_interface ((\a. CONSTR 0 (a,(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_LIBinterface10_def] Definition |- TNet_LIBinterface10 = (\a. mk_LIB_interface ((\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), a,(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_LIBinterface11_def] Definition |- TNet_LIBinterface11 = (\a. mk_LIB_interface ((\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))))) ((@v. T),(@v. T),(@v. T),a,(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_LIBinterface12_def] Definition |- TNet_LIBinterface12 = (\a. mk_LIB_interface ((\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),a,(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_LIBinterface13_def] Definition |- TNet_LIBinterface13 = (\a. mk_LIB_interface ((\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),a,@v. T) (\n. BOTTOM)) a)) [TNet_LIBinterface14_def] Definition |- TNet_LIBinterface14 = (\a. mk_LIB_interface ((\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))))))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),a,@v. T) (\n. BOTTOM)) a)) [TNet_LIBinterface15_def] Definition |- TNet_LIBinterface15 = (\a. mk_LIB_interface ((\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))))))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),a) (\n. BOTTOM)) a)) [TNet_LIBinterface16_def] Definition |- TNet_LIBinterface16 = (\a. mk_LIB_interface ((\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))))))))))) (a,(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_LIBinterface17_def] Definition |- TNet_LIBinterface17 = (\a. mk_LIB_interface ((\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))))))))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),a) (\n. BOTTOM)) a)) [TNet_LIBinterface18_def] Definition |- TNet_LIBinterface18 = (\a. mk_LIB_interface ((\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))))))))))))) (a,(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_LIBinterface19_def] Definition |- TNet_LIBinterface19 = (\a. mk_LIB_interface ((\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))))))))))))) (a,(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_LIBinterface1_def] Definition |- TNet_LIBinterface1 = (\a. mk_LIB_interface ((\a. CONSTR (SUC 0) ((@v. T),a,(@v. T),(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_LIBinterface20_def] Definition |- TNet_LIBinterface20 = (\a. mk_STORE_interface ((\a. CONSTR 0 (a,(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_LIBinterface21_def] Definition |- TNet_LIBinterface21 = (\a. mk_STORE_interface ((\a. CONSTR (SUC 0) ((@v. T),a,@v. T) (\n. BOTTOM)) a)) [TNet_LIBinterface22_def] Definition |- TNet_LIBinterface22 = (\a. mk_STORE_interface ((\a. CONSTR (SUC (SUC 0)) ((@v. T),(@v. T),a) (\n. BOTTOM)) a)) [TNet_LIBinterface23_def] Definition |- TNet_LIBinterface23 = (\a. mk_MODULE_interface ((\a. CONSTR 0 (a,@v. T) (\n. BOTTOM)) a)) [TNet_LIBinterface24_def] Definition |- TNet_LIBinterface24 = (\a. mk_MODULE_interface ((\a. CONSTR (SUC 0) ((@v. T),a) (\n. BOTTOM)) a)) [TNet_LIBinterface25_def] Definition |- TNet_LIBinterface25 = (\a. mk_MODULE_interface ((\a. CONSTR (SUC (SUC 0)) (a,@v. T) (\n. BOTTOM)) a)) [TNet_LIBinterface2_def] Definition |- TNet_LIBinterface2 = (\a. mk_LIB_interface ((\a. CONSTR (SUC (SUC 0)) ((@v. T),(@v. T),a,(@v. T),(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_LIBinterface3_def] Definition |- TNet_LIBinterface3 = (\a. mk_LIB_interface ((\a. CONSTR (SUC (SUC (SUC 0))) ((@v. T),(@v. T),(@v. T),a,(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_LIBinterface4_def] Definition |- TNet_LIBinterface4 = (\a. mk_LIB_interface ((\a. CONSTR (SUC (SUC (SUC (SUC 0)))) ((@v. T),(@v. T),(@v. T),a,(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_LIBinterface5_def] Definition |- TNet_LIBinterface5 = (\a. mk_LIB_interface ((\a. CONSTR (SUC (SUC (SUC (SUC (SUC 0))))) ((@v. T),(@v. T),(@v. T),a,(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_LIBinterface6_def] Definition |- TNet_LIBinterface6 = (\a. mk_LIB_interface ((\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC 0)))))) ((@v. T),(@v. T),(@v. T),(@v. T),a,(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_LIBinterface7_def] Definition |- TNet_LIBinterface7 = (\a. mk_LIB_interface ((\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),a,(@v. T), (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_LIBinterface8_def] Definition |- TNet_LIBinterface8 = (\a. mk_LIB_interface ((\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0)))))))) ((@v. T),(@v. T),(@v. T),a,(@v. T),(@v. T),(@v. T), (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_LIBinterface9_def] Definition |- TNet_LIBinterface9 = (\a. mk_LIB_interface ((\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),(@v. T),a, (@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a)) [bind] Definition |- bind = TNet_LIBinterface1 [close] Definition |- close = TNet_LIBinterface11 [connect] Definition |- connect = TNet_LIBinterface2 [create] Definition |- create = TNet_LIBinterface18 [delay] Definition |- delay = TNet_LIBinterface13 [disconnect] Definition |- disconnect = TNet_LIBinterface3 [exit] Definition |- exit = TNet_LIBinterface19 [get_status] Definition |- get_status = TNet_LIBinterface24 [geterr] Definition |- geterr = TNet_LIBinterface8 [getifaddrs] Definition |- getifaddrs = TNet_LIBinterface16 [getpeername] Definition |- getpeername = TNet_LIBinterface5 [getsockname] Definition |- getsockname = TNet_LIBinterface4 [getsockopt] Definition |- getsockopt = TNet_LIBinterface9 [ip_of_string] Definition |- ip_of_string = TNet_LIBinterface15 [port_of_int] Definition |- port_of_int = TNet_LIBinterface14 [print_endline_flush] Definition |- print_endline_flush = TNet_LIBinterface17 [recvfrom] Definition |- recvfrom = TNet_LIBinterface7 [retTypeM_def] Definition |- (!v0. retType (start_heartbeat_a v0) = TLty_ref TLty_int) /\ (!v1. retType (get_status v1) = TLty_int) /\ !v2. retType (start_heartbeat_b v2) = TLty_one [retTypeST_primitive_def] Definition |- retType = WFREC (@R. WF R) (\retTypeST a. case a of STnew v -> (case v of (v3,v4) -> v3) || STset v1 -> (case v1 of (v5,v6) -> case v6 of (v7,v8) -> TLty_one) || STget v2 -> case v2 of (v9,v10) -> v9) [retType_def] Definition |- (!v0. retType (socket v0) = TLty_err TLty_fd) /\ (!v1. retType (bind v1) = TLty_err TLty_one) /\ (!v2. retType (connect v2) = TLty_err TLty_one) /\ (!v3. retType (disconnect v3) = TLty_err TLty_one) /\ (!v4. retType (getsockname v4) = TLty_err (TLty_pair (TLty_lift TLty_ip,TLty_lift TLty_port))) /\ (!v5. retType (getpeername v5) = TLty_err (TLty_pair (TLty_lift TLty_ip,TLty_lift TLty_port))) /\ (!v6. retType (sendto v6) = TLty_err TLty_one) /\ (!v7. retType (recvfrom v7) = TLty_err (TLty_pair (TLty_ip,TLty_pair (TLty_lift TLty_port,TLty_string)))) /\ (!v8. retType (geterr v8) = TLty_err (TLty_lift TLty_error)) /\ (!v9. retType (getsockopt v9) = TLty_err TLty_bool) /\ (!v10. retType (setsockopt v10) = TLty_err TLty_one) /\ (!v11. retType (close v11) = TLty_err TLty_one) /\ (!v12. retType (select v12) = TLty_err (TLty_pair (TLty_list TLty_fd,TLty_list TLty_fd))) /\ (!v13. retType (delay v13) = TLty_err TLty_one) /\ (!v14. retType (port_of_int v14) = TLty_err TLty_port) /\ (!v15. retType (ip_of_string v15) = TLty_err TLty_ip) /\ (!v16. retType (getifaddrs v16) = TLty_err (TLty_list (TLty_pair (TLty_ifid, TLty_pair (TLty_ip, TLty_pair (TLty_list TLty_ip,TLty_netmask)))))) /\ (!v17. retType (print_endline_flush v17) = TLty_err TLty_one) /\ (!v18. retType (create v18) = TLty_err TLty_tid) /\ !v19. retType (exit v19) = TLty_void [select] Definition |- select = TNet_LIBinterface12 [sendto] Definition |- sendto = TNet_LIBinterface6 [setsockopt] Definition |- setsockopt = TNet_LIBinterface10 [socket] Definition |- socket = TNet_LIBinterface0 [start_heartbeat_a] Definition |- start_heartbeat_a = TNet_LIBinterface23 [start_heartbeat_b] Definition |- start_heartbeat_b = TNet_LIBinterface25 [LIB_interface_11] Theorem |- (!a a'. (socket a = socket a') = (a = a')) /\ (!a a'. (bind a = bind a') = (a = a')) /\ (!a a'. (connect a = connect a') = (a = a')) /\ (!a a'. (disconnect a = disconnect a') = (a = a')) /\ (!a a'. (getsockname a = getsockname a') = (a = a')) /\ (!a a'. (getpeername a = getpeername a') = (a = a')) /\ (!a a'. (sendto a = sendto a') = (a = a')) /\ (!a a'. (recvfrom a = recvfrom a') = (a = a')) /\ (!a a'. (geterr a = geterr a') = (a = a')) /\ (!a a'. (getsockopt a = getsockopt a') = (a = a')) /\ (!a a'. (setsockopt a = setsockopt a') = (a = a')) /\ (!a a'. (close a = close a') = (a = a')) /\ (!a a'. (select a = select a') = (a = a')) /\ (!a a'. (delay a = delay a') = (a = a')) /\ (!a a'. (port_of_int a = port_of_int a') = (a = a')) /\ (!a a'. (ip_of_string a = ip_of_string a') = (a = a')) /\ (!a a'. (getifaddrs a = getifaddrs a') = (a = a')) /\ (!a a'. (print_endline_flush a = print_endline_flush a') = (a = a')) /\ (!a a'. (create a = create a') = (a = a')) /\ !a a'. (exit a = exit a') = (a = a') [LIB_interface_Axiom] Theorem |- !f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19. ?fn. (!a. fn (socket a) = f0 a) /\ (!a. fn (bind a) = f1 a) /\ (!a. fn (connect a) = f2 a) /\ (!a. fn (disconnect a) = f3 a) /\ (!a. fn (getsockname a) = f4 a) /\ (!a. fn (getpeername a) = f5 a) /\ (!a. fn (sendto a) = f6 a) /\ (!a. fn (recvfrom a) = f7 a) /\ (!a. fn (geterr a) = f8 a) /\ (!a. fn (getsockopt a) = f9 a) /\ (!a. fn (setsockopt a) = f10 a) /\ (!a. fn (close a) = f11 a) /\ (!a. fn (select a) = f12 a) /\ (!a. fn (delay a) = f13 a) /\ (!a. fn (port_of_int a) = f14 a) /\ (!a. fn (ip_of_string a) = f15 a) /\ (!a. fn (getifaddrs a) = f16 a) /\ (!a. fn (print_endline_flush a) = f17 a) /\ (!a. fn (create a) = f18 a) /\ !a. fn (exit a) = f19 a [LIB_interface_case_cong] Theorem |- !M M' f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19. (M = M') /\ (!a. (M' = socket a) ==> (f a = f' a)) /\ (!a. (M' = bind a) ==> (f1 a = f1' a)) /\ (!a. (M' = connect a) ==> (f2 a = f2' a)) /\ (!a. (M' = disconnect a) ==> (f3 a = f3' a)) /\ (!a. (M' = getsockname a) ==> (f4 a = f4' a)) /\ (!a. (M' = getpeername a) ==> (f5 a = f5' a)) /\ (!a. (M' = sendto a) ==> (f6 a = f6' a)) /\ (!a. (M' = recvfrom a) ==> (f7 a = f7' a)) /\ (!a. (M' = geterr a) ==> (f8 a = f8' a)) /\ (!a. (M' = getsockopt a) ==> (f9 a = f9' a)) /\ (!a. (M' = setsockopt a) ==> (f10 a = f10' a)) /\ (!a. (M' = close a) ==> (f11 a = f11' a)) /\ (!a. (M' = select a) ==> (f12 a = f12' a)) /\ (!a. (M' = delay a) ==> (f13 a = f13' a)) /\ (!a. (M' = port_of_int a) ==> (f14 a = f14' a)) /\ (!a. (M' = ip_of_string a) ==> (f15 a = f15' a)) /\ (!a. (M' = getifaddrs a) ==> (f16 a = f16' a)) /\ (!a. (M' = print_endline_flush a) ==> (f17 a = f17' a)) /\ (!a. (M' = create a) ==> (f18 a = f18' a)) /\ (!a. (M' = exit a) ==> (f19 a = f19' a)) ==> (case f f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 M = case f' f1' f2' f3' f4' f5' f6' f7' f8' f9' f10' f11' f12' f13' f14' f15' f16' f17' f18' f19' M') [LIB_interface_distinct] Theorem |- (!a' a. ~(socket a = bind a')) /\ (!a' a. ~(socket a = connect a')) /\ (!a' a. ~(socket a = disconnect a')) /\ (!a' a. ~(socket a = getsockname a')) /\ (!a' a. ~(socket a = getpeername a')) /\ (!a' a. ~(socket a = sendto a')) /\ (!a' a. ~(socket a = recvfrom a')) /\ (!a' a. ~(socket a = geterr a')) /\ (!a' a. ~(socket a = getsockopt a')) /\ (!a' a. ~(socket a = setsockopt a')) /\ (!a' a. ~(socket a = close a')) /\ (!a' a. ~(socket a = select a')) /\ (!a' a. ~(socket a = delay a')) /\ (!a' a. ~(socket a = port_of_int a')) /\ (!a' a. ~(socket a = ip_of_string a')) /\ (!a' a. ~(socket a = getifaddrs a')) /\ (!a' a. ~(socket a = print_endline_flush a')) /\ (!a' a. ~(socket a = create a')) /\ (!a' a. ~(socket a = exit a')) /\ (!a' a. ~(bind a = connect a')) /\ (!a' a. ~(bind a = disconnect a')) /\ (!a' a. ~(bind a = getsockname a')) /\ (!a' a. ~(bind a = getpeername a')) /\ (!a' a. ~(bind a = sendto a')) /\ (!a' a. ~(bind a = recvfrom a')) /\ (!a' a. ~(bind a = geterr a')) /\ (!a' a. ~(bind a = getsockopt a')) /\ (!a' a. ~(bind a = setsockopt a')) /\ (!a' a. ~(bind a = close a')) /\ (!a' a. ~(bind a = select a')) /\ (!a' a. ~(bind a = delay a')) /\ (!a' a. ~(bind a = port_of_int a')) /\ (!a' a. ~(bind a = ip_of_string a')) /\ (!a' a. ~(bind a = getifaddrs a')) /\ (!a' a. ~(bind a = print_endline_flush a')) /\ (!a' a. ~(bind a = create a')) /\ (!a' a. ~(bind a = exit a')) /\ (!a' a. ~(connect a = disconnect a')) /\ (!a' a. ~(connect a = getsockname a')) /\ (!a' a. ~(connect a = getpeername a')) /\ (!a' a. ~(connect a = sendto a')) /\ (!a' a. ~(connect a = recvfrom a')) /\ (!a' a. ~(connect a = geterr a')) /\ (!a' a. ~(connect a = getsockopt a')) /\ (!a' a. ~(connect a = setsockopt a')) /\ (!a' a. ~(connect a = close a')) /\ (!a' a. ~(connect a = select a')) /\ (!a' a. ~(connect a = delay a')) /\ (!a' a. ~(connect a = port_of_int a')) /\ (!a' a. ~(connect a = ip_of_string a')) /\ (!a' a. ~(connect a = getifaddrs a')) /\ (!a' a. ~(connect a = print_endline_flush a')) /\ (!a' a. ~(connect a = create a')) /\ (!a' a. ~(connect a = exit a')) /\ (!a' a. ~(disconnect a = getsockname a')) /\ (!a' a. ~(disconnect a = getpeername a')) /\ (!a' a. ~(disconnect a = sendto a')) /\ (!a' a. ~(disconnect a = recvfrom a')) /\ (!a' a. ~(disconnect a = geterr a')) /\ (!a' a. ~(disconnect a = getsockopt a')) /\ (!a' a. ~(disconnect a = setsockopt a')) /\ (!a' a. ~(disconnect a = close a')) /\ (!a' a. ~(disconnect a = select a')) /\ (!a' a. ~(disconnect a = delay a')) /\ (!a' a. ~(disconnect a = port_of_int a')) /\ (!a' a. ~(disconnect a = ip_of_string a')) /\ (!a' a. ~(disconnect a = getifaddrs a')) /\ (!a' a. ~(disconnect a = print_endline_flush a')) /\ (!a' a. ~(disconnect a = create a')) /\ (!a' a. ~(disconnect a = exit a')) /\ (!a' a. ~(getsockname a = getpeername a')) /\ (!a' a. ~(getsockname a = sendto a')) /\ (!a' a. ~(getsockname a = recvfrom a')) /\ (!a' a. ~(getsockname a = geterr a')) /\ (!a' a. ~(getsockname a = getsockopt a')) /\ (!a' a. ~(getsockname a = setsockopt a')) /\ (!a' a. ~(getsockname a = close a')) /\ (!a' a. ~(getsockname a = select a')) /\ (!a' a. ~(getsockname a = delay a')) /\ (!a' a. ~(getsockname a = port_of_int a')) /\ (!a' a. ~(getsockname a = ip_of_string a')) /\ (!a' a. ~(getsockname a = getifaddrs a')) /\ (!a' a. ~(getsockname a = print_endline_flush a')) /\ (!a' a. ~(getsockname a = create a')) /\ (!a' a. ~(getsockname a = exit a')) /\ (!a' a. ~(getpeername a = sendto a')) /\ (!a' a. ~(getpeername a = recvfrom a')) /\ (!a' a. ~(getpeername a = geterr a')) /\ (!a' a. ~(getpeername a = getsockopt a')) /\ (!a' a. ~(getpeername a = setsockopt a')) /\ (!a' a. ~(getpeername a = close a')) /\ (!a' a. ~(getpeername a = select a')) /\ (!a' a. ~(getpeername a = delay a')) /\ (!a' a. ~(getpeername a = port_of_int a')) /\ (!a' a. ~(getpeername a = ip_of_string a')) /\ (!a' a. ~(getpeername a = getifaddrs a')) /\ (!a' a. ~(getpeername a = print_endline_flush a')) /\ (!a' a. ~(getpeername a = create a')) /\ (!a' a. ~(getpeername a = exit a')) /\ (!a' a. ~(sendto a = recvfrom a')) /\ (!a' a. ~(sendto a = geterr a')) /\ (!a' a. ~(sendto a = getsockopt a')) /\ (!a' a. ~(sendto a = setsockopt a')) /\ (!a' a. ~(sendto a = close a')) /\ (!a' a. ~(sendto a = select a')) /\ (!a' a. ~(sendto a = delay a')) /\ (!a' a. ~(sendto a = port_of_int a')) /\ (!a' a. ~(sendto a = ip_of_string a')) /\ (!a' a. ~(sendto a = getifaddrs a')) /\ (!a' a. ~(sendto a = print_endline_flush a')) /\ (!a' a. ~(sendto a = create a')) /\ (!a' a. ~(sendto a = exit a')) /\ (!a' a. ~(recvfrom a = geterr a')) /\ (!a' a. ~(recvfrom a = getsockopt a')) /\ (!a' a. ~(recvfrom a = setsockopt a')) /\ (!a' a. ~(recvfrom a = close a')) /\ (!a' a. ~(recvfrom a = select a')) /\ (!a' a. ~(recvfrom a = delay a')) /\ (!a' a. ~(recvfrom a = port_of_int a')) /\ (!a' a. ~(recvfrom a = ip_of_string a')) /\ (!a' a. ~(recvfrom a = getifaddrs a')) /\ (!a' a. ~(recvfrom a = print_endline_flush a')) /\ (!a' a. ~(recvfrom a = create a')) /\ (!a' a. ~(recvfrom a = exit a')) /\ (!a' a. ~(geterr a = getsockopt a')) /\ (!a' a. ~(geterr a = setsockopt a')) /\ (!a' a. ~(geterr a = close a')) /\ (!a' a. ~(geterr a = select a')) /\ (!a' a. ~(geterr a = delay a')) /\ (!a' a. ~(geterr a = port_of_int a')) /\ (!a' a. ~(geterr a = ip_of_string a')) /\ (!a' a. ~(geterr a = getifaddrs a')) /\ (!a' a. ~(geterr a = print_endline_flush a')) /\ (!a' a. ~(geterr a = create a')) /\ (!a' a. ~(geterr a = exit a')) /\ (!a' a. ~(getsockopt a = setsockopt a')) /\ (!a' a. ~(getsockopt a = close a')) /\ (!a' a. ~(getsockopt a = select a')) /\ (!a' a. ~(getsockopt a = delay a')) /\ (!a' a. ~(getsockopt a = port_of_int a')) /\ (!a' a. ~(getsockopt a = ip_of_string a')) /\ (!a' a. ~(getsockopt a = getifaddrs a')) /\ (!a' a. ~(getsockopt a = print_endline_flush a')) /\ (!a' a. ~(getsockopt a = create a')) /\ (!a' a. ~(getsockopt a = exit a')) /\ (!a' a. ~(setsockopt a = close a')) /\ (!a' a. ~(setsockopt a = select a')) /\ (!a' a. ~(setsockopt a = delay a')) /\ (!a' a. ~(setsockopt a = port_of_int a')) /\ (!a' a. ~(setsockopt a = ip_of_string a')) /\ (!a' a. ~(setsockopt a = getifaddrs a')) /\ (!a' a. ~(setsockopt a = print_endline_flush a')) /\ (!a' a. ~(setsockopt a = create a')) /\ (!a' a. ~(setsockopt a = exit a')) /\ (!a' a. ~(close a = select a')) /\ (!a' a. ~(close a = delay a')) /\ (!a' a. ~(close a = port_of_int a')) /\ (!a' a. ~(close a = ip_of_string a')) /\ (!a' a. ~(close a = getifaddrs a')) /\ (!a' a. ~(close a = print_endline_flush a')) /\ (!a' a. ~(close a = create a')) /\ (!a' a. ~(close a = exit a')) /\ (!a' a. ~(select a = delay a')) /\ (!a' a. ~(select a = port_of_int a')) /\ (!a' a. ~(select a = ip_of_string a')) /\ (!a' a. ~(select a = getifaddrs a')) /\ (!a' a. ~(select a = print_endline_flush a')) /\ (!a' a. ~(select a = create a')) /\ (!a' a. ~(select a = exit a')) /\ (!a' a. ~(delay a = port_of_int a')) /\ (!a' a. ~(delay a = ip_of_string a')) /\ (!a' a. ~(delay a = getifaddrs a')) /\ (!a' a. ~(delay a = print_endline_flush a')) /\ (!a' a. ~(delay a = create a')) /\ (!a' a. ~(delay a = exit a')) /\ (!a' a. ~(port_of_int a = ip_of_string a')) /\ (!a' a. ~(port_of_int a = getifaddrs a')) /\ (!a' a. ~(port_of_int a = print_endline_flush a')) /\ (!a' a. ~(port_of_int a = create a')) /\ (!a' a. ~(port_of_int a = exit a')) /\ (!a' a. ~(ip_of_string a = getifaddrs a')) /\ (!a' a. ~(ip_of_string a = print_endline_flush a')) /\ (!a' a. ~(ip_of_string a = create a')) /\ (!a' a. ~(ip_of_string a = exit a')) /\ (!a' a. ~(getifaddrs a = print_endline_flush a')) /\ (!a' a. ~(getifaddrs a = create a')) /\ (!a' a. ~(getifaddrs a = exit a')) /\ (!a' a. ~(print_endline_flush a = create a')) /\ (!a' a. ~(print_endline_flush a = exit a')) /\ !a' a. ~(create a = exit a') [LIB_interface_induction] Theorem |- !P. (!$o. P (socket $o)) /\ (!p. P (bind p)) /\ (!p. P (connect p)) /\ (!f. P (disconnect f)) /\ (!f. P (getsockname f)) /\ (!f. P (getpeername f)) /\ (!p. P (sendto p)) /\ (!p. P (recvfrom p)) /\ (!f. P (geterr f)) /\ (!p. P (getsockopt p)) /\ (!p. P (setsockopt p)) /\ (!f. P (close f)) /\ (!p. P (select p)) /\ (!i. P (delay i)) /\ (!i. P (port_of_int i)) /\ (!s. P (ip_of_string s)) /\ (!$o. P (getifaddrs $o)) /\ (!s. P (print_endline_flush s)) /\ (!$o. P (create $o)) /\ (!$o. P (exit $o)) ==> !L. P L [LIB_interface_nchotomy] Theorem |- !L. (?$o. L = socket $o) \/ (?p. L = bind p) \/ (?p. L = connect p) \/ (?f. L = disconnect f) \/ (?f. L = getsockname f) \/ (?f. L = getpeername f) \/ (?p. L = sendto p) \/ (?p. L = recvfrom p) \/ (?f. L = geterr f) \/ (?p. L = getsockopt p) \/ (?p. L = setsockopt p) \/ (?f. L = close f) \/ (?p. L = select p) \/ (?i. L = delay i) \/ (?i. L = port_of_int i) \/ (?s. L = ip_of_string s) \/ (?$o. L = getifaddrs $o) \/ (?s. L = print_endline_flush s) \/ (?$o. L = create $o) \/ ?$o. L = exit $o [MODULE_interface_11] Theorem |- (!a a'. (start_heartbeat_a a = start_heartbeat_a a') = (a = a')) /\ (!a a'. (get_status a = get_status a') = (a = a')) /\ !a a'. (start_heartbeat_b a = start_heartbeat_b a') = (a = a') [MODULE_interface_Axiom] Theorem |- !f0 f1 f2. ?fn. (!a. fn (start_heartbeat_a a) = f0 a) /\ (!a. fn (get_status a) = f1 a) /\ !a. fn (start_heartbeat_b a) = f2 a [MODULE_interface_case_cong] Theorem |- !M M' f f1 f2. (M = M') /\ (!a. (M' = start_heartbeat_a a) ==> (f a = f' a)) /\ (!a. (M' = get_status a) ==> (f1 a = f1' a)) /\ (!a. (M' = start_heartbeat_b a) ==> (f2 a = f2' a)) ==> (case f f1 f2 M = case f' f1' f2' M') [MODULE_interface_distinct] Theorem |- (!a' a. ~(start_heartbeat_a a = get_status a')) /\ (!a' a. ~(start_heartbeat_a a = start_heartbeat_b a')) /\ !a' a. ~(get_status a = start_heartbeat_b a') [MODULE_interface_induction] Theorem |- !P. (!$o. P (start_heartbeat_a $o)) /\ (!l. P (get_status l)) /\ (!$o. P (start_heartbeat_b $o)) ==> !M. P M [MODULE_interface_nchotomy] Theorem |- !M. (?$o. M = start_heartbeat_a $o) \/ (?l. M = get_status l) \/ ?$o. M = start_heartbeat_b $o [STORE_interface_11] Theorem |- (!a a'. (STnew a = STnew a') = (a = a')) /\ (!a a'. (STset a = STset a') = (a = a')) /\ !a a'. (STget a = STget a') = (a = a') [STORE_interface_Axiom] Theorem |- !f0 f1 f2. ?fn. (!a. fn (STnew a) = f0 a) /\ (!a. fn (STset a) = f1 a) /\ !a. fn (STget a) = f2 a [STORE_interface_case_cong] Theorem |- !M M' f f1 f2. (M = M') /\ (!a. (M' = STnew a) ==> (f a = f' a)) /\ (!a. (M' = STset a) ==> (f1 a = f1' a)) /\ (!a. (M' = STget a) ==> (f2 a = f2' a)) ==> (case f f1 f2 M = case f' f1' f2' M') [STORE_interface_distinct] Theorem |- (!a' a. ~(STnew a = STset a')) /\ (!a' a. ~(STnew a = STget a')) /\ !a' a. ~(STset a = STget a') [STORE_interface_induction] Theorem |- !P. (!p. P (STnew p)) /\ (!p. P (STset p)) /\ (!p. P (STget p)) ==> !S. P S [STORE_interface_nchotomy] Theorem |- !S. (?p. S = STnew p) \/ (?p. S = STset p) \/ ?p. S = STget p [retTypeST_def] Theorem |- (retType (STnew (tlty,v)) = tlty) /\ (retType (STset (tlty,l,v)) = TLty_one) /\ (retType (STget (tlty,l)) = tlty) [retTypeST_ind] Theorem |- !P. (!tlty v. P (STnew (tlty,v))) /\ (!tlty l v. P (STset (tlty,l,v))) /\ (!tlty l. P (STget (tlty,l))) ==> !v. P v *) end