diff options
Diffstat (limited to 'test/regress/regress1/ho/hoa0102.smt2')
| -rw-r--r-- | test/regress/regress1/ho/hoa0102.smt2 | 210 |
1 files changed, 105 insertions, 105 deletions
diff --git a/test/regress/regress1/ho/hoa0102.smt2 b/test/regress/regress1/ho/hoa0102.smt2 index c5840e6a9..cbdcf7480 100644 --- a/test/regress/regress1/ho/hoa0102.smt2 +++ b/test/regress/regress1/ho/hoa0102.smt2 @@ -129,9 +129,9 @@ (declare-fun these$ (Pname_option_set$) Pname_set$) (declare-fun while$ ((-> State$ Bool) Com$) Com$) (declare-fun finite$ (Pname_set$) Bool) -(declare-fun insert$ (State_triple$ State_triple_set$) State_triple_set$) +(declare-fun set.insert$ (State_triple$ State_triple_set$) State_triple_set$) (declare-fun map_le$ ((-> State_triple$ Com_option$) (-> State_triple$ Com_option$)) Bool) -(declare-fun member$ (State_triple$ State_triple_set$) Bool) +(declare-fun set.member$ (State_triple$ State_triple_set$) Bool) (declare-fun minus$a (State_triple_option_set$ State_triple_option_set$) State_triple_option_set$) (declare-fun minus$b (Com_option_set$ Com_option_set$) Com_option_set$) (declare-fun minus$c (State_triple_set$ State_triple_set$) State_triple_set$) @@ -146,18 +146,18 @@ (declare-fun collect$ ((-> Com$ Bool)) Com_set$) (declare-fun fun_upd$ ((-> State_triple$ Com_option$) State_triple$ Com_option$) (-> State_triple$ Com_option$)) (declare-fun getlocs$ (State$) (-> Loc$ Nat$)) -(declare-fun insert$a (Com$ Com_set$) Com_set$) -(declare-fun insert$b (Pname$ Pname_set$) Pname_set$) -(declare-fun insert$c (State_triple_option$ State_triple_option_set$) State_triple_option_set$) -(declare-fun insert$d (Com_option$ Com_option_set$) Com_option_set$) -(declare-fun insert$e (Pname_option$ Pname_option_set$) Pname_option_set$) -(declare-fun insert$f (State_triple_option_option$ State_triple_option_option_set$) State_triple_option_option_set$) -(declare-fun insert$g (Com_option_option$ Com_option_option_set$) Com_option_option_set$) +(declare-fun set.insert$a (Com$ Com_set$) Com_set$) +(declare-fun set.insert$b (Pname$ Pname_set$) Pname_set$) +(declare-fun set.insert$c (State_triple_option$ State_triple_option_set$) State_triple_option_set$) +(declare-fun set.insert$d (Com_option$ Com_option_set$) Com_option_set$) +(declare-fun set.insert$e (Pname_option$ Pname_option_set$) Pname_option_set$) +(declare-fun set.insert$f (State_triple_option_option$ State_triple_option_option_set$) State_triple_option_option_set$) +(declare-fun set.insert$g (Com_option_option$ Com_option_option_set$) Com_option_option_set$) (declare-fun map_le$a ((-> Pname$ Com_option$) (-> Pname$ Com_option$)) Bool) -(declare-fun member$a (Pname$ Pname_set$) Bool) -(declare-fun member$b (Com$ Com_set$) Bool) -(declare-fun member$c (State_triple_option$ State_triple_option_set$) Bool) -(declare-fun member$d (Com_option$ Com_option_set$) Bool) +(declare-fun set.member$a (Pname$ Pname_set$) Bool) +(declare-fun set.member$b (Com$ Com_set$) Bool) +(declare-fun set.member$c (State_triple_option$ State_triple_option_set$) Bool) +(declare-fun set.member$d (Com_option$ Com_option_set$) Bool) (declare-fun newlocs$ () (-> Loc$ Nat$)) (declare-fun setlocs$ (State$ (-> Loc$ Nat$)) State$) (declare-fun collect$a ((-> State_triple$ Bool)) State_triple_set$) @@ -206,9 +206,9 @@ (declare-fun restrict_map$i ((-> State_triple$ Com_option$) State_triple_set$) (-> State_triple$ Com_option$)) (declare-fun state_not_singleton$ () Bool) (assert (! (forall ((?v0 Bool)) (! (= (uut$ ?v0) (not ?v0)) :pattern ((uut$ ?v0)))) :named a0)) -(assert (! (forall ((?v0 State_triple_set$) (?v1 State_triple$)) (! (= (uua$ ?v0 ?v1) (member$ ?v1 ?v0)) :pattern ((uua$ ?v0 ?v1)))) :named a1)) -(assert (! (forall ((?v0 Pname_set$) (?v1 Pname$)) (! (= (uub$ ?v0 ?v1) (member$a ?v1 ?v0)) :pattern ((uub$ ?v0 ?v1)))) :named a2)) -(assert (! (forall ((?v0 Com_set$) (?v1 Com$)) (! (= (uu$ ?v0 ?v1) (member$b ?v1 ?v0)) :pattern ((uu$ ?v0 ?v1)))) :named a3)) +(assert (! (forall ((?v0 State_triple_set$) (?v1 State_triple$)) (! (= (uua$ ?v0 ?v1) (set.member$ ?v1 ?v0)) :pattern ((uua$ ?v0 ?v1)))) :named a1)) +(assert (! (forall ((?v0 Pname_set$) (?v1 Pname$)) (! (= (uub$ ?v0 ?v1) (set.member$a ?v1 ?v0)) :pattern ((uub$ ?v0 ?v1)))) :named a2)) +(assert (! (forall ((?v0 Com_set$) (?v1 Com$)) (! (= (uu$ ?v0 ?v1) (set.member$b ?v1 ?v0)) :pattern ((uu$ ?v0 ?v1)))) :named a3)) (assert (! (forall ((?v0 State$) (?v1 State$)) (! (= (uuq$ ?v0 ?v1) (= ?v0 ?v1)) :pattern ((uuq$ ?v0 ?v1)))) :named a4)) (assert (! (forall ((?v0 (-> State_triple$ Com_option$)) (?v1 State_triple$)) (! (= (uvh$ ?v0 ?v1) (not (= (?v0 ?v1) none$))) :pattern ((uvh$ ?v0 ?v1)))) :named a5)) (assert (! (forall ((?v0 (-> Pname$ State_triple_option$)) (?v1 Pname$)) (! (= (uvi$ ?v0 ?v1) (not (= (?v0 ?v1) none$a))) :pattern ((uvi$ ?v0 ?v1)))) :named a6)) @@ -284,9 +284,9 @@ (assert (! (forall ((?v0 Com$) (?v1 State$) (?v2 Nat$) (?v3 State$) (?v4 Com$) (?v5 State$)) (=> (and (evaln$ ?v0 ?v1 ?v2 ?v3) (evaln$ ?v4 ?v3 ?v2 ?v5)) (evaln$ (semi$ ?v0 ?v4) ?v1 ?v2 ?v5))) :named a76)) (assert (! (forall ((?v0 Com$) (?v1 Com$) (?v2 State$) (?v3 Nat$) (?v4 State$)) (=> (and (evaln$ (semi$ ?v0 ?v1) ?v2 ?v3 ?v4) (forall ((?v5 State$)) (=> (and (evaln$ ?v0 ?v2 ?v3 ?v5) (evaln$ ?v1 ?v5 ?v3 ?v4)) false))) false)) :named a77)) (assert (! (forall ((?v0 Vname$) (?v1 (-> State$ Nat$))) (not (= skip$ (ass$ ?v0 ?v1)))) :named a78)) -(assert (! (forall ((?v0 Com$) (?v1 (-> Com$ Bool))) (= (member$b ?v0 (collect$ ?v1)) (?v1 ?v0))) :named a79)) -(assert (! (forall ((?v0 State_triple$) (?v1 (-> State_triple$ Bool))) (= (member$ ?v0 (collect$a ?v1)) (?v1 ?v0))) :named a80)) -(assert (! (forall ((?v0 Pname$) (?v1 (-> Pname$ Bool))) (= (member$a ?v0 (collect$b ?v1)) (?v1 ?v0))) :named a81)) +(assert (! (forall ((?v0 Com$) (?v1 (-> Com$ Bool))) (= (set.member$b ?v0 (collect$ ?v1)) (?v1 ?v0))) :named a79)) +(assert (! (forall ((?v0 State_triple$) (?v1 (-> State_triple$ Bool))) (= (set.member$ ?v0 (collect$a ?v1)) (?v1 ?v0))) :named a80)) +(assert (! (forall ((?v0 Pname$) (?v1 (-> Pname$ Bool))) (= (set.member$a ?v0 (collect$b ?v1)) (?v1 ?v0))) :named a81)) (assert (! (forall ((?v0 Com_set$)) (= (collect$ (uu$ ?v0)) ?v0)) :named a82)) (assert (! (forall ((?v0 State_triple_set$)) (= (collect$a (uua$ ?v0)) ?v0)) :named a83)) (assert (! (forall ((?v0 Pname_set$)) (= (collect$b (uub$ ?v0)) ?v0)) :named a84)) @@ -388,9 +388,9 @@ (assert (! (forall ((?v0 Vname$)) (=> (and (forall ((?v1 Glb$)) (=> (= ?v0 (glb$ ?v1)) false)) (forall ((?v1 Loc$)) (=> (= ?v0 (loc$ ?v1)) false))) false)) :named a180)) (assert (! (forall ((?v0 Pname$) (?v1 Com$)) (=> (and wT_bodies$ (= (body$ ?v0) (some$ ?v1))) (wt$ ?v1))) :named a181)) (assert (! (forall ((?v0 Nat$) (?v1 (-> State$ (-> State$ Bool))) (?v2 Pname$) (?v3 (-> State$ (-> State$ Bool)))) (= (triple_valid$ ?v0 (triple$ ?v1 (the$ (body$ ?v2)) ?v3)) (triple_valid$ (suc$ ?v0) (triple$ ?v1 (body$a ?v2) ?v3)))) :named a182)) -(assert (! (forall ((?v0 Pname_option$)) (=> (not (= ?v0 none$b)) (member$a (the$b ?v0) (set_option$ ?v0)))) :named a183)) -(assert (! (forall ((?v0 State_triple_option$)) (=> (not (= ?v0 none$a)) (member$ (the$a ?v0) (set_option$a ?v0)))) :named a184)) -(assert (! (forall ((?v0 Com_option$)) (=> (not (= ?v0 none$)) (member$b (the$ ?v0) (set_option$b ?v0)))) :named a185)) +(assert (! (forall ((?v0 Pname_option$)) (=> (not (= ?v0 none$b)) (set.member$a (the$b ?v0) (set_option$ ?v0)))) :named a183)) +(assert (! (forall ((?v0 State_triple_option$)) (=> (not (= ?v0 none$a)) (set.member$ (the$a ?v0) (set_option$a ?v0)))) :named a184)) +(assert (! (forall ((?v0 Com_option$)) (=> (not (= ?v0 none$)) (set.member$b (the$ ?v0) (set_option$b ?v0)))) :named a185)) (assert (! (forall ((?v0 State_triple_option$) (?v1 (-> State_triple$ Com_option$))) (= (= (bind$ ?v0 ?v1) none$) (or (= ?v0 none$a) (= (?v1 (the$a ?v0)) none$)))) :named a186)) (assert (! (forall ((?v0 Com_option$) (?v1 (-> Com$ State_triple_option$))) (= (= (bind$a ?v0 ?v1) none$a) (or (= ?v0 none$) (= (?v1 (the$ ?v0)) none$a)))) :named a187)) (assert (! (forall ((?v0 State_triple_option$) (?v1 (-> State_triple$ State_triple_option$))) (= (= (bind$b ?v0 ?v1) none$a) (or (= ?v0 none$a) (= (?v1 (the$a ?v0)) none$a)))) :named a188)) @@ -449,7 +449,7 @@ (assert (! (forall ((?v0 Vname$) (?v1 (-> State$ Nat$))) (! (= (size$d (ass$ ?v0 ?v1)) zero$) :pattern ((ass$ ?v0 ?v1)))) :named a241)) (assert (! (= (size$d skip$) zero$) :named a242)) (assert (! (forall ((?v0 (-> State$ Bool)) (?v1 Com$)) (! (= (size$d (while$ ?v0 ?v1)) (plus$ (size$d ?v1) (suc$ zero$))) :pattern ((while$ ?v0 ?v1)))) :named a243)) -(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> State$ (-> State$ Bool))) (?v2 Pname$) (?v3 (-> State$ (-> State$ Bool))) (?v4 State$) (?v5 Vname$) (?v6 (-> State$ Nat$))) (=> (hoare_derivs$ ?v0 (insert$ (triple$ ?v1 (body$a ?v2) (uuc$ ?v3 ?v4 ?v5)) bot$d)) (hoare_derivs$ ?v0 (insert$ (triple$ (uud$ ?v1 ?v4 ?v6) (call$ ?v5 ?v2 ?v6) ?v3) bot$d)))) :named a244)) +(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> State$ (-> State$ Bool))) (?v2 Pname$) (?v3 (-> State$ (-> State$ Bool))) (?v4 State$) (?v5 Vname$) (?v6 (-> State$ Nat$))) (=> (hoare_derivs$ ?v0 (set.insert$ (triple$ ?v1 (body$a ?v2) (uuc$ ?v3 ?v4 ?v5)) bot$d)) (hoare_derivs$ ?v0 (set.insert$ (triple$ (uud$ ?v1 ?v4 ?v6) (call$ ?v5 ?v2 ?v6) ?v3) bot$d)))) :named a244)) (assert (! (forall ((?v0 Com_option$)) (= (bind$c ?v0 uue$) none$)) :named a245)) (assert (! (forall ((?v0 Bool) (?v1 (-> State_triple$ Bool)) (?v2 State_triple_option$)) (=> (and (case_option$a ?v0 ?v1 ?v2) (and (=> (and (= ?v2 none$a) ?v0) false) (forall ((?v3 State_triple$)) (=> (and (= ?v2 (some$a ?v3)) (?v1 ?v3)) false)))) false)) :named a246)) (assert (! (forall ((?v0 Bool) (?v1 (-> Com$ Bool)) (?v2 Com_option$)) (=> (and (case_option$ ?v0 ?v1 ?v2) (and (=> (and (= ?v2 none$) ?v0) false) (forall ((?v3 Com$)) (=> (and (= ?v2 (some$ ?v3)) (?v1 ?v3)) false)))) false)) :named a247)) @@ -458,50 +458,50 @@ (assert (! (forall ((?v0 Com_option$)) (= (not (= ?v0 none$)) (case_option$ false uug$ ?v0))) :named a250)) (assert (! (forall ((?v0 State_triple_option$)) (= (= ?v0 none$a) (case_option$a true uuh$ ?v0))) :named a251)) (assert (! (forall ((?v0 Com_option$)) (= (= ?v0 none$) (case_option$ true uui$ ?v0))) :named a252)) -(assert (! (forall ((?v0 State_triple_set$) (?v1 State_triple$) (?v2 State_triple_set$)) (=> (hoare_derivs$ ?v0 (insert$ ?v1 ?v2)) (and (hoare_derivs$ ?v0 (insert$ ?v1 bot$d)) (hoare_derivs$ ?v0 ?v2)))) :named a253)) +(assert (! (forall ((?v0 State_triple_set$) (?v1 State_triple$) (?v2 State_triple_set$)) (=> (hoare_derivs$ ?v0 (set.insert$ ?v1 ?v2)) (and (hoare_derivs$ ?v0 (set.insert$ ?v1 bot$d)) (hoare_derivs$ ?v0 ?v2)))) :named a253)) (assert (! (forall ((?v0 State_triple_set$)) (hoare_derivs$ ?v0 bot$d)) :named a254)) -(assert (! (forall ((?v0 State_triple_set$) (?v1 State_triple$) (?v2 State_triple_set$)) (=> (and (hoare_derivs$ ?v0 (insert$ ?v1 bot$d)) (hoare_derivs$ ?v0 ?v2)) (hoare_derivs$ ?v0 (insert$ ?v1 ?v2)))) :named a255)) -(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> State$ (-> State$ Bool))) (?v2 Com$) (?v3 (-> State$ (-> State$ Bool))) (?v4 Loc$) (?v5 State$) (?v6 (-> State$ Nat$))) (=> (hoare_derivs$ ?v0 (insert$ (triple$ ?v1 ?v2 (uuj$ ?v3 ?v4 ?v5)) bot$d)) (hoare_derivs$ ?v0 (insert$ (triple$ (uuk$ ?v1 ?v4 ?v5 ?v6) (local$ ?v4 ?v6 ?v2) ?v3) bot$d)))) :named a256)) -(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> State$ (-> State$ Bool))) (?v2 (-> State$ Bool)) (?v3 Com$)) (hoare_derivs$ ?v0 (insert$ (triple$ (uul$ ?v1 ?v2) (while$ ?v2 ?v3) ?v1) bot$d))) :named a257)) -(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> State$ (-> State$ Bool))) (?v2 Com$) (?v3 (-> State$ (-> State$ Bool))) (?v4 Com$) (?v5 (-> State$ (-> State$ Bool)))) (=> (and (hoare_derivs$ ?v0 (insert$ (triple$ ?v1 ?v2 ?v3) bot$d)) (hoare_derivs$ ?v0 (insert$ (triple$ ?v3 ?v4 ?v5) bot$d))) (hoare_derivs$ ?v0 (insert$ (triple$ ?v1 (semi$ ?v2 ?v4) ?v5) bot$d)))) :named a258)) -(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> State$ (-> State$ Bool)))) (hoare_derivs$ ?v0 (insert$ (triple$ ?v1 skip$ ?v1) bot$d))) :named a259)) -(assert (! (forall ((?v0 (-> State$ (-> State$ Bool))) (?v1 State_triple_set$) (?v2 Com$) (?v3 (-> State$ (-> State$ Bool)))) (=> (forall ((?v4 State$) (?v5 State$)) (=> (?v0 ?v4 ?v5) (exists ((?v6 (-> State$ (-> State$ Bool))) (?v7 (-> State$ (-> State$ Bool)))) (and (hoare_derivs$ ?v1 (insert$ (triple$ ?v6 ?v2 ?v7) bot$d)) (forall ((?v8 State$)) (=> (forall ((?v9 State$)) (=> (?v6 ?v9 ?v5) (?v7 ?v9 ?v8))) (?v3 ?v4 ?v8))))))) (hoare_derivs$ ?v1 (insert$ (triple$ ?v0 ?v2 ?v3) bot$d)))) :named a260)) -(assert (! (forall ((?v0 Bool) (?v1 State_triple_set$) (?v2 (-> State$ (-> State$ Bool))) (?v3 Com$) (?v4 (-> State$ (-> State$ Bool)))) (=> (=> ?v0 (hoare_derivs$ ?v1 (insert$ (triple$ ?v2 ?v3 ?v4) bot$d))) (hoare_derivs$ ?v1 (insert$ (triple$ (uum$ ?v0 ?v2) ?v3 ?v4) bot$d)))) :named a261)) -(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> State$ (-> State$ Bool))) (?v2 Com$) (?v3 (-> State$ (-> State$ Bool))) (?v4 (-> State$ (-> State$ Bool))) (?v5 (-> State$ (-> State$ Bool)))) (=> (and (hoare_derivs$ ?v0 (insert$ (triple$ ?v1 ?v2 ?v3) bot$d)) (forall ((?v6 State$) (?v7 State$)) (=> (?v4 ?v6 ?v7) (forall ((?v8 State$)) (=> (forall ((?v9 State$)) (=> (?v1 ?v9 ?v7) (?v3 ?v9 ?v8))) (?v5 ?v6 ?v8)))))) (hoare_derivs$ ?v0 (insert$ (triple$ ?v4 ?v2 ?v5) bot$d)))) :named a262)) -(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> State$ (-> State$ Bool))) (?v2 Com$) (?v3 (-> State$ (-> State$ Bool))) (?v4 (-> State$ (-> State$ Bool)))) (=> (and (hoare_derivs$ ?v0 (insert$ (triple$ ?v1 ?v2 ?v3) bot$d)) (forall ((?v5 State$) (?v6 State$)) (=> (?v3 ?v5 ?v6) (?v4 ?v5 ?v6)))) (hoare_derivs$ ?v0 (insert$ (triple$ ?v1 ?v2 ?v4) bot$d)))) :named a263)) -(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> State$ (-> State$ Bool))) (?v2 Com$) (?v3 (-> State$ (-> State$ Bool))) (?v4 (-> State$ (-> State$ Bool)))) (=> (and (hoare_derivs$ ?v0 (insert$ (triple$ ?v1 ?v2 ?v3) bot$d)) (forall ((?v5 State$) (?v6 State$)) (=> (?v4 ?v5 ?v6) (?v1 ?v5 ?v6)))) (hoare_derivs$ ?v0 (insert$ (triple$ ?v4 ?v2 ?v3) bot$d)))) :named a264)) -(assert (! (forall ((?v0 (-> State$ (-> State$ Bool))) (?v1 State_triple_set$) (?v2 Com$) (?v3 (-> State$ (-> State$ Bool)))) (=> (forall ((?v4 State$) (?v5 State$)) (=> (?v0 ?v4 ?v5) (hoare_derivs$ ?v1 (insert$ (triple$ (uun$ ?v5) ?v2 (uuo$ ?v3 ?v4)) bot$d)))) (hoare_derivs$ ?v1 (insert$ (triple$ ?v0 ?v2 ?v3) bot$d)))) :named a265)) -(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> State$ (-> State$ Bool))) (?v2 Vname$) (?v3 (-> State$ Nat$))) (hoare_derivs$ ?v0 (insert$ (triple$ (uup$ ?v1 ?v2 ?v3) (ass$ ?v2 ?v3) ?v1) bot$d))) :named a266)) -(assert (! (forall ((?v0 (-> State$ (-> State$ Bool))) (?v1 Pname$) (?v2 (-> State$ (-> State$ Bool))) (?v3 State_triple_set$)) (=> (hoare_derivs$ (insert$ (triple$ ?v0 (body$a ?v1) ?v2) ?v3) (insert$ (triple$ ?v0 (the$ (body$ ?v1)) ?v2) bot$d)) (hoare_derivs$ ?v3 (insert$ (triple$ ?v0 (body$a ?v1) ?v2) bot$d)))) :named a267)) -(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> State$ (-> State$ Bool))) (?v2 Pname$) (?v3 (-> State$ (-> State$ Bool)))) (=> (hoare_derivs$ ?v0 (insert$ (triple$ ?v1 (the$ (body$ ?v2)) ?v3) bot$d)) (hoare_derivs$ ?v0 (insert$ (triple$ ?v1 (body$a ?v2) ?v3) bot$d)))) :named a268)) +(assert (! (forall ((?v0 State_triple_set$) (?v1 State_triple$) (?v2 State_triple_set$)) (=> (and (hoare_derivs$ ?v0 (set.insert$ ?v1 bot$d)) (hoare_derivs$ ?v0 ?v2)) (hoare_derivs$ ?v0 (set.insert$ ?v1 ?v2)))) :named a255)) +(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> State$ (-> State$ Bool))) (?v2 Com$) (?v3 (-> State$ (-> State$ Bool))) (?v4 Loc$) (?v5 State$) (?v6 (-> State$ Nat$))) (=> (hoare_derivs$ ?v0 (set.insert$ (triple$ ?v1 ?v2 (uuj$ ?v3 ?v4 ?v5)) bot$d)) (hoare_derivs$ ?v0 (set.insert$ (triple$ (uuk$ ?v1 ?v4 ?v5 ?v6) (local$ ?v4 ?v6 ?v2) ?v3) bot$d)))) :named a256)) +(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> State$ (-> State$ Bool))) (?v2 (-> State$ Bool)) (?v3 Com$)) (hoare_derivs$ ?v0 (set.insert$ (triple$ (uul$ ?v1 ?v2) (while$ ?v2 ?v3) ?v1) bot$d))) :named a257)) +(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> State$ (-> State$ Bool))) (?v2 Com$) (?v3 (-> State$ (-> State$ Bool))) (?v4 Com$) (?v5 (-> State$ (-> State$ Bool)))) (=> (and (hoare_derivs$ ?v0 (set.insert$ (triple$ ?v1 ?v2 ?v3) bot$d)) (hoare_derivs$ ?v0 (set.insert$ (triple$ ?v3 ?v4 ?v5) bot$d))) (hoare_derivs$ ?v0 (set.insert$ (triple$ ?v1 (semi$ ?v2 ?v4) ?v5) bot$d)))) :named a258)) +(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> State$ (-> State$ Bool)))) (hoare_derivs$ ?v0 (set.insert$ (triple$ ?v1 skip$ ?v1) bot$d))) :named a259)) +(assert (! (forall ((?v0 (-> State$ (-> State$ Bool))) (?v1 State_triple_set$) (?v2 Com$) (?v3 (-> State$ (-> State$ Bool)))) (=> (forall ((?v4 State$) (?v5 State$)) (=> (?v0 ?v4 ?v5) (exists ((?v6 (-> State$ (-> State$ Bool))) (?v7 (-> State$ (-> State$ Bool)))) (and (hoare_derivs$ ?v1 (set.insert$ (triple$ ?v6 ?v2 ?v7) bot$d)) (forall ((?v8 State$)) (=> (forall ((?v9 State$)) (=> (?v6 ?v9 ?v5) (?v7 ?v9 ?v8))) (?v3 ?v4 ?v8))))))) (hoare_derivs$ ?v1 (set.insert$ (triple$ ?v0 ?v2 ?v3) bot$d)))) :named a260)) +(assert (! (forall ((?v0 Bool) (?v1 State_triple_set$) (?v2 (-> State$ (-> State$ Bool))) (?v3 Com$) (?v4 (-> State$ (-> State$ Bool)))) (=> (=> ?v0 (hoare_derivs$ ?v1 (set.insert$ (triple$ ?v2 ?v3 ?v4) bot$d))) (hoare_derivs$ ?v1 (set.insert$ (triple$ (uum$ ?v0 ?v2) ?v3 ?v4) bot$d)))) :named a261)) +(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> State$ (-> State$ Bool))) (?v2 Com$) (?v3 (-> State$ (-> State$ Bool))) (?v4 (-> State$ (-> State$ Bool))) (?v5 (-> State$ (-> State$ Bool)))) (=> (and (hoare_derivs$ ?v0 (set.insert$ (triple$ ?v1 ?v2 ?v3) bot$d)) (forall ((?v6 State$) (?v7 State$)) (=> (?v4 ?v6 ?v7) (forall ((?v8 State$)) (=> (forall ((?v9 State$)) (=> (?v1 ?v9 ?v7) (?v3 ?v9 ?v8))) (?v5 ?v6 ?v8)))))) (hoare_derivs$ ?v0 (set.insert$ (triple$ ?v4 ?v2 ?v5) bot$d)))) :named a262)) +(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> State$ (-> State$ Bool))) (?v2 Com$) (?v3 (-> State$ (-> State$ Bool))) (?v4 (-> State$ (-> State$ Bool)))) (=> (and (hoare_derivs$ ?v0 (set.insert$ (triple$ ?v1 ?v2 ?v3) bot$d)) (forall ((?v5 State$) (?v6 State$)) (=> (?v3 ?v5 ?v6) (?v4 ?v5 ?v6)))) (hoare_derivs$ ?v0 (set.insert$ (triple$ ?v1 ?v2 ?v4) bot$d)))) :named a263)) +(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> State$ (-> State$ Bool))) (?v2 Com$) (?v3 (-> State$ (-> State$ Bool))) (?v4 (-> State$ (-> State$ Bool)))) (=> (and (hoare_derivs$ ?v0 (set.insert$ (triple$ ?v1 ?v2 ?v3) bot$d)) (forall ((?v5 State$) (?v6 State$)) (=> (?v4 ?v5 ?v6) (?v1 ?v5 ?v6)))) (hoare_derivs$ ?v0 (set.insert$ (triple$ ?v4 ?v2 ?v3) bot$d)))) :named a264)) +(assert (! (forall ((?v0 (-> State$ (-> State$ Bool))) (?v1 State_triple_set$) (?v2 Com$) (?v3 (-> State$ (-> State$ Bool)))) (=> (forall ((?v4 State$) (?v5 State$)) (=> (?v0 ?v4 ?v5) (hoare_derivs$ ?v1 (set.insert$ (triple$ (uun$ ?v5) ?v2 (uuo$ ?v3 ?v4)) bot$d)))) (hoare_derivs$ ?v1 (set.insert$ (triple$ ?v0 ?v2 ?v3) bot$d)))) :named a265)) +(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> State$ (-> State$ Bool))) (?v2 Vname$) (?v3 (-> State$ Nat$))) (hoare_derivs$ ?v0 (set.insert$ (triple$ (uup$ ?v1 ?v2 ?v3) (ass$ ?v2 ?v3) ?v1) bot$d))) :named a266)) +(assert (! (forall ((?v0 (-> State$ (-> State$ Bool))) (?v1 Pname$) (?v2 (-> State$ (-> State$ Bool))) (?v3 State_triple_set$)) (=> (hoare_derivs$ (set.insert$ (triple$ ?v0 (body$a ?v1) ?v2) ?v3) (set.insert$ (triple$ ?v0 (the$ (body$ ?v1)) ?v2) bot$d)) (hoare_derivs$ ?v3 (set.insert$ (triple$ ?v0 (body$a ?v1) ?v2) bot$d)))) :named a267)) +(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> State$ (-> State$ Bool))) (?v2 Pname$) (?v3 (-> State$ (-> State$ Bool)))) (=> (hoare_derivs$ ?v0 (set.insert$ (triple$ ?v1 (the$ (body$ ?v2)) ?v3) bot$d)) (hoare_derivs$ ?v0 (set.insert$ (triple$ ?v1 (body$a ?v2) ?v3) bot$d)))) :named a268)) (assert (! (forall ((?v0 Com$)) (! (= (mgt$ ?v0) (triple$ uuq$ ?v0 (evalc$ ?v0))) :pattern ((mgt$ ?v0)))) :named a269)) -(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> Pname$ (-> State$ (-> State$ Bool)))) (?v2 (-> Pname$ (-> State$ (-> State$ Bool)))) (?v3 Pname_set$) (?v4 Pname$)) (=> (and (hoare_derivs$ (sup$ ?v0 (image$ (uur$ ?v1 ?v2) ?v3)) (image$ (uus$ ?v1 ?v2) ?v3)) (member$a ?v4 ?v3)) (hoare_derivs$ ?v0 (insert$ (triple$ (?v1 ?v4) (body$a ?v4) (?v2 ?v4)) bot$d)))) :named a270)) -(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> State$ (-> State$ Bool))) (?v2 (-> State$ Bool)) (?v3 Com$) (?v4 (-> State$ (-> State$ Bool))) (?v5 Com$)) (=> (and (hoare_derivs$ ?v0 (insert$ (triple$ (peek_and$ ?v1 ?v2) ?v3 ?v4) bot$d)) (hoare_derivs$ ?v0 (insert$ (triple$ (peek_and$ ?v1 (comp$ uut$ ?v2)) ?v5 ?v4) bot$d))) (hoare_derivs$ ?v0 (insert$ (triple$ ?v1 (cond$ ?v2 ?v3 ?v5) ?v4) bot$d)))) :named a271)) +(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> Pname$ (-> State$ (-> State$ Bool)))) (?v2 (-> Pname$ (-> State$ (-> State$ Bool)))) (?v3 Pname_set$) (?v4 Pname$)) (=> (and (hoare_derivs$ (sup$ ?v0 (image$ (uur$ ?v1 ?v2) ?v3)) (image$ (uus$ ?v1 ?v2) ?v3)) (set.member$a ?v4 ?v3)) (hoare_derivs$ ?v0 (set.insert$ (triple$ (?v1 ?v4) (body$a ?v4) (?v2 ?v4)) bot$d)))) :named a270)) +(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> State$ (-> State$ Bool))) (?v2 (-> State$ Bool)) (?v3 Com$) (?v4 (-> State$ (-> State$ Bool))) (?v5 Com$)) (=> (and (hoare_derivs$ ?v0 (set.insert$ (triple$ (peek_and$ ?v1 ?v2) ?v3 ?v4) bot$d)) (hoare_derivs$ ?v0 (set.insert$ (triple$ (peek_and$ ?v1 (comp$ uut$ ?v2)) ?v5 ?v4) bot$d))) (hoare_derivs$ ?v0 (set.insert$ (triple$ ?v1 (cond$ ?v2 ?v3 ?v5) ?v4) bot$d)))) :named a271)) (assert (! (forall ((?v0 (-> State$ (-> State$ Bool))) (?v1 (-> State$ Bool)) (?v2 State$) (?v3 State$)) (! (= (peek_and$ ?v0 ?v1 ?v2 ?v3) (and (?v0 ?v2 ?v3) (?v1 ?v3))) :pattern ((peek_and$ ?v0 ?v1 ?v2 ?v3)))) :named a272)) (assert (! (forall ((?v0 State_triple_set$) (?v1 (-> Pname$ (-> State$ (-> State$ Bool)))) (?v2 (-> Pname$ (-> State$ (-> State$ Bool)))) (?v3 Pname_set$)) (=> (hoare_derivs$ (sup$ ?v0 (image$ (uur$ ?v1 ?v2) ?v3)) (image$ (uus$ ?v1 ?v2) ?v3)) (hoare_derivs$ ?v0 (image$ (uur$ ?v1 ?v2) ?v3)))) :named a273)) -(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> State$ (-> State$ Bool))) (?v2 (-> State$ Bool)) (?v3 Com$)) (=> (hoare_derivs$ ?v0 (insert$ (triple$ (peek_and$ ?v1 ?v2) ?v3 ?v1) bot$d)) (hoare_derivs$ ?v0 (insert$ (triple$ ?v1 (while$ ?v2 ?v3) (peek_and$ ?v1 (comp$ uut$ ?v2))) bot$d)))) :named a274)) +(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> State$ (-> State$ Bool))) (?v2 (-> State$ Bool)) (?v3 Com$)) (=> (hoare_derivs$ ?v0 (set.insert$ (triple$ (peek_and$ ?v1 ?v2) ?v3 ?v1) bot$d)) (hoare_derivs$ ?v0 (set.insert$ (triple$ ?v1 (while$ ?v2 ?v3) (peek_and$ ?v1 (comp$ uut$ ?v2))) bot$d)))) :named a274)) (assert (! (forall ((?v0 State_triple_set$) (?v1 (-> Pname$ (-> State$ (-> State$ Bool)))) (?v2 (-> Pname$ (-> State$ (-> State$ Bool)))) (?v3 Pname_set$)) (=> (hoare_valids$ (sup$ ?v0 (image$ (uur$ ?v1 ?v2) ?v3)) (image$ (uus$ ?v1 ?v2) ?v3)) (hoare_valids$ ?v0 (image$ (uur$ ?v1 ?v2) ?v3)))) :named a275)) -(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> State$ (-> State$ Bool))) (?v2 (-> State$ Bool)) (?v3 Com$)) (=> (hoare_valids$ ?v0 (insert$ (triple$ (peek_and$ ?v1 ?v2) ?v3 ?v1) bot$d)) (hoare_valids$ ?v0 (insert$ (triple$ ?v1 (while$ ?v2 ?v3) (peek_and$ ?v1 (comp$ uut$ ?v2))) bot$d)))) :named a276)) +(assert (! (forall ((?v0 State_triple_set$) (?v1 (-> State$ (-> State$ Bool))) (?v2 (-> State$ Bool)) (?v3 Com$)) (=> (hoare_valids$ ?v0 (set.insert$ (triple$ (peek_and$ ?v1 ?v2) ?v3 ?v1) bot$d)) (hoare_valids$ ?v0 (set.insert$ (triple$ ?v1 (while$ ?v2 ?v3) (peek_and$ ?v1 (comp$ uut$ ?v2))) bot$d)))) :named a276)) (assert (! (forall ((?v0 State_triple_set$) (?v1 State_triple_set$)) (=> (hoare_derivs$ ?v0 ?v1) (hoare_valids$ ?v0 ?v1))) :named a277)) -(assert (! (forall ((?v0 Pname_set$) (?v1 State_triple_set$) (?v2 (-> Pname$ (-> State$ (-> State$ Bool)))) (?v3 (-> Pname$ Com$)) (?v4 (-> Pname$ (-> State$ (-> State$ Bool)))) (?v5 (-> Pname$ (-> State$ (-> State$ Bool)))) (?v6 (-> Pname$ (-> State$ (-> State$ Bool))))) (=> (and (finite$ ?v0) (and (forall ((?v7 Pname$)) (=> (hoare_derivs$ ?v1 (insert$ (triple$ (?v2 ?v7) (?v3 ?v7) (?v4 ?v7)) bot$d)) (hoare_derivs$ ?v1 (insert$ (triple$ (?v5 ?v7) (?v3 ?v7) (?v6 ?v7)) bot$d)))) (hoare_derivs$ ?v1 (image$ (uuu$ ?v2 ?v3 ?v4) ?v0)))) (hoare_derivs$ ?v1 (image$ (uuv$ ?v3 ?v5 ?v6) ?v0)))) :named a278)) -(assert (! (forall ((?v0 State_triple_set$) (?v1 Com$)) (=> (hoare_derivs$ ?v0 (insert$ (mgt$ ?v1) bot$d)) (hoare_derivs$ ?v0 (insert$ (triple$ (uuw$ ?v1) ?v1 uuq$) bot$d)))) :named a279)) +(assert (! (forall ((?v0 Pname_set$) (?v1 State_triple_set$) (?v2 (-> Pname$ (-> State$ (-> State$ Bool)))) (?v3 (-> Pname$ Com$)) (?v4 (-> Pname$ (-> State$ (-> State$ Bool)))) (?v5 (-> Pname$ (-> State$ (-> State$ Bool)))) (?v6 (-> Pname$ (-> State$ (-> State$ Bool))))) (=> (and (finite$ ?v0) (and (forall ((?v7 Pname$)) (=> (hoare_derivs$ ?v1 (set.insert$ (triple$ (?v2 ?v7) (?v3 ?v7) (?v4 ?v7)) bot$d)) (hoare_derivs$ ?v1 (set.insert$ (triple$ (?v5 ?v7) (?v3 ?v7) (?v6 ?v7)) bot$d)))) (hoare_derivs$ ?v1 (image$ (uuu$ ?v2 ?v3 ?v4) ?v0)))) (hoare_derivs$ ?v1 (image$ (uuv$ ?v3 ?v5 ?v6) ?v0)))) :named a278)) +(assert (! (forall ((?v0 State_triple_set$) (?v1 Com$)) (=> (hoare_derivs$ ?v0 (set.insert$ (mgt$ ?v1) bot$d)) (hoare_derivs$ ?v0 (set.insert$ (triple$ (uuw$ ?v1) ?v1 uuq$) bot$d)))) :named a279)) (assert (! (forall ((?v0 Nat$) (?v1 State_triple$)) (= (triple_valid$ ?v0 ?v1) (case_triple$ (uux$ ?v0) ?v1))) :named a280)) -(assert (! (forall ((?v0 (-> State_triple$ Com_option$)) (?v1 State_triple$) (?v2 Com$)) (=> (= (?v0 ?v1) none$) (= (ran$ (fun_upd$ ?v0 ?v1 (some$ ?v2))) (insert$a ?v2 (ran$ ?v0))))) :named a281)) -(assert (! (forall ((?v0 (-> Pname$ Com_option$)) (?v1 Pname$) (?v2 Com$)) (=> (= (?v0 ?v1) none$) (= (ran$a (fun_upd$a ?v0 ?v1 (some$ ?v2))) (insert$a ?v2 (ran$a ?v0))))) :named a282)) +(assert (! (forall ((?v0 (-> State_triple$ Com_option$)) (?v1 State_triple$) (?v2 Com$)) (=> (= (?v0 ?v1) none$) (= (ran$ (fun_upd$ ?v0 ?v1 (some$ ?v2))) (set.insert$a ?v2 (ran$ ?v0))))) :named a281)) +(assert (! (forall ((?v0 (-> Pname$ Com_option$)) (?v1 Pname$) (?v2 Com$)) (=> (= (?v0 ?v1) none$) (= (ran$a (fun_upd$a ?v0 ?v1 (some$ ?v2))) (set.insert$a ?v2 (ran$a ?v0))))) :named a282)) (assert (! (forall ((?v0 State_triple$) (?v1 State_triple$)) (= (fun_upd$ uuy$ ?v0 none$ ?v1) none$)) :named a283)) (assert (! (forall ((?v0 Pname$) (?v1 Pname$)) (= (fun_upd$a uuz$ ?v0 none$ ?v1) none$)) :named a284)) (assert (! (forall ((?v0 (-> State_triple$ Com_option$)) (?v1 State_triple$) (?v2 Com$)) (not (= (fun_upd$ ?v0 ?v1 (some$ ?v2)) uuy$))) :named a285)) (assert (! (forall ((?v0 (-> Pname$ Com_option$)) (?v1 Pname$) (?v2 Com$)) (not (= (fun_upd$a ?v0 ?v1 (some$ ?v2)) uuz$))) :named a286)) -(assert (! (forall ((?v0 (-> State_triple$ State_triple_option$)) (?v1 State_triple$)) (= (= (dom$ ?v0) (insert$ ?v1 bot$d)) (exists ((?v2 State_triple$)) (= ?v0 (fun_upd$b uva$ ?v1 (some$a ?v2)))))) :named a287)) -(assert (! (forall ((?v0 (-> Com$ State_triple_option$)) (?v1 Com$)) (= (= (dom$a ?v0) (insert$a ?v1 bot$c)) (exists ((?v2 State_triple$)) (= ?v0 (fun_upd$c uvb$ ?v1 (some$a ?v2)))))) :named a288)) -(assert (! (forall ((?v0 (-> Com$ Com_option$)) (?v1 Com$)) (= (= (dom$b ?v0) (insert$a ?v1 bot$c)) (exists ((?v2 Com$)) (= ?v0 (fun_upd$d uue$ ?v1 (some$ ?v2)))))) :named a289)) -(assert (! (forall ((?v0 (-> Pname$ State_triple_option$)) (?v1 Pname$)) (= (= (dom$c ?v0) (insert$b ?v1 bot$)) (exists ((?v2 State_triple$)) (= ?v0 (fun_upd$e uvc$ ?v1 (some$a ?v2)))))) :named a290)) -(assert (! (forall ((?v0 (-> State_triple_option$ State_triple_option$)) (?v1 State_triple_option$)) (= (= (dom$d ?v0) (insert$c ?v1 bot$a)) (exists ((?v2 State_triple$)) (= ?v0 (fun_upd$f uvd$ ?v1 (some$a ?v2)))))) :named a291)) -(assert (! (forall ((?v0 (-> State_triple_option$ Com_option$)) (?v1 State_triple_option$)) (= (= (dom$e ?v0) (insert$c ?v1 bot$a)) (exists ((?v2 Com$)) (= ?v0 (fun_upd$g uve$ ?v1 (some$ ?v2)))))) :named a292)) -(assert (! (forall ((?v0 (-> Com_option$ State_triple_option$)) (?v1 Com_option$)) (= (= (dom$f ?v0) (insert$d ?v1 bot$b)) (exists ((?v2 State_triple$)) (= ?v0 (fun_upd$h uvf$ ?v1 (some$a ?v2)))))) :named a293)) -(assert (! (forall ((?v0 (-> Com_option$ Com_option$)) (?v1 Com_option$)) (= (= (dom$g ?v0) (insert$d ?v1 bot$b)) (exists ((?v2 Com$)) (= ?v0 (fun_upd$i uvg$ ?v1 (some$ ?v2)))))) :named a294)) -(assert (! (forall ((?v0 (-> Pname$ Com_option$)) (?v1 Pname$)) (= (= (dom$h ?v0) (insert$b ?v1 bot$)) (exists ((?v2 Com$)) (= ?v0 (fun_upd$a uuz$ ?v1 (some$ ?v2)))))) :named a295)) -(assert (! (forall ((?v0 (-> State_triple$ Com_option$)) (?v1 State_triple$)) (= (= (dom$i ?v0) (insert$ ?v1 bot$d)) (exists ((?v2 Com$)) (= ?v0 (fun_upd$ uuy$ ?v1 (some$ ?v2)))))) :named a296)) +(assert (! (forall ((?v0 (-> State_triple$ State_triple_option$)) (?v1 State_triple$)) (= (= (dom$ ?v0) (set.insert$ ?v1 bot$d)) (exists ((?v2 State_triple$)) (= ?v0 (fun_upd$b uva$ ?v1 (some$a ?v2)))))) :named a287)) +(assert (! (forall ((?v0 (-> Com$ State_triple_option$)) (?v1 Com$)) (= (= (dom$a ?v0) (set.insert$a ?v1 bot$c)) (exists ((?v2 State_triple$)) (= ?v0 (fun_upd$c uvb$ ?v1 (some$a ?v2)))))) :named a288)) +(assert (! (forall ((?v0 (-> Com$ Com_option$)) (?v1 Com$)) (= (= (dom$b ?v0) (set.insert$a ?v1 bot$c)) (exists ((?v2 Com$)) (= ?v0 (fun_upd$d uue$ ?v1 (some$ ?v2)))))) :named a289)) +(assert (! (forall ((?v0 (-> Pname$ State_triple_option$)) (?v1 Pname$)) (= (= (dom$c ?v0) (set.insert$b ?v1 bot$)) (exists ((?v2 State_triple$)) (= ?v0 (fun_upd$e uvc$ ?v1 (some$a ?v2)))))) :named a290)) +(assert (! (forall ((?v0 (-> State_triple_option$ State_triple_option$)) (?v1 State_triple_option$)) (= (= (dom$d ?v0) (set.insert$c ?v1 bot$a)) (exists ((?v2 State_triple$)) (= ?v0 (fun_upd$f uvd$ ?v1 (some$a ?v2)))))) :named a291)) +(assert (! (forall ((?v0 (-> State_triple_option$ Com_option$)) (?v1 State_triple_option$)) (= (= (dom$e ?v0) (set.insert$c ?v1 bot$a)) (exists ((?v2 Com$)) (= ?v0 (fun_upd$g uve$ ?v1 (some$ ?v2)))))) :named a292)) +(assert (! (forall ((?v0 (-> Com_option$ State_triple_option$)) (?v1 Com_option$)) (= (= (dom$f ?v0) (set.insert$d ?v1 bot$b)) (exists ((?v2 State_triple$)) (= ?v0 (fun_upd$h uvf$ ?v1 (some$a ?v2)))))) :named a293)) +(assert (! (forall ((?v0 (-> Com_option$ Com_option$)) (?v1 Com_option$)) (= (= (dom$g ?v0) (set.insert$d ?v1 bot$b)) (exists ((?v2 Com$)) (= ?v0 (fun_upd$i uvg$ ?v1 (some$ ?v2)))))) :named a294)) +(assert (! (forall ((?v0 (-> Pname$ Com_option$)) (?v1 Pname$)) (= (= (dom$h ?v0) (set.insert$b ?v1 bot$)) (exists ((?v2 Com$)) (= ?v0 (fun_upd$a uuz$ ?v1 (some$ ?v2)))))) :named a295)) +(assert (! (forall ((?v0 (-> State_triple$ Com_option$)) (?v1 State_triple$)) (= (= (dom$i ?v0) (set.insert$ ?v1 bot$d)) (exists ((?v2 Com$)) (= ?v0 (fun_upd$ uuy$ ?v1 (some$ ?v2)))))) :named a296)) (assert (! (forall ((?v0 (-> State_triple$ Com_option$)) (?v1 (-> State_triple$ Com_option$)) (?v2 State_triple$) (?v3 Com$)) (=> (map_le$ ?v0 ?v1) (map_le$ (fun_upd$ ?v0 ?v2 none$) (fun_upd$ ?v1 ?v2 (some$ ?v3))))) :named a297)) (assert (! (forall ((?v0 (-> Pname$ Com_option$)) (?v1 (-> Pname$ Com_option$)) (?v2 Pname$) (?v3 Com$)) (=> (map_le$a ?v0 ?v1) (map_le$a (fun_upd$a ?v0 ?v2 none$) (fun_upd$a ?v1 ?v2 (some$ ?v3))))) :named a298)) (assert (! (forall ((?v0 (-> State_triple$ State_triple_option$))) (= (= (dom$ ?v0) bot$d) (= ?v0 uva$))) :named a299)) @@ -525,27 +525,27 @@ (assert (! (= (dom$h uuz$) bot$) :named a317)) (assert (! (= (dom$i uuy$) bot$d) :named a318)) (assert (! (finite$ (dom$h body$)) :named a319)) -(assert (! (forall ((?v0 Com$) (?v1 (-> Com$ Com_option$))) (= (member$b ?v0 (dom$b ?v1)) (not (= (?v1 ?v0) none$)))) :named a320)) -(assert (! (forall ((?v0 State_triple$) (?v1 (-> State_triple$ Com_option$))) (= (member$ ?v0 (dom$i ?v1)) (not (= (?v1 ?v0) none$)))) :named a321)) -(assert (! (forall ((?v0 Com$) (?v1 (-> Com$ State_triple_option$))) (= (member$b ?v0 (dom$a ?v1)) (not (= (?v1 ?v0) none$a)))) :named a322)) -(assert (! (forall ((?v0 Pname$) (?v1 (-> Pname$ State_triple_option$))) (= (member$a ?v0 (dom$c ?v1)) (not (= (?v1 ?v0) none$a)))) :named a323)) -(assert (! (forall ((?v0 State_triple$) (?v1 (-> State_triple$ State_triple_option$))) (= (member$ ?v0 (dom$ ?v1)) (not (= (?v1 ?v0) none$a)))) :named a324)) -(assert (! (forall ((?v0 Pname$) (?v1 (-> Pname$ Com_option$))) (= (member$a ?v0 (dom$h ?v1)) (not (= (?v1 ?v0) none$)))) :named a325)) +(assert (! (forall ((?v0 Com$) (?v1 (-> Com$ Com_option$))) (= (set.member$b ?v0 (dom$b ?v1)) (not (= (?v1 ?v0) none$)))) :named a320)) +(assert (! (forall ((?v0 State_triple$) (?v1 (-> State_triple$ Com_option$))) (= (set.member$ ?v0 (dom$i ?v1)) (not (= (?v1 ?v0) none$)))) :named a321)) +(assert (! (forall ((?v0 Com$) (?v1 (-> Com$ State_triple_option$))) (= (set.member$b ?v0 (dom$a ?v1)) (not (= (?v1 ?v0) none$a)))) :named a322)) +(assert (! (forall ((?v0 Pname$) (?v1 (-> Pname$ State_triple_option$))) (= (set.member$a ?v0 (dom$c ?v1)) (not (= (?v1 ?v0) none$a)))) :named a323)) +(assert (! (forall ((?v0 State_triple$) (?v1 (-> State_triple$ State_triple_option$))) (= (set.member$ ?v0 (dom$ ?v1)) (not (= (?v1 ?v0) none$a)))) :named a324)) +(assert (! (forall ((?v0 Pname$) (?v1 (-> Pname$ Com_option$))) (= (set.member$a ?v0 (dom$h ?v1)) (not (= (?v1 ?v0) none$)))) :named a325)) (assert (! (forall ((?v0 (-> State_triple$ Com_option$))) (= (dom$i ?v0) (collect$a (uvh$ ?v0)))) :named a326)) (assert (! (forall ((?v0 (-> Pname$ State_triple_option$))) (= (dom$c ?v0) (collect$b (uvi$ ?v0)))) :named a327)) (assert (! (forall ((?v0 (-> Pname$ Com_option$))) (= (dom$h ?v0) (collect$b (uvj$ ?v0)))) :named a328)) (assert (! (forall ((?v0 (-> State_triple$ Com_option$)) (?v1 State_triple$)) (map_le$ (fun_upd$ ?v0 ?v1 none$) ?v0)) :named a329)) (assert (! (forall ((?v0 (-> Pname$ Com_option$)) (?v1 Pname$)) (map_le$a (fun_upd$a ?v0 ?v1 none$) ?v0)) :named a330)) -(assert (! (forall ((?v0 (-> Com$ Com_option$)) (?v1 Com$) (?v2 Com_option$)) (= (dom$b (fun_upd$d ?v0 ?v1 ?v2)) (ite (= ?v2 none$) (minus$ (dom$b ?v0) (insert$a ?v1 bot$c)) (insert$a ?v1 (dom$b ?v0))))) :named a331)) -(assert (! (forall ((?v0 (-> Com$ State_triple_option$)) (?v1 Com$) (?v2 State_triple_option$)) (= (dom$a (fun_upd$c ?v0 ?v1 ?v2)) (ite (= ?v2 none$a) (minus$ (dom$a ?v0) (insert$a ?v1 bot$c)) (insert$a ?v1 (dom$a ?v0))))) :named a332)) -(assert (! (forall ((?v0 (-> State_triple_option$ Com_option$)) (?v1 State_triple_option$) (?v2 Com_option$)) (= (dom$e (fun_upd$g ?v0 ?v1 ?v2)) (ite (= ?v2 none$) (minus$a (dom$e ?v0) (insert$c ?v1 bot$a)) (insert$c ?v1 (dom$e ?v0))))) :named a333)) -(assert (! (forall ((?v0 (-> State_triple_option$ State_triple_option$)) (?v1 State_triple_option$) (?v2 State_triple_option$)) (= (dom$d (fun_upd$f ?v0 ?v1 ?v2)) (ite (= ?v2 none$a) (minus$a (dom$d ?v0) (insert$c ?v1 bot$a)) (insert$c ?v1 (dom$d ?v0))))) :named a334)) -(assert (! (forall ((?v0 (-> Com_option$ Com_option$)) (?v1 Com_option$) (?v2 Com_option$)) (= (dom$g (fun_upd$i ?v0 ?v1 ?v2)) (ite (= ?v2 none$) (minus$b (dom$g ?v0) (insert$d ?v1 bot$b)) (insert$d ?v1 (dom$g ?v0))))) :named a335)) -(assert (! (forall ((?v0 (-> Com_option$ State_triple_option$)) (?v1 Com_option$) (?v2 State_triple_option$)) (= (dom$f (fun_upd$h ?v0 ?v1 ?v2)) (ite (= ?v2 none$a) (minus$b (dom$f ?v0) (insert$d ?v1 bot$b)) (insert$d ?v1 (dom$f ?v0))))) :named a336)) -(assert (! (forall ((?v0 (-> State_triple$ State_triple_option$)) (?v1 State_triple$) (?v2 State_triple_option$)) (= (dom$ (fun_upd$b ?v0 ?v1 ?v2)) (ite (= ?v2 none$a) (minus$c (dom$ ?v0) (insert$ ?v1 bot$d)) (insert$ ?v1 (dom$ ?v0))))) :named a337)) -(assert (! (forall ((?v0 (-> Pname$ State_triple_option$)) (?v1 Pname$) (?v2 State_triple_option$)) (= (dom$c (fun_upd$e ?v0 ?v1 ?v2)) (ite (= ?v2 none$a) (minus$d (dom$c ?v0) (insert$b ?v1 bot$)) (insert$b ?v1 (dom$c ?v0))))) :named a338)) -(assert (! (forall ((?v0 (-> Pname$ Com_option$)) (?v1 Pname$) (?v2 Com_option$)) (= (dom$h (fun_upd$a ?v0 ?v1 ?v2)) (ite (= ?v2 none$) (minus$d (dom$h ?v0) (insert$b ?v1 bot$)) (insert$b ?v1 (dom$h ?v0))))) :named a339)) -(assert (! (forall ((?v0 (-> State_triple$ Com_option$)) (?v1 State_triple$) (?v2 Com_option$)) (= (dom$i (fun_upd$ ?v0 ?v1 ?v2)) (ite (= ?v2 none$) (minus$c (dom$i ?v0) (insert$ ?v1 bot$d)) (insert$ ?v1 (dom$i ?v0))))) :named a340)) +(assert (! (forall ((?v0 (-> Com$ Com_option$)) (?v1 Com$) (?v2 Com_option$)) (= (dom$b (fun_upd$d ?v0 ?v1 ?v2)) (ite (= ?v2 none$) (minus$ (dom$b ?v0) (set.insert$a ?v1 bot$c)) (set.insert$a ?v1 (dom$b ?v0))))) :named a331)) +(assert (! (forall ((?v0 (-> Com$ State_triple_option$)) (?v1 Com$) (?v2 State_triple_option$)) (= (dom$a (fun_upd$c ?v0 ?v1 ?v2)) (ite (= ?v2 none$a) (minus$ (dom$a ?v0) (set.insert$a ?v1 bot$c)) (set.insert$a ?v1 (dom$a ?v0))))) :named a332)) +(assert (! (forall ((?v0 (-> State_triple_option$ Com_option$)) (?v1 State_triple_option$) (?v2 Com_option$)) (= (dom$e (fun_upd$g ?v0 ?v1 ?v2)) (ite (= ?v2 none$) (minus$a (dom$e ?v0) (set.insert$c ?v1 bot$a)) (set.insert$c ?v1 (dom$e ?v0))))) :named a333)) +(assert (! (forall ((?v0 (-> State_triple_option$ State_triple_option$)) (?v1 State_triple_option$) (?v2 State_triple_option$)) (= (dom$d (fun_upd$f ?v0 ?v1 ?v2)) (ite (= ?v2 none$a) (minus$a (dom$d ?v0) (set.insert$c ?v1 bot$a)) (set.insert$c ?v1 (dom$d ?v0))))) :named a334)) +(assert (! (forall ((?v0 (-> Com_option$ Com_option$)) (?v1 Com_option$) (?v2 Com_option$)) (= (dom$g (fun_upd$i ?v0 ?v1 ?v2)) (ite (= ?v2 none$) (minus$b (dom$g ?v0) (set.insert$d ?v1 bot$b)) (set.insert$d ?v1 (dom$g ?v0))))) :named a335)) +(assert (! (forall ((?v0 (-> Com_option$ State_triple_option$)) (?v1 Com_option$) (?v2 State_triple_option$)) (= (dom$f (fun_upd$h ?v0 ?v1 ?v2)) (ite (= ?v2 none$a) (minus$b (dom$f ?v0) (set.insert$d ?v1 bot$b)) (set.insert$d ?v1 (dom$f ?v0))))) :named a336)) +(assert (! (forall ((?v0 (-> State_triple$ State_triple_option$)) (?v1 State_triple$) (?v2 State_triple_option$)) (= (dom$ (fun_upd$b ?v0 ?v1 ?v2)) (ite (= ?v2 none$a) (minus$c (dom$ ?v0) (set.insert$ ?v1 bot$d)) (set.insert$ ?v1 (dom$ ?v0))))) :named a337)) +(assert (! (forall ((?v0 (-> Pname$ State_triple_option$)) (?v1 Pname$) (?v2 State_triple_option$)) (= (dom$c (fun_upd$e ?v0 ?v1 ?v2)) (ite (= ?v2 none$a) (minus$d (dom$c ?v0) (set.insert$b ?v1 bot$)) (set.insert$b ?v1 (dom$c ?v0))))) :named a338)) +(assert (! (forall ((?v0 (-> Pname$ Com_option$)) (?v1 Pname$) (?v2 Com_option$)) (= (dom$h (fun_upd$a ?v0 ?v1 ?v2)) (ite (= ?v2 none$) (minus$d (dom$h ?v0) (set.insert$b ?v1 bot$)) (set.insert$b ?v1 (dom$h ?v0))))) :named a339)) +(assert (! (forall ((?v0 (-> State_triple$ Com_option$)) (?v1 State_triple$) (?v2 Com_option$)) (= (dom$i (fun_upd$ ?v0 ?v1 ?v2)) (ite (= ?v2 none$) (minus$c (dom$i ?v0) (set.insert$ ?v1 bot$d)) (set.insert$ ?v1 (dom$i ?v0))))) :named a340)) (assert (! (forall ((?v0 (-> Com$ Com$)) (?v1 Com_option$)) (= (map_option$ ?v0 ?v1) (case_option$b none$ (uvk$ ?v0) ?v1))) :named a341)) (assert (! (forall ((?v0 (-> State_triple$ Com$)) (?v1 State_triple_option$)) (= (= (map_option$a ?v0 ?v1) none$) (= ?v1 none$a))) :named a342)) (assert (! (forall ((?v0 (-> Com$ State_triple$)) (?v1 Com_option$)) (= (= (map_option$b ?v0 ?v1) none$a) (= ?v1 none$))) :named a343)) @@ -565,42 +565,42 @@ (assert (! (forall ((?v0 (-> Com$ Com$))) (! (= (map_option$ ?v0 none$) none$) :pattern ((map_option$ ?v0)))) :named a357)) (assert (! (forall ((?v0 State_triple_option$) (?v1 (-> State_triple$ Com$))) (=> (not (= ?v0 none$a)) (= (the$ (map_option$a ?v1 ?v0)) (?v1 (the$a ?v0))))) :named a358)) (assert (! (forall ((?v0 Com_option$) (?v1 (-> Com$ Com$))) (=> (not (= ?v0 none$)) (= (the$ (map_option$ ?v1 ?v0)) (?v1 (the$ ?v0))))) :named a359)) -(assert (! (forall ((?v0 (-> State_triple_option$ Com_option$)) (?v1 State_triple_option$) (?v2 State_triple_option_set$)) (=> (= (?v0 ?v1) none$) (= (minus$a (dom$e ?v0) (insert$c ?v1 ?v2)) (minus$a (dom$e ?v0) ?v2)))) :named a360)) -(assert (! (forall ((?v0 (-> Com_option$ Com_option$)) (?v1 Com_option$) (?v2 Com_option_set$)) (=> (= (?v0 ?v1) none$) (= (minus$b (dom$g ?v0) (insert$d ?v1 ?v2)) (minus$b (dom$g ?v0) ?v2)))) :named a361)) -(assert (! (forall ((?v0 (-> State_triple_option$ State_triple_option$)) (?v1 State_triple_option$) (?v2 State_triple_option_set$)) (=> (= (?v0 ?v1) none$a) (= (minus$a (dom$d ?v0) (insert$c ?v1 ?v2)) (minus$a (dom$d ?v0) ?v2)))) :named a362)) -(assert (! (forall ((?v0 (-> Com_option$ State_triple_option$)) (?v1 Com_option$) (?v2 Com_option_set$)) (=> (= (?v0 ?v1) none$a) (= (minus$b (dom$f ?v0) (insert$d ?v1 ?v2)) (minus$b (dom$f ?v0) ?v2)))) :named a363)) -(assert (! (forall ((?v0 (-> State_triple$ State_triple_option$)) (?v1 State_triple$) (?v2 State_triple_set$)) (=> (= (?v0 ?v1) none$a) (= (minus$c (dom$ ?v0) (insert$ ?v1 ?v2)) (minus$c (dom$ ?v0) ?v2)))) :named a364)) -(assert (! (forall ((?v0 (-> Pname$ State_triple_option$)) (?v1 Pname$) (?v2 Pname_set$)) (=> (= (?v0 ?v1) none$a) (= (minus$d (dom$c ?v0) (insert$b ?v1 ?v2)) (minus$d (dom$c ?v0) ?v2)))) :named a365)) -(assert (! (forall ((?v0 (-> Pname$ Com_option$)) (?v1 Pname$) (?v2 Pname_set$)) (=> (= (?v0 ?v1) none$) (= (minus$d (dom$h ?v0) (insert$b ?v1 ?v2)) (minus$d (dom$h ?v0) ?v2)))) :named a366)) -(assert (! (forall ((?v0 (-> State_triple$ Com_option$)) (?v1 State_triple$) (?v2 State_triple_set$)) (=> (= (?v0 ?v1) none$) (= (minus$c (dom$i ?v0) (insert$ ?v1 ?v2)) (minus$c (dom$i ?v0) ?v2)))) :named a367)) -(assert (! (forall ((?v0 (-> Com$ Com_option$)) (?v1 Com_set$) (?v2 Com$)) (= (fun_upd$d (restrict_map$ ?v0 ?v1) ?v2 none$) (ite (member$b ?v2 ?v1) (restrict_map$ ?v0 (minus$ ?v1 (insert$a ?v2 bot$c))) (restrict_map$ ?v0 ?v1)))) :named a368)) -(assert (! (forall ((?v0 (-> Com$ State_triple_option$)) (?v1 Com_set$) (?v2 Com$)) (= (fun_upd$c (restrict_map$a ?v0 ?v1) ?v2 none$a) (ite (member$b ?v2 ?v1) (restrict_map$a ?v0 (minus$ ?v1 (insert$a ?v2 bot$c))) (restrict_map$a ?v0 ?v1)))) :named a369)) -(assert (! (forall ((?v0 (-> State_triple_option$ Com_option$)) (?v1 State_triple_option_set$) (?v2 State_triple_option$)) (= (fun_upd$g (restrict_map$b ?v0 ?v1) ?v2 none$) (ite (member$c ?v2 ?v1) (restrict_map$b ?v0 (minus$a ?v1 (insert$c ?v2 bot$a))) (restrict_map$b ?v0 ?v1)))) :named a370)) -(assert (! (forall ((?v0 (-> State_triple_option$ State_triple_option$)) (?v1 State_triple_option_set$) (?v2 State_triple_option$)) (= (fun_upd$f (restrict_map$c ?v0 ?v1) ?v2 none$a) (ite (member$c ?v2 ?v1) (restrict_map$c ?v0 (minus$a ?v1 (insert$c ?v2 bot$a))) (restrict_map$c ?v0 ?v1)))) :named a371)) -(assert (! (forall ((?v0 (-> Com_option$ Com_option$)) (?v1 Com_option_set$) (?v2 Com_option$)) (= (fun_upd$i (restrict_map$d ?v0 ?v1) ?v2 none$) (ite (member$d ?v2 ?v1) (restrict_map$d ?v0 (minus$b ?v1 (insert$d ?v2 bot$b))) (restrict_map$d ?v0 ?v1)))) :named a372)) -(assert (! (forall ((?v0 (-> Com_option$ State_triple_option$)) (?v1 Com_option_set$) (?v2 Com_option$)) (= (fun_upd$h (restrict_map$e ?v0 ?v1) ?v2 none$a) (ite (member$d ?v2 ?v1) (restrict_map$e ?v0 (minus$b ?v1 (insert$d ?v2 bot$b))) (restrict_map$e ?v0 ?v1)))) :named a373)) -(assert (! (forall ((?v0 (-> State_triple$ State_triple_option$)) (?v1 State_triple_set$) (?v2 State_triple$)) (= (fun_upd$b (restrict_map$f ?v0 ?v1) ?v2 none$a) (ite (member$ ?v2 ?v1) (restrict_map$f ?v0 (minus$c ?v1 (insert$ ?v2 bot$d))) (restrict_map$f ?v0 ?v1)))) :named a374)) -(assert (! (forall ((?v0 (-> Pname$ Com_option$)) (?v1 Pname_set$) (?v2 Pname$)) (= (fun_upd$a (restrict_map$g ?v0 ?v1) ?v2 none$) (ite (member$a ?v2 ?v1) (restrict_map$g ?v0 (minus$d ?v1 (insert$b ?v2 bot$))) (restrict_map$g ?v0 ?v1)))) :named a375)) -(assert (! (forall ((?v0 (-> Pname$ State_triple_option$)) (?v1 Pname_set$) (?v2 Pname$)) (= (fun_upd$e (restrict_map$h ?v0 ?v1) ?v2 none$a) (ite (member$a ?v2 ?v1) (restrict_map$h ?v0 (minus$d ?v1 (insert$b ?v2 bot$))) (restrict_map$h ?v0 ?v1)))) :named a376)) -(assert (! (forall ((?v0 (-> State_triple$ Com_option$)) (?v1 State_triple_set$) (?v2 State_triple$)) (= (fun_upd$ (restrict_map$i ?v0 ?v1) ?v2 none$) (ite (member$ ?v2 ?v1) (restrict_map$i ?v0 (minus$c ?v1 (insert$ ?v2 bot$d))) (restrict_map$i ?v0 ?v1)))) :named a377)) -(assert (! (forall ((?v0 Pname_option_set$)) (= (not (= (these$ ?v0) bot$)) (and (not (= ?v0 bot$e)) (not (= ?v0 (insert$e none$b bot$e)))))) :named a378)) -(assert (! (forall ((?v0 State_triple_option_option_set$)) (= (not (= (these$a ?v0) bot$a)) (and (not (= ?v0 bot$f)) (not (= ?v0 (insert$f none$c bot$f)))))) :named a379)) -(assert (! (forall ((?v0 Com_option_option_set$)) (= (not (= (these$b ?v0) bot$b)) (and (not (= ?v0 bot$g)) (not (= ?v0 (insert$g none$d bot$g)))))) :named a380)) -(assert (! (forall ((?v0 Com_option_set$)) (= (not (= (these$c ?v0) bot$c)) (and (not (= ?v0 bot$b)) (not (= ?v0 (insert$d none$ bot$b)))))) :named a381)) -(assert (! (forall ((?v0 State_triple_option_set$)) (= (not (= (these$d ?v0) bot$d)) (and (not (= ?v0 bot$a)) (not (= ?v0 (insert$c none$a bot$a)))))) :named a382)) -(assert (! (forall ((?v0 Com$) (?v1 Com_set$) (?v2 (-> Com$ Com_option$))) (! (=> (not (member$b ?v0 ?v1)) (= (restrict_map$ ?v2 ?v1 ?v0) none$)) :pattern ((restrict_map$ ?v2 ?v1 ?v0)))) :named a383)) -(assert (! (forall ((?v0 Pname$) (?v1 Pname_set$) (?v2 (-> Pname$ Com_option$))) (! (=> (not (member$a ?v0 ?v1)) (= (restrict_map$g ?v2 ?v1 ?v0) none$)) :pattern ((restrict_map$g ?v2 ?v1 ?v0)))) :named a384)) -(assert (! (forall ((?v0 State_triple$) (?v1 State_triple_set$) (?v2 (-> State_triple$ Com_option$))) (! (=> (not (member$ ?v0 ?v1)) (= (restrict_map$i ?v2 ?v1 ?v0) none$)) :pattern ((restrict_map$i ?v2 ?v1 ?v0)))) :named a385)) -(assert (! (forall ((?v0 Com$) (?v1 Com_set$) (?v2 (-> Com$ State_triple_option$))) (! (=> (not (member$b ?v0 ?v1)) (= (restrict_map$a ?v2 ?v1 ?v0) none$a)) :pattern ((restrict_map$a ?v2 ?v1 ?v0)))) :named a386)) -(assert (! (forall ((?v0 Pname$) (?v1 Pname_set$) (?v2 (-> Pname$ State_triple_option$))) (! (=> (not (member$a ?v0 ?v1)) (= (restrict_map$h ?v2 ?v1 ?v0) none$a)) :pattern ((restrict_map$h ?v2 ?v1 ?v0)))) :named a387)) -(assert (! (forall ((?v0 State_triple$) (?v1 State_triple_set$) (?v2 (-> State_triple$ State_triple_option$))) (! (=> (not (member$ ?v0 ?v1)) (= (restrict_map$f ?v2 ?v1 ?v0) none$a)) :pattern ((restrict_map$f ?v2 ?v1 ?v0)))) :named a388)) +(assert (! (forall ((?v0 (-> State_triple_option$ Com_option$)) (?v1 State_triple_option$) (?v2 State_triple_option_set$)) (=> (= (?v0 ?v1) none$) (= (minus$a (dom$e ?v0) (set.insert$c ?v1 ?v2)) (minus$a (dom$e ?v0) ?v2)))) :named a360)) +(assert (! (forall ((?v0 (-> Com_option$ Com_option$)) (?v1 Com_option$) (?v2 Com_option_set$)) (=> (= (?v0 ?v1) none$) (= (minus$b (dom$g ?v0) (set.insert$d ?v1 ?v2)) (minus$b (dom$g ?v0) ?v2)))) :named a361)) +(assert (! (forall ((?v0 (-> State_triple_option$ State_triple_option$)) (?v1 State_triple_option$) (?v2 State_triple_option_set$)) (=> (= (?v0 ?v1) none$a) (= (minus$a (dom$d ?v0) (set.insert$c ?v1 ?v2)) (minus$a (dom$d ?v0) ?v2)))) :named a362)) +(assert (! (forall ((?v0 (-> Com_option$ State_triple_option$)) (?v1 Com_option$) (?v2 Com_option_set$)) (=> (= (?v0 ?v1) none$a) (= (minus$b (dom$f ?v0) (set.insert$d ?v1 ?v2)) (minus$b (dom$f ?v0) ?v2)))) :named a363)) +(assert (! (forall ((?v0 (-> State_triple$ State_triple_option$)) (?v1 State_triple$) (?v2 State_triple_set$)) (=> (= (?v0 ?v1) none$a) (= (minus$c (dom$ ?v0) (set.insert$ ?v1 ?v2)) (minus$c (dom$ ?v0) ?v2)))) :named a364)) +(assert (! (forall ((?v0 (-> Pname$ State_triple_option$)) (?v1 Pname$) (?v2 Pname_set$)) (=> (= (?v0 ?v1) none$a) (= (minus$d (dom$c ?v0) (set.insert$b ?v1 ?v2)) (minus$d (dom$c ?v0) ?v2)))) :named a365)) +(assert (! (forall ((?v0 (-> Pname$ Com_option$)) (?v1 Pname$) (?v2 Pname_set$)) (=> (= (?v0 ?v1) none$) (= (minus$d (dom$h ?v0) (set.insert$b ?v1 ?v2)) (minus$d (dom$h ?v0) ?v2)))) :named a366)) +(assert (! (forall ((?v0 (-> State_triple$ Com_option$)) (?v1 State_triple$) (?v2 State_triple_set$)) (=> (= (?v0 ?v1) none$) (= (minus$c (dom$i ?v0) (set.insert$ ?v1 ?v2)) (minus$c (dom$i ?v0) ?v2)))) :named a367)) +(assert (! (forall ((?v0 (-> Com$ Com_option$)) (?v1 Com_set$) (?v2 Com$)) (= (fun_upd$d (restrict_map$ ?v0 ?v1) ?v2 none$) (ite (set.member$b ?v2 ?v1) (restrict_map$ ?v0 (minus$ ?v1 (set.insert$a ?v2 bot$c))) (restrict_map$ ?v0 ?v1)))) :named a368)) +(assert (! (forall ((?v0 (-> Com$ State_triple_option$)) (?v1 Com_set$) (?v2 Com$)) (= (fun_upd$c (restrict_map$a ?v0 ?v1) ?v2 none$a) (ite (set.member$b ?v2 ?v1) (restrict_map$a ?v0 (minus$ ?v1 (set.insert$a ?v2 bot$c))) (restrict_map$a ?v0 ?v1)))) :named a369)) +(assert (! (forall ((?v0 (-> State_triple_option$ Com_option$)) (?v1 State_triple_option_set$) (?v2 State_triple_option$)) (= (fun_upd$g (restrict_map$b ?v0 ?v1) ?v2 none$) (ite (set.member$c ?v2 ?v1) (restrict_map$b ?v0 (minus$a ?v1 (set.insert$c ?v2 bot$a))) (restrict_map$b ?v0 ?v1)))) :named a370)) +(assert (! (forall ((?v0 (-> State_triple_option$ State_triple_option$)) (?v1 State_triple_option_set$) (?v2 State_triple_option$)) (= (fun_upd$f (restrict_map$c ?v0 ?v1) ?v2 none$a) (ite (set.member$c ?v2 ?v1) (restrict_map$c ?v0 (minus$a ?v1 (set.insert$c ?v2 bot$a))) (restrict_map$c ?v0 ?v1)))) :named a371)) +(assert (! (forall ((?v0 (-> Com_option$ Com_option$)) (?v1 Com_option_set$) (?v2 Com_option$)) (= (fun_upd$i (restrict_map$d ?v0 ?v1) ?v2 none$) (ite (set.member$d ?v2 ?v1) (restrict_map$d ?v0 (minus$b ?v1 (set.insert$d ?v2 bot$b))) (restrict_map$d ?v0 ?v1)))) :named a372)) +(assert (! (forall ((?v0 (-> Com_option$ State_triple_option$)) (?v1 Com_option_set$) (?v2 Com_option$)) (= (fun_upd$h (restrict_map$e ?v0 ?v1) ?v2 none$a) (ite (set.member$d ?v2 ?v1) (restrict_map$e ?v0 (minus$b ?v1 (set.insert$d ?v2 bot$b))) (restrict_map$e ?v0 ?v1)))) :named a373)) +(assert (! (forall ((?v0 (-> State_triple$ State_triple_option$)) (?v1 State_triple_set$) (?v2 State_triple$)) (= (fun_upd$b (restrict_map$f ?v0 ?v1) ?v2 none$a) (ite (set.member$ ?v2 ?v1) (restrict_map$f ?v0 (minus$c ?v1 (set.insert$ ?v2 bot$d))) (restrict_map$f ?v0 ?v1)))) :named a374)) +(assert (! (forall ((?v0 (-> Pname$ Com_option$)) (?v1 Pname_set$) (?v2 Pname$)) (= (fun_upd$a (restrict_map$g ?v0 ?v1) ?v2 none$) (ite (set.member$a ?v2 ?v1) (restrict_map$g ?v0 (minus$d ?v1 (set.insert$b ?v2 bot$))) (restrict_map$g ?v0 ?v1)))) :named a375)) +(assert (! (forall ((?v0 (-> Pname$ State_triple_option$)) (?v1 Pname_set$) (?v2 Pname$)) (= (fun_upd$e (restrict_map$h ?v0 ?v1) ?v2 none$a) (ite (set.member$a ?v2 ?v1) (restrict_map$h ?v0 (minus$d ?v1 (set.insert$b ?v2 bot$))) (restrict_map$h ?v0 ?v1)))) :named a376)) +(assert (! (forall ((?v0 (-> State_triple$ Com_option$)) (?v1 State_triple_set$) (?v2 State_triple$)) (= (fun_upd$ (restrict_map$i ?v0 ?v1) ?v2 none$) (ite (set.member$ ?v2 ?v1) (restrict_map$i ?v0 (minus$c ?v1 (set.insert$ ?v2 bot$d))) (restrict_map$i ?v0 ?v1)))) :named a377)) +(assert (! (forall ((?v0 Pname_option_set$)) (= (not (= (these$ ?v0) bot$)) (and (not (= ?v0 bot$e)) (not (= ?v0 (set.insert$e none$b bot$e)))))) :named a378)) +(assert (! (forall ((?v0 State_triple_option_option_set$)) (= (not (= (these$a ?v0) bot$a)) (and (not (= ?v0 bot$f)) (not (= ?v0 (set.insert$f none$c bot$f)))))) :named a379)) +(assert (! (forall ((?v0 Com_option_option_set$)) (= (not (= (these$b ?v0) bot$b)) (and (not (= ?v0 bot$g)) (not (= ?v0 (set.insert$g none$d bot$g)))))) :named a380)) +(assert (! (forall ((?v0 Com_option_set$)) (= (not (= (these$c ?v0) bot$c)) (and (not (= ?v0 bot$b)) (not (= ?v0 (set.insert$d none$ bot$b)))))) :named a381)) +(assert (! (forall ((?v0 State_triple_option_set$)) (= (not (= (these$d ?v0) bot$d)) (and (not (= ?v0 bot$a)) (not (= ?v0 (set.insert$c none$a bot$a)))))) :named a382)) +(assert (! (forall ((?v0 Com$) (?v1 Com_set$) (?v2 (-> Com$ Com_option$))) (! (=> (not (set.member$b ?v0 ?v1)) (= (restrict_map$ ?v2 ?v1 ?v0) none$)) :pattern ((restrict_map$ ?v2 ?v1 ?v0)))) :named a383)) +(assert (! (forall ((?v0 Pname$) (?v1 Pname_set$) (?v2 (-> Pname$ Com_option$))) (! (=> (not (set.member$a ?v0 ?v1)) (= (restrict_map$g ?v2 ?v1 ?v0) none$)) :pattern ((restrict_map$g ?v2 ?v1 ?v0)))) :named a384)) +(assert (! (forall ((?v0 State_triple$) (?v1 State_triple_set$) (?v2 (-> State_triple$ Com_option$))) (! (=> (not (set.member$ ?v0 ?v1)) (= (restrict_map$i ?v2 ?v1 ?v0) none$)) :pattern ((restrict_map$i ?v2 ?v1 ?v0)))) :named a385)) +(assert (! (forall ((?v0 Com$) (?v1 Com_set$) (?v2 (-> Com$ State_triple_option$))) (! (=> (not (set.member$b ?v0 ?v1)) (= (restrict_map$a ?v2 ?v1 ?v0) none$a)) :pattern ((restrict_map$a ?v2 ?v1 ?v0)))) :named a386)) +(assert (! (forall ((?v0 Pname$) (?v1 Pname_set$) (?v2 (-> Pname$ State_triple_option$))) (! (=> (not (set.member$a ?v0 ?v1)) (= (restrict_map$h ?v2 ?v1 ?v0) none$a)) :pattern ((restrict_map$h ?v2 ?v1 ?v0)))) :named a387)) +(assert (! (forall ((?v0 State_triple$) (?v1 State_triple_set$) (?v2 (-> State_triple$ State_triple_option$))) (! (=> (not (set.member$ ?v0 ?v1)) (= (restrict_map$f ?v2 ?v1 ?v0) none$a)) :pattern ((restrict_map$f ?v2 ?v1 ?v0)))) :named a388)) (assert (! (forall ((?v0 State_triple_set$) (?v1 State_triple$)) (= (restrict_map$i uuy$ ?v0 ?v1) none$)) :named a389)) (assert (! (forall ((?v0 (-> Com_option$ Com_option$)) (?v1 Com_option$)) (= (restrict_map$d ?v0 bot$b ?v1) none$)) :named a390)) (assert (! (forall ((?v0 (-> Com_option$ State_triple_option$)) (?v1 Com_option$)) (= (restrict_map$e ?v0 bot$b ?v1) none$a)) :named a391)) (assert (! (forall ((?v0 (-> State_triple$ Com_option$)) (?v1 State_triple$)) (= (restrict_map$i ?v0 bot$d ?v1) none$)) :named a392)) -(assert (! (forall ((?v0 Com_option_set$)) (= (these$c (insert$d none$ ?v0)) (these$c ?v0))) :named a393)) -(assert (! (forall ((?v0 Com_option_set$)) (= (= (these$c ?v0) bot$c) (or (= ?v0 bot$b) (= ?v0 (insert$d none$ bot$b))))) :named a394)) -(assert (! (forall ((?v0 State_triple_option_set$)) (= (= (these$d ?v0) bot$d) (or (= ?v0 bot$a) (= ?v0 (insert$c none$a bot$a))))) :named a395)) -(assert (! (forall ((?v0 (-> State_triple$ Com_option$)) (?v1 State_triple$)) (= (restrict_map$i ?v0 (uminus$ (insert$ ?v1 bot$d))) (fun_upd$ ?v0 ?v1 none$))) :named a396)) +(assert (! (forall ((?v0 Com_option_set$)) (= (these$c (set.insert$d none$ ?v0)) (these$c ?v0))) :named a393)) +(assert (! (forall ((?v0 Com_option_set$)) (= (= (these$c ?v0) bot$c) (or (= ?v0 bot$b) (= ?v0 (set.insert$d none$ bot$b))))) :named a394)) +(assert (! (forall ((?v0 State_triple_option_set$)) (= (= (these$d ?v0) bot$d) (or (= ?v0 bot$a) (= ?v0 (set.insert$c none$a bot$a))))) :named a395)) +(assert (! (forall ((?v0 (-> State_triple$ Com_option$)) (?v1 State_triple$)) (= (restrict_map$i ?v0 (uminus$ (set.insert$ ?v1 bot$d))) (fun_upd$ ?v0 ?v1 none$))) :named a396)) (check-sat) ;(get-proof) |