:: SCMPDS_I semantic presentation begin theorem :: SCMPDS_I:1 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k4_numbers :::"INT"::: ) )))) ; begin definitionfunc :::"SCMPDS-Instr"::: -> ($#m1_hidden :::"set"::: ) equals :: SCMPDS_I:def 1 (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set ($#k1_tarski :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Num 14) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "l")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where l "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) : (Bool verum) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Num 1) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "sp")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where sp "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) : (Bool verum) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "v")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where I "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)), v "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), c "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) : (Bool (Set (Var "I")) ($#r2_hidden :::"in"::: ) (Set ($#k2_tarski :::"{"::: ) (Num 2) "," (Num 3) ($#k2_tarski :::"}"::: ) )) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "v")) "," (Set (Var "c1")) "," (Set (Var "c2")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where I "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)), v "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), c1, c2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) : (Bool (Set (Var "I")) ($#r2_hidden :::"in"::: ) (Set ($#k3_enumset1 :::"{"::: ) (Num 4) "," (Num 5) "," (Num 6) "," (Num 7) "," (Num 8) ($#k3_enumset1 :::"}"::: ) )) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k7_finseq_4 :::"<*"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "c1")) "," (Set (Var "c2")) ($#k7_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where I "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)), v1, v2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), c1, c2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) : (Bool (Set (Var "I")) ($#r2_hidden :::"in"::: ) (Set ($#k3_enumset1 :::"{"::: ) (Num 9) "," (Num 10) "," (Num 11) "," (Num 12) "," (Num 13) ($#k3_enumset1 :::"}"::: ) )) "}" ); end; :: deftheorem defines :::"SCMPDS-Instr"::: SCMPDS_I:def 1 : (Bool (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set ($#k1_tarski :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Num 14) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "l")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where l "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) : (Bool verum) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Num 1) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "sp")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where sp "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) : (Bool verum) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "v")) "," (Set (Var "c")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where I "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)), v "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), c "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) : (Bool (Set (Var "I")) ($#r2_hidden :::"in"::: ) (Set ($#k2_tarski :::"{"::: ) (Num 2) "," (Num 3) ($#k2_tarski :::"}"::: ) )) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "v")) "," (Set (Var "c1")) "," (Set (Var "c2")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where I "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)), v "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), c1, c2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) : (Bool (Set (Var "I")) ($#r2_hidden :::"in"::: ) (Set ($#k3_enumset1 :::"{"::: ) (Num 4) "," (Num 5) "," (Num 6) "," (Num 7) "," (Num 8) ($#k3_enumset1 :::"}"::: ) )) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k7_finseq_4 :::"<*"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "c1")) "," (Set (Var "c2")) ($#k7_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where I "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)), v1, v2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), c1, c2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) : (Bool (Set (Var "I")) ($#r2_hidden :::"in"::: ) (Set ($#k3_enumset1 :::"{"::: ) (Num 9) "," (Num 10) "," (Num 11) "," (Num 12) "," (Num 13) ($#k3_enumset1 :::"}"::: ) )) "}" )); theorem :: SCMPDS_I:2 (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Num 14) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) )) ; registration cluster (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ); let "s" be ($#m1_hidden :::"Integer":::); :: original: :::"<*"::: redefine func :::"<*":::"d" "," "s":::"*>"::: -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k4_numbers :::"INT"::: ) )); end; definitionlet "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ); given "mk" being ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), "I" being ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)) such that (Bool (Set (Const "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Const "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Const "mk")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )) ; func "x" :::"address_1"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) means :: SCMPDS_I:def 2 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "x" ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) ")" )); end; :: deftheorem defines :::"address_1"::: SCMPDS_I:def 2 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) "st" (Bool (Bool "ex" (Set (Var "mk")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "I")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#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")) ($#k3_scmpds_i :::"address_1"::: ) )) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) ")" )) ")" ))); theorem :: SCMPDS_I:3 (Bool "for" (Set (Var "I")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) (Bool "for" (Set (Var "mk")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "x")) ($#k3_scmpds_i :::"address_1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "mk")))))) ; definitionlet "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ); given "r" being ($#m1_hidden :::"Integer":::), "I" being ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)) such that (Bool (Set (Const "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Const "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Const "r")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )) ; func "x" :::"const_INT"::: -> ($#m1_hidden :::"Integer":::) means :: SCMPDS_I:def 3 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "x" ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) ")" )); end; :: deftheorem defines :::"const_INT"::: SCMPDS_I:def 3 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) "st" (Bool (Bool "ex" (Set (Var "r")) "being" ($#m1_hidden :::"Integer":::)(Bool "ex" (Set (Var "I")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "r")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))))) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_scmpds_i :::"const_INT"::: ) )) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) ")" )) ")" ))); theorem :: SCMPDS_I:4 (Bool "for" (Set (Var "I")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "k")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "x")) ($#k4_scmpds_i :::"const_INT"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "k")))))) ; definitionlet "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ); given "mk" being ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), "r" being ($#m1_hidden :::"Integer":::), "I" being ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)) such that (Bool (Set (Const "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Const "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k2_scmpds_i :::"<*"::: ) (Set (Const "mk")) "," (Set (Const "r")) ($#k2_scmpds_i :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )) ; func "x" :::"P21address"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) means :: SCMPDS_I:def 4 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k4_numbers :::"INT"::: ) )) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "x" ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) ")" )); func "x" :::"P22const"::: -> ($#m1_hidden :::"Integer":::) means :: SCMPDS_I:def 5 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k4_numbers :::"INT"::: ) )) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "x" ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2))) ")" )); end; :: deftheorem defines :::"P21address"::: SCMPDS_I:def 4 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) "st" (Bool (Bool "ex" (Set (Var "mk")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "r")) "being" ($#m1_hidden :::"Integer":::)(Bool "ex" (Set (Var "I")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k2_scmpds_i :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "r")) ($#k2_scmpds_i :::"*>"::: ) ) ($#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")) ($#k5_scmpds_i :::"P21address"::: ) )) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k4_numbers :::"INT"::: ) )) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) ")" )) ")" ))); :: deftheorem defines :::"P22const"::: SCMPDS_I:def 5 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) "st" (Bool (Bool "ex" (Set (Var "mk")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "r")) "being" ($#m1_hidden :::"Integer":::)(Bool "ex" (Set (Var "I")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k2_scmpds_i :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "r")) ($#k2_scmpds_i :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))))) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_scmpds_i :::"P22const"::: ) )) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k4_numbers :::"INT"::: ) )) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2))) ")" )) ")" ))); theorem :: SCMPDS_I:5 (Bool "for" (Set (Var "I")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) (Bool "for" (Set (Var "mk")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k2_scmpds_i :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "r")) ($#k2_scmpds_i :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k5_scmpds_i :::"P21address"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "mk"))) & (Bool (Set (Set (Var "x")) ($#k6_scmpds_i :::"P22const"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "r"))) ")" ))))) ; definitionlet "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ); given "m1" being ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), "k1", "k2" being ($#m1_hidden :::"Integer":::), "I" being ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)) such that (Bool (Set (Const "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Const "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Const "m1")) "," (Set (Const "k1")) "," (Set (Const "k2")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )) ; func "x" :::"P31address"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) means :: SCMPDS_I:def 6 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k4_numbers :::"INT"::: ) )) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "x" ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) ")" )); func "x" :::"P32const"::: -> ($#m1_hidden :::"Integer":::) means :: SCMPDS_I:def 7 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k4_numbers :::"INT"::: ) )) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "x" ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2))) ")" )); func "x" :::"P33const"::: -> ($#m1_hidden :::"Integer":::) means :: SCMPDS_I:def 8 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k4_numbers :::"INT"::: ) )) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "x" ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 3))) ")" )); end; :: deftheorem defines :::"P31address"::: SCMPDS_I:def 6 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) "st" (Bool (Bool "ex" (Set (Var "m1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::)(Bool "ex" (Set (Var "I")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "m1")) "," (Set (Var "k1")) "," (Set (Var "k2")) ($#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")) ($#k7_scmpds_i :::"P31address"::: ) )) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k4_numbers :::"INT"::: ) )) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) ")" )) ")" ))); :: deftheorem defines :::"P32const"::: SCMPDS_I:def 7 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) "st" (Bool (Bool "ex" (Set (Var "m1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::)(Bool "ex" (Set (Var "I")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "m1")) "," (Set (Var "k1")) "," (Set (Var "k2")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))))) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k8_scmpds_i :::"P32const"::: ) )) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k4_numbers :::"INT"::: ) )) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2))) ")" )) ")" ))); :: deftheorem defines :::"P33const"::: SCMPDS_I:def 8 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) "st" (Bool (Bool "ex" (Set (Var "m1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::)(Bool "ex" (Set (Var "I")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "m1")) "," (Set (Var "k1")) "," (Set (Var "k2")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))))) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k9_scmpds_i :::"P33const"::: ) )) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k4_numbers :::"INT"::: ) )) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 3))) ")" )) ")" ))); theorem :: SCMPDS_I:6 (Bool "for" (Set (Var "I")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) (Bool "for" (Set (Var "d1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "d1")) "," (Set (Var "k1")) "," (Set (Var "k2")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k7_scmpds_i :::"P31address"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "d1"))) & (Bool (Set (Set (Var "x")) ($#k8_scmpds_i :::"P32const"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "k1"))) & (Bool (Set (Set (Var "x")) ($#k9_scmpds_i :::"P33const"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "k2"))) ")" ))))) ; definitionlet "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ); given "m1", "m2" being ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), "k1", "k2" being ($#m1_hidden :::"Integer":::), "I" being ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)) such that (Bool (Set (Const "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Const "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k7_finseq_4 :::"<*"::: ) (Set (Const "m1")) "," (Set (Const "m2")) "," (Set (Const "k1")) "," (Set (Const "k2")) ($#k7_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )) ; func "x" :::"P41address"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) means :: SCMPDS_I:def 9 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k4_numbers :::"INT"::: ) )) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "x" ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) ")" )); func "x" :::"P42address"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) means :: SCMPDS_I:def 10 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k4_numbers :::"INT"::: ) )) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "x" ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2))) ")" )); func "x" :::"P43const"::: -> ($#m1_hidden :::"Integer":::) means :: SCMPDS_I:def 11 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k4_numbers :::"INT"::: ) )) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "x" ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 3))) ")" )); func "x" :::"P44const"::: -> ($#m1_hidden :::"Integer":::) means :: SCMPDS_I:def 12 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k4_numbers :::"INT"::: ) )) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "x" ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 4))) ")" )); end; :: deftheorem defines :::"P41address"::: SCMPDS_I:def 9 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) "st" (Bool (Bool "ex" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::)(Bool "ex" (Set (Var "I")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k7_finseq_4 :::"<*"::: ) (Set (Var "m1")) "," (Set (Var "m2")) "," (Set (Var "k1")) "," (Set (Var "k2")) ($#k7_finseq_4 :::"*>"::: ) ) ($#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")) ($#k10_scmpds_i :::"P41address"::: ) )) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k4_numbers :::"INT"::: ) )) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) ")" )) ")" ))); :: deftheorem defines :::"P42address"::: SCMPDS_I:def 10 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) "st" (Bool (Bool "ex" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::)(Bool "ex" (Set (Var "I")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k7_finseq_4 :::"<*"::: ) (Set (Var "m1")) "," (Set (Var "m2")) "," (Set (Var "k1")) "," (Set (Var "k2")) ($#k7_finseq_4 :::"*>"::: ) ) ($#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")) ($#k11_scmpds_i :::"P42address"::: ) )) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k4_numbers :::"INT"::: ) )) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2))) ")" )) ")" ))); :: deftheorem defines :::"P43const"::: SCMPDS_I:def 11 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) "st" (Bool (Bool "ex" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::)(Bool "ex" (Set (Var "I")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k7_finseq_4 :::"<*"::: ) (Set (Var "m1")) "," (Set (Var "m2")) "," (Set (Var "k1")) "," (Set (Var "k2")) ($#k7_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))))) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k12_scmpds_i :::"P43const"::: ) )) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k4_numbers :::"INT"::: ) )) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 3))) ")" )) ")" ))); :: deftheorem defines :::"P44const"::: SCMPDS_I:def 12 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) "st" (Bool (Bool "ex" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::)(Bool "ex" (Set (Var "I")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k7_finseq_4 :::"<*"::: ) (Set (Var "m1")) "," (Set (Var "m2")) "," (Set (Var "k1")) "," (Set (Var "k2")) ($#k7_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))))) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k13_scmpds_i :::"P44const"::: ) )) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k4_numbers :::"INT"::: ) )) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 4))) ")" )) ")" ))); theorem :: SCMPDS_I:7 (Bool "for" (Set (Var "I")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k7_finseq_4 :::"<*"::: ) (Set (Var "d1")) "," (Set (Var "d2")) "," (Set (Var "k1")) "," (Set (Var "k2")) ($#k7_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k10_scmpds_i :::"P41address"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "d1"))) & (Bool (Set (Set (Var "x")) ($#k11_scmpds_i :::"P42address"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "d2"))) & (Bool (Set (Set (Var "x")) ($#k12_scmpds_i :::"P43const"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "k1"))) & (Bool (Set (Set (Var "x")) ($#k13_scmpds_i :::"P44const"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "k2"))) ")" ))))) ; definitionfunc :::"RetSP"::: -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: SCMPDS_I:def 13 (Set ($#k6_numbers :::"0"::: ) ); func :::"RetIC"::: -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: SCMPDS_I:def 14 (Num 1); end; :: deftheorem defines :::"RetSP"::: SCMPDS_I:def 13 : (Bool (Set ($#k14_scmpds_i :::"RetSP"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )); :: deftheorem defines :::"RetIC"::: SCMPDS_I:def 14 : (Bool (Set ($#k15_scmpds_i :::"RetIC"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)); theorem :: SCMPDS_I:8 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set ($#k4_xtuple_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Num 14) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "l")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where l "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) : (Bool verum) "}" ) & (Bool (Set ($#k4_xtuple_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 14)) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Num 1) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "sp")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where sp "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) : (Bool verum) "}" ) & (Bool (Set ($#k4_xtuple_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k2_scmpds_i :::"<*"::: ) (Set (Var "v")) "," (Set (Var "c")) ($#k2_scmpds_i :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where I "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)), v "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), c "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) : (Bool (Set (Var "I")) ($#r2_hidden :::"in"::: ) (Set ($#k2_tarski :::"{"::: ) (Num 2) "," (Num 3) ($#k2_tarski :::"}"::: ) )) "}" ) & (Bool "(" (Bool (Set ($#k4_xtuple_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 2)) "or" (Bool (Set ($#k4_xtuple_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 3)) ")" ) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "v")) "," (Set (Var "c1")) "," (Set (Var "c2")) ($#k11_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where I "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)), v "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), c1, c2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) : (Bool (Set (Var "I")) ($#r2_hidden :::"in"::: ) (Set ($#k3_enumset1 :::"{"::: ) (Num 4) "," (Num 5) "," (Num 6) "," (Num 7) "," (Num 8) ($#k3_enumset1 :::"}"::: ) )) "}" ) & (Bool "(" (Bool (Set ($#k4_xtuple_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 4)) "or" (Bool (Set ($#k4_xtuple_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 5)) "or" (Bool (Set ($#k4_xtuple_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 6)) "or" (Bool (Set ($#k4_xtuple_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 7)) "or" (Bool (Set ($#k4_xtuple_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 8)) ")" ) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k7_finseq_4 :::"<*"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "c1")) "," (Set (Var "c2")) ($#k7_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where I "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 15)), v1, v2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), c1, c2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) : (Bool (Set (Var "I")) ($#r2_hidden :::"in"::: ) (Set ($#k3_enumset1 :::"{"::: ) (Num 9) "," (Num 10) "," (Num 11) "," (Num 12) "," (Num 13) ($#k3_enumset1 :::"}"::: ) )) "}" ) & (Bool "(" (Bool (Set ($#k4_xtuple_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 9)) "or" (Bool (Set ($#k4_xtuple_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 10)) "or" (Bool (Set ($#k4_xtuple_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 11)) "or" (Bool (Set ($#k4_xtuple_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 12)) "or" (Bool (Set ($#k4_xtuple_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 13)) ")" ) ")" ) ")" )) ; begin registration cluster (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) )) -> ($#v3_finseq_1 :::"FinSequence-membered"::: ) ; end; registration cluster (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) -> ($#v1_compos_0 :::"standard-ins"::: ) ; end; registration cluster (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) -> ($#v2_compos_0 :::"homogeneous"::: ) ; end; registration cluster (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) -> ($#v3_compos_0 :::"J/A-independent"::: ) ; end; registration cluster (Set ($#k1_scmpds_i :::"SCMPDS-Instr"::: ) ) -> ($#v5_compos_0 :::"with_halt"::: ) ; end;