%Patch files loaded: patch2 version 2.417 $$$PVSHOME/pvs-strategies (defstep lazy-grind (&optional (if-match t) (defs !) rewrites theories exclude (updates? t)) (then (grind$ :if-match nil :defs defs :rewrites rewrites :theories theories :exclude exclude :updates? updates?) (reduce$ :if-match if-match :updates? updates?)) "Equiv. to (grind) with the instantiations postponed until after simplification." "By skolemization, if-lifting, simplification and instantiation") (defstep stew (&optional lazy-match (if-match t) (defs !) rewrites theories exclude (updates? t) &rest lemmas) (then (if lemmas (let ((lemmata (if (listp lemmas) lemmas (list lemmas))) (x `(then ,@(loop for lemma in lemmata append `((skosimp*)(use ,lemma)))))) x) (skip)) (if lazy-match (then (grind$ :if-match nil :defs defs :rewrites rewrites :theories theories :exclude exclude :updates? updates?) (reduce$ :if-match if-match :updates? updates?)) (grind$ :if-match if-match :defs defs :rewrites rewrites :theories theories :exclude exclude :updates? updates?))) "Does a combination of (lemma) and (grind)." "~%Grinding away with the supplied lemmas,") (defstep store-state (var) (let ((x (set var *ps*))) '(skip)) "" "") (defstep store-context (var) (let ((x (set var *current-context*))) '(skip)) "" "") $$$top.pvs % Authors : Todd Fine, Duane Olawsky % % Protection Notice : % % THIS IS AN UNPUBLISHED WORK CONTAINING SECURE COMPUTING % CORPORATION CONFIDENTIAL AND PROPRIETARY INFORMATION. % IF PUBLICATION OCCURS, THE FOLLOWING NOTICE APPLIES: % % (c) Copyright, 1995-1998, Secure Computing Corporation, All Rights Reserved. % % Revision Id : $Id: ac_translators.pvs.ref,v 1.2 1997/02/06 21:49:19 sundquis Exp $ % % Update Locker : $Locker: $ % % Contents : % % This file is part of the PVS version of the DTOS Composability Study. % It is the top theory. Its primary purpose is to pull everything % together to produce a PVS dump file. % % % Change History : % top : THEORY BEGIN IMPORTING system_props IMPORTING beh_equiv IMPORTING cmp_thm2 IMPORTING compose_associative IMPORTING compose_right END top $$$compose_right.pvs compose_right[ST: NONEMPTY_TYPE, AG: NONEMPTY_TYPE]: THEORY BEGIN IMPORTING cmp_thm[ST,AG] IMPORTING compose_idempotent[ST,AG] cset: VAR (composable[ST,AG]) b: VAR trace_t[ST,AG] cmp: VAR (comp_t) n: VAR nat cr_init: THEOREM (forall cmp: member(cmp,cset) implies member(b,prop_for(cmp))) implies initial_okay(compose(cset),b) cr_rely: THEOREM (forall cmp: member(cmp,cset) implies member(b,prop_for(cmp)) and member((sts(b)(n),sts(b)(n+1),ags(b)(n)),rely(cmp))) implies member((sts(b)(n),sts(b)(n+1),ags(b)(n)),steps(compose(cset))) cr_guar: THEOREM (forall cmp: member(cmp,cset) implies member(b,prop_for(cmp))) and (exists cmp: member(cmp,cset) and not member((sts(b)(n),sts(b)(n+1),ags(b)(n)),rely(cmp))) implies member((sts(b)(n),sts(b)(n+1),ags(b)(n)),steps(compose(cset))) cr_steps: THEOREM (forall cmp: member(cmp,cset) implies member(b,prop_for(cmp))) implies steps_okay(compose(cset),b) cr_wfar: THEOREM (forall cmp: member(cmp,cset) implies member(b,prop_for(cmp))) implies is_wfar(compose(cset),b) cr_sfar: THEOREM (forall cmp: member(cmp,cset) implies member(b,prop_for(cmp))) implies is_sfar(compose(cset),b) cr_aux: THEOREM (forall cmp: member(cmp,cset) implies member(b,prop_for(cmp))) implies member(b,prop_for(compose(cset))) compose_right: THEOREM (forall cmp: member(cmp,cset) implies tolerates(singleton(cmp),cset)) implies ( (forall cmp: member(cmp,cset) implies member(b,prop_for(cmp))) iff member(b,prop_for(compose(cset)))) END compose_right $$$compose_right.prf (|compose_right| (|cr_init| "" (SKOSIMP*) (("" (EXPAND "initial_okay") (("" (EXPAND "compose") (("" (EXPAND "member" +) (("" (EXPAND "compose_init") (("" (EXPAND "gen_intersection") (("" (SKOSIMP*) (("" (EXPAND "member" -2) (("" (EXPAND "inits_for") (("" (SKOSIMP*) (("" (REPLACE -3 :HIDE? -3) (("" (INST?) (("" (GROUND) (("" (EXPAND "member" -1) (("" (EXPAND "prop_for") (("" (FLATTEN) (("" (EXPAND "initial_okay") (("" (PROPAX) NIL))))))))))))))))))))))))))))))))))) (|cr_rely| "" (SKOSIMP*) (("" (CASE "not member((sts(b!1)(n!1), sts(b!1)(n!1 + 1), ags(b!1)(n!1)),rely(compose(cset!1)))") (("1" (DELETE 2) (("1" (EXPAND "member" +) (("1" (EXPAND "compose") (("1" (EXPAND "compose_rely") (("1" (EXPAND "gen_intersection") (("1" (SKOSIMP*) (("1" (EXPAND "member" -1) (("1" (EXPAND "relys_for") (("1" (SKOSIMP*) (("1" (REPLACE -2 :HIDE? -2) (("1" (INST?) (("1" (GROUND) NIL))))))))))))))))))))))) ("2" (DELETE -2) (("2" (EXPAND "member") (("2" (EXPAND "steps") (("2" (GROUND) NIL))))))))))) (|cr_guar| "" (SKOSIMP*) (("" (CASE "not member((sts(b!1)(n!1), sts(b!1)(n!1 + 1), ags(b!1)(n!1)),guar(compose(cset!1)))") (("1" (DELETE 3) (("1" (EXPAND "member" 1) (("1" (EXPAND "compose") (("1" (EXPAND "compose_guar") (("1" (EXPAND "intersection") (("1" (SPLIT) (("1" (EXPAND "member" 1) (("1" (EXPAND "gen_intersection") (("1" (SKOSIMP*) (("1" (EXPAND "member" -1) (("1" (EXPAND "guar_or_hidds_for") (("1" (SKOSIMP*) (("1" (REPLACE -2 :HIDE? -2) (("1" (EXPAND "member" 1) (("1" (EXPAND "union") (("1" (EXPAND "member") (("1" (INST?) (("1" (GROUND) (("1" (EXPAND "prop_for") (("1" (EXPAND "steps_okay") (("1" (FLATTEN) (("1" (INST?) (("1" (EXPAND "member") (("1" (EXPAND "steps") (("1" (USE "component_rely_hidd") (("1" (EXPAND "rely_hidd_restriction") (("1" (EXPAND "subset?") (("1" (EXPAND "member") (("1" (INST?) (("1" (GROUND) NIL))))))))))))))))))))))))))))))))))))))))))))))) ("2" (INST?) (("2" (GROUND) (("2" (EXPAND "member" 1) (("2" (EXPAND "gen_union") (("2" (INSTANTIATE 1 "guar(cmp!1)") (("2" (GROUND) (("1" (EXPAND "member") (("1" (EXPAND "guars_for") (("1" (INST?) (("1" (EXPAND "member") (("1" (PROPAX) NIL))))))))) ("2" (EXPAND "member") (("2" (EXPAND "prop_for") (("2" (EXPAND "steps_okay") (("2" (FLATTEN) (("2" (EXPAND "member") (("2" (EXPAND "steps") (("2" (INST?) (("2" (GROUND) NIL))))))))))))))))))))))))))))))))))))))) ("2" (EXPAND "member") (("2" (EXPAND "steps") (("2" (GROUND) NIL))))))))) (|cr_steps| "" (SKOSIMP*) (("" (EXPAND "steps_okay") (("" (SKOSIMP*) (("" (REWRITE "cr_guar") (("" (REWRITE "cr_rely") (("" (SKOSIMP*) (("" (INST?) (("" (INST?) (("" (GROUND) NIL))))))))))))))))) (|cr_wfar| "" (SKOSIMP*) (("" (EXPAND "is_wfar") (("" (SKOSIMP*) (("" (EXPAND "member" -2) (("" (EXPAND "compose") (("" (EXPAND "compose_wfar") (("" (EXPAND "gen_union") (("" (SKOSIMP*) (("" (EXPAND "member" -2) (("" (EXPAND "wfars_for") (("" (SKOSIMP*) (("" (INST?) (("" (REPLACE -3 :HIDE? -3) (("" (GROUND) (("" (EXPAND "member" -1) (("" (EXPAND "prop_for") (("" (EXPAND "is_wfar") (("" (FLATTEN) (("" (INST?) (("" (GROUND) (("" (INST?) NIL))))))))))))))))))))))))))))))))))))))))) (|cr_sfar| "" (SKOSIMP*) (("" (EXPAND "is_sfar") (("" (SKOSIMP*) (("" (EXPAND "member" -2) (("" (EXPAND "compose") (("" (EXPAND "compose_sfar") (("" (EXPAND "gen_union") (("" (SKOSIMP*) (("" (EXPAND "member" -2) (("" (EXPAND "sfars_for") (("" (SKOSIMP*) (("" (INST?) (("" (REPLACE -3 :HIDE? -3) (("" (GROUND) (("" (EXPAND "member" -1) (("" (EXPAND "prop_for") (("" (EXPAND "is_sfar") (("" (FLATTEN) (("" (INST?) (("" (GROUND) (("" (INST?) NIL))))))))))))))))))))))))))))))))))))))))) (|cr_aux| "" (SKOSIMP*) (("" (EXPAND "member" +) (("" (EXPAND "prop_for" +) (("" (REWRITE "cr_init") (("" (REWRITE "cr_steps") (("" (REWRITE "cr_wfar") (("" (REWRITE "cr_sfar") (("" (GROUND) NIL))))))))))))))) (|compose_right| "" (SKOSIMP*) (("" (GROUND) (("1" (REWRITE "cr_aux") NIL) ("2" (SKOSIMP*) (("2" (LEMMA "cmp_thm") (("2" (INSTANTIATE -1 ("singleton(cmp!1)" "cset!1" "prop_for(cmp!1)")) (("2" (CASE "compose(singleton(cmp!1)) = cmp!1") (("1" (REPLACE -1 :HIDE? -1) (("1" (INST?) (("1" (TYPEPRED "cset!1") (("1" (GROUND) (("1" (EXPAND "satisfies") (("1" (INST?) (("1" (EXPAND "member") (("1" (GROUND) NIL))))))) ("2" (EXPAND "subset?") (("2" (SKOSIMP*) (("2" (EXPAND "member") (("2" (EXPAND "singleton") (("2" (GROUND) NIL))))))))) ("3" (LEMMA "nonempty_th[(comp_t)]") (("3" (INSTANTIATE -1 "singleton(cmp!1)") (("3" (GROUND) (("3" (INST?) (("3" (EXPAND "member") (("3" (EXPAND "singleton") (("3" (PROPAX) NIL))))))))))))) ("4" (EXPAND "satisfies") (("4" (SKOSIMP*) NIL))))))))))) ("2" (REWRITE "ci_component") NIL) ("3" (REWRITE "ci_composable") NIL)))))))))))))) $$$compose_associative.pvs compose_associative[ST: NONEMPTY_TYPE, AG: NONEMPTY_TYPE]: THEORY BEGIN IMPORTING compose[ST, AG] cset: VAR (composable) csets: VAR setof[(composable)] cmp: VAR (comp_t) ca_composable: THEOREM composable(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets))) IFF composable({cmp | (EXISTS cset: member(cset, csets) AND cmp = compose(cset))}) ca_init: THEOREM composable(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets))) IMPLIES init(compose(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets)))) = init(compose({cmp | (EXISTS cset: member(cset, csets) AND cmp = compose(cset))})) ca_cags: THEOREM composable(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets))) IMPLIES cags(compose(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets)))) = cags(compose({cmp | (EXISTS cset: member(cset, csets) AND cmp = compose(cset))})) tran: VAR [ST, ST, AG] ca_guar1: THEOREM composable(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets))) AND guar(compose(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets)))) (tran) IMPLIES gen_union(guars_for({cmp | (EXISTS cset: member(cset, csets) AND cmp = compose(cset))}))(tran) ca_guar2: THEOREM composable(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets))) AND guar(compose(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets)))) (tran) IMPLIES gen_intersection(guar_or_hidds_for({cmp | (EXISTS cset: member(cset, csets) AND cmp = compose(cset))})) (tran) ca_guar3: THEOREM composable(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets))) AND guar(compose(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets)))) (tran) IMPLIES guar(compose({cmp | (EXISTS cset: member(cset, csets) AND cmp = compose(cset))}))(tran) ca_guar4: THEOREM composable(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets))) AND guar(compose({cmp | (EXISTS cset: member(cset, csets) AND cmp = compose(cset))}))(tran) IMPLIES gen_union(guars_for(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets)))) (tran) ca_guar5: THEOREM composable(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets))) AND guar(compose({cmp | (EXISTS cset: member(cset, csets) AND cmp = compose(cset))}))(tran) IMPLIES gen_intersection (guar_or_hidds_for(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets)))) (tran) ca_guar6: THEOREM composable(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets))) AND guar(compose({cmp | (EXISTS cset: member(cset, csets) AND cmp = compose(cset))}))(tran) IMPLIES guar(compose(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets)))) (tran) ca_guar: THEOREM composable(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets))) IMPLIES guar(compose(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets)))) = guar(compose({cmp | (EXISTS cset: member(cset, csets) AND cmp = compose(cset))})) ca_rely: THEOREM composable(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets))) IMPLIES rely(compose(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets)))) = rely(compose({cmp | (EXISTS cset: member(cset, csets) AND cmp = compose(cset))})) ca_hidd: THEOREM composable(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets))) IMPLIES hidd(compose(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets)))) = hidd(compose({cmp | (EXISTS cset: member(cset, csets) AND cmp = compose(cset))})) ca_view: THEOREM composable(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets))) IMPLIES view(compose(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets)))) = view(compose({cmp | (EXISTS cset: member(cset, csets) AND cmp = compose(cset))})) ca_sfar: THEOREM composable(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets))) IMPLIES sfar(compose(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets)))) = sfar(compose({cmp | (EXISTS cset: member(cset, csets) AND cmp = compose(cset))})) ca_wfar: THEOREM composable(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets))) IMPLIES wfar(compose(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets)))) = wfar(compose({cmp | (EXISTS cset: member(cset, csets) AND cmp = compose(cset))})) ca_component: THEOREM composable(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets))) IMPLIES compose(gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets))) = compose({cmp | (EXISTS cset: member(cset, csets) AND cmp = compose(cset))}) END compose_associative $$$compose_associative.prf (|compose_associative| (|ca_composable| "" (SKOLEM!) (("" (CASE "not (csets!1 /= emptyset)") (("1" (FLATTEN) (("1" (REPLACE -1) (("1" (EXPAND "composable") (("1" (EXPAND "gen_union") (("1" (EXPAND "member") (("1" (EXPAND "extend") (("1" (EXPAND "emptyset") (("1" (PROPAX) NIL))))))))))))))) ("2" (REWRITE "nonempty_th") (("2" (SKOLEM!) (("2" (CASE "not (x!1 /= emptyset)") (("1" (DELETE -1 2) (("1" (TYPEPRED "x!1") (("1" (EXPAND "composable") (("1" (GROUND) NIL))))))) ("2" (REWRITE "nonempty_th") (("2" (SKOLEM!) (("2" (CASE "not (gen_union(extend[setof[((comp_t[ST, AG]))], ((composable)), bool, FALSE](csets!1)) /= emptyset)") (("1" (DELETE 2) (("1" (REWRITE "nonempty_th") (("1" (INST?) (("1" (EXPAND "member" +) (("1" (EXPAND "gen_union") (("1" (INST?) (("1" (GROUND) (("1" (EXPAND "extend") (("1" (EXPAND "member") (("1" (PROPAX) NIL))))))))))))))))))) ("2" (CASE "not ({cmp: (comp_t) | (EXISTS (cset: (composable)): member(cset, csets!1) AND cmp = compose(cset))} /= emptyset)") (("1" (DELETE -1 2) (("1" (REWRITE "nonempty_th") (("1" (INSTANTIATE 1 "compose(x!1)") (("1" (EXPAND "member") (("1" (INST?) (("1" (GROUND) NIL))))))))))) ("2" (EXPAND "composable") (("2" (GROUND) (("1" (DELETE -2 -3 2 3 4) (("1" (EXPAND "agreeable_start") (("1" (SKOSIMP*) (("1" (INST?) (("1" (SKOSIMP*) (("1" (EXPAND "member") (("1" (SKOSIMP*) (("1" (REPLACE -2 :HIDE? -2) (("1" (EXPAND "compose") (("1" (EXPAND "compose_init") (("1" (EXPAND "gen_intersection") (("1" (SKOSIMP*) (("1" (EXPAND "member") (("1" (EXPAND "inits_for") (("1" (SKOSIMP*) (("1" (REPLACE -3 :HIDE? -3) (("1" (INST?) (("1" (EXPAND "gen_union") (("1" (GROUND) (("1" (INST?) (("1" (EXPAND "member") (("1" (EXPAND "extend") (("1" (PROPAX) NIL))))))))))))))))))))))))))))))))))))))))))))) ("2" (DELETE -2 -3 2 3 4) (("2" (EXPAND "agreeable_start") (("2" (SKOSIMP*) (("2" (INST?) (("2" (SKOSIMP*) (("2" (EXPAND "member") (("2" (EXPAND "gen_union") (("2" (SKOSIMP*) (("2" (EXPAND "member") (("2" (EXPAND "extend") (("2" (GROUND) (("2" (INSTANTIATE -4 "compose(s!1)") (("2" (GROUND) (("1" (EXPAND "compose") (("1" (EXPAND "compose_init") (("1" (EXPAND "gen_intersection") (("1" (INST?) (("1" (EXPAND "member") (("1" (EXPAND "inits_for") (("1" (INST?) (("1" (EXPAND "member") (("1" (PROPAX) NIL))))))))))))))))) ("2" (INST?) (("2" (GROUND) NIL))))))))))))))))))))))))))))))))))))))))))))))))))) (|ca_init_TCC1| "" (SKOSIMP*) (("" (REWRITE "ca_composable") NIL))) (|ca_init| "" (SKOSIMP*) (("" (EXTENSIONALITY "setof[ST]") (("" (INST?) (("1" (GROUND) (("1" (DELETE 2) (("1" (SKOLEM!) (("1" (IFF) (("1" (EXPAND "compose" 1 1) (("1" (EXPAND "compose" 1 1) (("1" (EXPAND "compose_init") (("1" (EXPAND "gen_intersection") (("1" (EXPAND "member") (("1" (EXPAND "inits_for") (("1" (EXPAND "member") (("1" (EXPAND "gen_union") (("1" (EXPAND "member") (("1" (EXPAND "extend") (("1" (GROUND) (("1" (SKOSIMP*) (("1" (REPLACE -4 :HIDE? -4) (("1" (REPLACE -3 :HIDE? -3) (("1" (EXPAND "compose" +) (("1" (EXPAND "compose_init") (("1" (EXPAND "gen_intersection") (("1" (SKOSIMP*) (("1" (EXPAND "member") (("1" (EXPAND "inits_for") (("1" (SKOSIMP*) (("1" (EXPAND "member") (("1" (REPLACE -4 :HIDE? -4) (("1" (INST?) (("1" (GROUND) (("1" (INST?) (("1" (GROUND) (("1" (INSTANTIATE 1 "cset!1") (("1" (GROUND) NIL))))))))))))))))))))))))))))))))))) ("2" (SKOSIMP*) (("2" (GROUND) (("2" (REPLACE -5 :HIDE? -5) (("2" (INSTANTIATE -3 "init(compose(s!2))") (("2" (GROUND) (("1" (EXPAND "compose") (("1" (EXPAND "compose_init") (("1" (EXPAND "gen_intersection") (("1" (INST?) (("1" (EXPAND "member") (("1" (GROUND) (("1" (EXPAND "inits_for") (("1" (INST?) (("1" (EXPAND "member") (("1" (PROPAX) NIL))))))))))))))))))) ("2" (INSTANTIATE 1 "compose(s!2)") (("2" (GROUND) (("2" (INST?) (("2" (GROUND) NIL))))))))))))))))))))))))))))))))))))))))))))))) ("2" (REWRITE "ca_composable") NIL))))))) (|ca_cags| "" (SKOSIMP*) (("" (EXTENSIONALITY "setof[AG]") (("" (INST?) (("1" (GROUND) (("1" (DELETE 2) (("1" (SKOLEM!) (("1" (IFF) (("1" (EXPAND "compose" 1 1) (("1" (EXPAND "compose" 1 1) (("1" (EXPAND "compose_cags") (("1" (EXPAND "gen_union" +) (("1" (EXPAND "cagss_for") (("1" (EXPAND "member") (("1" (EXPAND "extend" +) (("1" (GROUND) (("1" (SKOSIMP*) (("1" (GROUND) (("1" (REPLACE -4 :HIDE? -4) (("1" (INSTANTIATE 1 "cags(compose(s!2))") (("1" (GROUND) (("1" (INSTANTIATE 1 "compose(s!2)") (("1" (GROUND) (("1" (INSTANTIATE 1 "s!2") (("1" (GROUND) NIL))))))) ("2" (EXPAND "compose") (("2" (EXPAND "compose_cags") (("2" (EXPAND "gen_union") (("2" (INST?) (("2" (EXPAND "member") (("2" (EXPAND "cagss_for") (("2" (INST?) (("2" (EXPAND "member") (("2" (PROPAX) NIL))))))))))))))))))))))))))) ("2" (SKOSIMP*) (("2" (REPLACE -2 :HIDE? -2) (("2" (REPLACE -2 :HIDE? -2) (("2" (EXPAND "compose") (("2" (EXPAND "compose_cags") (("2" (EXPAND "gen_union") (("2" (SKOSIMP*) (("2" (EXPAND "member") (("2" (EXPAND "cagss_for") (("2" (SKOSIMP*) (("2" (EXPAND "member") (("2" (REPLACE -3 :HIDE? -3) (("2" (INST?) (("2" (GROUND) (("2" (INST?) (("2" (GROUND) (("2" (INSTANTIATE 1 "cset!1") (("2" (GROUND) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (REWRITE "ca_composable") NIL))))))) (|ca_guar1| "" (SKOSIMP*) (("" (EXPAND "compose" -) (("" (EXPAND "compose_guar") (("" (EXPAND "intersection") (("" (EXPAND "member") (("" (EXPAND "gen_intersection") (("" (FLATTEN) (("" (EXPAND "gen_union" -3 1) (("" (EXPAND "gen_union" +) (("" (EXPAND "member") (("" (SKOSIMP*) (("" (EXPAND "guars_for") (("" (EXPAND "guar_or_hidds_for") (("" (EXPAND "member") (("" (EXPAND "gen_union" -2) (("" (EXPAND "gen_union" -3) (("" (EXPAND "member") (("" (EXPAND "extend" -2) (("" (EXPAND "extend" -3) (("" (SKOSIMP*) (("" (REPLACE -5 :HIDE? -5) (("" (GROUND) (("" (INSTANTIATE 1 "guar(compose(s!2))") (("" (GROUND) (("1" (INSTANTIATE 1 "compose(s!2)") (("1" (GROUND) (("1" (INST?) (("1" (GROUND) NIL))))))) ("2" (EXPAND "compose") (("2" (EXPAND "compose_guar") (("2" (EXPAND "intersection") (("2" (EXPAND "member") (("2" (SPLIT) (("1" (EXPAND "gen_intersection") (("1" (SKOSIMP*) (("1" (EXPAND "member") (("1" (EXPAND "guar_or_hidds_for") (("1" (SKOSIMP*) (("1" (EXPAND "member") (("1" (INSTANTIATE -6 "s!3") (("1" (GROUND) (("1" (INSTANTIATE 1 "cmp!2") (("1" (GROUND) (("1" (INSTANTIATE 1 "s!2") (("1" (GROUND) NIL))))))))))))))))))))))) ("2" (EXPAND "gen_union" +) (("2" (INSTANTIATE 1 "guar(cmp!1)") (("2" (EXPAND "member") (("2" (EXPAND "guars_for") (("2" (EXPAND "member") (("2" (INSTANTIATE 1 "cmp!1") (("2" (GROUND) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (|ca_guar2| "" (SKOSIMP*) (("" (EXPAND "compose" -2) (("" (EXPAND "compose_guar") (("" (EXPAND "intersection") (("" (EXPAND "member") (("" (FLATTEN) (("" (DELETE -3) (("" (EXPAND "gen_intersection") (("" (EXPAND "member") (("" (SKOSIMP*) (("" (EXPAND "guar_or_hidds_for") (("" (SKOSIMP*) (("" (REPLACE -4 :HIDE? -4) (("" (EXPAND "member") (("" (SKOSIMP*) (("" (REPLACE -4 :HIDE? -4) (("" (EXPAND "union" +) (("" (EXPAND "member") (("" (EXPAND "compose") (("" (EXPAND "compose_guar") (("" (EXPAND "compose_hidd") (("" (FLATTEN) (("" (CASE "not (exists cmp: cset!1(cmp) and guar(cmp)(tran!1))") (("1" (EXPAND "gen_intersection") (("1" (SKOSIMP*) (("1" (EXPAND "member") (("1" (EXPAND "hidds_for") (("1" (SKOSIMP*) (("1" (EXPAND "member") (("1" (REPLACE -5 :HIDE? -5) (("1" (INSTANTIATE -2 "union(guar(cmp!2),hidd(cmp!2))") (("1" (EXPAND "union") (("1" (EXPAND "member") (("1" (GROUND) (("1" (INST?) (("1" (GROUND) NIL))) ("2" (INST?) (("2" (EXPAND "gen_union" +) (("2" (EXPAND "member") (("2" (EXPAND "extend") (("2" (INSTANTIATE 1 "cset!1") (("2" (GROUND) NIL))))))))))))))))))))))))))))))))) ("2" (DELETE 2) (("2" (SKOSIMP*) (("2" (EXPAND "intersection") (("2" (EXPAND "member") (("2" (SPLIT) (("1" (EXPAND "gen_intersection") (("1" (SKOSIMP*) (("1" (EXPAND "member") (("1" (EXPAND "guar_or_hidds_for") (("1" (SKOSIMP*) (("1" (EXPAND "member") (("1" (REPLACE -2 :HIDE? -2) (("1" (INSTANTIATE -5 "union(guar(cmp!3),hidd(cmp!3))") (("1" (GROUND) (("1" (INSTANTIATE 1 "cmp!3") (("1" (GROUND) (("1" (EXPAND "gen_union" +) (("1" (INSTANTIATE 1 "cset!1") (("1" (EXPAND "member") (("1" (EXPAND "extend") (("1" (PROPAX) NIL))))))))))))))))))))))))))))))) ("2" (EXPAND "gen_union") (("2" (INSTANTIATE 1 "guar(cmp!2)") (("2" (EXPAND "member") (("2" (EXPAND "guars_for") (("2" (GROUND) (("2" (INSTANTIATE 1 "cmp!2") (("2" (EXPAND "member") (("2" (PROPAX) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (|ca_guar3_TCC1| "" (SKOSIMP*) (("" (REWRITE "ca_composable") NIL))) (|ca_guar3| "" (SKOSIMP*) (("" (EXPAND "compose" 1 1) (("" (EXPAND "compose_guar") (("" (EXPAND "intersection") (("" (EXPAND "member") (("" (LEMMA "ca_guar1") (("" (INST?) (("" (GROUND) (("1" (LEMMA "ca_guar2") (("1" (INST?) (("1" (GROUND) (("1" (EXPAND "member") (("1" (PROPAX) NIL))))))))) ("2" (EXPAND "member") (("2" (PROPAX) NIL))))))))))))))))))) (|ca_guar4| "" (SKOSIMP*) (("" (EXPAND "gen_union" +) (("" (EXPAND "member") (("" (EXPAND "guars_for") (("" (EXPAND "member") (("" (EXPAND "extend" +) (("" (EXPAND "compose" -2 1) (("" (EXPAND "compose_guar") (("" (EXPAND "intersection") (("" (EXPAND "member") (("" (FLATTEN) (("" (DELETE -2) (("" (EXPAND "gen_union" -2) (("" (SKOSIMP*) (("" (EXPAND "member") (("" (EXPAND "guars_for") (("" (SKOSIMP*) (("" (EXPAND "member") (("" (SKOSIMP*) (("" (REPLACE -3 :HIDE? -3) (("" (REPLACE -3 :HIDE? -3) (("" (EXPAND "compose") (("" (EXPAND "compose_guar") (("" (EXPAND "intersection") (("" (EXPAND "member") (("" (FLATTEN) (("" (DELETE -3) (("" (EXPAND "gen_union") (("" (SKOSIMP*) (("" (EXPAND "member") (("" (EXPAND "guars_for") (("" (SKOSIMP*) (("" (EXPAND "member") (("" (REPLACE -4 :HIDE? -4) (("" (INST?) (("" (GROUND) (("" (INST?) (("" (GROUND) (("" (INSTANTIATE 1 "cset!1") (("" (GROUND) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (|ca_guar5| "" (SKOSIMP*) (("" (EXPAND "gen_intersection") (("" (SKOSIMP*) (("" (EXPAND "member") (("" (EXPAND "guar_or_hidds_for") (("" (SKOSIMP*) (("" (EXPAND "member") (("" (EXPAND "gen_union" -3) (("" (REPLACE -4 :HIDE? -4) (("" (SKOSIMP*) (("" (EXPAND "member") (("" (EXPAND "extend" -3) (("" (GROUND) (("" (EXPAND "compose" -4 1) (("" (EXPAND "compose_guar") (("" (EXPAND "intersection") (("" (EXPAND "member") (("" (EXPAND "gen_intersection") (("" (EXPAND "member") (("" (EXPAND "guar_or_hidds_for") (("" (EXPAND "member") (("" (FLATTEN) (("" (INSTANTIATE -4 "union(guar(compose(s!2)),hidd(compose(s!2)))") (("" (GROUND) (("1" (EXPAND "union") (("1" (EXPAND "member") (("1" (EXPAND "compose" -1) (("1" (EXPAND "compose_guar") (("1" (FLATTEN) (("1" (SPLIT) (("1" (EXPAND "intersection") (("1" (EXPAND "member") (("1" (EXPAND "gen_intersection") (("1" (EXPAND "member") (("1" (EXPAND "guar_or_hidds_for") (("1" (EXPAND "member") (("1" (EXPAND "union") (("1" (EXPAND "member") (("1" (FLATTEN) (("1" (INSTANTIATE -1 "{x: transition[ST,AG] | (guar(cmp!1)(x) or hidd(cmp!1)(x))}") (("1" (GROUND) (("1" (INST?) (("1" (GROUND) NIL))))))))))))))))))))))))) ("2" (EXPAND "compose_hidd") (("2" (EXPAND "gen_intersection") (("2" (INSTANTIATE -1 "hidd(cmp!1)") (("2" (EXPAND "member") (("2" (GROUND) (("2" (EXPAND "hidds_for") (("2" (EXPAND "member") (("2" (INST?) (("2" (GROUND) NIL))))))))))))))))))))))))))))) ("2" (INSTANTIATE 1 "compose(s!2)") (("2" (GROUND) (("2" (INSTANTIATE 1 "s!2") (("2" (GROUND) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))) (|ca_guar6_TCC1| "" (SKOSIMP*) NIL) (|ca_guar6| "" (SKOSIMP*) (("" (LEMMA "ca_guar4") (("" (INST?) (("" (EXPAND "member") (("" (GROUND) (("" (LEMMA "ca_guar5") (("" (INST?) (("" (EXPAND "member") (("" (INST?) (("" (GROUND) (("" (EXPAND "compose" +) (("" (EXPAND "compose_guar") (("" (EXPAND "intersection") (("" (EXPAND "member") (("" (PROPAX) NIL))))))))))))))))))))))))))))) (|ca_guar| "" (SKOSIMP*) (("" (EXTENSIONALITY "setof[transition]") (("" (INST?) (("1" (GROUND) (("1" (DELETE 2) (("1" (SKOLEM!) (("1" (IFF) (("1" (GROUND) (("1" (REWRITE "ca_guar3") NIL) ("2" (REWRITE "ca_guar6") NIL))))))))))) ("2" (REWRITE "ca_composable") NIL))))))) (|ca_rely| "" (SKOSIMP*) (("" (EXTENSIONALITY "setof[[ST,ST,AG]]") (("" (INST?) (("1" (GROUND) (("1" (DELETE 2) (("1" (SKOLEM!) (("1" (IFF) (("1" (EXPAND "compose" 1 1) (("1" (EXPAND "compose" 1 1) (("1" (EXPAND "compose_rely") (("1" (EXPAND "gen_intersection") (("1" (EXPAND "member") (("1" (EXPAND "relys_for") (("1" (EXPAND "member") (("1" (EXPAND "gen_union") (("1" (EXPAND "member") (("1" (EXPAND "extend") (("1" (GROUND) (("1" (SKOSIMP*) (("1" (REPLACE -4 :HIDE? -4) (("1" (REPLACE -3 :HIDE? -3) (("1" (EXPAND "compose" +) (("1" (EXPAND "compose_rely") (("1" (EXPAND "gen_intersection") (("1" (SKOSIMP*) (("1" (EXPAND "member") (("1" (EXPAND "relys_for") (("1" (SKOSIMP*) (("1" (EXPAND "member") (("1" (REPLACE -4 :HIDE? -4) (("1" (INST?) (("1" (GROUND) (("1" (INST?) (("1" (GROUND) (("1" (INSTANTIATE 1 "cset!1") (("1" (GROUND) NIL))))))))))))))))))))))))))))))))))) ("2" (SKOSIMP*) (("2" (GROUND) (("2" (REPLACE -5 :HIDE? -5) (("2" (INSTANTIATE -3 "rely(compose(s!2))") (("2" (GROUND) (("1" (EXPAND "compose") (("1" (EXPAND "compose_rely") (("1" (EXPAND "gen_intersection") (("1" (INST?) (("1" (EXPAND "member") (("1" (GROUND) (("1" (EXPAND "relys_for") (("1" (INST?) (("1" (EXPAND "member") (("1" (PROPAX) NIL))))))))))))))))))) ("2" (INSTANTIATE 1 "compose(s!2)") (("2" (GROUND) (("2" (INST?) (("2" (GROUND) NIL))))))))))))))))))))))))))))))))))))))))))))))) ("2" (REWRITE "ca_composable") NIL))))))) (|ca_hidd| "" (SKOSIMP*) (("" (EXTENSIONALITY "setof[[ST,ST,AG]]") (("" (INST?) (("1" (GROUND) (("1" (DELETE 2) (("1" (SKOLEM!) (("1" (IFF) (("1" (EXPAND "compose" 1 1) (("1" (EXPAND "compose" 1 1) (("1" (EXPAND "compose_hidd") (("1" (EXPAND "gen_intersection") (("1" (EXPAND "member") (("1" (EXPAND "hidds_for") (("1" (EXPAND "member") (("1" (EXPAND "gen_union") (("1" (EXPAND "member") (("1" (EXPAND "extend") (("1" (GROUND) (("1" (SKOSIMP*) (("1" (REPLACE -4 :HIDE? -4) (("1" (REPLACE -3 :HIDE? -3) (("1" (EXPAND "compose" +) (("1" (EXPAND "compose_hidd") (("1" (EXPAND "gen_intersection") (("1" (SKOSIMP*) (("1" (EXPAND "member") (("1" (EXPAND "hidds_for") (("1" (SKOSIMP*) (("1" (EXPAND "member") (("1" (REPLACE -4 :HIDE? -4) (("1" (INST?) (("1" (GROUND) (("1" (INST?) (("1" (GROUND) (("1" (INSTANTIATE 1 "cset!1") (("1" (GROUND) NIL))))))))))))))))))))))))))))))))))) ("2" (SKOSIMP*) (("2" (GROUND) (("2" (REPLACE -5 :HIDE? -5) (("2" (INSTANTIATE -3 "hidd(compose(s!2))") (("2" (GROUND) (("1" (EXPAND "compose") (("1" (EXPAND "compose_hidd") (("1" (EXPAND "gen_intersection") (("1" (INST?) (("1" (EXPAND "member") (("1" (GROUND) (("1" (EXPAND "hidds_for") (("1" (INST?) (("1" (EXPAND "member") (("1" (PROPAX) NIL))))))))))))))))))) ("2" (INSTANTIATE 1 "compose(s!2)") (("2" (GROUND) (("2" (INST?) (("2" (GROUND) NIL))))))))))))))))))))))))))))))))))))))))))))))) ("2" (REWRITE "ca_composable") NIL))))))) (|ca_view| "" (SKOSIMP*) (("" (EXTENSIONALITY "setof[[ST,ST]] ") (("" (INST?) (("1" (GROUND) (("1" (DELETE 2) (("1" (SKOLEM!) (("1" (IFF) (("1" (EXPAND "compose" 1 1) (("1" (EXPAND "compose" 1 1) (("1" (EXPAND "compose_view") (("1" (EXPAND "gen_intersection") (("1" (EXPAND "member") (("1" (EXPAND "extend" +) (("1" (EXPAND "views_for") (("1" (EXPAND "member") (("1" (EXPAND "gen_union" +) (("1" (EXPAND "member") (("1" (GROUND) (("1" (SKOSIMP*) (("1" (GROUND) (("1" (SKOSIMP*) (("1" (REPLACE -4 :HIDE? -4) (("1" (REPLACE -3 :HIDE? -3) (("1" (EXPAND "compose" +) (("1" (EXPAND "compose_view") (("1" (EXPAND "gen_intersection") (("1" (SKOSIMP*) (("1" (EXPAND "member") (("1" (EXPAND "extend" -4) (("1" (GROUND) (("1" (EXPAND "views_for") (("1" (SKOSIMP*) (("1" (EXPAND "member") (("1" (REPLACE -3 :HIDE? -3) (("1" (INST?) (("1" (GROUND) (("1" (INST?) (("1" (GROUND) (("1" (INSTANTIATE 1 "cset!1") (("1" (GROUND) NIL))))))))))))))))))))))))))))))))))))))))))) ("2" (SKOSIMP*) (("2" (GROUND) (("2" (SKOSIMP*) (("2" (REPLACE -4 :HIDE? -4) (("2" (INSTANTIATE -4 "view(compose(s!2))") (("1" (GROUND) (("1" (EXPAND "compose") (("1" (EXPAND "compose_view") (("1" (EXPAND "gen_intersection") (("1" (INST?) (("1" (EXPAND "member") (("1" (EXPAND "extend") (("1" (EXPAND "views_for") (("1" (INST?) (("1" (EXPAND "member") (("1" (PROPAX) NIL))))))))))))))))))) ("2" (INSTANTIATE 1 "compose(s!2)") (("2" (GROUND) (("2" (INSTANTIATE 1 "s!2") (("2" (GROUND) NIL))))))))) ("2" (GROUND) NIL))))))))))))))))))))))))))))))))))))))))) ("2" (REWRITE "ca_composable") NIL))))))) (|ca_sfar| "" (SKOSIMP*) (("" (EXTENSIONALITY "setof[TRANSITION_CLASS]") (("" (INST?) (("1" (GROUND) (("1" (DELETE 2) (("1" (SKOLEM!) (("1" (IFF) (("1" (EXPAND "compose" 1 1) (("1" (EXPAND "compose" 1 1) (("1" (EXPAND "compose_sfar") (("1" (EXPAND "gen_union" +) (("1" (EXPAND "sfars_for") (("1" (EXPAND "member") (("1" (EXPAND "extend" +) (("1" (GROUND) (("1" (SKOSIMP*) (("1" (GROUND) (("1" (REPLACE -4 :HIDE? -4) (("1" (INSTANTIATE 1 "sfar(compose(s!2))") (("1" (GROUND) (("1" (INSTANTIATE 1 "compose(s!2)") (("1" (GROUND) (("1" (INSTANTIATE 1 "s!2") (("1" (GROUND) NIL))))))) ("2" (EXPAND "compose") (("2" (EXPAND "compose_sfar") (("2" (EXPAND "gen_union") (("2" (INST?) (("2" (EXPAND "member") (("2" (EXPAND "sfars_for") (("2" (INST?) (("2" (EXPAND "member") (("2" (PROPAX) NIL))))))))))))))))))))))))))) ("2" (SKOSIMP*) (("2" (REPLACE -2 :HIDE? -2) (("2" (REPLACE -2 :HIDE? -2) (("2" (EXPAND "compose") (("2" (EXPAND "compose_sfar") (("2" (EXPAND "gen_union") (("2" (SKOSIMP*) (("2" (EXPAND "member") (("2" (EXPAND "sfars_for") (("2" (SKOSIMP*) (("2" (EXPAND "member") (("2" (REPLACE -3 :HIDE? -3) (("2" (INST?) (("2" (GROUND) (("2" (INST?) (("2" (GROUND) (("2" (INSTANTIATE 1 "cset!1") (("2" (GROUND) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (REWRITE "ca_composable") NIL))))))) (|ca_wfar| "" (SKOSIMP*) (("" (EXTENSIONALITY "setof[TRANSITION_CLASS]") (("" (INST?) (("1" (GROUND) (("1" (DELETE 2) (("1" (SKOLEM!) (("1" (IFF) (("1" (EXPAND "compose" 1 1) (("1" (EXPAND "compose" 1 1) (("1" (EXPAND "compose_wfar") (("1" (EXPAND "gen_union" +) (("1" (EXPAND "wfars_for") (("1" (EXPAND "member") (("1" (EXPAND "extend" +) (("1" (GROUND) (("1" (SKOSIMP*) (("1" (GROUND) (("1" (REPLACE -4 :HIDE? -4) (("1" (INSTANTIATE 1 "wfar(compose(s!2))") (("1" (GROUND) (("1" (INSTANTIATE 1 "compose(s!2)") (("1" (GROUND) (("1" (INSTANTIATE 1 "s!2") (("1" (GROUND) NIL))))))) ("2" (EXPAND "compose") (("2" (EXPAND "compose_wfar") (("2" (EXPAND "gen_union") (("2" (INST?) (("2" (EXPAND "member") (("2" (EXPAND "wfars_for") (("2" (INST?) (("2" (EXPAND "member") (("2" (PROPAX) NIL))))))))))))))))))))))))))) ("2" (SKOSIMP*) (("2" (REPLACE -2 :HIDE? -2) (("2" (REPLACE -2 :HIDE? -2) (("2" (EXPAND "compose") (("2" (EXPAND "compose_wfar") (("2" (EXPAND "gen_union") (("2" (SKOSIMP*) (("2" (EXPAND "member") (("2" (EXPAND "wfars_for") (("2" (SKOSIMP*) (("2" (EXPAND "member") (("2" (REPLACE -3 :HIDE? -3) (("2" (INST?) (("2" (GROUND) (("2" (INST?) (("2" (GROUND) (("2" (INSTANTIATE 1 "cset!1") (("2" (GROUND) NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (REWRITE "ca_composable") NIL))))))) (|ca_component| "" (SKOSIMP*) (("" (EXTENSIONALITY "(comp_t)") (("" (INST?) (("1" (GROUND) (("1" (REWRITE "ca_cags") NIL) ("2" (REWRITE "ca_guar") NIL) ("3" (REWRITE "ca_hidd") NIL) ("4" (REWRITE "ca_init") NIL) ("5" (REWRITE "ca_rely") NIL) ("6" (REWRITE "ca_sfar") NIL) ("7" (REWRITE "ca_view") NIL) ("8" (REWRITE "ca_wfar") NIL))) ("2" (REWRITE "ca_composable") NIL)))))))) $$$compose2.pvs compose2[ST: NONEMPTY_TYPE, ST1: NONEMPTY_TYPE, ST2: NONEMPTY_TYPE, AG: NONEMPTY_TYPE, AG1: NONEMPTY_TYPE, AG2: NONEMPTY_TYPE]: THEORY BEGIN IMPORTING cmp_translators[ST1,AG1,ST,AG] IMPORTING cmp_translators[ST2,AG2,ST,AG] IMPORTING compose[ST,AG] cset: VAR setof[(comp_t[ST,AG])] cmp, cmpa, cmpb: VAR (comp_t[ST,AG]) cmp1 : VAR (comp_t[ST1,AG1]) cmp2 : VAR (comp_t[ST2,AG2]) sttran1 : VAR (translator_t[ST1,ST]) agtran1 : VAR (weak_translator_t[AG1,AG]) sttran2 : VAR (translator_t[ST2,ST]) agtran2 : VAR (weak_translator_t[AG2,AG]) make_two_set(cmpa,cmpb) : setof[(comp_t[ST,AG])] = (LAMBDA cmp: cmp = cmpa or cmp = cmpb) make_two_set_tr(cmp1,cmp2,sttran1,sttran2,agtran1,agtran2) : setof[(comp_t[ST,AG])] = make_two_set(tran_cmp(cmp1,sttran1,agtran1),tran_cmp(cmp2,sttran2,agtran2)) compose_init2(cmp1, cmp2, sttran1, sttran2, agtran1, agtran2): setof[ST] = intersection(tmap(sttran1, init(cmp1)), tmap(sttran2, init(cmp2))) compose_init2_def: THEOREM compose_init(make_two_set_tr(cmp1,cmp2,sttran1,sttran2,agtran1,agtran2)) = compose_init2(cmp1,cmp2,sttran1,sttran2,agtran1,agtran2) compose_guar2(cmp1, cmp2, sttran1, sttran2, agtran1, agtran2): setof[[ST, ST, AG]] = union(intersection(tr_ac(guar(cmp1),sttran1,agtran1), union(tr_ac(hidd(cmp2),sttran2, agtran2), env_stutter(cmp2,sttran2,agtran2))), union(intersection(tr_ac(guar(cmp2),sttran2,agtran2), union(tr_ac(hidd(cmp1),sttran1,agtran1), env_stutter(cmp1,sttran1,agtran1))), intersection(tr_ac(guar(cmp1),sttran1,agtran1), tr_ac(guar(cmp2),sttran2,agtran2)))) compose_guar2_def: THEOREM compose_guar(make_two_set_tr(cmp1,cmp2,sttran1,sttran2,agtran1,agtran2)) = compose_guar2(cmp1,cmp2,sttran1,sttran2,agtran1,agtran2) compose_rely2(cmp1, cmp2, sttran1, sttran2, agtran1, agtran2): setof[[ST, ST, AG]] = intersection(union(tr_ac(rely(cmp1),sttran1,agtran1), env_stutter(cmp1,sttran1,agtran1)), union(tr_ac(rely(cmp2), sttran2, agtran2), env_stutter(cmp2,sttran2,agtran2))) compose_rely2_def: THEOREM compose_rely(make_two_set_tr(cmp1,cmp2,sttran1,sttran2,agtran1,agtran2)) = compose_rely2(cmp1,cmp2,sttran1,sttran2,agtran1,agtran2) compose_cags2(cmp1, cmp2, sttran1, sttran2, agtran1, agtran2): setof[AG] = union(tmap(agtran1, cags(cmp1)), tmap(agtran2, cags(cmp2))) compose_cags2_def: THEOREM compose_cags(make_two_set_tr(cmp1,cmp2,sttran1,sttran2,agtran1,agtran2)) = compose_cags2(cmp1,cmp2,sttran1,sttran2,agtran1,agtran2) compose_view2(cmp1, cmp2, sttran1, sttran2, agtran1, agtran2): setof[[ST, ST]] = intersection(vmap(sttran1, view(cmp1)), vmap(sttran2, view(cmp2))) compose_view2_def: THEOREM compose_view(make_two_set_tr(cmp1,cmp2,sttran1,sttran2,agtran1,agtran2)) = compose_view2(cmp1,cmp2,sttran1,sttran2,agtran1,agtran2) compose_hidd2(cmp1, cmp2, sttran1, sttran2, agtran1, agtran2): setof[[ST, ST,AG]] = intersection(union(tr_ac(hidd(cmp1),sttran1,agtran1), env_stutter(cmp1,sttran1,agtran1)), union(tr_ac(hidd(cmp2), sttran2, agtran2), env_stutter(cmp2,sttran2,agtran2))) compose_hidd2_def: THEOREM compose_hidd(make_two_set_tr(cmp1,cmp2,sttran1,sttran2,agtran1,agtran2)) = compose_hidd2(cmp1,cmp2,sttran1,sttran2,agtran1,agtran2) compose_wfar2(cmp1, cmp2,sttran1,sttran2,agtran1,agtran2): setof[TRANSITION_CLASS[ST,AG]] = union(tr_tcs(wfar(cmp1), sttran1,agtran1), tr_tcs(wfar(cmp2), sttran2,agtran2)) compose_wfar2_def: THEOREM compose_wfar(make_two_set_tr(cmp1,cmp2,sttran1,sttran2,agtran1,agtran2)) = compose_wfar2(cmp1,cmp2,sttran1,sttran2,agtran1,agtran2) compose_sfar2(cmp1, cmp2,sttran1,sttran2,agtran1,agtran2): setof[TRANSITION_CLASS[ST,AG]] = union(tr_tcs(sfar(cmp1), sttran1,agtran1), tr_tcs(sfar(cmp2), sttran2,agtran2)) compose_sfar2_def: THEOREM compose_sfar(make_two_set_tr(cmp1,cmp2,sttran1,sttran2,agtran1,agtran2)) = compose_sfar2(cmp1,cmp2,sttran1,sttran2,agtran1,agtran2) composable_init2(cmp1, cmp2, sttran1, sttran2, agtran1, agtran2): bool = compose_init2(cmp1, cmp2, sttran1, sttran2, agtran1, agtran2) /= emptyset composable_init2_def: THEOREM agreeable_start(make_two_set_tr(cmp1,cmp2,sttran1,sttran2,agtran1,agtran2)) = composable_init2(cmp1,cmp2,sttran1,sttran2,agtran1,agtran2) composable2(cmp1, cmp2, sttran1, sttran2, agtran1, agtran2): bool = composable_init2(cmp1, cmp2, sttran1, sttran2, agtran1, agtran2) composable2_def: THEOREM composable(make_two_set_tr(cmp1,cmp2,sttran1,sttran2,agtran1,agtran2)) = composable2(cmp1,cmp2,sttran1,sttran2,agtran1,agtran2) c: VAR (composable2) compose_base2(c): base_comp_t[ST, AG] = (# init := compose_init2(c), guar := compose_guar2(c), rely := compose_rely2(c), cags := compose_cags2(c), view := compose_view2(c), wfar := compose_wfar2(c), sfar := compose_sfar2(c), hidd := compose_hidd2(c) #) compose_base2_def: THEOREM compose_base2(c) = compose_base(make_two_set_tr(c)) compose2(c): (comp_t[ST, AG]) = compose_base2(c) compose2_def: THEOREM compose2(c) = compose(make_two_set_tr(c)) END compose2 $$$compose2.prf (|compose2| (|compose_init2_def| "" (SKOLEM!) (("" (EXTENSIONALITY "setof[ST]") (("" (INST?) (("" (GROUND) (("" (DELETE 2) (("" (SKOLEM!) (("" (IFF) (("" (EXPAND "compose_init") (("" (EXPAND "compose_init2") (("" (EXPAND "gen_intersection") (("" (EXPAND "member") (("" (EXPAND "inits_for") (("" (EXPAND "intersection") (("" (EXPAND "member") (("" (EXPAND "make_two_set_tr") (("" (EXPAND "make_two_set") (("" (GROUND) (("1" (INST?) (("1" (GROUND) (("1" (INST?) (("1" (GROUND) (("1" (EXPAND "tran_cmp") (("1" (EXPAND "tr_cmp") (("1" (PROPAX) NIL))))))))))))) ("2" (INST?) (("2" (GROUND) (("2" (INSTANTIATE 1 "tran_cmp(cmp2!1, sttran2!1, agtran2!1)") (("2" (GROUND) (("2" (EXPAND "tran_cmp") (("2" (EXPAND "tr_cmp") (("2" (PROPAX) NIL))))))))))))) ("3" (SKOSIMP*) (("3" (SPLIT) (("1" (REPLACE -1 :HIDE? -1) (("1" (EXPAND "tran_cmp") (("1" (EXPAND "tr_cmp") (("1" (GROUND) NIL))))))) ("2" (REPLACE -1 :HIDE? -1) (("2" (EXPAND "tran_cmp") (("2" (EXPAND "tr_cmp") (("2" (GROUND) NIL))))))))))))))))))))))))))))))))))))))))))))) (|compose_guar2_def| "" (SKOLEM!) (("" (EXTENSIONALITY "setof[[ST,ST,AG]]") (("" (INST?) (("" (GROUND) (("" (DELETE 2) (("" (SKOLEM!) (("" (IFF) (("" (GROUND) (("1" (EXPAND "compose_guar") (("1" (EXPAND "intersection") (("1" (FLATTEN) (("1" (EXPAND "member") (("1" (EXPAND "gen_union") (("1" (EXPAND "gen_intersection") (("1" (SKOSIMP*) (("1" (EXPAND "member") (("1" (EXPAND "guars_for") (("1" (EXPAND "guar_or_hidds_for") (("1" (EXPAND "member") (("1" (EXPAND "make_two_set_tr") (("1" (EXPAND "make_two_set") (("1" (SKOSIMP*) (("1" (REPLACE -3 :HIDE? -3) (("1" (EXPAND "compose_guar2") (("1" (EXPAND "union" +) (("1" (EXPAND "intersection" +) (("1" (EXPAND "member") (("1" (SPLIT -2) (("1" (REPLACE -1 :HIDE? -1) (("1" (INSTANTIATE -1 "union(guar(tran_cmp(cmp2!1,sttran2!1,agtran2!1)),hidd(tran_cmp(cmp2!1,sttran2!1,agtran2!1)))") (("1" (SPLIT -1) (("1" (EXPAND "tran_cmp") (("1" (EXPAND "tr_cmp") (("1" (EXPAND "union") (("1" (EXPAND "member") (("1" (FLATTEN) (("1" (DELETE 2) (("1" (GROUND) NIL))))))))))))) ("2" (INSTANTIATE 1 "tran_cmp(cmp2!1,sttran2!1,agtran2!1)") (("2" (GROUND) NIL))))))))) ("2" (REPLACE -1 :HIDE? -1) (("2" (INSTANTIATE -1 "union(guar(tran_cmp(cmp1!1,sttran1!1,agtran1!1)),hidd(tran_cmp(cmp1!1,sttran1!1,agtran1!1)))") (("2" (SPLIT -1) (("1" (EXPAND "tran_cmp") (("1" (EXPAND "tr_cmp") (("1" (EXPAND "union") (("1" (EXPAND "member") (("1" (GROUND) NIL))))))))) ("2" (INSTANTIATE 1 "tran_cmp(cmp1!1,sttran1!1,agtran1!1)") (("2" (GROUND) NIL))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (EXPAND "compose_guar") (("2" (EXPAND "intersection") (("2" (EXPAND "compose_guar2") (("2" (EXPAND "union") (("2" (EXPAND "intersection") (("2" (EXPAND "member") (("2" (EXPAND "gen_intersection") (("2" (EXPAND "gen_union") (("2" (EXPAND "member") (("2" (EXPAND "guar_or_hidds_for") (("2" (EXPAND "guars_for") (("2" (EXPAND "member") (("2" (EXPAND "make_two_set_tr") (("2" (EXPAND "make_two_set") (("2" (SPLIT -1) (("1" (FLATTEN) (("1" (SPLIT 1) (("1" (SKOSIMP*) (("1" (REPLACE -2 :HIDE? -2) (("1" (SPLIT -1) (("1" (REPLACE -1 :HIDE? -1) (("1" (EXPAND "union") (("1" (EXPAND "member") (("1" (EXPAND "tran_cmp") (("1" (EXPAND "tr_cmp") (("1" (GROUND) NIL))))))))))) ("2" (REPLACE -1 :HIDE? -1) (("2" (EXPAND "tran_cmp") (("2" (EXPAND "tr_cmp") (("2" (EXPAND "union") (("2" (EXPAND "member") (("2" (GROUND) NIL))))))))))))))))) ("2" (INST?) (("2" (GROUND) (("1" (INST?) (("1" (GROUND) (("1" (EXPAND "tran_cmp") (("1" (EXPAND "tr_cmp") (("1" (PROPAX) NIL))))))))) ("2" (INST?) (("2" (GROUND) (("2" (EXPAND "tran_cmp") (("2" (EXPAND "tr_cmp") (("2" (PROPAX) NIL))))))))))))))))) ("2" (FLATTEN) (("2" (SPLIT 1) (("1" (SKOSIMP*) (("1" (REPLACE -2 :HIDE? -2) (("1" (SPLIT -1) (("1" (REPLACE -1 :HIDE? -1) (("1" (EXPAND "tran_cmp") (("1" (EXPAND "tr_cmp") (("1" (EXPAND "union") (