path: root/test/regress/regress1/ho/hoa0102.smt2

; 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)