diff options
Diffstat (limited to 'test/regress/regress0/ho/hoa0102.smt2')
| -rw-r--r-- | test/regress/regress0/ho/hoa0102.smt2 | 606 |
1 files changed, 0 insertions, 606 deletions
diff --git a/test/regress/regress0/ho/hoa0102.smt2 b/test/regress/regress0/ho/hoa0102.smt2 deleted file mode 100644 index 6be063783..000000000 --- a/test/regress/regress0/ho/hoa0102.smt2 +++ /dev/null @@ -1,606 +0,0 @@ -; COMMAND-LINE: --uf-ho --full-saturate-quant -; EXPECT: unsat -(set-logic ALL) -(set-info :status unsat) -(declare-sort Com$ 0) -(declare-sort Glb$ 0) -(declare-sort Loc$ 0) -(declare-sort Nat$ 0) -(declare-sort Pname$ 0) -(declare-sort State$ 0) -(declare-sort Vname$ 0) -(declare-sort Com_set$ 0) -(declare-sort Pname_set$ 0) -(declare-sort Com_option$ 0) -(declare-sort Pname_option$ 0) -(declare-sort State_triple$ 0) -(declare-sort Com_option_set$ 0) -(declare-sort Pname_option_set$ 0) -(declare-sort State_triple_set$ 0) -(declare-sort Com_option_option$ 0) -(declare-sort State_triple_option$ 0) -(declare-sort Com_option_option_set$ 0) -(declare-sort State_triple_option_set$ 0) -(declare-sort State_triple_option_option$ 0) -(declare-sort State_triple_option_option_set$ 0) -(declare-fun c$ () Com$) -(declare-fun s$ () State$) -(declare-fun z$ () State$) -(declare-fun uu$ (Com_set$ Com$) Bool) -(declare-fun wt$ (Com$) Bool) -(declare-fun arg$ () Loc$) -(declare-fun ass$ (Vname$ (-> State$ Nat$)) Com$) -(declare-fun bot$ () Pname_set$) -(declare-fun dom$ ((-> State_triple$ State_triple_option$)) State_triple_set$) -(declare-fun glb$ (Glb$) Vname$) -(declare-fun loc$ (Loc$) Vname$) -(declare-fun mgt$ (Com$) State_triple$) -(declare-fun ran$ ((-> State_triple$ Com_option$)) Com_set$) -(declare-fun res$ () Loc$) -(declare-fun suc$ (Nat$) Nat$) -(declare-fun sup$ (State_triple_set$ State_triple_set$) State_triple_set$) -(declare-fun the$ (Com_option$) Com$) -(declare-fun uua$ (State_triple_set$ State_triple$) Bool) -(declare-fun uub$ (Pname_set$ Pname$) Bool) -(declare-fun uuc$ ((-> State$ (-> State$ Bool)) State$ Vname$ State$ State$) Bool) -(declare-fun uud$ ((-> State$ (-> State$ Bool)) State$ (-> State$ Nat$) State$ State$) Bool) -(declare-fun uue$ (Com$) Com_option$) -(declare-fun uuf$ (State_triple$) Bool) -(declare-fun uug$ (Com$) Bool) -(declare-fun uuh$ (State_triple$) Bool) -(declare-fun uui$ (Com$) Bool) -(declare-fun uuj$ ((-> State$ (-> State$ Bool)) Loc$ State$ State$ State$) Bool) -(declare-fun uuk$ ((-> State$ (-> State$ Bool)) Loc$ State$ (-> State$ Nat$) State$ State$) Bool) -(declare-fun uul$ ((-> State$ (-> State$ Bool)) (-> State$ Bool) State$ State$) Bool) -(declare-fun uum$ (Bool (-> State$ (-> State$ Bool)) State$ State$) Bool) -(declare-fun uun$ (State$ State$ State$) Bool) -(declare-fun uuo$ ((-> State$ (-> State$ Bool)) State$ State$) (-> State$ Bool)) -(declare-fun uup$ ((-> State$ (-> State$ Bool)) Vname$ (-> State$ Nat$) State$ State$) Bool) -(declare-fun uuq$ (State$ State$) Bool) -(declare-fun uur$ ((-> Pname$ (-> State$ (-> State$ Bool))) (-> Pname$ (-> State$ (-> State$ Bool))) Pname$) State_triple$) -(declare-fun uus$ ((-> Pname$ (-> State$ (-> State$ Bool))) (-> Pname$ (-> State$ (-> State$ Bool))) Pname$) State_triple$) -(declare-fun uut$ (Bool) Bool) -(declare-fun uuu$ ((-> Pname$ (-> State$ (-> State$ Bool))) (-> Pname$ Com$) (-> Pname$ (-> State$ (-> State$ Bool))) Pname$) State_triple$) -(declare-fun uuv$ ((-> Pname$ Com$) (-> Pname$ (-> State$ (-> State$ Bool))) (-> Pname$ (-> State$ (-> State$ Bool))) Pname$) State_triple$) -(declare-fun uuw$ (Com$ State$ State$) Bool) -(declare-fun uux$ (Nat$ (-> State$ (-> State$ Bool)) Com$ (-> State$ (-> State$ Bool))) Bool) -(declare-fun uuy$ (State_triple$) Com_option$) -(declare-fun uuz$ (Pname$) Com_option$) -(declare-fun uva$ (State_triple$) State_triple_option$) -(declare-fun uvb$ (Com$) State_triple_option$) -(declare-fun uvc$ (Pname$) State_triple_option$) -(declare-fun uvd$ (State_triple_option$) State_triple_option$) -(declare-fun uve$ (State_triple_option$) Com_option$) -(declare-fun uvf$ (Com_option$) State_triple_option$) -(declare-fun uvg$ (Com_option$) Com_option$) -(declare-fun uvh$ ((-> State_triple$ Com_option$) State_triple$) Bool) -(declare-fun uvi$ ((-> Pname$ State_triple_option$) Pname$) Bool) -(declare-fun uvj$ ((-> Pname$ Com_option$) Pname$) Bool) -(declare-fun uvk$ ((-> Com$ Com$) Com$) Com_option$) -(declare-fun bind$ (State_triple_option$ (-> State_triple$ Com_option$)) Com_option$) -(declare-fun body$ (Pname$) Com_option$) -(declare-fun bot$a () State_triple_option_set$) -(declare-fun bot$b () Com_option_set$) -(declare-fun bot$c () Com_set$) -(declare-fun bot$d () State_triple_set$) -(declare-fun bot$e () Pname_option_set$) -(declare-fun bot$f () State_triple_option_option_set$) -(declare-fun bot$g () Com_option_option_set$) -(declare-fun call$ (Vname$ Pname$ (-> State$ Nat$)) Com$) -(declare-fun comp$ ((-> Bool Bool) (-> State$ Bool)) (-> State$ Bool)) -(declare-fun cond$ ((-> State$ Bool) Com$ Com$) Com$) -(declare-fun dom$a ((-> Com$ State_triple_option$)) Com_set$) -(declare-fun dom$b ((-> Com$ Com_option$)) Com_set$) -(declare-fun dom$c ((-> Pname$ State_triple_option$)) Pname_set$) -(declare-fun dom$d ((-> State_triple_option$ State_triple_option$)) State_triple_option_set$) -(declare-fun dom$e ((-> State_triple_option$ Com_option$)) State_triple_option_set$) -(declare-fun dom$f ((-> Com_option$ State_triple_option$)) Com_option_set$) -(declare-fun dom$g ((-> Com_option$ Com_option$)) Com_option_set$) -(declare-fun dom$h ((-> Pname$ Com_option$)) Pname_set$) -(declare-fun dom$i ((-> State_triple$ Com_option$)) State_triple_set$) -(declare-fun none$ () Com_option$) -(declare-fun plus$ (Nat$ Nat$) Nat$) -(declare-fun ran$a ((-> Pname$ Com_option$)) Com_set$) -(declare-fun semi$ (Com$ Com$) Com$) -(declare-fun size$ (State_triple$) Nat$) -(declare-fun skip$ () Com$) -(declare-fun some$ (Com$) Com_option$) -(declare-fun the$a (State_triple_option$) State_triple$) -(declare-fun the$b (Pname_option$) Pname$) -(declare-fun zero$ () Nat$) -(declare-fun bind$a (Com_option$ (-> Com$ State_triple_option$)) State_triple_option$) -(declare-fun bind$b (State_triple_option$ (-> State_triple$ State_triple_option$)) State_triple_option$) -(declare-fun bind$c (Com_option$ (-> Com$ Com_option$)) Com_option$) -(declare-fun body$a (Pname$) Com$) -(declare-fun evalc$ (Com$ State$ State$) Bool) -(declare-fun evaln$ (Com$ State$ Nat$ State$) Bool) -(declare-fun image$ ((-> Pname$ State_triple$) Pname_set$) State_triple_set$) -(declare-fun local$ (Loc$ (-> State$ Nat$) Com$) Com$) -(declare-fun minus$ (Com_set$ Com_set$) Com_set$) -(declare-fun none$a () State_triple_option$) -(declare-fun none$b () Pname_option$) -(declare-fun none$c () State_triple_option_option$) -(declare-fun none$d () Com_option_option$) -(declare-fun size$a (State_triple_option$) Nat$) -(declare-fun size$b (Com_option$) Nat$) -(declare-fun size$c (Vname$) Nat$) -(declare-fun size$d (Com$) Nat$) -(declare-fun some$a (State_triple$) State_triple_option$) -(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 map_le$ ((-> State_triple$ Com_option$) (-> State_triple$ Com_option$)) Bool) -(declare-fun 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$) -(declare-fun minus$d (Pname_set$ Pname_set$) Pname_set$) -(declare-fun these$a (State_triple_option_option_set$) State_triple_option_set$) -(declare-fun these$b (Com_option_option_set$) Com_option_set$) -(declare-fun these$c (Com_option_set$) Com_set$) -(declare-fun these$d (State_triple_option_set$) State_triple_set$) -(declare-fun triple$ ((-> State$ (-> State$ Bool)) Com$ (-> State$ (-> State$ Bool))) State_triple$) -(declare-fun uminus$ (State_triple_set$) State_triple_set$) -(declare-fun update$ (State$ Vname$ Nat$) State$) -(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 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 newlocs$ () (-> Loc$ Nat$)) -(declare-fun setlocs$ (State$ (-> Loc$ Nat$)) State$) -(declare-fun collect$a ((-> State_triple$ Bool)) State_triple_set$) -(declare-fun collect$b ((-> Pname$ Bool)) Pname_set$) -(declare-fun fun_upd$a ((-> Pname$ Com_option$) Pname$ Com_option$) (-> Pname$ Com_option$)) -(declare-fun fun_upd$b ((-> State_triple$ State_triple_option$) State_triple$ State_triple_option$) (-> State_triple$ State_triple_option$)) -(declare-fun fun_upd$c ((-> Com$ State_triple_option$) Com$ State_triple_option$) (-> Com$ State_triple_option$)) -(declare-fun fun_upd$d ((-> Com$ Com_option$) Com$ Com_option$) (-> Com$ Com_option$)) -(declare-fun fun_upd$e ((-> Pname$ State_triple_option$) Pname$ State_triple_option$) (-> Pname$ State_triple_option$)) -(declare-fun fun_upd$f ((-> State_triple_option$ State_triple_option$) State_triple_option$ State_triple_option$) (-> State_triple_option$ State_triple_option$)) -(declare-fun fun_upd$g ((-> State_triple_option$ Com_option$) State_triple_option$ Com_option$) (-> State_triple_option$ Com_option$)) -(declare-fun fun_upd$h ((-> Com_option$ State_triple_option$) Com_option$ State_triple_option$) (-> Com_option$ State_triple_option$)) -(declare-fun fun_upd$i ((-> Com_option$ Com_option$) Com_option$ Com_option$) (-> Com_option$ Com_option$)) -(declare-fun peek_and$ ((-> State$ (-> State$ Bool)) (-> State$ Bool)) (-> State$ (-> State$ Bool))) -(declare-fun size_com$ (Com$) Nat$) -(declare-fun wT_bodies$ () Bool) -(declare-fun map_option$ ((-> Com$ Com$) Com_option$) Com_option$) -(declare-fun set_option$ (Pname_option$) Pname_set$) -(declare-fun size_vname$ (Vname$) Nat$) -(declare-fun case_option$ (Bool (-> Com$ Bool) Com_option$) Bool) -(declare-fun case_triple$ ((-> (-> State$ (-> State$ Bool)) (-> Com$ (-> (-> State$ (-> State$ Bool)) Bool))) State_triple$) Bool) -(declare-fun map_option$a ((-> State_triple$ Com$) State_triple_option$) Com_option$) -(declare-fun map_option$b ((-> Com$ State_triple$) Com_option$) State_triple_option$) -(declare-fun map_option$c ((-> State_triple$ State_triple$) State_triple_option$) State_triple_option$) -(declare-fun set_option$a (State_triple_option$) State_triple_set$) -(declare-fun set_option$b (Com_option$) Com_set$) -(declare-fun set_option$c (State_triple_option_option$) State_triple_option_set$) -(declare-fun set_option$d (Com_option_option$) Com_option_set$) -(declare-fun size_option$ ((-> State_triple$ Nat$)) (-> State_triple_option$ Nat$)) -(declare-fun size_triple$ ((-> State$ Nat$) State_triple$) Nat$) -(declare-fun case_option$a (Bool (-> State_triple$ Bool) State_triple_option$) Bool) -(declare-fun case_option$b (Com_option$ (-> Com$ Com_option$) Com_option$) Com_option$) -(declare-fun hoare_derivs$ (State_triple_set$ State_triple_set$) Bool) -(declare-fun hoare_valids$ (State_triple_set$ State_triple_set$) Bool) -(declare-fun restrict_map$ ((-> Com$ Com_option$) Com_set$) (-> Com$ Com_option$)) -(declare-fun size_option$a ((-> Com$ Nat$)) (-> Com_option$ Nat$)) -(declare-fun triple_valid$ (Nat$ State_triple$) Bool) -(declare-fun restrict_map$a ((-> Com$ State_triple_option$) Com_set$) (-> Com$ State_triple_option$)) -(declare-fun restrict_map$b ((-> State_triple_option$ Com_option$) State_triple_option_set$) (-> State_triple_option$ Com_option$)) -(declare-fun restrict_map$c ((-> State_triple_option$ State_triple_option$) State_triple_option_set$) (-> State_triple_option$ State_triple_option$)) -(declare-fun restrict_map$d ((-> Com_option$ Com_option$) Com_option_set$) (-> Com_option$ Com_option$)) -(declare-fun restrict_map$e ((-> Com_option$ State_triple_option$) Com_option_set$) (-> Com_option$ State_triple_option$)) -(declare-fun restrict_map$f ((-> State_triple$ State_triple_option$) State_triple_set$) (-> State_triple$ State_triple_option$)) -(declare-fun restrict_map$g ((-> Pname$ Com_option$) Pname_set$) (-> Pname$ Com_option$)) -(declare-fun restrict_map$h ((-> Pname$ State_triple_option$) Pname_set$) (-> Pname$ State_triple_option$)) -(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$) (?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)) -(assert (! (forall ((?v0 (-> Pname$ Com_option$)) (?v1 Pname$)) (! (= (uvj$ ?v0 ?v1) (not (= (?v0 ?v1) none$))) :pattern ((uvj$ ?v0 ?v1)))) :named a7)) -(assert (! (forall ((?v0 (-> Com$ Com$)) (?v1 Com$)) (! (= (uvk$ ?v0 ?v1) (some$ (?v0 ?v1))) :pattern ((uvk$ ?v0 ?v1)))) :named a8)) -(assert (! (forall ((?v0 (-> Pname$ (-> State$ (-> State$ Bool)))) (?v1 (-> Pname$ (-> State$ (-> State$ Bool)))) (?v2 Pname$)) (! (= (uus$ ?v0 ?v1 ?v2) (triple$ (?v0 ?v2) (the$ (body$ ?v2)) (?v1 ?v2))) :pattern ((uus$ ?v0 ?v1 ?v2)))) :named a9)) -(assert (! (forall ((?v0 (-> Pname$ (-> State$ (-> State$ Bool)))) (?v1 (-> Pname$ (-> State$ (-> State$ Bool)))) (?v2 Pname$)) (! (= (uur$ ?v0 ?v1 ?v2) (triple$ (?v0 ?v2) (body$a ?v2) (?v1 ?v2))) :pattern ((uur$ ?v0 ?v1 ?v2)))) :named a10)) -(assert (! (forall ((?v0 State$) (?v1 State$) (?v2 State$)) (! (= (uun$ ?v0 ?v1 ?v2) (= ?v2 ?v0)) :pattern ((uun$ ?v0 ?v1 ?v2)))) :named a11)) -(assert (! (forall ((?v0 (-> State$ (-> State$ Bool))) (?v1 State$) (?v2 State$)) (! (= (uuo$ ?v0 ?v1 ?v2) (?v0 ?v1)) :pattern ((uuo$ ?v0 ?v1 ?v2)))) :named a12)) -(assert (! (forall ((?v0 Com$) (?v1 State$) (?v2 State$)) (! (= (uuw$ ?v0 ?v1 ?v2) (forall ((?v3 State$)) (=> (evalc$ ?v0 ?v2 ?v3) (= ?v1 ?v3)))) :pattern ((uuw$ ?v0 ?v1 ?v2)))) :named a13)) -(assert (! (forall ((?v0 (-> Pname$ (-> State$ (-> State$ Bool)))) (?v1 (-> Pname$ Com$)) (?v2 (-> Pname$ (-> State$ (-> State$ Bool)))) (?v3 Pname$)) (! (= (uuu$ ?v0 ?v1 ?v2 ?v3) (triple$ (?v0 ?v3) (?v1 ?v3) (?v2 ?v3))) :pattern ((uuu$ ?v0 ?v1 ?v2 ?v3)))) :named a14)) -(assert (! (forall ((?v0 (-> Pname$ Com$)) (?v1 (-> Pname$ (-> State$ (-> State$ Bool)))) (?v2 (-> Pname$ (-> State$ (-> State$ Bool)))) (?v3 Pname$)) (! (= (uuv$ ?v0 ?v1 ?v2 ?v3) (triple$ (?v1 ?v3) (?v0 ?v3) (?v2 ?v3))) :pattern ((uuv$ ?v0 ?v1 ?v2 ?v3)))) :named a15)) -(assert (! (forall ((?v0 (-> State$ (-> State$ Bool))) (?v1 (-> State$ Bool)) (?v2 State$) (?v3 State$)) (! (= (uul$ ?v0 ?v1 ?v2 ?v3) (and (?v0 ?v2 ?v3) (not (?v1 ?v3)))) :pattern ((uul$ ?v0 ?v1 ?v2 ?v3)))) :named a16)) -(assert (! (forall ((?v0 Bool) (?v1 (-> State$ (-> State$ Bool))) (?v2 State$) (?v3 State$)) (! (= (uum$ ?v0 ?v1 ?v2 ?v3) (and (?v1 ?v2 ?v3) ?v0)) :pattern ((uum$ ?v0 ?v1 ?v2 ?v3)))) :named a17)) -(assert (! (forall ((?v0 Nat$) (?v1 (-> State$ (-> State$ Bool))) (?v2 Com$) (?v3 (-> State$ (-> State$ Bool)))) (! (= (uux$ ?v0 ?v1 ?v2 ?v3) (forall ((?v4 State$) (?v5 State$)) (=> (?v1 ?v4 ?v5) (forall ((?v6 State$)) (=> (evaln$ ?v2 ?v5 ?v0 ?v6) (?v3 ?v4 ?v6)))))) :pattern ((uux$ ?v0 ?v1 ?v2 ?v3)))) :named a18)) -(assert (! (forall ((?v0 (-> State$ (-> State$ Bool))) (?v1 State$) (?v2 Vname$) (?v3 State$) (?v4 State$)) (! (= (uuc$ ?v0 ?v1 ?v2 ?v3 ?v4) (?v0 ?v3 (update$ (setlocs$ ?v4 (getlocs$ ?v1)) ?v2 (getlocs$ ?v4 res$)))) :pattern ((uuc$ ?v0 ?v1 ?v2 ?v3 ?v4)))) :named a19)) -(assert (! (forall ((?v0 (-> State$ (-> State$ Bool))) (?v1 Loc$) (?v2 State$) (?v3 State$) (?v4 State$)) (! (= (uuj$ ?v0 ?v1 ?v2 ?v3 ?v4) (?v0 ?v3 (update$ ?v4 (loc$ ?v1) (getlocs$ ?v2 ?v1)))) :pattern ((uuj$ ?v0 ?v1 ?v2 ?v3 ?v4)))) :named a20)) -(assert (! (forall ((?v0 (-> State$ (-> State$ Bool))) (?v1 Vname$) (?v2 (-> State$ Nat$)) (?v3 State$) (?v4 State$)) (! (= (uup$ ?v0 ?v1 ?v2 ?v3 ?v4) (?v0 ?v3 (update$ ?v4 ?v1 (?v2 ?v4)))) :pattern ((uup$ ?v0 ?v1 ?v2 ?v3 ?v4)))) :named a21)) -(assert (! (forall ((?v0 (-> State$ (-> State$ Bool))) (?v1 State$) (?v2 (-> State$ Nat$)) (?v3 State$) (?v4 State$)) (! (= (uud$ ?v0 ?v1 ?v2 ?v3 ?v4) (and (= ?v1 ?v4) (?v0 ?v3 (update$ (setlocs$ ?v4 newlocs$) (loc$ arg$) (?v2 ?v4))))) :pattern ((uud$ ?v0 ?v1 ?v2 ?v3 ?v4)))) :named a22)) -(assert (! (forall ((?v0 (-> State$ (-> State$ Bool))) (?v1 Loc$) (?v2 State$) (?v3 (-> State$ Nat$)) (?v4 State$) (?v5 State$)) (! (= (uuk$ ?v0 ?v1 ?v2 ?v3 ?v4 ?v5) (and (= ?v2 ?v5) (?v0 ?v4 (update$ ?v5 (loc$ ?v1) (?v3 ?v5))))) :pattern ((uuk$ ?v0 ?v1 ?v2 ?v3 ?v4 ?v5)))) :named a23)) -(assert (! (forall ((?v0 State_triple$)) (! (= (uva$ ?v0) none$a) :pattern ((uva$ ?v0)))) :named a24)) -(assert (! (forall ((?v0 State_triple$)) (! (= (uuy$ ?v0) none$) :pattern ((uuy$ ?v0)))) :named a25)) -(assert (! (forall ((?v0 State_triple_option$)) (! (= (uvd$ ?v0) none$a) :pattern ((uvd$ ?v0)))) :named a26)) -(assert (! (forall ((?v0 State_triple_option$)) (! (= (uve$ ?v0) none$) :pattern ((uve$ ?v0)))) :named a27)) -(assert (! (forall ((?v0 Com_option$)) (! (= (uvf$ ?v0) none$a) :pattern ((uvf$ ?v0)))) :named a28)) -(assert (! (forall ((?v0 Com_option$)) (! (= (uvg$ ?v0) none$) :pattern ((uvg$ ?v0)))) :named a29)) -(assert (! (forall ((?v0 Pname$)) (! (= (uvc$ ?v0) none$a) :pattern ((uvc$ ?v0)))) :named a30)) -(assert (! (forall ((?v0 Pname$)) (! (= (uuz$ ?v0) none$) :pattern ((uuz$ ?v0)))) :named a31)) -(assert (! (forall ((?v0 Com$)) (! (= (uvb$ ?v0) none$a) :pattern ((uvb$ ?v0)))) :named a32)) -(assert (! (forall ((?v0 Com$)) (! (= (uue$ ?v0) none$) :pattern ((uue$ ?v0)))) :named a33)) -(assert (! (forall ((?v0 State_triple$)) (! (= (uuh$ ?v0) false) :pattern ((uuh$ ?v0)))) :named a34)) -(assert (! (forall ((?v0 Com$)) (! (= (uui$ ?v0) false) :pattern ((uui$ ?v0)))) :named a35)) -(assert (! (forall ((?v0 State_triple$)) (! (= (uuf$ ?v0) true) :pattern ((uuf$ ?v0)))) :named a36)) -(assert (! (forall ((?v0 Com$)) (! (= (uug$ ?v0) true) :pattern ((uug$ ?v0)))) :named a37)) -(assert (! (not false) :named a38)) -(assert (! (forall ((?v0 State$)) (= ?v0 s$)) :named a39)) -(assert (! (forall ((?v0 State$)) (not (evalc$ c$ z$ ?v0))) :named a40)) -(assert (! (forall ((?v0 State$)) (=> (forall ((?v1 State$)) (= ?v1 ?v0)) false)) :named a41)) -(assert (! (forall ((?v0 Com$) (?v1 State$) (?v2 State$) (?v3 State$)) (=> (and (evalc$ ?v0 ?v1 ?v2) (evalc$ ?v0 ?v1 ?v3)) (= ?v3 ?v2))) :named a42)) -(assert (! (=> state_not_singleton$ (forall ((?v0 State$)) (=> (forall ((?v1 State$)) (= ?v1 ?v0)) false))) :named a43)) -(assert (! (= state_not_singleton$ (exists ((?v0 State$) (?v1 State$)) (not (= ?v0 ?v1)))) :named a44)) -(assert (! (forall ((?v0 State$) (?v1 State$)) (=> (and (evalc$ skip$ ?v0 ?v1) (=> (= ?v1 ?v0) false)) false)) :named a45)) -(assert (! (forall ((?v0 State$)) (evalc$ skip$ ?v0 ?v0)) :named a46)) -(assert (! (forall ((?v0 Com$) (?v1 Com$) (?v2 State$) (?v3 State$)) (=> (and (evalc$ (semi$ ?v0 ?v1) ?v2 ?v3) (forall ((?v4 State$)) (=> (and (evalc$ ?v0 ?v2 ?v4) (evalc$ ?v1 ?v4 ?v3)) false))) false)) :named a47)) -(assert (! (forall ((?v0 Com$) (?v1 State$) (?v2 State$) (?v3 Com$) (?v4 State$)) (=> (and (evalc$ ?v0 ?v1 ?v2) (evalc$ ?v3 ?v2 ?v4)) (evalc$ (semi$ ?v0 ?v3) ?v1 ?v4))) :named a48)) -(assert (! (forall ((?v0 (-> State$ Bool)) (?v1 Com$) (?v2 Com$) (?v3 State$) (?v4 State$)) (=> (and (evalc$ (cond$ ?v0 ?v1 ?v2) ?v3 ?v4) (and (=> (and (?v0 ?v3) (evalc$ ?v1 ?v3 ?v4)) false) (=> (and (not (?v0 ?v3)) (evalc$ ?v2 ?v3 ?v4)) false))) false)) :named a49)) -(assert (! (forall ((?v0 (-> State$ Bool)) (?v1 State$) (?v2 Com$) (?v3 State$) (?v4 Com$)) (=> (and (?v0 ?v1) (evalc$ ?v2 ?v1 ?v3)) (evalc$ (cond$ ?v0 ?v2 ?v4) ?v1 ?v3))) :named a50)) -(assert (! (forall ((?v0 (-> State$ Bool)) (?v1 State$) (?v2 Com$) (?v3 State$) (?v4 Com$)) (=> (and (not (?v0 ?v1)) (evalc$ ?v2 ?v1 ?v3)) (evalc$ (cond$ ?v0 ?v4 ?v2) ?v1 ?v3))) :named a51)) -(assert (! (forall ((?v0 (-> State$ Bool)) (?v1 State$) (?v2 Com$) (?v3 State$) (?v4 State$)) (=> (and (?v0 ?v1) (and (evalc$ ?v2 ?v1 ?v3) (evalc$ (while$ ?v0 ?v2) ?v3 ?v4))) (evalc$ (while$ ?v0 ?v2) ?v1 ?v4))) :named a52)) -(assert (! (forall ((?v0 (-> State$ Bool)) (?v1 State$) (?v2 Com$)) (=> (not (?v0 ?v1)) (evalc$ (while$ ?v0 ?v2) ?v1 ?v1))) :named a53)) -(assert (! (forall ((?v0 (-> State$ Bool)) (?v1 Com$) (?v2 State$) (?v3 State$)) (=> (and (evalc$ (while$ ?v0 ?v1) ?v2 ?v3) (and (=> (and (= ?v3 ?v2) (not (?v0 ?v2))) false) (forall ((?v4 State$)) (=> (and (?v0 ?v2) (and (evalc$ ?v1 ?v2 ?v4) (evalc$ (while$ ?v0 ?v1) ?v4 ?v3))) false)))) false)) :named a54)) -(assert (! (forall ((?v0 Com$) (?v1 Com$) (?v2 Com$) (?v3 Com$)) (= (= (semi$ ?v0 ?v1) (semi$ ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))) :named a55)) -(assert (! (forall ((?v0 (-> State$ Bool)) (?v1 Com$) (?v2 Com$) (?v3 (-> State$ Bool)) (?v4 Com$) (?v5 Com$)) (= (= (cond$ ?v0 ?v1 ?v2) (cond$ ?v3 ?v4 ?v5)) (and (= ?v0 ?v3) (and (= ?v1 ?v4) (= ?v2 ?v5))))) :named a56)) -(assert (! (forall ((?v0 (-> State$ Bool)) (?v1 Com$) (?v2 (-> State$ Bool)) (?v3 Com$)) (= (= (while$ ?v0 ?v1) (while$ ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))) :named a57)) -(assert (! (forall ((?v0 Com$) (?v1 Com$)) (not (= skip$ (semi$ ?v0 ?v1)))) :named a58)) -(assert (! (forall ((?v0 (-> State$ Bool)) (?v1 Com$) (?v2 Com$)) (not (= skip$ (cond$ ?v0 ?v1 ?v2)))) :named a59)) -(assert (! (forall ((?v0 Com$) (?v1 Com$) (?v2 (-> State$ Bool)) (?v3 Com$) (?v4 Com$)) (not (= (semi$ ?v0 ?v1) (cond$ ?v2 ?v3 ?v4)))) :named a60)) -(assert (! (forall ((?v0 (-> State$ Bool)) (?v1 Com$)) (not (= skip$ (while$ ?v0 ?v1)))) :named a61)) -(assert (! (forall ((?v0 Com$) (?v1 Com$) (?v2 (-> State$ Bool)) (?v3 Com$)) (not (= (semi$ ?v0 ?v1) (while$ ?v2 ?v3)))) :named a62)) -(assert (! (forall ((?v0 (-> State$ Bool)) (?v1 Com$) (?v2 Com$) (?v3 (-> State$ Bool)) (?v4 Com$)) (not (= (cond$ ?v0 ?v1 ?v2) (while$ ?v3 ?v4)))) :named a63)) -(assert (! (forall ((?v0 State$) (?v1 Nat$) (?v2 State$)) (=> (and (evaln$ skip$ ?v0 ?v1 ?v2) (=> (= ?v2 ?v0) false)) false)) :named a64)) -(assert (! (forall ((?v0 State$) (?v1 Nat$)) (evaln$ skip$ ?v0 ?v1 ?v0)) :named a65)) -(assert (! (forall ((?v0 Com$) (?v1 State$) (?v2 Nat$) (?v3 State$) (?v4 Com$) (?v5 State$) (?v6 Nat$) (?v7 State$)) (=> (and (evaln$ ?v0 ?v1 ?v2 ?v3) (evaln$ ?v4 ?v5 ?v6 ?v7)) (exists ((?v8 Nat$)) (and (evaln$ ?v0 ?v1 ?v8 ?v3) (evaln$ ?v4 ?v5 ?v8 ?v7))))) :named a66)) -(assert (! (forall ((?v0 Com$) (?v1 State$) (?v2 State$)) (= (evalc$ ?v0 ?v1 ?v2) (exists ((?v3 Nat$)) (evaln$ ?v0 ?v1 ?v3 ?v2)))) :named a67)) -(assert (! (forall ((?v0 Com$) (?v1 State$) (?v2 State$)) (=> (evalc$ ?v0 ?v1 ?v2) (exists ((?v3 Nat$)) (evaln$ ?v0 ?v1 ?v3 ?v2)))) :named a68)) -(assert (! (forall ((?v0 Com$) (?v1 State$) (?v2 Nat$) (?v3 State$)) (=> (evaln$ ?v0 ?v1 ?v2 ?v3) (evalc$ ?v0 ?v1 ?v3))) :named a69)) -(assert (! (forall ((?v0 (-> State$ Bool)) (?v1 Com$) (?v2 State$) (?v3 Nat$) (?v4 State$)) (=> (and (evaln$ (while$ ?v0 ?v1) ?v2 ?v3 ?v4) (and (=> (and (= ?v4 ?v2) (not (?v0 ?v2))) false) (forall ((?v5 State$)) (=> (and (?v0 ?v2) (and (evaln$ ?v1 ?v2 ?v3 ?v5) (evaln$ (while$ ?v0 ?v1) ?v5 ?v3 ?v4))) false)))) false)) :named a70)) -(assert (! (forall ((?v0 (-> State$ Bool)) (?v1 State$) (?v2 Com$) (?v3 Nat$)) (=> (not (?v0 ?v1)) (evaln$ (while$ ?v0 ?v2) ?v1 ?v3 ?v1))) :named a71)) -(assert (! (forall ((?v0 (-> State$ Bool)) (?v1 State$) (?v2 Com$) (?v3 Nat$) (?v4 State$) (?v5 State$)) (=> (and (?v0 ?v1) (and (evaln$ ?v2 ?v1 ?v3 ?v4) (evaln$ (while$ ?v0 ?v2) ?v4 ?v3 ?v5))) (evaln$ (while$ ?v0 ?v2) ?v1 ?v3 ?v5))) :named a72)) -(assert (! (forall ((?v0 (-> State$ Bool)) (?v1 State$) (?v2 Com$) (?v3 Nat$) (?v4 State$) (?v5 Com$)) (=> (and (not (?v0 ?v1)) (evaln$ ?v2 ?v1 ?v3 ?v4)) (evaln$ (cond$ ?v0 ?v5 ?v2) ?v1 ?v3 ?v4))) :named a73)) -(assert (! (forall ((?v0 (-> State$ Bool)) (?v1 State$) (?v2 Com$) (?v3 Nat$) (?v4 State$) (?v5 Com$)) (=> (and (?v0 ?v1) (evaln$ ?v2 ?v1 ?v3 ?v4)) (evaln$ (cond$ ?v0 ?v2 ?v5) ?v1 ?v3 ?v4))) :named a74)) -(assert (! (forall ((?v0 (-> State$ Bool)) (?v1 Com$) (?v2 Com$) (?v3 State$) (?v4 Nat$) (?v5 State$)) (=> (and (evaln$ (cond$ ?v0 ?v1 ?v2) ?v3 ?v4 ?v5) (and (=> (and (?v0 ?v3) (evaln$ ?v1 ?v3 ?v4 ?v5)) false) (=> (and (not (?v0 ?v3)) (evaln$ ?v2 ?v3 ?v4 ?v5)) false))) false)) :named a75)) -(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_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)) -(assert (! (forall ((?v0 (-> Pname$ Bool)) (?v1 (-> Pname$ Bool))) (=> (forall ((?v2 Pname$)) (= (?v0 ?v2) (?v1 ?v2))) (= (collect$b ?v0) (collect$b ?v1)))) :named a85)) -(assert (! (forall ((?v0 Loc$) (?v1 (-> State$ Nat$)) (?v2 Com$)) (not (= skip$ (local$ ?v0 ?v1 ?v2)))) :named a86)) -(assert (! (forall ((?v0 Vname$) (?v1 (-> State$ Nat$)) (?v2 Vname$) (?v3 (-> State$ Nat$))) (= (= (ass$ ?v0 ?v1) (ass$ ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))) :named a87)) -(assert (! (forall ((?v0 Loc$) (?v1 (-> State$ Nat$)) (?v2 Com$) (?v3 Loc$) (?v4 (-> State$ Nat$)) (?v5 Com$)) (= (= (local$ ?v0 ?v1 ?v2) (local$ ?v3 ?v4 ?v5)) (and (= ?v0 ?v3) (and (= ?v1 ?v4) (= ?v2 ?v5))))) :named a88)) -(assert (! (forall ((?v0 Vname$) (?v1 (-> State$ Nat$)) (?v2 Loc$) (?v3 (-> State$ Nat$)) (?v4 Com$)) (not (= (ass$ ?v0 ?v1) (local$ ?v2 ?v3 ?v4)))) :named a89)) -(assert (! (forall ((?v0 Loc$) (?v1 (-> State$ Nat$)) (?v2 Com$) (?v3 (-> State$ Bool)) (?v4 Com$)) (not (= (local$ ?v0 ?v1 ?v2) (while$ ?v3 ?v4)))) :named a90)) -(assert (! (forall ((?v0 Vname$) (?v1 (-> State$ Nat$)) (?v2 (-> State$ Bool)) (?v3 Com$)) (not (= (ass$ ?v0 ?v1) (while$ ?v2 ?v3)))) :named a91)) -(assert (! (forall ((?v0 Loc$) (?v1 (-> State$ Nat$)) (?v2 Com$) (?v3 (-> State$ Bool)) (?v4 Com$) (?v5 Com$)) (not (= (local$ ?v0 ?v1 ?v2) (cond$ ?v3 ?v4 ?v5)))) :named a92)) -(assert (! (forall ((?v0 Vname$) (?v1 (-> State$ Nat$)) (?v2 (-> State$ Bool)) (?v3 Com$) (?v4 Com$)) (not (= (ass$ ?v0 ?v1) (cond$ ?v2 ?v3 ?v4)))) :named a93)) -(assert (! (forall ((?v0 Loc$) (?v1 (-> State$ Nat$)) (?v2 Com$) (?v3 Com$) (?v4 Com$)) (not (= (local$ ?v0 ?v1 ?v2) (semi$ ?v3 ?v4)))) :named a94)) -(assert (! (forall ((?v0 Vname$) (?v1 (-> State$ Nat$)) (?v2 Com$) (?v3 Com$)) (not (= (ass$ ?v0 ?v1) (semi$ ?v2 ?v3)))) :named a95)) -(assert (! (forall ((?v0 Com$)) (=> (and (=> (= ?v0 skip$) false) (and (forall ((?v1 Vname$) (?v2 (-> State$ Nat$))) (=> (= ?v0 (ass$ ?v1 ?v2)) false)) (and (forall ((?v1 Loc$) (?v2 (-> State$ Nat$)) (?v3 Com$)) (=> (= ?v0 (local$ ?v1 ?v2 ?v3)) false)) (and (forall ((?v1 Com$) (?v2 Com$)) (=> (= ?v0 (semi$ ?v1 ?v2)) false)) (and (forall ((?v1 (-> State$ Bool)) (?v2 Com$) (?v3 Com$)) (=> (= ?v0 (cond$ ?v1 ?v2 ?v3)) false)) (and (forall ((?v1 (-> State$ Bool)) (?v2 Com$)) (=> (= ?v0 (while$ ?v1 ?v2)) false)) (and (forall ((?v1 Pname$)) (=> (= ?v0 (body$a ?v1)) false)) (forall ((?v1 Vname$) (?v2 Pname$) (?v3 (-> State$ Nat$))) (=> (= ?v0 (call$ ?v1 ?v2 ?v3)) false))))))))) false)) :named a96)) -(assert (! (forall ((?v0 Vname$) (?v1 (-> State$ Nat$)) (?v2 State$)) (evalc$ (ass$ ?v0 ?v1) ?v2 (update$ ?v2 ?v0 (?v1 ?v2)))) :named a97)) -(assert (! (forall ((?v0 Vname$) (?v1 (-> State$ Nat$)) (?v2 State$) (?v3 State$)) (=> (and (evalc$ (ass$ ?v0 ?v1) ?v2 ?v3) (=> (= ?v3 (update$ ?v2 ?v0 (?v1 ?v2))) false)) false)) :named a98)) -(assert (! (forall ((?v0 Vname$) (?v1 (-> State$ Nat$)) (?v2 State$) (?v3 Nat$)) (evaln$ (ass$ ?v0 ?v1) ?v2 ?v3 (update$ ?v2 ?v0 (?v1 ?v2)))) :named a99)) -(assert (! (forall ((?v0 Vname$) (?v1 (-> State$ Nat$)) (?v2 State$) (?v3 Nat$) (?v4 State$)) (=> (and (evaln$ (ass$ ?v0 ?v1) ?v2 ?v3 ?v4) (=> (= ?v4 (update$ ?v2 ?v0 (?v1 ?v2))) false)) false)) :named a100)) -(assert (! (forall ((?v0 Vname$) (?v1 Pname$) (?v2 (-> State$ Nat$))) (not (= skip$ (call$ ?v0 ?v1 ?v2)))) :named a101)) -(assert (! (forall ((?v0 Pname$) (?v1 Pname$)) (= (= (body$a ?v0) (body$a ?v1)) (= ?v0 ?v1))) :named a102)) -(assert (! (forall ((?v0 Vname$) (?v1 Pname$) (?v2 (-> State$ Nat$)) (?v3 Vname$) (?v4 Pname$) (?v5 (-> State$ Nat$))) (= (= (call$ ?v0 ?v1 ?v2) (call$ ?v3 ?v4 ?v5)) (and (= ?v0 ?v3) (and (= ?v1 ?v4) (= ?v2 ?v5))))) :named a103)) -(assert (! (forall ((?v0 Pname$) (?v1 Vname$) (?v2 Pname$) (?v3 (-> State$ Nat$))) (not (= (body$a ?v0) (call$ ?v1 ?v2 ?v3)))) :named a104)) -(assert (! (forall ((?v0 (-> State$ Bool)) (?v1 Com$) (?v2 Pname$)) (not (= (while$ ?v0 ?v1) (body$a ?v2)))) :named a105)) -(assert (! (forall ((?v0 (-> State$ Bool)) (?v1 Com$) (?v2 Com$) (?v3 Pname$)) (not (= (cond$ ?v0 ?v1 ?v2) (body$a ?v3)))) :named a106)) -(assert (! (forall ((?v0 Com$) (?v1 Com$) (?v2 Pname$)) (not (= (semi$ ?v0 ?v1) (body$a ?v2)))) :named a107)) -(assert (! (forall ((?v0 Loc$) (?v1 (-> State$ Nat$)) (?v2 Com$) (?v3 Pname$)) (not (= (local$ ?v0 ?v1 ?v2) (body$a ?v3)))) :named a108)) -(assert (! (forall ((?v0 Vname$) (?v1 (-> State$ Nat$)) (?v2 Pname$)) (not (= (ass$ ?v0 ?v1) (body$a ?v2)))) :named a109)) -(assert (! (forall ((?v0 Pname$)) (not (= skip$ (body$a ?v0)))) :named a110)) -(assert (! (forall ((?v0 (-> State$ Bool)) (?v1 Com$) (?v2 Vname$) (?v3 Pname$) (?v4 (-> State$ Nat$))) (not (= (while$ ?v0 ?v1) (call$ ?v2 ?v3 ?v4)))) :named a111)) -(assert (! (forall ((?v0 (-> State$ Bool)) (?v1 Com$) (?v2 Com$) (?v3 Vname$) (?v4 Pname$) (?v5 (-> State$ Nat$))) (not (= (cond$ ?v0 ?v1 ?v2) (call$ ?v3 ?v4 ?v5)))) :named a112)) -(assert (! (forall ((?v0 Com$) (?v1 Com$) (?v2 Vname$) (?v3 Pname$) (?v4 (-> State$ Nat$))) (not (= (semi$ ?v0 ?v1) (call$ ?v2 ?v3 ?v4)))) :named a113)) -(assert (! (forall ((?v0 Loc$) (?v1 (-> State$ Nat$)) (?v2 Com$) (?v3 Vname$) (?v4 Pname$) (?v5 (-> State$ Nat$))) (not (= (local$ ?v0 ?v1 ?v2) (call$ ?v3 ?v4 ?v5)))) :named a114)) -(assert (! (forall ((?v0 Vname$) (?v1 (-> State$ Nat$)) (?v2 Vname$) (?v3 Pname$) (?v4 (-> State$ Nat$))) (not (= (ass$ ?v0 ?v1) (call$ ?v2 ?v3 ?v4)))) :named a115)) -(assert (! (forall ((?v0 Com$)) (= (wt$ ?v0) (or (= ?v0 skip$) (or (exists ((?v1 Vname$) (?v2 (-> State$ Nat$))) (= ?v0 (ass$ ?v1 ?v2))) (or (exists ((?v1 Com$) (?v2 Loc$) (?v3 (-> State$ Nat$))) (and (= ?v0 (local$ ?v2 ?v3 ?v1)) (wt$ ?v1))) (or (exists ((?v1 Com$) (?v2 Com$)) (and (= ?v0 (semi$ ?v1 ?v2)) (and (wt$ ?v1) (wt$ ?v2)))) (or (exists ((?v1 Com$) (?v2 Com$) (?v3 (-> State$ Bool))) (and (= ?v0 (cond$ ?v3 ?v1 ?v2)) (and (wt$ ?v1) (wt$ ?v2)))) (or (exists ((?v1 Com$) (?v2 (-> State$ Bool))) (and (= ?v0 (while$ ?v2 ?v1)) (wt$ ?v1))) (or (exists ((?v1 Pname$)) (and (= ?v0 (body$a ?v1)) (not (= (body$ ?v1) none$)))) (exists ((?v1 Pname$) (?v2 Vname$) (?v3 (-> State$ Nat$))) (and (= ?v0 (call$ ?v2 ?v1 ?v3)) (wt$ (body$a ?v1))))))))))))) :named a116)) -(assert (! (forall ((?v0 Com$)) (=> (and (wt$ ?v0) (and (=> (= ?v0 skip$) false) (and (forall ((?v1 Vname$) (?v2 (-> State$ Nat$))) (=> (= ?v0 (ass$ ?v1 ?v2)) false)) (and (forall ((?v1 Com$) (?v2 Loc$) (?v3 (-> State$ Nat$))) (=> (and (= ?v0 (local$ ?v2 ?v3 ?v1)) (wt$ ?v1)) false)) (and (forall ((?v1 Com$) (?v2 Com$)) (=> (and (= ?v0 (semi$ ?v1 ?v2)) (and (wt$ ?v1) (wt$ ?v2))) false)) (and (forall ((?v1 Com$) (?v2 Com$) (?v3 (-> State$ Bool))) (=> (and (= ?v0 (cond$ ?v3 ?v1 ?v2)) (and (wt$ ?v1) (wt$ ?v2))) false)) (and (forall ((?v1 Com$) (?v2 (-> State$ Bool))) (=> (and (= ?v0 (while$ ?v2 ?v1)) (wt$ ?v1)) false)) (and (forall ((?v1 Pname$)) (=> (and (= ?v0 (body$a ?v1)) (not (= (body$ ?v1) none$))) false)) (forall ((?v1 Pname$) (?v2 Vname$) (?v3 (-> State$ Nat$))) (=> (and (= ?v0 (call$ ?v2 ?v1 ?v3)) (wt$ (body$a ?v1))) false)))))))))) false)) :named a117)) -(assert (! (forall ((?v0 Vname$) (?v1 Pname$) (?v2 (-> State$ Nat$))) (=> (and (wt$ (call$ ?v0 ?v1 ?v2)) (=> (wt$ (body$a ?v1)) false)) false)) :named a118)) -(assert (! (forall ((?v0 Pname$) (?v1 Vname$) (?v2 (-> State$ Nat$))) (=> (wt$ (body$a ?v0)) (wt$ (call$ ?v1 ?v0 ?v2)))) :named a119)) -(assert (! (forall ((?v0 Loc$) (?v1 (-> State$ Nat$)) (?v2 Com$) (?v3 State$) (?v4 State$)) (=> (and (evalc$ (local$ ?v0 ?v1 ?v2) ?v3 ?v4) (forall ((?v5 State$)) (=> (and (= ?v4 (update$ ?v5 (loc$ ?v0) (getlocs$ ?v3 ?v0))) (evalc$ ?v2 (update$ ?v3 (loc$ ?v0) (?v1 ?v3)) ?v5)) false))) false)) :named a120)) -(assert (! (forall ((?v0 Com$) (?v1 State$) (?v2 Loc$) (?v3 (-> State$ Nat$)) (?v4 State$)) (=> (evalc$ ?v0 (update$ ?v1 (loc$ ?v2) (?v3 ?v1)) ?v4) (evalc$ (local$ ?v2 ?v3 ?v0) ?v1 (update$ ?v4 (loc$ ?v2) (getlocs$ ?v1 ?v2))))) :named a121)) -(assert (! (forall ((?v0 Com$) (?v1 State$) (?v2 Loc$) (?v3 (-> State$ Nat$)) (?v4 Nat$) (?v5 State$)) (=> (evaln$ ?v0 (update$ ?v1 (loc$ ?v2) (?v3 ?v1)) ?v4 ?v5) (evaln$ (local$ ?v2 ?v3 ?v0) ?v1 ?v4 (update$ ?v5 (loc$ ?v2) (getlocs$ ?v1 ?v2))))) :named a122)) -(assert (! (forall ((?v0 Loc$) (?v1 Loc$)) (= (= (loc$ ?v0) (loc$ ?v1)) (= ?v0 ?v1))) :named a123)) -(assert (! (forall ((?v0 Pname$)) (=> (not (= (body$ ?v0) none$)) (wt$ (body$a ?v0)))) :named a124)) -(assert (! (forall ((?v0 (-> State$ Bool)) (?v1 Com$)) (=> (and (wt$ (while$ ?v0 ?v1)) (=> (wt$ ?v1) false)) false)) :named a125)) -(assert (! (forall ((?v0 Com$) (?v1 (-> State$ Bool))) (=> (wt$ ?v0) (wt$ (while$ ?v1 ?v0)))) :named a126)) -(assert (! (forall ((?v0 (-> State$ Bool)) (?v1 Com$) (?v2 Com$)) (=> (and (wt$ (cond$ ?v0 ?v1 ?v2)) (=> (and (wt$ ?v1) (wt$ ?v2)) false)) false)) :named a127)) -(assert (! (forall ((?v0 Com$) (?v1 Com$) (?v2 (-> State$ Bool))) (=> (and (wt$ ?v0) (wt$ ?v1)) (wt$ (cond$ ?v2 ?v0 ?v1)))) :named a128)) -(assert (! (forall ((?v0 Vname$) (?v1 (-> State$ Nat$))) (wt$ (ass$ ?v0 ?v1))) :named a129)) -(assert (! (forall ((?v0 Com$) (?v1 Loc$) (?v2 (-> State$ Nat$))) (=> (wt$ ?v0) (wt$ (local$ ?v1 ?v2 ?v0)))) :named a130)) -(assert (! (forall ((?v0 Vname$) (?v1 (-> State$ Nat$))) (=> (and (wt$ (ass$ ?v0 ?v1)) false) false)) :named a131)) -(assert (! (forall ((?v0 Loc$) (?v1 (-> State$ Nat$)) (?v2 Com$)) (=> (and (wt$ (local$ ?v0 ?v1 ?v2)) (=> (wt$ ?v2) false)) false)) :named a132)) -(assert (! (forall ((?v0 Com$) (?v1 Com$)) (=> (and (wt$ (semi$ ?v0 ?v1)) (=> (and (wt$ ?v0) (wt$ ?v1)) false)) false)) :named a133)) -(assert (! (forall ((?v0 Com$) (?v1 Com$)) (=> (and (wt$ ?v0) (wt$ ?v1)) (wt$ (semi$ ?v0 ?v1)))) :named a134)) -(assert (! (=> (and (wt$ skip$) false) false) :named a135)) -(assert (! (wt$ skip$) :named a136)) -(assert (! (forall ((?v0 Loc$) (?v1 (-> State$ Nat$)) (?v2 Com$) (?v3 State$) (?v4 Nat$) (?v5 State$)) (=> (and (evaln$ (local$ ?v0 ?v1 ?v2) ?v3 ?v4 ?v5) (forall ((?v6 State$)) (=> (and (= ?v5 (update$ ?v6 (loc$ ?v0) (getlocs$ ?v3 ?v0))) (evaln$ ?v2 (update$ ?v3 (loc$ ?v0) (?v1 ?v3)) ?v4 ?v6)) false))) false)) :named a137)) -(assert (! (forall ((?v0 Pname$) (?v1 State$) (?v2 State$)) (=> (evalc$ (the$ (body$ ?v0)) ?v1 ?v2) (evalc$ (body$a ?v0) ?v1 ?v2))) :named a138)) -(assert (! (forall ((?v0 Pname$) (?v1 State$) (?v2 State$)) (=> (and (evalc$ (body$a ?v0) ?v1 ?v2) (=> (evalc$ (the$ (body$ ?v0)) ?v1 ?v2) false)) false)) :named a139)) -(assert (! (forall ((?v0 Pname$) (?v1 State$) (?v2 (-> State$ Nat$)) (?v3 State$) (?v4 Vname$)) (=> (evalc$ (body$a ?v0) (update$ (setlocs$ ?v1 newlocs$) (loc$ arg$) (?v2 ?v1)) ?v3) (evalc$ (call$ ?v4 ?v0 ?v2) ?v1 (update$ (setlocs$ ?v3 (getlocs$ ?v1)) ?v4 (getlocs$ ?v3 res$))))) :named a140)) -(assert (! (forall ((?v0 Vname$) (?v1 Pname$) (?v2 (-> State$ Nat$)) (?v3 State$) (?v4 State$)) (=> (and (evalc$ (call$ ?v0 ?v1 ?v2) ?v3 ?v4) (forall ((?v5 State$)) (=> (and (= ?v4 (update$ (setlocs$ ?v5 (getlocs$ ?v3)) ?v0 (getlocs$ ?v5 res$))) (evalc$ (body$a ?v1) (update$ (setlocs$ ?v3 newlocs$) (loc$ arg$) (?v2 ?v3)) ?v5)) false))) false)) :named a141)) -(assert (! (forall ((?v0 Vname$) (?v1 Pname$) (?v2 (-> State$ Nat$)) (?v3 State$) (?v4 Nat$) (?v5 State$)) (=> (and (evaln$ (call$ ?v0 ?v1 ?v2) ?v3 ?v4 ?v5) (forall ((?v6 State$)) (=> (and (= ?v5 (update$ (setlocs$ ?v6 (getlocs$ ?v3)) ?v0 (getlocs$ ?v6 res$))) (evaln$ (body$a ?v1) (update$ (setlocs$ ?v3 newlocs$) (loc$ arg$) (?v2 ?v3)) ?v4 ?v6)) false))) false)) :named a142)) -(assert (! (forall ((?v0 Pname$) (?v1 State$) (?v2 (-> State$ Nat$)) (?v3 Nat$) (?v4 State$) (?v5 Vname$)) (=> (evaln$ (body$a ?v0) (update$ (setlocs$ ?v1 newlocs$) (loc$ arg$) (?v2 ?v1)) ?v3 ?v4) (evaln$ (call$ ?v5 ?v0 ?v2) ?v1 ?v3 (update$ (setlocs$ ?v4 (getlocs$ ?v1)) ?v5 (getlocs$ ?v4 res$))))) :named a143)) -(assert (! (forall ((?v0 State_triple_option$) (?v1 State_triple_option$)) (=> (and (= (= ?v0 none$a) (= ?v1 none$a)) (=> (and (not (= ?v0 none$a)) (not (= ?v1 none$a))) (= (the$a ?v0) (the$a ?v1)))) (= ?v0 ?v1))) :named a144)) -(assert (! (forall ((?v0 Com_option$) (?v1 Com_option$)) (=> (and (= (= ?v0 none$) (= ?v1 none$)) (=> (and (not (= ?v0 none$)) (not (= ?v1 none$))) (= (the$ ?v0) (the$ ?v1)))) (= ?v0 ?v1))) :named a145)) -(assert (! (forall ((?v0 Pname$) (?v1 State$) (?v2 Nat$) (?v3 State$)) (=> (and (evaln$ (body$a ?v0) ?v1 ?v2 ?v3) (forall ((?v4 Nat$)) (=> (and (= ?v2 (suc$ ?v4)) (evaln$ (the$ (body$ ?v0)) ?v1 ?v4 ?v3)) false))) false)) :named a146)) -(assert (! (forall ((?v0 Pname$) (?v1 State$) (?v2 Nat$) (?v3 State$)) (=> (evaln$ (the$ (body$ ?v0)) ?v1 ?v2 ?v3) (evaln$ (body$a ?v0) ?v1 (suc$ ?v2) ?v3))) :named a147)) -(assert (! (forall ((?v0 State_triple_option$)) (=> (and (=> (= ?v0 none$a) false) (=> (not (= ?v0 none$a)) false)) false)) :named a148)) -(assert (! (forall ((?v0 Com_option$)) (=> (and (=> (= ?v0 none$) false) (=> (not (= ?v0 none$)) false)) false)) :named a149)) -(assert (! (forall ((?v0 Com$) (?v1 State$) (?v2 Nat$) (?v3 State$)) (=> (evaln$ ?v0 ?v1 ?v2 ?v3) (evaln$ ?v0 ?v1 (suc$ ?v2) ?v3))) :named a150)) -(assert (! (forall ((?v0 Pname$)) (=> (and (wt$ (body$a ?v0)) (forall ((?v1 Com$)) (=> (= (body$ ?v0) (some$ ?v1)) false))) false)) :named a151)) -(assert (! (forall ((?v0 Bool) (?v1 (-> Com$ Bool)) (?v2 Com_option$)) (! (= (case_option$ ?v0 ?v1 ?v2) (ite (= ?v2 none$) ?v0 (?v1 (the$ ?v2)))) :pattern ((case_option$ ?v0 ?v1 ?v2)))) :named a152)) -(assert (! (forall ((?v0 Glb$) (?v1 Glb$)) (= (= (glb$ ?v0) (glb$ ?v1)) (= ?v0 ?v1))) :named a153)) -(assert (! (forall ((?v0 State_triple_option$)) (= (not (= ?v0 none$a)) (exists ((?v1 State_triple$)) (= ?v0 (some$a ?v1))))) :named a154)) -(assert (! (forall ((?v0 Com_option$)) (= (not (= ?v0 none$)) (exists ((?v1 Com$)) (= ?v0 (some$ ?v1))))) :named a155)) -(assert (! (forall ((?v0 State_triple_option$)) (= (forall ((?v1 State_triple$)) (not (= ?v0 (some$a ?v1)))) (= ?v0 none$a))) :named a156)) -(assert (! (forall ((?v0 Com_option$)) (= (forall ((?v1 Com$)) (not (= ?v0 (some$ ?v1)))) (= ?v0 none$))) :named a157)) -(assert (! (forall ((?v0 State_triple_option$)) (=> (not (= ?v0 none$a)) (= (some$a (the$a ?v0)) ?v0))) :named a158)) -(assert (! (forall ((?v0 Com_option$)) (=> (not (= ?v0 none$)) (= (some$ (the$ ?v0)) ?v0))) :named a159)) -(assert (! (forall ((?v0 (-> Bool Bool)) (?v1 Bool) (?v2 (-> Com$ Bool)) (?v3 Com_option$)) (= (?v0 (case_option$ ?v1 ?v2 ?v3)) (and (=> (= ?v3 none$) (?v0 ?v1)) (=> (= ?v3 (some$ (the$ ?v3))) (?v0 (?v2 (the$ ?v3))))))) :named a160)) -(assert (! (forall ((?v0 (-> Bool Bool)) (?v1 Bool) (?v2 (-> Com$ Bool)) (?v3 Com_option$)) (= (?v0 (case_option$ ?v1 ?v2 ?v3)) (not (or (and (= ?v3 none$) (not (?v0 ?v1))) (and (= ?v3 (some$ (the$ ?v3))) (not (?v0 (?v2 (the$ ?v3))))))))) :named a161)) -(assert (! (forall ((?v0 State_triple_option$) (?v1 (-> State_triple_option$ (-> State_triple_option$ Bool))) (?v2 State_triple_option$)) (=> (and (=> (= ?v0 none$a) (?v1 ?v0 ?v2)) (and (=> (= ?v2 none$a) (?v1 ?v0 ?v2)) (forall ((?v3 State_triple$) (?v4 State_triple$)) (=> (and (= ?v0 (some$a ?v3)) (= ?v2 (some$a ?v4))) (?v1 ?v0 ?v2))))) (?v1 ?v0 ?v2))) :named a162)) -(assert (! (forall ((?v0 State_triple_option$) (?v1 (-> State_triple_option$ (-> Com_option$ Bool))) (?v2 Com_option$)) (=> (and (=> (= ?v0 none$a) (?v1 ?v0 ?v2)) (and (=> (= ?v2 none$) (?v1 ?v0 ?v2)) (forall ((?v3 State_triple$) (?v4 Com$)) (=> (and (= ?v0 (some$a ?v3)) (= ?v2 (some$ ?v4))) (?v1 ?v0 ?v2))))) (?v1 ?v0 ?v2))) :named a163)) -(assert (! (forall ((?v0 Com_option$) (?v1 (-> Com_option$ (-> State_triple_option$ Bool))) (?v2 State_triple_option$)) (=> (and (=> (= ?v0 none$) (?v1 ?v0 ?v2)) (and (=> (= ?v2 none$a) (?v1 ?v0 ?v2)) (forall ((?v3 Com$) (?v4 State_triple$)) (=> (and (= ?v0 (some$ ?v3)) (= ?v2 (some$a ?v4))) (?v1 ?v0 ?v2))))) (?v1 ?v0 ?v2))) :named a164)) -(assert (! (forall ((?v0 Com_option$) (?v1 (-> Com_option$ (-> Com_option$ Bool))) (?v2 Com_option$)) (=> (and (=> (= ?v0 none$) (?v1 ?v0 ?v2)) (and (=> (= ?v2 none$) (?v1 ?v0 ?v2)) (forall ((?v3 Com$) (?v4 Com$)) (=> (and (= ?v0 (some$ ?v3)) (= ?v2 (some$ ?v4))) (?v1 ?v0 ?v2))))) (?v1 ?v0 ?v2))) :named a165)) -(assert (! (forall ((?v0 (-> State_triple_option$ Bool))) (= (forall ((?v1 State_triple_option$)) (?v0 ?v1)) (and (?v0 none$a) (forall ((?v1 State_triple$)) (?v0 (some$a ?v1)))))) :named a166)) -(assert (! (forall ((?v0 (-> Com_option$ Bool))) (= (forall ((?v1 Com_option$)) (?v0 ?v1)) (and (?v0 none$) (forall ((?v1 Com$)) (?v0 (some$ ?v1)))))) :named a167)) -(assert (! (forall ((?v0 (-> State_triple_option$ Bool))) (= (exists ((?v1 State_triple_option$)) (?v0 ?v1)) (or (?v0 none$a) (exists ((?v1 State_triple$)) (?v0 (some$a ?v1)))))) :named a168)) -(assert (! (forall ((?v0 (-> Com_option$ Bool))) (= (exists ((?v1 Com_option$)) (?v0 ?v1)) (or (?v0 none$) (exists ((?v1 Com$)) (?v0 (some$ ?v1)))))) :named a169)) -(assert (! (forall ((?v0 State_triple_option$)) (=> (and (=> (= ?v0 none$a) false) (forall ((?v1 State_triple$)) (=> (= ?v0 (some$a ?v1)) false))) false)) :named a170)) -(assert (! (forall ((?v0 Com_option$)) (=> (and (=> (= ?v0 none$) false) (forall ((?v1 Com$)) (=> (= ?v0 (some$ ?v1)) false))) false)) :named a171)) -(assert (! (forall ((?v0 State_triple_option$) (?v1 State_triple$)) (=> (= ?v0 (some$a ?v1)) (not (= ?v0 none$a)))) :named a172)) -(assert (! (forall ((?v0 Com_option$) (?v1 Com$)) (=> (= ?v0 (some$ ?v1)) (not (= ?v0 none$)))) :named a173)) -(assert (! (forall ((?v0 State_triple$)) (not (= none$a (some$a ?v0)))) :named a174)) -(assert (! (forall ((?v0 Com$)) (not (= none$ (some$ ?v0)))) :named a175)) -(assert (! (forall ((?v0 Bool) (?v1 (-> Com$ Bool))) (! (= (case_option$ ?v0 ?v1 none$) ?v0) :pattern ((case_option$ ?v0 ?v1)))) :named a176)) -(assert (! (forall ((?v0 State_triple_option$)) (=> (and (=> (= ?v0 none$a) false) (=> (= ?v0 (some$a (the$a ?v0))) false)) false)) :named a177)) -(assert (! (forall ((?v0 Com_option$)) (=> (and (=> (= ?v0 none$) false) (=> (= ?v0 (some$ (the$ ?v0))) false)) false)) :named a178)) -(assert (! (forall ((?v0 Glb$) (?v1 Loc$)) (not (= (glb$ ?v0) (loc$ ?v1)))) :named a179)) -(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 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)) -(assert (! (forall ((?v0 Com_option$) (?v1 (-> Com$ Com_option$))) (= (= (bind$c ?v0 ?v1) none$) (or (= ?v0 none$) (= (?v1 (the$ ?v0)) none$)))) :named a189)) -(assert (! (forall ((?v0 (-> State$ (-> State$ Bool))) (?v1 Com$) (?v2 (-> State$ (-> State$ Bool))) (?v3 (-> State$ (-> State$ Bool))) (?v4 Com$) (?v5 (-> State$ (-> State$ Bool)))) (= (= (triple$ ?v0 ?v1 ?v2) (triple$ ?v3 ?v4 ?v5)) (and (= ?v0 ?v3) (and (= ?v1 ?v4) (= ?v2 ?v5))))) :named a190)) -(assert (! (forall ((?v0 Nat$) (?v1 (-> State$ (-> State$ Bool))) (?v2 Com$) (?v3 (-> State$ (-> State$ Bool)))) (= (triple_valid$ ?v0 (triple$ ?v1 ?v2 ?v3)) (forall ((?v4 State$) (?v5 State$)) (=> (?v1 ?v4 ?v5) (forall ((?v6 State$)) (=> (evaln$ ?v2 ?v5 ?v0 ?v6) (?v3 ?v4 ?v6))))))) :named a191)) -(assert (! (forall ((?v0 State_triple$)) (=> (forall ((?v1 (-> State$ (-> State$ Bool))) (?v2 Com$) (?v3 (-> State$ (-> State$ Bool)))) (=> (= ?v0 (triple$ ?v1 ?v2 ?v3)) false)) false)) :named a192)) -(assert (! (forall ((?v0 (-> Com$ State_triple_option$))) (! (= (bind$a none$ ?v0) none$a) :pattern ((bind$a none$ ?v0)))) :named a193)) -(assert (! (forall ((?v0 (-> State_triple$ Com_option$))) (! (= (bind$ none$a ?v0) none$) :pattern ((bind$ none$a ?v0)))) :named a194)) -(assert (! (forall ((?v0 (-> State_triple$ State_triple_option$))) (! (= (bind$b none$a ?v0) none$a) :pattern ((bind$b none$a ?v0)))) :named a195)) -(assert (! (forall ((?v0 (-> Com$ Com_option$))) (! (= (bind$c none$ ?v0) none$) :pattern ((bind$c none$ ?v0)))) :named a196)) -(assert (! (forall ((?v0 Nat$) (?v1 State_triple$)) (=> (triple_valid$ (suc$ ?v0) ?v1) (triple_valid$ ?v0 ?v1))) :named a197)) -(assert (! (forall ((?v0 (-> Com_option$ Bool)) (?v1 State_triple_option$) (?v2 (-> State_triple$ Com_option$))) (= (?v0 (bind$ ?v1 ?v2)) (and (=> (= ?v1 none$a) (?v0 none$)) (forall ((?v3 State_triple$)) (=> (= ?v1 (some$a ?v3)) (?v0 (?v2 ?v3))))))) :named a198)) -(assert (! (forall ((?v0 (-> State_triple_option$ Bool)) (?v1 State_triple_option$) (?v2 (-> State_triple$ State_triple_option$))) (= (?v0 (bind$b ?v1 ?v2)) (and (=> (= ?v1 none$a) (?v0 none$a)) (forall ((?v3 State_triple$)) (=> (= ?v1 (some$a ?v3)) (?v0 (?v2 ?v3))))))) :named a199)) -(assert (! (forall ((?v0 (-> State_triple_option$ Bool)) (?v1 Com_option$) (?v2 (-> Com$ State_triple_option$))) (= (?v0 (bind$a ?v1 ?v2)) (and (=> (= ?v1 none$) (?v0 none$a)) (forall ((?v3 Com$)) (=> (= ?v1 (some$ ?v3)) (?v0 (?v2 ?v3))))))) :named a200)) -(assert (! (forall ((?v0 (-> Com_option$ Bool)) (?v1 Com_option$) (?v2 (-> Com$ Com_option$))) (= (?v0 (bind$c ?v1 ?v2)) (and (=> (= ?v1 none$) (?v0 none$)) (forall ((?v3 Com$)) (=> (= ?v1 (some$ ?v3)) (?v0 (?v2 ?v3))))))) :named a201)) -(assert (! (forall ((?v0 (-> Com_option$ Bool)) (?v1 State_triple_option$) (?v2 (-> State_triple$ Com_option$))) (= (?v0 (bind$ ?v1 ?v2)) (not (or (and (= ?v1 none$a) (not (?v0 none$))) (exists ((?v3 State_triple$)) (and (= ?v1 (some$a ?v3)) (not (?v0 (?v2 ?v3))))))))) :named a202)) -(assert (! (forall ((?v0 (-> State_triple_option$ Bool)) (?v1 State_triple_option$) (?v2 (-> State_triple$ State_triple_option$))) (= (?v0 (bind$b ?v1 ?v2)) (not (or (and (= ?v1 none$a) (not (?v0 none$a))) (exists ((?v3 State_triple$)) (and (= ?v1 (some$a ?v3)) (not (?v0 (?v2 ?v3))))))))) :named a203)) -(assert (! (forall ((?v0 (-> State_triple_option$ Bool)) (?v1 Com_option$) (?v2 (-> Com$ State_triple_option$))) (= (?v0 (bind$a ?v1 ?v2)) (not (or (and (= ?v1 none$) (not (?v0 none$a))) (exists ((?v3 Com$)) (and (= ?v1 (some$ ?v3)) (not (?v0 (?v2 ?v3))))))))) :named a204)) -(assert (! (forall ((?v0 (-> Com_option$ Bool)) (?v1 Com_option$) (?v2 (-> Com$ Com_option$))) (= (?v0 (bind$c ?v1 ?v2)) (not (or (and (= ?v1 none$) (not (?v0 none$))) (exists ((?v3 Com$)) (and (= ?v1 (some$ ?v3)) (not (?v0 (?v2 ?v3))))))))) :named a205)) -(assert (! (forall ((?v0 (-> State$ (-> State$ Bool))) (?v1 Pname$) (?v2 (-> State$ (-> State$ Bool)))) (triple_valid$ zero$ (triple$ ?v0 (body$a ?v1) ?v2))) :named a206)) -(assert (! (forall ((?v0 Pname_option$)) (= (= (set_option$ ?v0) bot$) (= ?v0 none$b))) :named a207)) -(assert (! (forall ((?v0 State_triple_option_option$)) (= (= (set_option$c ?v0) bot$a) (= ?v0 none$c))) :named a208)) -(assert (! (forall ((?v0 Com_option_option$)) (= (= (set_option$d ?v0) bot$b) (= ?v0 none$d))) :named a209)) -(assert (! (forall ((?v0 Com_option$)) (= (= (set_option$b ?v0) bot$c) (= ?v0 none$))) :named a210)) -(assert (! (forall ((?v0 State_triple_option$)) (= (= (set_option$a ?v0) bot$d) (= ?v0 none$a))) :named a211)) -(assert (! (= (set_option$ none$b) bot$) :named a212)) -(assert (! (= (set_option$c none$c) bot$a) :named a213)) -(assert (! (= (set_option$d none$d) bot$b) :named a214)) -(assert (! (= (set_option$b none$) bot$c) :named a215)) -(assert (! (= (set_option$a none$a) bot$d) :named a216)) -(assert (! (forall ((?v0 (-> State$ Nat$)) (?v1 (-> State$ (-> State$ Bool))) (?v2 Com$) (?v3 (-> State$ (-> State$ Bool)))) (! (= (size_triple$ ?v0 (triple$ ?v1 ?v2 ?v3)) (suc$ zero$)) :pattern ((size_triple$ ?v0 (triple$ ?v1 ?v2 ?v3))))) :named a217)) -(assert (! (forall ((?v0 Glb$)) (! (= (size_vname$ (glb$ ?v0)) zero$) :pattern ((glb$ ?v0)))) :named a218)) -(assert (! (forall ((?v0 Loc$)) (! (= (size_vname$ (loc$ ?v0)) zero$) :pattern ((loc$ ?v0)))) :named a219)) -(assert (! (forall ((?v0 (-> State_triple$ Nat$))) (! (= (size_option$ ?v0 none$a) (suc$ zero$)) :pattern ((size_option$ ?v0)))) :named a220)) -(assert (! (forall ((?v0 (-> Com$ Nat$))) (! (= (size_option$a ?v0 none$) (suc$ zero$)) :pattern ((size_option$a ?v0)))) :named a221)) -(assert (! (forall ((?v0 (-> State$ (-> State$ Bool))) (?v1 Com$) (?v2 (-> State$ (-> State$ Bool)))) (! (= (size$ (triple$ ?v0 ?v1 ?v2)) (suc$ zero$)) :pattern ((triple$ ?v0 ?v1 ?v2)))) :named a222)) -(assert (! (= (size$a none$a) (suc$ zero$)) :named a223)) -(assert (! (= (size$b none$) (suc$ zero$)) :named a224)) -(assert (! (forall ((?v0 State_triple$)) (not (= (size$ ?v0) zero$))) :named a225)) -(assert (! (forall ((?v0 Glb$)) (! (= (size$c (glb$ ?v0)) zero$) :pattern ((glb$ ?v0)))) :named a226)) -(assert (! (forall ((?v0 Loc$)) (! (= (size$c (loc$ ?v0)) zero$) :pattern ((loc$ ?v0)))) :named a227)) -(assert (! (= (size_com$ skip$) zero$) :named a228)) -(assert (! (forall ((?v0 Pname$)) (! (= (size_com$ (body$a ?v0)) zero$) :pattern ((body$a ?v0)))) :named a229)) -(assert (! (forall ((?v0 Vname$) (?v1 Pname$) (?v2 (-> State$ Nat$))) (! (= (size_com$ (call$ ?v0 ?v1 ?v2)) zero$) :pattern ((call$ ?v0 ?v1 ?v2)))) :named a230)) -(assert (! (forall ((?v0 Vname$) (?v1 (-> State$ Nat$))) (! (= (size_com$ (ass$ ?v0 ?v1)) zero$) :pattern ((ass$ ?v0 ?v1)))) :named a231)) -(assert (! (forall ((?v0 Loc$) (?v1 (-> State$ Nat$)) (?v2 Com$)) (! (= (size_com$ (local$ ?v0 ?v1 ?v2)) (plus$ (size_com$ ?v2) (suc$ zero$))) :pattern ((local$ ?v0 ?v1 ?v2)))) :named a232)) -(assert (! (forall ((?v0 Com$) (?v1 Com$)) (! (= (size_com$ (semi$ ?v0 ?v1)) (plus$ (plus$ (size_com$ ?v0) (size_com$ ?v1)) (suc$ zero$))) :pattern ((semi$ ?v0 ?v1)))) :named a233)) -(assert (! (forall ((?v0 (-> State$ Bool)) (?v1 Com$) (?v2 Com$)) (! (= (size_com$ (cond$ ?v0 ?v1 ?v2)) (plus$ (plus$ (size_com$ ?v1) (size_com$ ?v2)) (suc$ zero$))) :pattern ((cond$ ?v0 ?v1 ?v2)))) :named a234)) -(assert (! (forall ((?v0 (-> State$ Bool)) (?v1 Com$)) (! (= (size_com$ (while$ ?v0 ?v1)) (plus$ (size_com$ ?v1) (suc$ zero$))) :pattern ((while$ ?v0 ?v1)))) :named a235)) -(assert (! (forall ((?v0 Loc$) (?v1 (-> State$ Nat$)) (?v2 Com$)) (! (= (size$d (local$ ?v0 ?v1 ?v2)) (plus$ (size$d ?v2) (suc$ zero$))) :pattern ((local$ ?v0 ?v1 ?v2)))) :named a236)) -(assert (! (forall ((?v0 Com$) (?v1 Com$)) (! (= (size$d (semi$ ?v0 ?v1)) (plus$ (plus$ (size$d ?v0) (size$d ?v1)) (suc$ zero$))) :pattern ((semi$ ?v0 ?v1)))) :named a237)) -(assert (! (forall ((?v0 (-> State$ Bool)) (?v1 Com$) (?v2 Com$)) (! (= (size$d (cond$ ?v0 ?v1 ?v2)) (plus$ (plus$ (size$d ?v1) (size$d ?v2)) (suc$ zero$))) :pattern ((cond$ ?v0 ?v1 ?v2)))) :named a238)) -(assert (! (forall ((?v0 Pname$)) (! (= (size$d (body$a ?v0)) zero$) :pattern ((body$a ?v0)))) :named a239)) -(assert (! (forall ((?v0 Vname$) (?v1 Pname$) (?v2 (-> State$ Nat$))) (! (= (size$d (call$ ?v0 ?v1 ?v2)) zero$) :pattern ((call$ ?v0 ?v1 ?v2)))) :named a240)) -(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 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)) -(assert (! (forall ((?v0 State_triple_set$) (?v1 State_triple_set$) (?v2 State_triple_set$)) (=> (and (hoare_derivs$ ?v0 ?v1) (hoare_derivs$ ?v2 ?v0)) (hoare_derivs$ ?v2 ?v1))) :named a248)) -(assert (! (forall ((?v0 State_triple_option$)) (= (not (= ?v0 none$a)) (case_option$a false uuf$ ?v0))) :named a249)) -(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$)) (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 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$ (-> 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 (-> 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_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 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$) (?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$ 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)) -(assert (! (forall ((?v0 (-> Com$ Com_option$))) (= (= (dom$b ?v0) bot$c) (= ?v0 uue$))) :named a300)) -(assert (! (forall ((?v0 (-> Com$ State_triple_option$))) (= (= (dom$a ?v0) bot$c) (= ?v0 uvb$))) :named a301)) -(assert (! (forall ((?v0 (-> Pname$ State_triple_option$))) (= (= (dom$c ?v0) bot$) (= ?v0 uvc$))) :named a302)) -(assert (! (forall ((?v0 (-> State_triple_option$ Com_option$))) (= (= (dom$e ?v0) bot$a) (= ?v0 uve$))) :named a303)) -(assert (! (forall ((?v0 (-> State_triple_option$ State_triple_option$))) (= (= (dom$d ?v0) bot$a) (= ?v0 uvd$))) :named a304)) -(assert (! (forall ((?v0 (-> Com_option$ Com_option$))) (= (= (dom$g ?v0) bot$b) (= ?v0 uvg$))) :named a305)) -(assert (! (forall ((?v0 (-> Com_option$ State_triple_option$))) (= (= (dom$f ?v0) bot$b) (= ?v0 uvf$))) :named a306)) -(assert (! (forall ((?v0 (-> Pname$ Com_option$))) (= (= (dom$h ?v0) bot$) (= ?v0 uuz$))) :named a307)) -(assert (! (forall ((?v0 (-> State_triple$ Com_option$))) (= (= (dom$i ?v0) bot$d) (= ?v0 uuy$))) :named a308)) -(assert (! (= (dom$ uva$) bot$d) :named a309)) -(assert (! (= (dom$b uue$) bot$c) :named a310)) -(assert (! (= (dom$a uvb$) bot$c) :named a311)) -(assert (! (= (dom$c uvc$) bot$) :named a312)) -(assert (! (= (dom$e uve$) bot$a) :named a313)) -(assert (! (= (dom$d uvd$) bot$a) :named a314)) -(assert (! (= (dom$g uvg$) bot$b) :named a315)) -(assert (! (= (dom$f uvf$) bot$b) :named a316)) -(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 (-> 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$)) (?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)) -(assert (! (forall ((?v0 (-> State_triple$ State_triple$)) (?v1 State_triple_option$)) (= (= (map_option$c ?v0 ?v1) none$a) (= ?v1 none$a))) :named a344)) -(assert (! (forall ((?v0 (-> Com$ Com$)) (?v1 Com_option$)) (= (= (map_option$ ?v0 ?v1) none$) (= ?v1 none$))) :named a345)) -(assert (! (forall ((?v0 (-> State_triple$ Com$)) (?v1 State_triple_option$)) (= (= (map_option$a ?v0 ?v1) none$) (= ?v1 none$a))) :named a346)) -(assert (! (forall ((?v0 (-> Com$ State_triple$)) (?v1 Com_option$)) (= (= (map_option$b ?v0 ?v1) none$a) (= ?v1 none$))) :named a347)) -(assert (! (forall ((?v0 (-> State_triple$ State_triple$)) (?v1 State_triple_option$)) (= (= (map_option$c ?v0 ?v1) none$a) (= ?v1 none$a))) :named a348)) -(assert (! (forall ((?v0 (-> Com$ Com$)) (?v1 Com_option$)) (= (= (map_option$ ?v0 ?v1) none$) (= ?v1 none$))) :named a349)) -(assert (! (forall ((?v0 (-> State_triple$ Com$)) (?v1 State_triple_option$)) (= (= none$ (map_option$a ?v0 ?v1)) (= ?v1 none$a))) :named a350)) -(assert (! (forall ((?v0 (-> Com$ State_triple$)) (?v1 Com_option$)) (= (= none$a (map_option$b ?v0 ?v1)) (= ?v1 none$))) :named a351)) -(assert (! (forall ((?v0 (-> State_triple$ State_triple$)) (?v1 State_triple_option$)) (= (= none$a (map_option$c ?v0 ?v1)) (= ?v1 none$a))) :named a352)) -(assert (! (forall ((?v0 (-> Com$ Com$)) (?v1 Com_option$)) (= (= none$ (map_option$ ?v0 ?v1)) (= ?v1 none$))) :named a353)) -(assert (! (forall ((?v0 (-> Com$ State_triple$))) (! (= (map_option$b ?v0 none$) none$a) :pattern ((map_option$b ?v0)))) :named a354)) -(assert (! (forall ((?v0 (-> State_triple$ Com$))) (! (= (map_option$a ?v0 none$a) none$) :pattern ((map_option$a ?v0)))) :named a355)) -(assert (! (forall ((?v0 (-> State_triple$ State_triple$))) (! (= (map_option$c ?v0 none$a) none$a) :pattern ((map_option$c ?v0)))) :named a356)) -(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_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)) -(check-sat) -;(get-proof) |