:: SCMFSA_1 semantic presentation begin notationsynonym :::"SCM+FSA-Data-Loc"::: for :::"SCM-Data-Loc"::: ; end; definitioncanceled; func :::"SCM+FSA-Memory"::: -> ($#m1_hidden :::"set"::: ) equals :: SCMFSA_1:def 2 (Set (Set ($#k1_ami_2 :::"SCM-Memory"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) )); end; :: deftheorem SCMFSA_1:def 1 : canceled; :: deftheorem defines :::"SCM+FSA-Memory"::: SCMFSA_1:def 2 : (Bool (Set ($#k1_scmfsa_1 :::"SCM+FSA-Memory"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_ami_2 :::"SCM-Memory"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) ))); registration cluster (Set ($#k1_scmfsa_1 :::"SCM+FSA-Memory"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: SCMFSA_1:1 (Bool (Set ($#k1_ami_2 :::"SCM-Memory"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_scmfsa_1 :::"SCM+FSA-Memory"::: ) )) ; definition:: original: :::"SCM+FSA-Data-Loc"::: redefine func :::"SCM+FSA-Data-Loc"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_scmfsa_1 :::"SCM+FSA-Memory"::: ) ); end; definition:: original: :::"SCM+FSA-Data*-Loc"::: redefine func :::"SCM+FSA-Data*-Loc"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_scmfsa_1 :::"SCM+FSA-Memory"::: ) ); end; registration cluster (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitioncanceled; func :::"SCM+FSA-OK"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_scmfsa_1 :::"SCM+FSA-Memory"::: ) ) "," (Num 3) equals :: SCMFSA_1:def 4 (Set (Set "(" (Set ($#k1_scmfsa_1 :::"SCM+FSA-Memory"::: ) ) ($#k8_funcop_1 :::"-->"::: ) (Num 2) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set ($#k3_ami_2 :::"SCM-OK"::: ) )); end; :: deftheorem SCMFSA_1:def 3 : canceled; :: deftheorem defines :::"SCM+FSA-OK"::: SCMFSA_1:def 4 : (Bool (Set ($#k4_scmfsa_1 :::"SCM+FSA-OK"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k1_scmfsa_1 :::"SCM+FSA-Memory"::: ) ) ($#k8_funcop_1 :::"-->"::: ) (Num 2) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set ($#k3_ami_2 :::"SCM-OK"::: ) ))); theorem :: SCMFSA_1:2 canceled; theorem :: SCMFSA_1:3 canceled; theorem :: SCMFSA_1:4 canceled; theorem :: SCMFSA_1:5 (Bool (Set ($#k5_numbers :::"NAT"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_scmfsa_1 :::"SCM+FSA-Memory"::: ) )) ; theorem :: SCMFSA_1:6 canceled; theorem :: SCMFSA_1:7 canceled; theorem :: SCMFSA_1:8 (Bool (Set ($#k1_scmfsa_1 :::"SCM+FSA-Memory"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k1_tarski :::"{"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_scmfsa_1 :::"SCM+FSA-Data-Loc"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k3_scmfsa_1 :::"SCM+FSA-Data*-Loc"::: ) ))) ; definitionfunc :::"SCM*-VAL"::: -> ($#m1_hidden :::"ManySortedSet":::) "of" (Num 3) equals :: SCMFSA_1:def 5 (Set ($#k7_afinsq_1 :::"<%"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k4_numbers :::"INT"::: ) ) "," (Set "(" (Set ($#k4_numbers :::"INT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k7_afinsq_1 :::"%>"::: ) ); end; :: deftheorem defines :::"SCM*-VAL"::: SCMFSA_1:def 5 : (Bool (Set ($#k5_scmfsa_1 :::"SCM*-VAL"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_afinsq_1 :::"<%"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k4_numbers :::"INT"::: ) ) "," (Set "(" (Set ($#k4_numbers :::"INT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k7_afinsq_1 :::"%>"::: ) )); theorem :: SCMFSA_1:9 (Bool (Set (Set "(" (Set ($#k5_scmfsa_1 :::"SCM*-VAL"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set ($#k4_scmfsa_1 :::"SCM+FSA-OK"::: ) ) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ; theorem :: SCMFSA_1:10 (Bool "for" (Set (Var "b")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_scmfsa_1 :::"SCM+FSA-Data-Loc"::: ) ) "holds" (Bool (Set (Set "(" (Set ($#k5_scmfsa_1 :::"SCM*-VAL"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set ($#k4_scmfsa_1 :::"SCM+FSA-OK"::: ) ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k4_numbers :::"INT"::: ) ))) ; theorem :: SCMFSA_1:11 (Bool "for" (Set (Var "f")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_scmfsa_1 :::"SCM+FSA-Data*-Loc"::: ) ) "holds" (Bool (Set (Set "(" (Set ($#k5_scmfsa_1 :::"SCM*-VAL"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set ($#k4_scmfsa_1 :::"SCM+FSA-OK"::: ) ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_numbers :::"INT"::: ) ) ($#k3_finseq_2 :::"*"::: ) ))) ; registration cluster (Set (Set ($#k4_scmfsa_1 :::"SCM+FSA-OK"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set ($#k5_scmfsa_1 :::"SCM*-VAL"::: ) )) -> ($#v2_relat_1 :::"non-empty"::: ) ; end; definitionmode SCM+FSA-State is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" (Set ($#k5_scmfsa_1 :::"SCM*-VAL"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set ($#k4_scmfsa_1 :::"SCM+FSA-OK"::: ) ) ")" )); end; theorem :: SCMFSA_1:12 canceled; theorem :: SCMFSA_1:13 canceled; theorem :: SCMFSA_1:14 canceled; theorem :: SCMFSA_1:15 canceled; theorem :: SCMFSA_1:16 canceled; theorem :: SCMFSA_1:17 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM+FSA-State":::) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ) "holds" (Bool (Set (Set (Var "s")) ($#k11_card_3 :::"|"::: ) (Set ($#k1_ami_2 :::"SCM-Memory"::: ) )) "is" ($#m1_subset_1 :::"SCM-State":::)))) ; theorem :: SCMFSA_1:18 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM+FSA-State":::) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"SCM-State":::) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "s1"))) "is" ($#m1_subset_1 :::"SCM+FSA-State":::)))) ; definitionlet "s" be ($#m1_subset_1 :::"SCM+FSA-State":::); let "u" be ($#m1_hidden :::"Nat":::); func :::"SCM+FSA-Chg"::: "(" "s" "," "u" ")" -> ($#m1_subset_1 :::"SCM+FSA-State":::) equals :: SCMFSA_1:def 6 (Set "s" ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k5_numbers :::"NAT"::: ) ) ($#k16_funcop_1 :::".-->"::: ) "u" ")" )); end; :: deftheorem defines :::"SCM+FSA-Chg"::: SCMFSA_1:def 6 : (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM+FSA-State":::) (Bool "for" (Set (Var "u")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k6_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set (Var "s")) "," (Set (Var "u")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k5_numbers :::"NAT"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "u")) ")" ))))); definitionlet "s" be ($#m1_subset_1 :::"SCM+FSA-State":::); let "t" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_scmfsa_1 :::"SCM+FSA-Data-Loc"::: ) ); let "u" be ($#m1_hidden :::"Integer":::); func :::"SCM+FSA-Chg"::: "(" "s" "," "t" "," "u" ")" -> ($#m1_subset_1 :::"SCM+FSA-State":::) equals :: SCMFSA_1:def 7 (Set "s" ($#k1_funct_4 :::"+*"::: ) (Set "(" "t" ($#k16_funcop_1 :::".-->"::: ) "u" ")" )); end; :: deftheorem defines :::"SCM+FSA-Chg"::: SCMFSA_1:def 7 : (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM+FSA-State":::) (Bool "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_scmfsa_1 :::"SCM+FSA-Data-Loc"::: ) ) (Bool "for" (Set (Var "u")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k7_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "t")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "u")) ")" )))))); definitionlet "s" be ($#m1_subset_1 :::"SCM+FSA-State":::); let "t" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_scmfsa_1 :::"SCM+FSA-Data*-Loc"::: ) ); let "u" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ); func :::"SCM+FSA-Chg"::: "(" "s" "," "t" "," "u" ")" -> ($#m1_subset_1 :::"SCM+FSA-State":::) equals :: SCMFSA_1:def 8 (Set "s" ($#k1_funct_4 :::"+*"::: ) (Set "(" "t" ($#k16_funcop_1 :::".-->"::: ) "u" ")" )); end; :: deftheorem defines :::"SCM+FSA-Chg"::: SCMFSA_1:def 8 : (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM+FSA-State":::) (Bool "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_scmfsa_1 :::"SCM+FSA-Data*-Loc"::: ) ) (Bool "for" (Set (Var "u")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "holds" (Bool (Set ($#k8_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "t")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "u")) ")" )))))); registrationlet "s" be ($#m1_subset_1 :::"SCM+FSA-State":::); let "a" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_scmfsa_1 :::"SCM+FSA-Data-Loc"::: ) ); cluster (Set "s" ($#k1_funct_1 :::"."::: ) "a") -> ($#v1_int_1 :::"integer"::: ) ; end; definitionlet "s" be ($#m1_subset_1 :::"SCM+FSA-State":::); let "a" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_scmfsa_1 :::"SCM+FSA-Data*-Loc"::: ) ); :: original: :::"."::: redefine func "s" :::"."::: "a" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ); end; definitioncanceled; canceled; canceled; canceled; canceled; canceled; let "s" be ($#m1_subset_1 :::"SCM+FSA-State":::); func :::"IC"::: "s" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: SCMFSA_1:def 15 (Set "s" ($#k1_funct_1 :::"."::: ) (Set ($#k5_numbers :::"NAT"::: ) )); end; :: deftheorem SCMFSA_1:def 9 : canceled; :: deftheorem SCMFSA_1:def 10 : canceled; :: deftheorem SCMFSA_1:def 11 : canceled; :: deftheorem SCMFSA_1:def 12 : canceled; :: deftheorem SCMFSA_1:def 13 : canceled; :: deftheorem SCMFSA_1:def 14 : canceled; :: deftheorem defines :::"IC"::: SCMFSA_1:def 15 : (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM+FSA-State":::) "holds" (Bool (Set ($#k10_scmfsa_1 :::"IC"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set ($#k5_numbers :::"NAT"::: ) )))); definitionlet "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ); let "s" be ($#m1_subset_1 :::"SCM+FSA-State":::); func :::"SCM+FSA-Exec-Res"::: "(" "x" "," "s" ")" -> ($#m1_subset_1 :::"SCM+FSA-State":::) means :: SCMFSA_1:def 16 (Bool "ex" (Set (Var "x9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_scm_inst :::"SCM-Instr"::: ) )(Bool "ex" (Set (Var "s9")) "being" ($#m1_subset_1 :::"SCM-State":::) "st" (Bool "(" (Bool "x" ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool (Set (Var "s9")) ($#r1_hidden :::"="::: ) (Set "s" ($#k11_card_3 :::"|"::: ) (Set ($#k1_ami_2 :::"SCM-Memory"::: ) ))) & (Bool it ($#r1_hidden :::"="::: ) (Set "s" ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k8_ami_2 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x9")) "," (Set (Var "s9")) ")" ")" ))) ")" ))) if (Bool (Set "x" ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Num 8)) (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::)(Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set ($#k1_int_2 :::"abs"::: ) (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" "x" ($#k4_scmfsa_i :::"int_addr2"::: ) ")" ) ")" ))) & (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set "(" "s" ($#k9_scmfsa_1 :::"."::: ) (Set "(" "x" ($#k5_scmfsa_i :::"coll_addr1"::: ) ")" ) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set "(" ($#k7_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" "s" "," (Set "(" "x" ($#k3_scmfsa_i :::"int_addr1"::: ) ")" ) "," (Set (Var "i")) ")" ")" ) "," (Set "(" ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k10_scmfsa_1 :::"IC"::: ) "s" ")" ) ")" ) ")" )) ")" ))) if (Bool (Set "x" ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Num 9)) (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) )(Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set ($#k1_int_2 :::"abs"::: ) (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" "x" ($#k4_scmfsa_i :::"int_addr2"::: ) ")" ) ")" ))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set "(" "s" ($#k9_scmfsa_1 :::"."::: ) (Set "(" "x" ($#k5_scmfsa_i :::"coll_addr1"::: ) ")" ) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "k")) "," (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" "x" ($#k3_scmfsa_i :::"int_addr1"::: ) ")" ) ")" ) ")" )) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set "(" ($#k8_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" "s" "," (Set "(" "x" ($#k5_scmfsa_i :::"coll_addr1"::: ) ")" ) "," (Set (Var "f")) ")" ")" ) "," (Set "(" ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k10_scmfsa_1 :::"IC"::: ) "s" ")" ) ")" ) ")" )) ")" ))) if (Bool (Set "x" ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Num 10)) (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set "(" ($#k7_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" "s" "," (Set "(" "x" ($#k7_scmfsa_i :::"int_addr3"::: ) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" "s" ($#k9_scmfsa_1 :::"."::: ) (Set "(" "x" ($#k8_scmfsa_i :::"coll_addr2"::: ) ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k10_scmfsa_1 :::"IC"::: ) "s" ")" ) ")" ) ")" )) if (Bool (Set "x" ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Num 11)) (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) )(Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set ($#k1_int_2 :::"abs"::: ) (Set "(" "s" ($#k1_funct_1 :::"."::: ) (Set "(" "x" ($#k7_scmfsa_i :::"int_addr3"::: ) ")" ) ")" ))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k5_finseq_2 :::"|->"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set "(" ($#k8_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" "s" "," (Set "(" "x" ($#k8_scmfsa_i :::"coll_addr2"::: ) ")" ) "," (Set (Var "f")) ")" ")" ) "," (Set "(" ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k10_scmfsa_1 :::"IC"::: ) "s" ")" ) ")" ) ")" )) ")" ))) if (Bool (Set "x" ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Num 12)) (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool "(" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set "(" ($#k7_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" "s" "," (Set "(" "x" ($#k6_scmfsa_i :::"int_addr"::: ) ")" ) "," (Set (Var "i")) ")" ")" ) "," (Set "(" ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k10_scmfsa_1 :::"IC"::: ) "s" ")" ) ")" ) ")" )) ")" )) if (Bool (Set "x" ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Num 13)) otherwise (Bool it ($#r1_hidden :::"="::: ) "s"); end; :: deftheorem defines :::"SCM+FSA-Exec-Res"::: SCMFSA_1:def 16 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ) (Bool "for" (Set (Var "s")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"SCM+FSA-State":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "x")) ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Num 8))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_1 :::"SCM+FSA-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" )) "iff" (Bool "ex" (Set (Var "x9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_scm_inst :::"SCM-Instr"::: ) )(Bool "ex" (Set (Var "s9")) "being" ($#m1_subset_1 :::"SCM-State":::) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool (Set (Var "s9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k11_card_3 :::"|"::: ) (Set ($#k1_ami_2 :::"SCM-Memory"::: ) ))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k8_ami_2 :::"SCM-Exec-Res"::: ) "(" (Set (Var "x9")) "," (Set (Var "s9")) ")" ")" ))) ")" ))) ")" ) ")" & "(" (Bool (Bool (Set (Set (Var "x")) ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Num 9))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_1 :::"SCM+FSA-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" )) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::)(Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set ($#k1_int_2 :::"abs"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k4_scmfsa_i :::"int_addr2"::: ) ")" ) ")" ))) & (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k9_scmfsa_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k5_scmfsa_i :::"coll_addr1"::: ) ")" ) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "k")))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set "(" ($#k7_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k3_scmfsa_i :::"int_addr1"::: ) ")" ) "," (Set (Var "i")) ")" ")" ) "," (Set "(" ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k10_scmfsa_1 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) ")" )) ")" ))) ")" ) ")" & "(" (Bool (Bool (Set (Set (Var "x")) ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Num 10))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_1 :::"SCM+FSA-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" )) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) )(Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set ($#k1_int_2 :::"abs"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k4_scmfsa_i :::"int_addr2"::: ) ")" ) ")" ))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k9_scmfsa_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k5_scmfsa_i :::"coll_addr1"::: ) ")" ) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set (Var "k")) "," (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k3_scmfsa_i :::"int_addr1"::: ) ")" ) ")" ) ")" )) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set "(" ($#k8_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k5_scmfsa_i :::"coll_addr1"::: ) ")" ) "," (Set (Var "f")) ")" ")" ) "," (Set "(" ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k10_scmfsa_1 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) ")" )) ")" ))) ")" ) ")" & "(" (Bool (Bool (Set (Set (Var "x")) ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Num 11))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_1 :::"SCM+FSA-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" )) "iff" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set "(" ($#k7_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k7_scmfsa_i :::"int_addr3"::: ) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "s")) ($#k9_scmfsa_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k8_scmfsa_i :::"coll_addr2"::: ) ")" ) ")" ) ")" ) ")" ")" ) "," (Set "(" ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k10_scmfsa_1 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) ")" )) ")" ) ")" & "(" (Bool (Bool (Set (Set (Var "x")) ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Num 12))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_1 :::"SCM+FSA-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" )) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) )(Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set ($#k1_int_2 :::"abs"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_scmfsa_i :::"int_addr3"::: ) ")" ) ")" ))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k5_finseq_2 :::"|->"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set "(" ($#k8_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k8_scmfsa_i :::"coll_addr2"::: ) ")" ) "," (Set (Var "f")) ")" ")" ) "," (Set "(" ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k10_scmfsa_1 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) ")" )) ")" ))) ")" ) ")" & "(" (Bool (Bool (Set (Set (Var "x")) ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Num 13))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_1 :::"SCM+FSA-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" )) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool "(" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set "(" ($#k7_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "x")) ($#k6_scmfsa_i :::"int_addr"::: ) ")" ) "," (Set (Var "i")) ")" ")" ) "," (Set "(" ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k10_scmfsa_1 :::"IC"::: ) (Set (Var "s")) ")" ) ")" ) ")" )) ")" )) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Set (Var "x")) ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Num 8))) & (Bool (Bool "not" (Set (Set (Var "x")) ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Num 9))) & (Bool (Bool "not" (Set (Set (Var "x")) ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Num 10))) & (Bool (Bool "not" (Set (Set (Var "x")) ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Num 11))) & (Bool (Bool "not" (Set (Set (Var "x")) ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Num 12))) & (Bool (Bool "not" (Set (Set (Var "x")) ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Num 13)))) "implies" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_1 :::"SCM+FSA-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "s")) ")" )) "iff" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Var "s"))) ")" ) ")" ")" ))); definitionfunc :::"SCM+FSA-Exec"::: -> ($#m1_subset_1 :::"Action":::) "of" (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ) "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" (Set ($#k5_scmfsa_1 :::"SCM*-VAL"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set ($#k4_scmfsa_1 :::"SCM+FSA-OK"::: ) ) ")" ) ")" ) means :: SCMFSA_1:def 17 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"SCM+FSA-State":::) "holds" (Bool (Set (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_1 :::"SCM+FSA-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))); end; :: deftheorem defines :::"SCM+FSA-Exec"::: SCMFSA_1:def 17 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Action":::) "of" (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ) "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" (Set ($#k5_scmfsa_1 :::"SCM*-VAL"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set ($#k4_scmfsa_1 :::"SCM+FSA-OK"::: ) ) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k12_scmfsa_1 :::"SCM+FSA-Exec"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"SCM+FSA-State":::) "holds" (Bool (Set (Set "(" (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k11_scmfsa_1 :::"SCM+FSA-Exec-Res"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))) ")" )); theorem :: SCMFSA_1:19 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM+FSA-State":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k6_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set (Var "s")) "," (Set (Var "u")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "u"))))) ; theorem :: SCMFSA_1:20 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM+FSA-State":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "mk")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_scmfsa_1 :::"SCM+FSA-Data-Loc"::: ) ) "holds" (Bool (Set (Set "(" ($#k6_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set (Var "s")) "," (Set (Var "u")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "mk"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "mk"))))))) ; theorem :: SCMFSA_1:21 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM+FSA-State":::) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_scmfsa_1 :::"SCM+FSA-Data*-Loc"::: ) ) "holds" (Bool (Set (Set "(" ($#k6_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set (Var "s")) "," (Set (Var "u")) ")" ")" ) ($#k9_scmfsa_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k9_scmfsa_1 :::"."::: ) (Set (Var "p"))))))) ; theorem :: SCMFSA_1:22 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM+FSA-State":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k6_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set (Var "s")) "," (Set (Var "u")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "v")))))) ; theorem :: SCMFSA_1:23 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM+FSA-State":::) (Bool "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_scmfsa_1 :::"SCM+FSA-Data-Loc"::: ) ) (Bool "for" (Set (Var "u")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set "(" ($#k7_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set ($#k5_numbers :::"NAT"::: ) )))))) ; theorem :: SCMFSA_1:24 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM+FSA-State":::) (Bool "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_scmfsa_1 :::"SCM+FSA-Data-Loc"::: ) ) (Bool "for" (Set (Var "u")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set "(" ($#k7_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Var "u")))))) ; theorem :: SCMFSA_1:25 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM+FSA-State":::) (Bool "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_scmfsa_1 :::"SCM+FSA-Data-Loc"::: ) ) (Bool "for" (Set (Var "u")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "mk")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_scmfsa_1 :::"SCM+FSA-Data-Loc"::: ) ) "st" (Bool (Bool (Set (Var "mk")) ($#r1_hidden :::"<>"::: ) (Set (Var "t")))) "holds" (Bool (Set (Set "(" ($#k7_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "mk"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "mk")))))))) ; theorem :: SCMFSA_1:26 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM+FSA-State":::) (Bool "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_scmfsa_1 :::"SCM+FSA-Data-Loc"::: ) ) (Bool "for" (Set (Var "u")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "f")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_scmfsa_1 :::"SCM+FSA-Data*-Loc"::: ) ) "holds" (Bool (Set (Set "(" ($#k7_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) ")" ")" ) ($#k9_scmfsa_1 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k9_scmfsa_1 :::"."::: ) (Set (Var "f")))))))) ; theorem :: SCMFSA_1:27 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM+FSA-State":::) (Bool "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_scmfsa_1 :::"SCM+FSA-Data*-Loc"::: ) ) (Bool "for" (Set (Var "u")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "holds" (Bool (Set (Set "(" ($#k8_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) ")" ")" ) ($#k9_scmfsa_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Var "u")))))) ; theorem :: SCMFSA_1:28 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM+FSA-State":::) (Bool "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_scmfsa_1 :::"SCM+FSA-Data*-Loc"::: ) ) (Bool "for" (Set (Var "u")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) (Bool "for" (Set (Var "mk")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_scmfsa_1 :::"SCM+FSA-Data*-Loc"::: ) ) "st" (Bool (Bool (Set (Var "mk")) ($#r1_hidden :::"<>"::: ) (Set (Var "t")))) "holds" (Bool (Set (Set "(" ($#k8_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) ")" ")" ) ($#k9_scmfsa_1 :::"."::: ) (Set (Var "mk"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k9_scmfsa_1 :::"."::: ) (Set (Var "mk")))))))) ; theorem :: SCMFSA_1:29 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM+FSA-State":::) (Bool "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k3_scmfsa_1 :::"SCM+FSA-Data*-Loc"::: ) ) (Bool "for" (Set (Var "u")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k2_scmfsa_1 :::"SCM+FSA-Data-Loc"::: ) ) "holds" (Bool (Set (Set "(" ($#k8_scmfsa_1 :::"SCM+FSA-Chg"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))))))) ; theorem :: SCMFSA_1:30 (Bool (Set ($#k3_scmfsa_1 :::"SCM+FSA-Data*-Loc"::: ) ) ($#r1_subset_1 :::"misses"::: ) (Set ($#k1_ami_2 :::"SCM-Memory"::: ) )) ; theorem :: SCMFSA_1:31 canceled; theorem :: SCMFSA_1:32 (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set ($#k5_scmfsa_1 :::"SCM*-VAL"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set ($#k4_scmfsa_1 :::"SCM+FSA-OK"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_scmfsa_1 :::"SCM+FSA-Memory"::: ) )) ; theorem :: SCMFSA_1:33 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM+FSA-State":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k1_scmfsa_1 :::"SCM+FSA-Memory"::: ) ))) ;