signature TNet_threadAxTheory = sig type thm = Thm.thm (* Definitions *) val Lt_RETOut : thm val Lt_RetHostIn : thm val Lt_RetStoreIn : thm val Lt_callHostCreateOut : thm val Lt_callHostOut : thm val Lt_callModuleIn : thm val Lt_callStoreOut : thm val Lt_tau : thm val Lthread_TY_DEF : thm val Lthread_case_def : thm val Lthread_repfns : thm val Lthread_size_def : thm val TNet_threadAx0_def : thm val TNet_threadAx1_def : thm val TNet_threadAx2_def : thm val TNet_threadAx3_def : thm val TNet_threadAx4_def : thm val TNet_threadAx5_def : thm val TNet_threadAx6_def : thm val TNet_threadAx7_def : thm val TNet_threadAx8_def : thm val pairwise_disjoint_def : thm val reachable_def : thm val thread : thm val thread_CallHost : thm val thread_CallHostCreate : thm val thread_CallHostCreate_fupd : thm val thread_CallHostCreate_update : thm val thread_CallHost_fupd : thm val thread_CallHost_update : thm val thread_CallStore : thm val thread_CallStore_fupd : thm val thread_CallStore_update : thm val thread_Module : thm val thread_Module_fupd : thm val thread_Module_update : thm val thread_Prog : thm val thread_Prog_fupd : thm val thread_Prog_update : thm val thread_RETtl : thm val thread_RETtl_fupd : thm val thread_RETtl_update : thm val thread_RetHosttl : thm val thread_RetHosttl_fupd : thm val thread_RetHosttl_update : thm val thread_RetStoretl : thm val thread_RetStoretl_fupd : thm val thread_RetStoretl_update : thm val thread_Rettl : thm val thread_Rettl_fupd : thm val thread_Rettl_update : thm val thread_TY_DEF : thm val thread_Tau : thm val thread_Tau_fupd : thm val thread_Tau_update : thm val thread_Term : thm val thread_Term_fupd : thm val thread_Term_update : thm val thread_case_def : thm val thread_initial : thm val thread_initial_fupd : thm val thread_initial_update : thm val thread_lts'_def : thm val thread_ok_def : thm val thread_repfns : thm val thread_size_def : thm val thread_transition : thm val thread_transition_fupd : thm val thread_transition_update : thm (* Theorems *) val Lthread_11 : thm val Lthread_Axiom : thm val Lthread_case_cong : thm val Lthread_distinct : thm val Lthread_induction : thm val Lthread_nchotomy : thm val thread_11 : thm val thread_Axiom : thm val thread_CallHostCreate_update_semi11 : thm val thread_CallHost_update_semi11 : thm val thread_CallStore_update_semi11 : thm val thread_Module_update_semi11 : thm val thread_Prog_update_semi11 : thm val thread_RETtl_update_semi11 : thm val thread_RetHosttl_update_semi11 : thm val thread_RetStoretl_update_semi11 : thm val thread_Rettl_update_semi11 : thm val thread_Tau_update_semi11 : thm val thread_Term_update_semi11 : thm val thread_accessors : thm val thread_accfupds : thm val thread_accupds : thm val thread_case_cong : thm val thread_component_equality : thm val thread_cupdaccs : thm val thread_fn_updates : thm val thread_induction : thm val thread_initial_update_semi11 : thm val thread_nchotomy : thm val thread_transition_update_semi11 : thm val thread_updaccs : thm val thread_updates : thm val thread_updates_eq_literal : thm val thread_updcanon : thm val thread_updupds : thm val TNet_threadAx_grammars : parse_type.grammar * term_grammar.grammar (* [TNet_LIBinterface] Parent theory of "TNet_threadAx" [Lt_RETOut] Definition |- Lt_RETOut = TNet_threadAx6 [Lt_RetHostIn] Definition |- Lt_RetHostIn = TNet_threadAx4 [Lt_RetStoreIn] Definition |- Lt_RetStoreIn = TNet_threadAx5 [Lt_callHostCreateOut] Definition |- Lt_callHostCreateOut = TNet_threadAx2 [Lt_callHostOut] Definition |- Lt_callHostOut = TNet_threadAx1 [Lt_callModuleIn] Definition |- Lt_callModuleIn = TNet_threadAx0 [Lt_callStoreOut] Definition |- Lt_callStoreOut = TNet_threadAx3 [Lt_tau] Definition |- Lt_tau = TNet_threadAx7 [Lthread_TY_DEF] Definition |- ?rep'. TYPE_DEFINITION (\a0. !'Lthread'. (!a0. (?a. a0 = (\a. CONSTR 0 (a,(@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) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC 0)) ((@v. T),(@v. T),a,(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC 0))) ((@v. T),(@v. T),(@v. T),a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC 0)))) ((@v. T),(@v. T),(@v. T),(@v. T),a) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC 0))))) ((@v. T),(@v. T),(@v. T),(@v. T),a) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC 0)))))) ((@v. T),(@v. T),(@v. T),(@v. T),a) (\n. BOTTOM)) a) \/ (a0 = CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))) ((@v. T),(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) ==> 'Lthread' a0) ==> 'Lthread' a0) rep' [Lthread_case_def] Definition |- (!f f1 f2 f3 f4 f5 f6 v a. case f f1 f2 f3 f4 f5 f6 v (Lt_callModuleIn a) = f a) /\ (!f f1 f2 f3 f4 f5 f6 v a. case f f1 f2 f3 f4 f5 f6 v (Lt_callHostOut a) = f1 a) /\ (!f f1 f2 f3 f4 f5 f6 v a. case f f1 f2 f3 f4 f5 f6 v (Lt_callHostCreateOut a) = f2 a) /\ (!f f1 f2 f3 f4 f5 f6 v a. case f f1 f2 f3 f4 f5 f6 v (Lt_callStoreOut a) = f3 a) /\ (!f f1 f2 f3 f4 f5 f6 v a. case f f1 f2 f3 f4 f5 f6 v (Lt_RetHostIn a) = f4 a) /\ (!f f1 f2 f3 f4 f5 f6 v a. case f f1 f2 f3 f4 f5 f6 v (Lt_RetStoreIn a) = f5 a) /\ (!f f1 f2 f3 f4 f5 f6 v a. case f f1 f2 f3 f4 f5 f6 v (Lt_RETOut a) = f6 a) /\ !f f1 f2 f3 f4 f5 f6 v. case f f1 f2 f3 f4 f5 f6 v Lt_tau = v [Lthread_repfns] Definition |- (!a. mk_Lthread (dest_Lthread a) = a) /\ !r. (\a0. !'Lthread'. (!a0. (?a. a0 = (\a. CONSTR 0 (a,(@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) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC 0)) ((@v. T),(@v. T),a,(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC 0))) ((@v. T),(@v. T),(@v. T),a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC 0)))) ((@v. T),(@v. T),(@v. T),(@v. T),a) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC 0))))) ((@v. T),(@v. T),(@v. T),(@v. T),a) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC 0)))))) ((@v. T),(@v. T),(@v. T),(@v. T),a) (\n. BOTTOM)) a) \/ (a0 = CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))) ((@v. T),(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) ==> 'Lthread' a0) ==> 'Lthread' a0) r = (dest_Lthread (mk_Lthread r) = r) [Lthread_size_def] Definition |- (!f a. Lthread_size f (Lt_callModuleIn a) = 1 + MODULE_interface_size a) /\ (!f a. Lthread_size f (Lt_callHostOut a) = 1 + LIB_interface_size a) /\ (!f a. Lthread_size f (Lt_callHostCreateOut a) = 1 + f a) /\ (!f a. Lthread_size f (Lt_callStoreOut a) = 1 + STORE_interface_size a) /\ (!f a. Lthread_size f (Lt_RetHostIn a) = 1 + TLang_size a) /\ (!f a. Lthread_size f (Lt_RetStoreIn a) = 1 + TLang_size a) /\ (!f a. Lthread_size f (Lt_RETOut a) = 1 + TLang_size a) /\ !f. Lthread_size f Lt_tau = 0 [TNet_threadAx0_def] Definition |- TNet_threadAx0 = (\a. mk_Lthread ((\a. CONSTR 0 (a,(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_threadAx1_def] Definition |- TNet_threadAx1 = (\a. mk_Lthread ((\a. CONSTR (SUC 0) ((@v. T),a,(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_threadAx2_def] Definition |- TNet_threadAx2 = (\a. mk_Lthread ((\a. CONSTR (SUC (SUC 0)) ((@v. T),(@v. T),a,(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_threadAx3_def] Definition |- TNet_threadAx3 = (\a. mk_Lthread ((\a. CONSTR (SUC (SUC (SUC 0))) ((@v. T),(@v. T),(@v. T),a,@v. T) (\n. BOTTOM)) a)) [TNet_threadAx4_def] Definition |- TNet_threadAx4 = (\a. mk_Lthread ((\a. CONSTR (SUC (SUC (SUC (SUC 0)))) ((@v. T),(@v. T),(@v. T),(@v. T),a) (\n. BOTTOM)) a)) [TNet_threadAx5_def] Definition |- TNet_threadAx5 = (\a. mk_Lthread ((\a. CONSTR (SUC (SUC (SUC (SUC (SUC 0))))) ((@v. T),(@v. T),(@v. T),(@v. T),a) (\n. BOTTOM)) a)) [TNet_threadAx6_def] Definition |- TNet_threadAx6 = (\a. mk_Lthread ((\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC 0)))))) ((@v. T),(@v. T),(@v. T),(@v. T),a) (\n. BOTTOM)) a)) [TNet_threadAx7_def] Definition |- TNet_threadAx7 = mk_Lthread (CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))) ((@v. T),(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) [TNet_threadAx8_def] Definition |- TNet_threadAx8 = (\a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12. mk_thread ((\a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12. CONSTR 0 (a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12) (\n. BOTTOM)) a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12)) [pairwise_disjoint_def] Definition |- !x. pairwise_disjoint x = !u v. u IN x /\ v IN x /\ (u <> v) ==> DISJOINT u v [reachable_def] Definition |- !t s. reachable t s = RTC (\s0 s. ?l. t.transition s0 s l) t.initial s [thread] Definition |- thread = TNet_threadAx8 [thread_CallHost] Definition |- !a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10).CallHost = f1 [thread_CallHostCreate] Definition |- !a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10).CallHostCreate = f2 [thread_CallHostCreate_fupd] Definition |- !f x. x with CallHostCreate updated_by f = x with CallHostCreate := f x.CallHostCreate [thread_CallHostCreate_update] Definition |- !f11 a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 with CallHostCreate := f11 = thread a f f0 f1 f11 f3 f4 f5 f6 f7 f8 f9 f10 [thread_CallHost_fupd] Definition |- !f x. x with CallHost updated_by f = x with CallHost := f x.CallHost [thread_CallHost_update] Definition |- !f11 a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 with CallHost := f11 = thread a f f0 f11 f2 f3 f4 f5 f6 f7 f8 f9 f10 [thread_CallStore] Definition |- !a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10).CallStore = f3 [thread_CallStore_fupd] Definition |- !f x. x with CallStore updated_by f = x with CallStore := f x.CallStore [thread_CallStore_update] Definition |- !f11 a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 with CallStore := f11 = thread a f f0 f1 f2 f11 f4 f5 f6 f7 f8 f9 f10 [thread_Module] Definition |- !a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10).Module = f0 [thread_Module_fupd] Definition |- !f x. x with Module updated_by f = x with Module := f x.Module [thread_Module_update] Definition |- !f11 a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 with Module := f11 = thread a f f11 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 [thread_Prog] Definition |- !a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10).Prog = f10 [thread_Prog_fupd] Definition |- !f x. x with Prog updated_by f = x with Prog := f x.Prog [thread_Prog_update] Definition |- !f11 a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 with Prog := f11 = thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f11 [thread_RETtl] Definition |- !a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10).RETtl = f6 [thread_RETtl_fupd] Definition |- !f x. x with RETtl updated_by f = x with RETtl := f x.RETtl [thread_RETtl_update] Definition |- !f11 a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 with RETtl := f11 = thread a f f0 f1 f2 f3 f4 f5 f11 f7 f8 f9 f10 [thread_RetHosttl] Definition |- !a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10).RetHosttl = f4 [thread_RetHosttl_fupd] Definition |- !f x. x with RetHosttl updated_by f = x with RetHosttl := f x.RetHosttl [thread_RetHosttl_update] Definition |- !f11 a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 with RetHosttl := f11 = thread a f f0 f1 f2 f3 f11 f5 f6 f7 f8 f9 f10 [thread_RetStoretl] Definition |- !a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10).RetStoretl = f5 [thread_RetStoretl_fupd] Definition |- !f x. x with RetStoretl updated_by f = x with RetStoretl := f x.RetStoretl [thread_RetStoretl_update] Definition |- !f11 a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 with RetStoretl := f11 = thread a f f0 f1 f2 f3 f4 f11 f6 f7 f8 f9 f10 [thread_Rettl] Definition |- !a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10).Rettl = f9 [thread_Rettl_fupd] Definition |- !f x. x with Rettl updated_by f = x with Rettl := f x.Rettl [thread_Rettl_update] Definition |- !f11 a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 with Rettl := f11 = thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f11 f10 [thread_TY_DEF] Definition |- ?rep'. TYPE_DEFINITION (\a0'. !'thread'. (!a0'. (?a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12. a0' = (\a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12. CONSTR 0 (a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12) (\n. BOTTOM)) a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12) ==> 'thread' a0') ==> 'thread' a0') rep' [thread_Tau] Definition |- !a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10).Tau = f7 [thread_Tau_fupd] Definition |- !f x. x with Tau updated_by f = x with Tau := f x.Tau [thread_Tau_update] Definition |- !f11 a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 with Tau := f11 = thread a f f0 f1 f2 f3 f4 f5 f6 f11 f8 f9 f10 [thread_Term] Definition |- !a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10).Term = f8 [thread_Term_fupd] Definition |- !f x. x with Term updated_by f = x with Term := f x.Term [thread_Term_update] Definition |- !f11 a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 with Term := f11 = thread a f f0 f1 f2 f3 f4 f5 f6 f7 f11 f9 f10 [thread_case_def] Definition |- !f a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12. case f (thread a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12) = f a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 [thread_initial] Definition |- !a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10).initial = a [thread_initial_fupd] Definition |- !f x. x with initial updated_by f = x with initial := f x.initial [thread_initial_update] Definition |- !a0 a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 with initial := a0 = thread a0 f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 [thread_lts'_def] Definition |- !t l t'. t --- l ->>> t' = ?s'. t.transition t.initial s' l /\ (t' = t with initial := s') [thread_ok_def] Definition |- !t. thread_ok t = (t.Prog = t.Tau UNION {s | ?fh. s IN t.CallHost fh} UNION t.CallHostCreate UNION {s | ?fs. s IN t.CallStore fs} UNION {s | ?tlty. s IN t.RETtl tlty}) /\ (!tlty. t.Rettl tlty = t.RetHosttl tlty UNION t.RetStoretl tlty) /\ (!s. s IN reachable t ==> s IN t.Module \/ s IN t.Prog \/ (?tlty. s IN t.Rettl tlty) \/ s IN t.Term) /\ pairwise_disjoint ({t.Module; t.CallHostCreate; t.Tau; t.Term} UNION {t.CallHost fhv | T} UNION {t.CallStore fsv | T} UNION {t.RetHosttl tl | T} UNION {t.RetStoretl tl | T} UNION {t.RETtl tl | T}) /\ (!s s'. ~t.transition s s' (Lt_callHostOut (create ()))) /\ (!s s' fmv. t.transition s s' (Lt_callModuleIn fmv) ==> s IN t.Module /\ s' IN t.Prog) /\ (!s s' fv. t.transition s s' (Lt_callHostOut fv) ==> s IN t.CallHost fv /\ s' IN t.Rettl (retType fv)) /\ (!s s' s2. t.transition s s' (Lt_callHostCreateOut s2) ==> s IN t.CallHostCreate /\ s' IN t.Rettl (retType (create ())) /\ s2 IN t.Prog) /\ (!s s' fv. t.transition s s' (Lt_callStoreOut fv) ==> s IN t.CallStore fv /\ s' IN t.Rettl (retType fv)) /\ (!s s' v. t.transition s s' (Lt_RetHostIn v) ==> ?tlty. s IN t.RetHosttl tlty /\ s' IN t.Prog /\ tlang_typing v tlty) /\ (!s s' v. t.transition s s' (Lt_RetStoreIn v) ==> ?tlty. s IN t.RetStoretl tlty /\ s' IN t.Prog /\ tlang_typing v tlty) /\ (!s s' v. t.transition s s' (Lt_RETOut v) ==> ?tlty. s IN t.RETtl tlty /\ s' IN t.Term /\ tlang_typing v tlty) /\ (!s s'. t.transition s s' Lt_tau ==> s IN t.Tau /\ s' IN t.Prog) /\ (!s s' s'' l. (l <> Lt_tau) /\ t.transition s s' l /\ t.transition s s'' l ==> (s' = s'')) /\ (!s gv. s IN t.Module ==> ?s'. t.transition s s' (Lt_callModuleIn gv)) /\ (!s. s IN t.Prog ==> ?s' l. t.transition s s' l) /\ (!tlty s. s IN t.RetHosttl tlty ==> !r. tlang_typing r tlty ==> ?!s'. t.transition s s' (Lt_RetHostIn r)) /\ (!tlty s. s IN t.RetStoretl tlty ==> !r. tlang_typing r tlty ==> ?!s'. t.transition s s' (Lt_RetStoreIn r)) /\ !s s' s'' gv tlty. s IN t.Module /\ t.transition s s' (Lt_callModuleIn gv) /\ RTC (\s0 s. ?l. t.transition s0 s l) s' s'' /\ s'' IN t.RETtl tlty ==> (tlty = retType gv) [thread_repfns] Definition |- (!a. mk_thread (dest_thread a) = a) /\ !r. (\a0'. !'thread'. (!a0'. (?a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12. a0' = (\a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12. CONSTR 0 (a0,a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12) (\n. BOTTOM)) a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12) ==> 'thread' a0') ==> 'thread' a0') r = (dest_thread (mk_thread r) = r) [thread_size_def] Definition |- !f a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12. thread_size f (thread a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12) = 1 + f a0 [thread_transition] Definition |- !a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10).transition = f [thread_transition_fupd] Definition |- !f x. x with transition updated_by f = x with transition := f x.transition [thread_transition_update] Definition |- !f11 a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 with transition := f11 = thread a f11 f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 [Lthread_11] Theorem |- (!a a'. (Lt_callModuleIn a = Lt_callModuleIn a') = (a = a')) /\ (!a a'. (Lt_callHostOut a = Lt_callHostOut a') = (a = a')) /\ (!a a'. (Lt_callHostCreateOut a = Lt_callHostCreateOut a') = (a = a')) /\ (!a a'. (Lt_callStoreOut a = Lt_callStoreOut a') = (a = a')) /\ (!a a'. (Lt_RetHostIn a = Lt_RetHostIn a') = (a = a')) /\ (!a a'. (Lt_RetStoreIn a = Lt_RetStoreIn a') = (a = a')) /\ !a a'. (Lt_RETOut a = Lt_RETOut a') = (a = a') [Lthread_Axiom] Theorem |- !f0 f1 f2 f3 f4 f5 f6 f7. ?fn. (!a. fn (Lt_callModuleIn a) = f0 a) /\ (!a. fn (Lt_callHostOut a) = f1 a) /\ (!a. fn (Lt_callHostCreateOut a) = f2 a) /\ (!a. fn (Lt_callStoreOut a) = f3 a) /\ (!a. fn (Lt_RetHostIn a) = f4 a) /\ (!a. fn (Lt_RetStoreIn a) = f5 a) /\ (!a. fn (Lt_RETOut a) = f6 a) /\ (fn Lt_tau = f7) [Lthread_case_cong] Theorem |- !M M' f f1 f2 f3 f4 f5 f6 v. (M = M') /\ (!a. (M' = Lt_callModuleIn a) ==> (f a = f' a)) /\ (!a. (M' = Lt_callHostOut a) ==> (f1 a = f1' a)) /\ (!a. (M' = Lt_callHostCreateOut a) ==> (f2 a = f2' a)) /\ (!a. (M' = Lt_callStoreOut a) ==> (f3 a = f3' a)) /\ (!a. (M' = Lt_RetHostIn a) ==> (f4 a = f4' a)) /\ (!a. (M' = Lt_RetStoreIn a) ==> (f5 a = f5' a)) /\ (!a. (M' = Lt_RETOut a) ==> (f6 a = f6' a)) /\ ((M' = Lt_tau) ==> (v = v')) ==> (case f f1 f2 f3 f4 f5 f6 v M = case f' f1' f2' f3' f4' f5' f6' v' M') [Lthread_distinct] Theorem |- (!a' a. ~(Lt_callModuleIn a = Lt_callHostOut a')) /\ (!a' a. ~(Lt_callModuleIn a = Lt_callHostCreateOut a')) /\ (!a' a. ~(Lt_callModuleIn a = Lt_callStoreOut a')) /\ (!a' a. ~(Lt_callModuleIn a = Lt_RetHostIn a')) /\ (!a' a. ~(Lt_callModuleIn a = Lt_RetStoreIn a')) /\ (!a' a. ~(Lt_callModuleIn a = Lt_RETOut a')) /\ (!a. ~(Lt_callModuleIn a = Lt_tau)) /\ (!a' a. ~(Lt_callHostOut a = Lt_callHostCreateOut a')) /\ (!a' a. ~(Lt_callHostOut a = Lt_callStoreOut a')) /\ (!a' a. ~(Lt_callHostOut a = Lt_RetHostIn a')) /\ (!a' a. ~(Lt_callHostOut a = Lt_RetStoreIn a')) /\ (!a' a. ~(Lt_callHostOut a = Lt_RETOut a')) /\ (!a. ~(Lt_callHostOut a = Lt_tau)) /\ (!a' a. ~(Lt_callHostCreateOut a = Lt_callStoreOut a')) /\ (!a' a. ~(Lt_callHostCreateOut a = Lt_RetHostIn a')) /\ (!a' a. ~(Lt_callHostCreateOut a = Lt_RetStoreIn a')) /\ (!a' a. ~(Lt_callHostCreateOut a = Lt_RETOut a')) /\ (!a. ~(Lt_callHostCreateOut a = Lt_tau)) /\ (!a' a. ~(Lt_callStoreOut a = Lt_RetHostIn a')) /\ (!a' a. ~(Lt_callStoreOut a = Lt_RetStoreIn a')) /\ (!a' a. ~(Lt_callStoreOut a = Lt_RETOut a')) /\ (!a. ~(Lt_callStoreOut a = Lt_tau)) /\ (!a' a. ~(Lt_RetHostIn a = Lt_RetStoreIn a')) /\ (!a' a. ~(Lt_RetHostIn a = Lt_RETOut a')) /\ (!a. ~(Lt_RetHostIn a = Lt_tau)) /\ (!a' a. ~(Lt_RetStoreIn a = Lt_RETOut a')) /\ (!a. ~(Lt_RetStoreIn a = Lt_tau)) /\ !a. ~(Lt_RETOut a = Lt_tau) [Lthread_induction] Theorem |- !P. (!M. P (Lt_callModuleIn M)) /\ (!L. P (Lt_callHostOut L)) /\ (!a. P (Lt_callHostCreateOut a)) /\ (!S. P (Lt_callStoreOut S)) /\ (!T. P (Lt_RetHostIn T)) /\ (!T. P (Lt_RetStoreIn T)) /\ (!T. P (Lt_RETOut T)) /\ P Lt_tau ==> !L. P L [Lthread_nchotomy] Theorem |- !L. (?M. L = Lt_callModuleIn M) \/ (?L'. L = Lt_callHostOut L') \/ (?a. L = Lt_callHostCreateOut a) \/ (?S. L = Lt_callStoreOut S) \/ (?T. L = Lt_RetHostIn T) \/ (?T. L = Lt_RetStoreIn T) \/ (?T. L = Lt_RETOut T) \/ (L = Lt_tau) [thread_11] Theorem |- !a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a0' a1' a2' a3' a4' a5' a6' a7' a8' a9' a10' a11' a12'. (thread a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 = thread a0' a1' a2' a3' a4' a5' a6' a7' a8' a9' a10' a11' a12') = (a0 = a0') /\ (a1 = a1') /\ (a2 = a2') /\ (a3 = a3') /\ (a4 = a4') /\ (a5 = a5') /\ (a6 = a6') /\ (a7 = a7') /\ (a8 = a8') /\ (a9 = a9') /\ (a10 = a10') /\ (a11 = a11') /\ (a12 = a12') [thread_Axiom] Theorem |- !f. ?fn. !a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12. fn (thread a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12) = f a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 [thread_CallHostCreate_update_semi11] Theorem |- !x y r1 r2. (r1 with CallHostCreate := x = r2 with CallHostCreate := y) ==> (x = y) [thread_CallHost_update_semi11] Theorem |- !x y r1 r2. (r1 with CallHost := x = r2 with CallHost := y) ==> (x = y) [thread_CallStore_update_semi11] Theorem |- !x y r1 r2. (r1 with CallStore := x = r2 with CallStore := y) ==> (x = y) [thread_Module_update_semi11] Theorem |- !x y r1 r2. (r1 with Module := x = r2 with Module := y) ==> (x = y) [thread_Prog_update_semi11] Theorem |- !x y r1 r2. (r1 with Prog := x = r2 with Prog := y) ==> (x = y) [thread_RETtl_update_semi11] Theorem |- !x y r1 r2. (r1 with RETtl := x = r2 with RETtl := y) ==> (x = y) [thread_RetHosttl_update_semi11] Theorem |- !x y r1 r2. (r1 with RetHosttl := x = r2 with RetHosttl := y) ==> (x = y) [thread_RetStoretl_update_semi11] Theorem |- !x y r1 r2. (r1 with RetStoretl := x = r2 with RetStoretl := y) ==> (x = y) [thread_Rettl_update_semi11] Theorem |- !x y r1 r2. (r1 with Rettl := x = r2 with Rettl := y) ==> (x = y) [thread_Tau_update_semi11] Theorem |- !x y r1 r2. (r1 with Tau := x = r2 with Tau := y) ==> (x = y) [thread_Term_update_semi11] Theorem |- !x y r1 r2. (r1 with Term := x = r2 with Term := y) ==> (x = y) [thread_accessors] Theorem |- (!a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10).initial = a) /\ (!a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10).transition = f) /\ (!a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10).Module = f0) /\ (!a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10).CallHost = f1) /\ (!a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10).CallHostCreate = f2) /\ (!a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10).CallStore = f3) /\ (!a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10).RetHosttl = f4) /\ (!a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10).RetStoretl = f5) /\ (!a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10).RETtl = f6) /\ (!a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10).Tau = f7) /\ (!a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10).Term = f8) /\ (!a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10).Rettl = f9) /\ !a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10).Prog = f10 [thread_accfupds] Theorem |- (!t f. (t with transition updated_by f).initial = t.initial) /\ (!t f. (t with Module updated_by f).initial = t.initial) /\ (!t f. (t with CallHost updated_by f).initial = t.initial) /\ (!t f. (t with CallHostCreate updated_by f).initial = t.initial) /\ (!t f. (t with CallStore updated_by f).initial = t.initial) /\ (!t f. (t with RetHosttl updated_by f).initial = t.initial) /\ (!t f. (t with RetStoretl updated_by f).initial = t.initial) /\ (!t f. (t with RETtl updated_by f).initial = t.initial) /\ (!t f. (t with Tau updated_by f).initial = t.initial) /\ (!t f. (t with Term updated_by f).initial = t.initial) /\ (!t f. (t with Rettl updated_by f).initial = t.initial) /\ (!t f. (t with Prog updated_by f).initial = t.initial) /\ (!t f. (t with initial updated_by f).transition = t.transition) /\ (!t f. (t with Module updated_by f).transition = t.transition) /\ (!t f. (t with CallHost updated_by f).transition = t.transition) /\ (!t f. (t with CallHostCreate updated_by f).transition = t.transition) /\ (!t f. (t with CallStore updated_by f).transition = t.transition) /\ (!t f. (t with RetHosttl updated_by f).transition = t.transition) /\ (!t f. (t with RetStoretl updated_by f).transition = t.transition) /\ (!t f. (t with RETtl updated_by f).transition = t.transition) /\ (!t f. (t with Tau updated_by f).transition = t.transition) /\ (!t f. (t with Term updated_by f).transition = t.transition) /\ (!t f. (t with Rettl updated_by f).transition = t.transition) /\ (!t f. (t with Prog updated_by f).transition = t.transition) /\ (!t f. (t with initial updated_by f).Module = t.Module) /\ (!t f. (t with transition updated_by f).Module = t.Module) /\ (!t f. (t with CallHost updated_by f).Module = t.Module) /\ (!t f. (t with CallHostCreate updated_by f).Module = t.Module) /\ (!t f. (t with CallStore updated_by f).Module = t.Module) /\ (!t f. (t with RetHosttl updated_by f).Module = t.Module) /\ (!t f. (t with RetStoretl updated_by f).Module = t.Module) /\ (!t f. (t with RETtl updated_by f).Module = t.Module) /\ (!t f. (t with Tau updated_by f).Module = t.Module) /\ (!t f. (t with Term updated_by f).Module = t.Module) /\ (!t f. (t with Rettl updated_by f).Module = t.Module) /\ (!t f. (t with Prog updated_by f).Module = t.Module) /\ (!t f. (t with initial updated_by f).CallHost = t.CallHost) /\ (!t f. (t with transition updated_by f).CallHost = t.CallHost) /\ (!t f. (t with Module updated_by f).CallHost = t.CallHost) /\ (!t f. (t with CallHostCreate updated_by f).CallHost = t.CallHost) /\ (!t f. (t with CallStore updated_by f).CallHost = t.CallHost) /\ (!t f. (t with RetHosttl updated_by f).CallHost = t.CallHost) /\ (!t f. (t with RetStoretl updated_by f).CallHost = t.CallHost) /\ (!t f. (t with RETtl updated_by f).CallHost = t.CallHost) /\ (!t f. (t with Tau updated_by f).CallHost = t.CallHost) /\ (!t f. (t with Term updated_by f).CallHost = t.CallHost) /\ (!t f. (t with Rettl updated_by f).CallHost = t.CallHost) /\ (!t f. (t with Prog updated_by f).CallHost = t.CallHost) /\ (!t f. (t with initial updated_by f).CallHostCreate = t.CallHostCreate) /\ (!t f. (t with transition updated_by f).CallHostCreate = t.CallHostCreate) /\ (!t f. (t with Module updated_by f).CallHostCreate = t.CallHostCreate) /\ (!t f. (t with CallHost updated_by f).CallHostCreate = t.CallHostCreate) /\ (!t f. (t with CallStore updated_by f).CallHostCreate = t.CallHostCreate) /\ (!t f. (t with RetHosttl updated_by f).CallHostCreate = t.CallHostCreate) /\ (!t f. (t with RetStoretl updated_by f).CallHostCreate = t.CallHostCreate) /\ (!t f. (t with RETtl updated_by f).CallHostCreate = t.CallHostCreate) /\ (!t f. (t with Tau updated_by f).CallHostCreate = t.CallHostCreate) /\ (!t f. (t with Term updated_by f).CallHostCreate = t.CallHostCreate) /\ (!t f. (t with Rettl updated_by f).CallHostCreate = t.CallHostCreate) /\ (!t f. (t with Prog updated_by f).CallHostCreate = t.CallHostCreate) /\ (!t f. (t with initial updated_by f).CallStore = t.CallStore) /\ (!t f. (t with transition updated_by f).CallStore = t.CallStore) /\ (!t f. (t with Module updated_by f).CallStore = t.CallStore) /\ (!t f. (t with CallHost updated_by f).CallStore = t.CallStore) /\ (!t f. (t with CallHostCreate updated_by f).CallStore = t.CallStore) /\ (!t f. (t with RetHosttl updated_by f).CallStore = t.CallStore) /\ (!t f. (t with RetStoretl updated_by f).CallStore = t.CallStore) /\ (!t f. (t with RETtl updated_by f).CallStore = t.CallStore) /\ (!t f. (t with Tau updated_by f).CallStore = t.CallStore) /\ (!t f. (t with Term updated_by f).CallStore = t.CallStore) /\ (!t f. (t with Rettl updated_by f).CallStore = t.CallStore) /\ (!t f. (t with Prog updated_by f).CallStore = t.CallStore) /\ (!t f. (t with initial updated_by f).RetHosttl = t.RetHosttl) /\ (!t f. (t with transition updated_by f).RetHosttl = t.RetHosttl) /\ (!t f. (t with Module updated_by f).RetHosttl = t.RetHosttl) /\ (!t f. (t with CallHost updated_by f).RetHosttl = t.RetHosttl) /\ (!t f. (t with CallHostCreate updated_by f).RetHosttl = t.RetHosttl) /\ (!t f. (t with CallStore updated_by f).RetHosttl = t.RetHosttl) /\ (!t f. (t with RetStoretl updated_by f).RetHosttl = t.RetHosttl) /\ (!t f. (t with RETtl updated_by f).RetHosttl = t.RetHosttl) /\ (!t f. (t with Tau updated_by f).RetHosttl = t.RetHosttl) /\ (!t f. (t with Term updated_by f).RetHosttl = t.RetHosttl) /\ (!t f. (t with Rettl updated_by f).RetHosttl = t.RetHosttl) /\ (!t f. (t with Prog updated_by f).RetHosttl = t.RetHosttl) /\ (!t f. (t with initial updated_by f).RetStoretl = t.RetStoretl) /\ (!t f. (t with transition updated_by f).RetStoretl = t.RetStoretl) /\ (!t f. (t with Module updated_by f).RetStoretl = t.RetStoretl) /\ (!t f. (t with CallHost updated_by f).RetStoretl = t.RetStoretl) /\ (!t f. (t with CallHostCreate updated_by f).RetStoretl = t.RetStoretl) /\ (!t f. (t with CallStore updated_by f).RetStoretl = t.RetStoretl) /\ (!t f. (t with RetHosttl updated_by f).RetStoretl = t.RetStoretl) /\ (!t f. (t with RETtl updated_by f).RetStoretl = t.RetStoretl) /\ (!t f. (t with Tau updated_by f).RetStoretl = t.RetStoretl) /\ (!t f. (t with Term updated_by f).RetStoretl = t.RetStoretl) /\ (!t f. (t with Rettl updated_by f).RetStoretl = t.RetStoretl) /\ (!t f. (t with Prog updated_by f).RetStoretl = t.RetStoretl) /\ (!t f. (t with initial updated_by f).RETtl = t.RETtl) /\ (!t f. (t with transition updated_by f).RETtl = t.RETtl) /\ (!t f. (t with Module updated_by f).RETtl = t.RETtl) /\ (!t f. (t with CallHost updated_by f).RETtl = t.RETtl) /\ (!t f. (t with CallHostCreate updated_by f).RETtl = t.RETtl) /\ (!t f. (t with CallStore updated_by f).RETtl = t.RETtl) /\ (!t f. (t with RetHosttl updated_by f).RETtl = t.RETtl) /\ (!t f. (t with RetStoretl updated_by f).RETtl = t.RETtl) /\ (!t f. (t with Tau updated_by f).RETtl = t.RETtl) /\ (!t f. (t with Term updated_by f).RETtl = t.RETtl) /\ (!t f. (t with Rettl updated_by f).RETtl = t.RETtl) /\ (!t f. (t with Prog updated_by f).RETtl = t.RETtl) /\ (!t f. (t with initial updated_by f).Tau = t.Tau) /\ (!t f. (t with transition updated_by f).Tau = t.Tau) /\ (!t f. (t with Module updated_by f).Tau = t.Tau) /\ (!t f. (t with CallHost updated_by f).Tau = t.Tau) /\ (!t f. (t with CallHostCreate updated_by f).Tau = t.Tau) /\ (!t f. (t with CallStore updated_by f).Tau = t.Tau) /\ (!t f. (t with RetHosttl updated_by f).Tau = t.Tau) /\ (!t f. (t with RetStoretl updated_by f).Tau = t.Tau) /\ (!t f. (t with RETtl updated_by f).Tau = t.Tau) /\ (!t f. (t with Term updated_by f).Tau = t.Tau) /\ (!t f. (t with Rettl updated_by f).Tau = t.Tau) /\ (!t f. (t with Prog updated_by f).Tau = t.Tau) /\ (!t f. (t with initial updated_by f).Term = t.Term) /\ (!t f. (t with transition updated_by f).Term = t.Term) /\ (!t f. (t with Module updated_by f).Term = t.Term) /\ (!t f. (t with CallHost updated_by f).Term = t.Term) /\ (!t f. (t with CallHostCreate updated_by f).Term = t.Term) /\ (!t f. (t with CallStore updated_by f).Term = t.Term) /\ (!t f. (t with RetHosttl updated_by f).Term = t.Term) /\ (!t f. (t with RetStoretl updated_by f).Term = t.Term) /\ (!t f. (t with RETtl updated_by f).Term = t.Term) /\ (!t f. (t with Tau updated_by f).Term = t.Term) /\ (!t f. (t with Rettl updated_by f).Term = t.Term) /\ (!t f. (t with Prog updated_by f).Term = t.Term) /\ (!t f. (t with initial updated_by f).Rettl = t.Rettl) /\ (!t f. (t with transition updated_by f).Rettl = t.Rettl) /\ (!t f. (t with Module updated_by f).Rettl = t.Rettl) /\ (!t f. (t with CallHost updated_by f).Rettl = t.Rettl) /\ (!t f. (t with CallHostCreate updated_by f).Rettl = t.Rettl) /\ (!t f. (t with CallStore updated_by f).Rettl = t.Rettl) /\ (!t f. (t with RetHosttl updated_by f).Rettl = t.Rettl) /\ (!t f. (t with RetStoretl updated_by f).Rettl = t.Rettl) /\ (!t f. (t with RETtl updated_by f).Rettl = t.Rettl) /\ (!t f. (t with Tau updated_by f).Rettl = t.Rettl) /\ (!t f. (t with Term updated_by f).Rettl = t.Rettl) /\ (!t f. (t with Prog updated_by f).Rettl = t.Rettl) /\ (!t f. (t with initial updated_by f).Prog = t.Prog) /\ (!t f. (t with transition updated_by f).Prog = t.Prog) /\ (!t f. (t with Module updated_by f).Prog = t.Prog) /\ (!t f. (t with CallHost updated_by f).Prog = t.Prog) /\ (!t f. (t with CallHostCreate updated_by f).Prog = t.Prog) /\ (!t f. (t with CallStore updated_by f).Prog = t.Prog) /\ (!t f. (t with RetHosttl updated_by f).Prog = t.Prog) /\ (!t f. (t with RetStoretl updated_by f).Prog = t.Prog) /\ (!t f. (t with RETtl updated_by f).Prog = t.Prog) /\ (!t f. (t with Tau updated_by f).Prog = t.Prog) /\ (!t f. (t with Term updated_by f).Prog = t.Prog) /\ (!t f. (t with Rettl updated_by f).Prog = t.Prog) /\ (!t f. (t with initial updated_by f).initial = f t.initial) /\ (!t f. (t with transition updated_by f).transition = f t.transition) /\ (!t f. (t with Module updated_by f).Module = f t.Module) /\ (!t f. (t with CallHost updated_by f).CallHost = f t.CallHost) /\ (!t f. (t with CallHostCreate updated_by f).CallHostCreate = f t.CallHostCreate) /\ (!t f. (t with CallStore updated_by f).CallStore = f t.CallStore) /\ (!t f. (t with RetHosttl updated_by f).RetHosttl = f t.RetHosttl) /\ (!t f. (t with RetStoretl updated_by f).RetStoretl = f t.RetStoretl) /\ (!t f. (t with RETtl updated_by f).RETtl = f t.RETtl) /\ (!t f. (t with Tau updated_by f).Tau = f t.Tau) /\ (!t f. (t with Term updated_by f).Term = f t.Term) /\ (!t f. (t with Rettl updated_by f).Rettl = f t.Rettl) /\ !t f. (t with Prog updated_by f).Prog = f t.Prog [thread_accupds] Theorem |- (!x t. (t with transition := x).initial = t.initial) /\ (!x t. (t with Module := x).initial = t.initial) /\ (!x t. (t with CallHost := x).initial = t.initial) /\ (!x t. (t with CallHostCreate := x).initial = t.initial) /\ (!x t. (t with CallStore := x).initial = t.initial) /\ (!x t. (t with RetHosttl := x).initial = t.initial) /\ (!x t. (t with RetStoretl := x).initial = t.initial) /\ (!x t. (t with RETtl := x).initial = t.initial) /\ (!x t. (t with Tau := x).initial = t.initial) /\ (!x t. (t with Term := x).initial = t.initial) /\ (!x t. (t with Rettl := x).initial = t.initial) /\ (!x t. (t with Prog := x).initial = t.initial) /\ (!x t. (t with initial := x).transition = t.transition) /\ (!x t. (t with Module := x).transition = t.transition) /\ (!x t. (t with CallHost := x).transition = t.transition) /\ (!x t. (t with CallHostCreate := x).transition = t.transition) /\ (!x t. (t with CallStore := x).transition = t.transition) /\ (!x t. (t with RetHosttl := x).transition = t.transition) /\ (!x t. (t with RetStoretl := x).transition = t.transition) /\ (!x t. (t with RETtl := x).transition = t.transition) /\ (!x t. (t with Tau := x).transition = t.transition) /\ (!x t. (t with Term := x).transition = t.transition) /\ (!x t. (t with Rettl := x).transition = t.transition) /\ (!x t. (t with Prog := x).transition = t.transition) /\ (!x t. (t with initial := x).Module = t.Module) /\ (!x t. (t with transition := x).Module = t.Module) /\ (!x t. (t with CallHost := x).Module = t.Module) /\ (!x t. (t with CallHostCreate := x).Module = t.Module) /\ (!x t. (t with CallStore := x).Module = t.Module) /\ (!x t. (t with RetHosttl := x).Module = t.Module) /\ (!x t. (t with RetStoretl := x).Module = t.Module) /\ (!x t. (t with RETtl := x).Module = t.Module) /\ (!x t. (t with Tau := x).Module = t.Module) /\ (!x t. (t with Term := x).Module = t.Module) /\ (!x t. (t with Rettl := x).Module = t.Module) /\ (!x t. (t with Prog := x).Module = t.Module) /\ (!x t. (t with initial := x).CallHost = t.CallHost) /\ (!x t. (t with transition := x).CallHost = t.CallHost) /\ (!x t. (t with Module := x).CallHost = t.CallHost) /\ (!x t. (t with CallHostCreate := x).CallHost = t.CallHost) /\ (!x t. (t with CallStore := x).CallHost = t.CallHost) /\ (!x t. (t with RetHosttl := x).CallHost = t.CallHost) /\ (!x t. (t with RetStoretl := x).CallHost = t.CallHost) /\ (!x t. (t with RETtl := x).CallHost = t.CallHost) /\ (!x t. (t with Tau := x).CallHost = t.CallHost) /\ (!x t. (t with Term := x).CallHost = t.CallHost) /\ (!x t. (t with Rettl := x).CallHost = t.CallHost) /\ (!x t. (t with Prog := x).CallHost = t.CallHost) /\ (!x t. (t with initial := x).CallHostCreate = t.CallHostCreate) /\ (!x t. (t with transition := x).CallHostCreate = t.CallHostCreate) /\ (!x t. (t with Module := x).CallHostCreate = t.CallHostCreate) /\ (!x t. (t with CallHost := x).CallHostCreate = t.CallHostCreate) /\ (!x t. (t with CallStore := x).CallHostCreate = t.CallHostCreate) /\ (!x t. (t with RetHosttl := x).CallHostCreate = t.CallHostCreate) /\ (!x t. (t with RetStoretl := x).CallHostCreate = t.CallHostCreate) /\ (!x t. (t with RETtl := x).CallHostCreate = t.CallHostCreate) /\ (!x t. (t with Tau := x).CallHostCreate = t.CallHostCreate) /\ (!x t. (t with Term := x).CallHostCreate = t.CallHostCreate) /\ (!x t. (t with Rettl := x).CallHostCreate = t.CallHostCreate) /\ (!x t. (t with Prog := x).CallHostCreate = t.CallHostCreate) /\ (!x t. (t with initial := x).CallStore = t.CallStore) /\ (!x t. (t with transition := x).CallStore = t.CallStore) /\ (!x t. (t with Module := x).CallStore = t.CallStore) /\ (!x t. (t with CallHost := x).CallStore = t.CallStore) /\ (!x t. (t with CallHostCreate := x).CallStore = t.CallStore) /\ (!x t. (t with RetHosttl := x).CallStore = t.CallStore) /\ (!x t. (t with RetStoretl := x).CallStore = t.CallStore) /\ (!x t. (t with RETtl := x).CallStore = t.CallStore) /\ (!x t. (t with Tau := x).CallStore = t.CallStore) /\ (!x t. (t with Term := x).CallStore = t.CallStore) /\ (!x t. (t with Rettl := x).CallStore = t.CallStore) /\ (!x t. (t with Prog := x).CallStore = t.CallStore) /\ (!x t. (t with initial := x).RetHosttl = t.RetHosttl) /\ (!x t. (t with transition := x).RetHosttl = t.RetHosttl) /\ (!x t. (t with Module := x).RetHosttl = t.RetHosttl) /\ (!x t. (t with CallHost := x).RetHosttl = t.RetHosttl) /\ (!x t. (t with CallHostCreate := x).RetHosttl = t.RetHosttl) /\ (!x t. (t with CallStore := x).RetHosttl = t.RetHosttl) /\ (!x t. (t with RetStoretl := x).RetHosttl = t.RetHosttl) /\ (!x t. (t with RETtl := x).RetHosttl = t.RetHosttl) /\ (!x t. (t with Tau := x).RetHosttl = t.RetHosttl) /\ (!x t. (t with Term := x).RetHosttl = t.RetHosttl) /\ (!x t. (t with Rettl := x).RetHosttl = t.RetHosttl) /\ (!x t. (t with Prog := x).RetHosttl = t.RetHosttl) /\ (!x t. (t with initial := x).RetStoretl = t.RetStoretl) /\ (!x t. (t with transition := x).RetStoretl = t.RetStoretl) /\ (!x t. (t with Module := x).RetStoretl = t.RetStoretl) /\ (!x t. (t with CallHost := x).RetStoretl = t.RetStoretl) /\ (!x t. (t with CallHostCreate := x).RetStoretl = t.RetStoretl) /\ (!x t. (t with CallStore := x).RetStoretl = t.RetStoretl) /\ (!x t. (t with RetHosttl := x).RetStoretl = t.RetStoretl) /\ (!x t. (t with RETtl := x).RetStoretl = t.RetStoretl) /\ (!x t. (t with Tau := x).RetStoretl = t.RetStoretl) /\ (!x t. (t with Term := x).RetStoretl = t.RetStoretl) /\ (!x t. (t with Rettl := x).RetStoretl = t.RetStoretl) /\ (!x t. (t with Prog := x).RetStoretl = t.RetStoretl) /\ (!x t. (t with initial := x).RETtl = t.RETtl) /\ (!x t. (t with transition := x).RETtl = t.RETtl) /\ (!x t. (t with Module := x).RETtl = t.RETtl) /\ (!x t. (t with CallHost := x).RETtl = t.RETtl) /\ (!x t. (t with CallHostCreate := x).RETtl = t.RETtl) /\ (!x t. (t with CallStore := x).RETtl = t.RETtl) /\ (!x t. (t with RetHosttl := x).RETtl = t.RETtl) /\ (!x t. (t with RetStoretl := x).RETtl = t.RETtl) /\ (!x t. (t with Tau := x).RETtl = t.RETtl) /\ (!x t. (t with Term := x).RETtl = t.RETtl) /\ (!x t. (t with Rettl := x).RETtl = t.RETtl) /\ (!x t. (t with Prog := x).RETtl = t.RETtl) /\ (!x t. (t with initial := x).Tau = t.Tau) /\ (!x t. (t with transition := x).Tau = t.Tau) /\ (!x t. (t with Module := x).Tau = t.Tau) /\ (!x t. (t with CallHost := x).Tau = t.Tau) /\ (!x t. (t with CallHostCreate := x).Tau = t.Tau) /\ (!x t. (t with CallStore := x).Tau = t.Tau) /\ (!x t. (t with RetHosttl := x).Tau = t.Tau) /\ (!x t. (t with RetStoretl := x).Tau = t.Tau) /\ (!x t. (t with RETtl := x).Tau = t.Tau) /\ (!x t. (t with Term := x).Tau = t.Tau) /\ (!x t. (t with Rettl := x).Tau = t.Tau) /\ (!x t. (t with Prog := x).Tau = t.Tau) /\ (!x t. (t with initial := x).Term = t.Term) /\ (!x t. (t with transition := x).Term = t.Term) /\ (!x t. (t with Module := x).Term = t.Term) /\ (!x t. (t with CallHost := x).Term = t.Term) /\ (!x t. (t with CallHostCreate := x).Term = t.Term) /\ (!x t. (t with CallStore := x).Term = t.Term) /\ (!x t. (t with RetHosttl := x).Term = t.Term) /\ (!x t. (t with RetStoretl := x).Term = t.Term) /\ (!x t. (t with RETtl := x).Term = t.Term) /\ (!x t. (t with Tau := x).Term = t.Term) /\ (!x t. (t with Rettl := x).Term = t.Term) /\ (!x t. (t with Prog := x).Term = t.Term) /\ (!x t. (t with initial := x).Rettl = t.Rettl) /\ (!x t. (t with transition := x).Rettl = t.Rettl) /\ (!x t. (t with Module := x).Rettl = t.Rettl) /\ (!x t. (t with CallHost := x).Rettl = t.Rettl) /\ (!x t. (t with CallHostCreate := x).Rettl = t.Rettl) /\ (!x t. (t with CallStore := x).Rettl = t.Rettl) /\ (!x t. (t with RetHosttl := x).Rettl = t.Rettl) /\ (!x t. (t with RetStoretl := x).Rettl = t.Rettl) /\ (!x t. (t with RETtl := x).Rettl = t.Rettl) /\ (!x t. (t with Tau := x).Rettl = t.Rettl) /\ (!x t. (t with Term := x).Rettl = t.Rettl) /\ (!x t. (t with Prog := x).Rettl = t.Rettl) /\ (!x t. (t with initial := x).Prog = t.Prog) /\ (!x t. (t with transition := x).Prog = t.Prog) /\ (!x t. (t with Module := x).Prog = t.Prog) /\ (!x t. (t with CallHost := x).Prog = t.Prog) /\ (!x t. (t with CallHostCreate := x).Prog = t.Prog) /\ (!x t. (t with CallStore := x).Prog = t.Prog) /\ (!x t. (t with RetHosttl := x).Prog = t.Prog) /\ (!x t. (t with RetStoretl := x).Prog = t.Prog) /\ (!x t. (t with RETtl := x).Prog = t.Prog) /\ (!x t. (t with Tau := x).Prog = t.Prog) /\ (!x t. (t with Term := x).Prog = t.Prog) /\ (!x t. (t with Rettl := x).Prog = t.Prog) /\ (!x t. (t with initial := x).initial = x) /\ (!x t. (t with transition := x).transition = x) /\ (!x t. (t with Module := x).Module = x) /\ (!x t. (t with CallHost := x).CallHost = x) /\ (!x t. (t with CallHostCreate := x).CallHostCreate = x) /\ (!x t. (t with CallStore := x).CallStore = x) /\ (!x t. (t with RetHosttl := x).RetHosttl = x) /\ (!x t. (t with RetStoretl := x).RetStoretl = x) /\ (!x t. (t with RETtl := x).RETtl = x) /\ (!x t. (t with Tau := x).Tau = x) /\ (!x t. (t with Term := x).Term = x) /\ (!x t. (t with Rettl := x).Rettl = x) /\ !x t. (t with Prog := x).Prog = x [thread_case_cong] Theorem |- !M M' f. (M = M') /\ (!a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12. (M' = thread a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12) ==> (f a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 = f' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12)) ==> (case f M = case f' M') [thread_component_equality] Theorem |- !t1 t2. (t1 = t2) = (t1.initial = t2.initial) /\ (t1.transition = t2.transition) /\ (t1.Module = t2.Module) /\ (t1.CallHost = t2.CallHost) /\ (t1.CallHostCreate = t2.CallHostCreate) /\ (t1.CallStore = t2.CallStore) /\ (t1.RetHosttl = t2.RetHosttl) /\ (t1.RetStoretl = t2.RetStoretl) /\ (t1.RETtl = t2.RETtl) /\ (t1.Tau = t2.Tau) /\ (t1.Term = t2.Term) /\ (t1.Rettl = t2.Rettl) /\ (t1.Prog = t2.Prog) [thread_cupdaccs] Theorem |- (!val t. (val = t.initial) ==> (t with initial := val = t)) /\ (!val t. (val = t.transition) ==> (t with transition := val = t)) /\ (!val t. (val = t.Module) ==> (t with Module := val = t)) /\ (!val t. (val = t.CallHost) ==> (t with CallHost := val = t)) /\ (!val t. (val = t.CallHostCreate) ==> (t with CallHostCreate := val = t)) /\ (!val t. (val = t.CallStore) ==> (t with CallStore := val = t)) /\ (!val t. (val = t.RetHosttl) ==> (t with RetHosttl := val = t)) /\ (!val t. (val = t.RetStoretl) ==> (t with RetStoretl := val = t)) /\ (!val t. (val = t.RETtl) ==> (t with RETtl := val = t)) /\ (!val t. (val = t.Tau) ==> (t with Tau := val = t)) /\ (!val t. (val = t.Term) ==> (t with Term := val = t)) /\ (!val t. (val = t.Rettl) ==> (t with Rettl := val = t)) /\ !val t. (val = t.Prog) ==> (t with Prog := val = t) [thread_fn_updates] Theorem |- (!f x. x with initial updated_by f = x with initial := f x.initial) /\ (!f x. x with transition updated_by f = x with transition := f x.transition) /\ (!f x. x with Module updated_by f = x with Module := f x.Module) /\ (!f x. x with CallHost updated_by f = x with CallHost := f x.CallHost) /\ (!f x. x with CallHostCreate updated_by f = x with CallHostCreate := f x.CallHostCreate) /\ (!f x. x with CallStore updated_by f = x with CallStore := f x.CallStore) /\ (!f x. x with RetHosttl updated_by f = x with RetHosttl := f x.RetHosttl) /\ (!f x. x with RetStoretl updated_by f = x with RetStoretl := f x.RetStoretl) /\ (!f x. x with RETtl updated_by f = x with RETtl := f x.RETtl) /\ (!f x. x with Tau updated_by f = x with Tau := f x.Tau) /\ (!f x. x with Term updated_by f = x with Term := f x.Term) /\ (!f x. x with Rettl updated_by f = x with Rettl := f x.Rettl) /\ !f x. x with Prog updated_by f = x with Prog := f x.Prog [thread_induction] Theorem |- !P. (!a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. P (thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10)) ==> !t. P t [thread_initial_update_semi11] Theorem |- !x y r1 r2. (r1 with initial := x = r2 with initial := y) ==> (x = y) [thread_nchotomy] Theorem |- !t. ?a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. t = thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 [thread_transition_update_semi11] Theorem |- !x y r1 r2. (r1 with transition := x = r2 with transition := y) ==> (x = y) [thread_updaccs] Theorem |- (!t. t with initial := t.initial = t) /\ (!t. t with transition := t.transition = t) /\ (!t. t with Module := t.Module = t) /\ (!t. t with CallHost := t.CallHost = t) /\ (!t. t with CallHostCreate := t.CallHostCreate = t) /\ (!t. t with CallStore := t.CallStore = t) /\ (!t. t with RetHosttl := t.RetHosttl = t) /\ (!t. t with RetStoretl := t.RetStoretl = t) /\ (!t. t with RETtl := t.RETtl = t) /\ (!t. t with Tau := t.Tau = t) /\ (!t. t with Term := t.Term = t) /\ (!t. t with Rettl := t.Rettl = t) /\ !t. t with Prog := t.Prog = t [thread_updates] Theorem |- (!a0 a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 with initial := a0 = thread a0 f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10) /\ (!f11 a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 with transition := f11 = thread a f11 f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10) /\ (!f11 a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 with Module := f11 = thread a f f11 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10) /\ (!f11 a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 with CallHost := f11 = thread a f f0 f11 f2 f3 f4 f5 f6 f7 f8 f9 f10) /\ (!f11 a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 with CallHostCreate := f11 = thread a f f0 f1 f11 f3 f4 f5 f6 f7 f8 f9 f10) /\ (!f11 a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 with CallStore := f11 = thread a f f0 f1 f2 f11 f4 f5 f6 f7 f8 f9 f10) /\ (!f11 a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 with RetHosttl := f11 = thread a f f0 f1 f2 f3 f11 f5 f6 f7 f8 f9 f10) /\ (!f11 a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 with RetStoretl := f11 = thread a f f0 f1 f2 f3 f4 f11 f6 f7 f8 f9 f10) /\ (!f11 a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 with RETtl := f11 = thread a f f0 f1 f2 f3 f4 f5 f11 f7 f8 f9 f10) /\ (!f11 a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 with Tau := f11 = thread a f f0 f1 f2 f3 f4 f5 f6 f11 f8 f9 f10) /\ (!f11 a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 with Term := f11 = thread a f f0 f1 f2 f3 f4 f5 f6 f7 f11 f9 f10) /\ (!f11 a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 with Rettl := f11 = thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f11 f10) /\ !f11 a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 with Prog := f11 = thread a f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f11 [thread_updates_eq_literal] Theorem |- !t f9 f8 f7 f6 f5 f4 f3 f2 f10 f1 f0 f a. t with <|initial := a; transition := f10; Module := f9; CallHost := f8; CallHostCreate := f7; CallStore := f6; RetHosttl := f5; RetStoretl := f4; RETtl := f3; Tau := f2; Term := f1; Rettl := f0; Prog := f|> = <|initial := a; transition := f10; Module := f9; CallHost := f8; CallHostCreate := f7; CallStore := f6; RetHosttl := f5; RetStoretl := f4; RETtl := f3; Tau := f2; Term := f1; Rettl := f0; Prog := f|> [thread_updcanon] Theorem |- (!z x t. t with <|transition := x; initial := z|> = t with <|initial := z; transition := x|>) /\ (!z x t. t with <|Module := x; initial := z|> = t with <|initial := z; Module := x|>) /\ (!z x t. t with <|Module := x; transition := z|> = t with <|transition := z; Module := x|>) /\ (!z x t. t with <|CallHost := x; initial := z|> = t with <|initial := z; CallHost := x|>) /\ (!z x t. t with <|CallHost := x; transition := z|> = t with <|transition := z; CallHost := x|>) /\ (!z x t. t with <|CallHost := x; Module := z|> = t with <|Module := z; CallHost := x|>) /\ (!z x t. t with <|CallHostCreate := x; initial := z|> = t with <|initial := z; CallHostCreate := x|>) /\ (!z x t. t with <|CallHostCreate := x; transition := z|> = t with <|transition := z; CallHostCreate := x|>) /\ (!z x t. t with <|CallHostCreate := x; Module := z|> = t with <|Module := z; CallHostCreate := x|>) /\ (!z x t. t with <|CallHostCreate := x; CallHost := z|> = t with <|CallHost := z; CallHostCreate := x|>) /\ (!z x t. t with <|CallStore := x; initial := z|> = t with <|initial := z; CallStore := x|>) /\ (!z x t. t with <|CallStore := x; transition := z|> = t with <|transition := z; CallStore := x|>) /\ (!z x t. t with <|CallStore := x; Module := z|> = t with <|Module := z; CallStore := x|>) /\ (!z x t. t with <|CallStore := x; CallHost := z|> = t with <|CallHost := z; CallStore := x|>) /\ (!z x t. t with <|CallStore := x; CallHostCreate := z|> = t with <|CallHostCreate := z; CallStore := x|>) /\ (!z x t. t with <|RetHosttl := x; initial := z|> = t with <|initial := z; RetHosttl := x|>) /\ (!z x t. t with <|RetHosttl := x; transition := z|> = t with <|transition := z; RetHosttl := x|>) /\ (!z x t. t with <|RetHosttl := x; Module := z|> = t with <|Module := z; RetHosttl := x|>) /\ (!z x t. t with <|RetHosttl := x; CallHost := z|> = t with <|CallHost := z; RetHosttl := x|>) /\ (!z x t. t with <|RetHosttl := x; CallHostCreate := z|> = t with <|CallHostCreate := z; RetHosttl := x|>) /\ (!z x t. t with <|RetHosttl := x; CallStore := z|> = t with <|CallStore := z; RetHosttl := x|>) /\ (!z x t. t with <|RetStoretl := x; initial := z|> = t with <|initial := z; RetStoretl := x|>) /\ (!z x t. t with <|RetStoretl := x; transition := z|> = t with <|transition := z; RetStoretl := x|>) /\ (!z x t. t with <|RetStoretl := x; Module := z|> = t with <|Module := z; RetStoretl := x|>) /\ (!z x t. t with <|RetStoretl := x; CallHost := z|> = t with <|CallHost := z; RetStoretl := x|>) /\ (!z x t. t with <|RetStoretl := x; CallHostCreate := z|> = t with <|CallHostCreate := z; RetStoretl := x|>) /\ (!z x t. t with <|RetStoretl := x; CallStore := z|> = t with <|CallStore := z; RetStoretl := x|>) /\ (!z x t. t with <|RetStoretl := x; RetHosttl := z|> = t with <|RetHosttl := z; RetStoretl := x|>) /\ (!z x t. t with <|RETtl := x; initial := z|> = t with <|initial := z; RETtl := x|>) /\ (!z x t. t with <|RETtl := x; transition := z|> = t with <|transition := z; RETtl := x|>) /\ (!z x t. t with <|RETtl := x; Module := z|> = t with <|Module := z; RETtl := x|>) /\ (!z x t. t with <|RETtl := x; CallHost := z|> = t with <|CallHost := z; RETtl := x|>) /\ (!z x t. t with <|RETtl := x; CallHostCreate := z|> = t with <|CallHostCreate := z; RETtl := x|>) /\ (!z x t. t with <|RETtl := x; CallStore := z|> = t with <|CallStore := z; RETtl := x|>) /\ (!z x t. t with <|RETtl := x; RetHosttl := z|> = t with <|RetHosttl := z; RETtl := x|>) /\ (!z x t. t with <|RETtl := x; RetStoretl := z|> = t with <|RetStoretl := z; RETtl := x|>) /\ (!z x t. t with <|Tau := x; initial := z|> = t with <|initial := z; Tau := x|>) /\ (!z x t. t with <|Tau := x; transition := z|> = t with <|transition := z; Tau := x|>) /\ (!z x t. t with <|Tau := x; Module := z|> = t with <|Module := z; Tau := x|>) /\ (!z x t. t with <|Tau := x; CallHost := z|> = t with <|CallHost := z; Tau := x|>) /\ (!z x t. t with <|Tau := x; CallHostCreate := z|> = t with <|CallHostCreate := z; Tau := x|>) /\ (!z x t. t with <|Tau := x; CallStore := z|> = t with <|CallStore := z; Tau := x|>) /\ (!z x t. t with <|Tau := x; RetHosttl := z|> = t with <|RetHosttl := z; Tau := x|>) /\ (!z x t. t with <|Tau := x; RetStoretl := z|> = t with <|RetStoretl := z; Tau := x|>) /\ (!z x t. t with <|Tau := x; RETtl := z|> = t with <|RETtl := z; Tau := x|>) /\ (!z x t. t with <|Term := x; initial := z|> = t with <|initial := z; Term := x|>) /\ (!z x t. t with <|Term := x; transition := z|> = t with <|transition := z; Term := x|>) /\ (!z x t. t with <|Term := x; Module := z|> = t with <|Module := z; Term := x|>) /\ (!z x t. t with <|Term := x; CallHost := z|> = t with <|CallHost := z; Term := x|>) /\ (!z x t. t with <|Term := x; CallHostCreate := z|> = t with <|CallHostCreate := z; Term := x|>) /\ (!z x t. t with <|Term := x; CallStore := z|> = t with <|CallStore := z; Term := x|>) /\ (!z x t. t with <|Term := x; RetHosttl := z|> = t with <|RetHosttl := z; Term := x|>) /\ (!z x t. t with <|Term := x; RetStoretl := z|> = t with <|RetStoretl := z; Term := x|>) /\ (!z x t. t with <|Term := x; RETtl := z|> = t with <|RETtl := z; Term := x|>) /\ (!z x t. t with <|Term := x; Tau := z|> = t with <|Tau := z; Term := x|>) /\ (!z x t. t with <|Rettl := x; initial := z|> = t with <|initial := z; Rettl := x|>) /\ (!z x t. t with <|Rettl := x; transition := z|> = t with <|transition := z; Rettl := x|>) /\ (!z x t. t with <|Rettl := x; Module := z|> = t with <|Module := z; Rettl := x|>) /\ (!z x t. t with <|Rettl := x; CallHost := z|> = t with <|CallHost := z; Rettl := x|>) /\ (!z x t. t with <|Rettl := x; CallHostCreate := z|> = t with <|CallHostCreate := z; Rettl := x|>) /\ (!z x t. t with <|Rettl := x; CallStore := z|> = t with <|CallStore := z; Rettl := x|>) /\ (!z x t. t with <|Rettl := x; RetHosttl := z|> = t with <|RetHosttl := z; Rettl := x|>) /\ (!z x t. t with <|Rettl := x; RetStoretl := z|> = t with <|RetStoretl := z; Rettl := x|>) /\ (!z x t. t with <|Rettl := x; RETtl := z|> = t with <|RETtl := z; Rettl := x|>) /\ (!z x t. t with <|Rettl := x; Tau := z|> = t with <|Tau := z; Rettl := x|>) /\ (!z x t. t with <|Rettl := x; Term := z|> = t with <|Term := z; Rettl := x|>) /\ (!z x t. t with <|Prog := x; initial := z|> = t with <|initial := z; Prog := x|>) /\ (!z x t. t with <|Prog := x; transition := z|> = t with <|transition := z; Prog := x|>) /\ (!z x t. t with <|Prog := x; Module := z|> = t with <|Module := z; Prog := x|>) /\ (!z x t. t with <|Prog := x; CallHost := z|> = t with <|CallHost := z; Prog := x|>) /\ (!z x t. t with <|Prog := x; CallHostCreate := z|> = t with <|CallHostCreate := z; Prog := x|>) /\ (!z x t. t with <|Prog := x; CallStore := z|> = t with <|CallStore := z; Prog := x|>) /\ (!z x t. t with <|Prog := x; RetHosttl := z|> = t with <|RetHosttl := z; Prog := x|>) /\ (!z x t. t with <|Prog := x; RetStoretl := z|> = t with <|RetStoretl := z; Prog := x|>) /\ (!z x t. t with <|Prog := x; RETtl := z|> = t with <|RETtl := z; Prog := x|>) /\ (!z x t. t with <|Prog := x; Tau := z|> = t with <|Tau := z; Prog := x|>) /\ (!z x t. t with <|Prog := x; Term := z|> = t with <|Term := z; Prog := x|>) /\ !z x t. t with <|Prog := x; Rettl := z|> = t with <|Rettl := z; Prog := x|> [thread_updupds] Theorem |- (!x2 x1 t. t with <|initial := x1; initial := x2|> = t with initial := x1) /\ (!x2 x1 t. t with <|transition := x1; transition := x2|> = t with transition := x1) /\ (!x2 x1 t. t with <|Module := x1; Module := x2|> = t with Module := x1) /\ (!x2 x1 t. t with <|CallHost := x1; CallHost := x2|> = t with CallHost := x1) /\ (!x2 x1 t. t with <|CallHostCreate := x1; CallHostCreate := x2|> = t with CallHostCreate := x1) /\ (!x2 x1 t. t with <|CallStore := x1; CallStore := x2|> = t with CallStore := x1) /\ (!x2 x1 t. t with <|RetHosttl := x1; RetHosttl := x2|> = t with RetHosttl := x1) /\ (!x2 x1 t. t with <|RetStoretl := x1; RetStoretl := x2|> = t with RetStoretl := x1) /\ (!x2 x1 t. t with <|RETtl := x1; RETtl := x2|> = t with RETtl := x1) /\ (!x2 x1 t. t with <|Tau := x1; Tau := x2|> = t with Tau := x1) /\ (!x2 x1 t. t with <|Term := x1; Term := x2|> = t with Term := x1) /\ (!x2 x1 t. t with <|Rettl := x1; Rettl := x2|> = t with Rettl := x1) /\ !x2 x1 t. t with <|Prog := x1; Prog := x2|> = t with Prog := x1 *) end