:: SCMFSA_I semantic presentation begin definitionfunc :::"SCM+FSA-Data*-Loc"::: -> ($#m1_hidden :::"set"::: ) equals :: SCMFSA_I:def 1 (Set (Set ($#k4_numbers :::"INT"::: ) ) ($#k6_subset_1 :::"\"::: ) (Set ($#k5_numbers :::"NAT"::: ) )); end; :: deftheorem defines :::"SCM+FSA-Data*-Loc"::: SCMFSA_I:def 1 : (Bool (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_numbers :::"INT"::: ) ) ($#k6_subset_1 :::"\"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))); registration cluster (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionfunc :::"SCM+FSA-Instr"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) equals :: SCMFSA_I:def 2 (Set (Set "(" (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "J")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "b")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where J "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 13)), c, b "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), f "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) ) : (Bool (Set (Var "J")) ($#r2_hidden :::"in"::: ) (Set ($#k2_tarski :::"{"::: ) (Num 9) "," (Num 10) ($#k2_tarski :::"}"::: ) )) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "K")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c1")) "," (Set (Var "f1")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where K "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 13)), c1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), f1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) ) : (Bool (Set (Var "K")) ($#r2_hidden :::"in"::: ) (Set ($#k2_tarski :::"{"::: ) (Num 11) "," (Num 12) ($#k2_tarski :::"}"::: ) )) "}" ); end; :: deftheorem defines :::"SCM+FSA-Instr"::: SCMFSA_I:def 2 : (Bool (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "J")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "b")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where J "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 13)), c, b "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), f "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) ) : (Bool (Set (Var "J")) ($#r2_hidden :::"in"::: ) (Set ($#k2_tarski :::"{"::: ) (Num 9) "," (Num 10) ($#k2_tarski :::"}"::: ) )) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "K")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c1")) "," (Set (Var "f1")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where K "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 13)), c1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), f1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) ) : (Bool (Set (Var "K")) ($#r2_hidden :::"in"::: ) (Set ($#k2_tarski :::"{"::: ) (Num 11) "," (Num 12) ($#k2_tarski :::"}"::: ) )) "}" )); theorem :: SCMFSA_I:1 (Bool (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) )) ; registration cluster (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) )) -> ($#v3_finseq_1 :::"FinSequence-membered"::: ) ; end; registration cluster (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ; end; theorem :: SCMFSA_I:2 (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ) "st" (Bool (Bool (Set (Set (Var "I")) ($#k4_xtuple_0 :::"`1_3"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Num 8))) "holds" (Bool (Set (Var "I")) ($#r2_hidden :::"in"::: ) (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ))) ; theorem :: SCMFSA_I:3 (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) )) ; theorem :: SCMFSA_I:4 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_tarski :::"{"::: ) (Num 9) "," (Num 10) ($#k2_tarski :::"}"::: ) ))) "holds" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "b")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ))))) ; theorem :: SCMFSA_I:5 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_tarski :::"{"::: ) (Num 11) "," (Num 12) ($#k2_tarski :::"}"::: ) ))) "holds" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "f")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ))))) ; definitionlet "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ); given "c" being ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), "f" being ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) ), "b" being ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), "J" being ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 13)) such that (Bool (Set (Const "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Const "J")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Const "c")) "," (Set (Const "f")) "," (Set (Const "b")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )) ; func "x" :::"int_addr1"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) means :: SCMFSA_I:def 3 (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) )(Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) "st" (Bool "(" (Bool (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "b")) ($#k11_finseq_1 :::"*>"::: ) ) ($#r1_hidden :::"="::: ) (Set "x" ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" )))); func "x" :::"int_addr2"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) means :: SCMFSA_I:def 4 (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) )(Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) "st" (Bool "(" (Bool (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "b")) ($#k11_finseq_1 :::"*>"::: ) ) ($#r1_hidden :::"="::: ) (Set "x" ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" )))); func "x" :::"coll_addr1"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) ) means :: SCMFSA_I:def 5 (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) )(Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) "st" (Bool "(" (Bool (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "b")) ($#k11_finseq_1 :::"*>"::: ) ) ($#r1_hidden :::"="::: ) (Set "x" ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set (Var "f"))) ")" )))); end; :: deftheorem defines :::"int_addr1"::: SCMFSA_I:def 3 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ) "st" (Bool (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) )(Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "J")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 13)) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "J")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "b")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))))))) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_scmfsa_i :::"int_addr1"::: ) )) "iff" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) )(Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) "st" (Bool "(" (Bool (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "b")) ($#k11_finseq_1 :::"*>"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" )))) ")" ))); :: deftheorem defines :::"int_addr2"::: SCMFSA_I:def 4 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ) "st" (Bool (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) )(Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "J")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 13)) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "J")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "b")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))))))) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_scmfsa_i :::"int_addr2"::: ) )) "iff" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) )(Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) "st" (Bool "(" (Bool (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "b")) ($#k11_finseq_1 :::"*>"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" )))) ")" ))); :: deftheorem defines :::"coll_addr1"::: SCMFSA_I:def 5 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ) "st" (Bool (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) )(Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "J")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 13)) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "J")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "b")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))))))) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_scmfsa_i :::"coll_addr1"::: ) )) "iff" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) )(Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) "st" (Bool "(" (Bool (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "b")) ($#k11_finseq_1 :::"*>"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Var "f"))) ")" )))) ")" ))); definitionlet "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ); given "c" being ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) such that (Bool (Set (Const "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 13) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Const "c")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )) ; func "x" :::"int_addr"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) means :: SCMFSA_I:def 6 (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) "st" (Bool "(" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "c")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r1_hidden :::"="::: ) (Set "x" ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" )); end; :: deftheorem defines :::"int_addr"::: SCMFSA_I:def 6 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ) "st" (Bool (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 13) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "c")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_scmfsa_i :::"int_addr"::: ) )) "iff" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) "st" (Bool "(" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "c")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" )) ")" ))); definitionlet "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ); given "c" being ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), "f" being ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) ), "J" being ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 13)) such that (Bool (Set (Const "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Const "J")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Const "c")) "," (Set (Const "f")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )) ; func "x" :::"int_addr3"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) means :: SCMFSA_I:def 7 (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) ) "st" (Bool "(" (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "f")) ($#k10_finseq_1 :::"*>"::: ) ) ($#r1_hidden :::"="::: ) (Set "x" ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" ))); func "x" :::"coll_addr2"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) ) means :: SCMFSA_I:def 8 (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) ) "st" (Bool "(" (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "f")) ($#k10_finseq_1 :::"*>"::: ) ) ($#r1_hidden :::"="::: ) (Set "x" ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set (Var "f"))) ")" ))); end; :: deftheorem defines :::"int_addr3"::: SCMFSA_I:def 7 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ) "st" (Bool (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) )(Bool "ex" (Set (Var "J")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 13)) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "J")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "f")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))))) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k7_scmfsa_i :::"int_addr3"::: ) )) "iff" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) ) "st" (Bool "(" (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "f")) ($#k10_finseq_1 :::"*>"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" ))) ")" ))); :: deftheorem defines :::"coll_addr2"::: SCMFSA_I:def 8 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ) "st" (Bool (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) )(Bool "ex" (Set (Var "J")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 13)) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "J")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "f")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))))) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k8_scmfsa_i :::"coll_addr2"::: ) )) "iff" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) ) "st" (Bool "(" (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "f")) ($#k10_finseq_1 :::"*>"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Var "f"))) ")" ))) ")" ))); theorem :: SCMFSA_I:6 (Bool (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" (Set ($#k5_numbers :::"NAT"::: ) ) ($#k13_finseq_1 :::"*"::: ) ")" ) "," (Set "(" ($#k10_xtuple_0 :::"proj2"::: ) (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ) ")" ) ($#k3_zfmisc_1 :::":]"::: ) )) ; theorem :: SCMFSA_I:7 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_scm_inst :::"SCM-Instr"::: ) )) & (Bool "(" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 1)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 2)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 3)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 4)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 5)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 6)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 7)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 8)) ")" ) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "J")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "c")) "," (Set (Var "f")) "," (Set (Var "b")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where J "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 13)), c, b "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), f "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) ) : (Bool (Set (Var "J")) ($#r2_hidden :::"in"::: ) (Set ($#k2_tarski :::"{"::: ) (Num 9) "," (Num 10) ($#k2_tarski :::"}"::: ) )) "}" ) & (Bool "(" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 9)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 10)) ")" ) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "K")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "c1")) "," (Set (Var "f1")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where K "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 13)), c1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), f1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmfsa_i :::"SCM+FSA-Data*-Loc"::: ) ) : (Bool (Set (Var "K")) ($#r2_hidden :::"in"::: ) (Set ($#k2_tarski :::"{"::: ) (Num 11) "," (Num 12) ($#k2_tarski :::"}"::: ) )) "}" ) & (Bool "(" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 11)) "or" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 12)) ")" ) ")" ) ")" )) ; registration cluster (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compos_0 :::"homogeneous"::: ) ; end; theorem :: SCMFSA_I:8 (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"InsType":::) "of" (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Num 9)) "or" (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Num 10)) ")" )) "holds" (Bool (Set ($#k3_compos_0 :::"JumpParts"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: SCMFSA_I:9 (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"InsType":::) "of" (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Num 11)) "or" (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Num 12)) ")" )) "holds" (Bool (Set ($#k3_compos_0 :::"JumpParts"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; registration cluster (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_compos_0 :::"J/A-independent"::: ) ; end; registration cluster (Set ($#k2_scmfsa_i :::"SCM+FSA-Instr"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v5_compos_0 :::"with_halt"::: ) ; end;