:: SCM_INST semantic presentation begin notationsynonym :::"SCM-Halt"::: for :::"{}"::: ; end; definition:: original: :::"SCM-Halt"::: redefine func :::"SCM-Halt"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 9)); end; definitionfunc :::"SCM-Data-Loc"::: -> ($#m1_hidden :::"set"::: ) equals :: SCM_INST:def 1 (Set ($#k8_mcart_1 :::"[:"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Num 1) ($#k6_domain_1 :::"}"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k8_mcart_1 :::":]"::: ) ); end; :: deftheorem defines :::"SCM-Data-Loc"::: SCM_INST:def 1 : (Bool (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k8_mcart_1 :::"[:"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Num 1) ($#k6_domain_1 :::"}"::: ) ) "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k8_mcart_1 :::":]"::: ) )); registration cluster (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionfunc :::"SCM-Instr"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) equals :: SCM_INST:def 2 (Set (Set "(" (Set "(" (Set ($#k1_tarski :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k1_scm_inst :::"SCM-Halt"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "J")) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where J "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 9)), a "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "J")) ($#r1_hidden :::"="::: ) (Num 6)) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "K")) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "a1")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "b1")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where K "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 9)), a1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), b1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) : (Bool (Set (Var "K")) ($#r2_hidden :::"in"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Num 7) "," (Num 8) ($#k7_domain_1 :::"}"::: ) )) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k2_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where I "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 9)), b, c "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) : (Bool (Set (Var "I")) ($#r2_hidden :::"in"::: ) (Set ($#k10_domain_1 :::"{"::: ) (Num 1) "," (Num 2) "," (Num 3) "," (Num 4) "," (Num 5) ($#k10_domain_1 :::"}"::: ) )) "}" ); end; :: deftheorem defines :::"SCM-Instr"::: SCM_INST:def 2 : (Bool (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k1_tarski :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k1_scm_inst :::"SCM-Halt"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "J")) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where J "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 9)), a "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "J")) ($#r1_hidden :::"="::: ) (Num 6)) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "K")) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "a1")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "b1")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where K "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 9)), a1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), b1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) : (Bool (Set (Var "K")) ($#r2_hidden :::"in"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Num 7) "," (Num 8) ($#k7_domain_1 :::"}"::: ) )) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k2_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where I "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 9)), b, c "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) : (Bool (Set (Var "I")) ($#r2_hidden :::"in"::: ) (Set ($#k10_domain_1 :::"{"::: ) (Num 1) "," (Num 2) "," (Num 3) "," (Num 4) "," (Num 5) ($#k10_domain_1 :::"}"::: ) )) "}" )); theorem :: SCM_INST:1 (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_scm_inst :::"SCM-Instr"::: ) )) ; registration cluster (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: SCM_INST:2 (Bool "for" (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Num 6) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "a2")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ))) ; theorem :: SCM_INST:3 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Num 7) "," (Num 8) ($#k7_domain_1 :::"}"::: ) ))) "holds" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x")) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "a2")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "b2")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ))))) ; theorem :: SCM_INST:4 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "c1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_domain_1 :::"{"::: ) (Num 1) "," (Num 2) "," (Num 3) "," (Num 4) "," (Num 5) ($#k10_domain_1 :::"}"::: ) ))) "holds" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "b1")) "," (Set (Var "c1")) ($#k2_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_scm_inst :::"SCM-Instr"::: ) )))) ; definitionlet "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ); given "mk", "ml" being ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), "I" being ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 9)) such that (Bool (Set (Const "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Const "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Const "mk")) "," (Set (Const "ml")) ($#k2_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )) ; func "x" :::"address_1"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) means :: SCM_INST:def 3 (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))) ")" )); func "x" :::"address_2"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) means :: SCM_INST:def 4 (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 2))) ")" )); end; :: deftheorem defines :::"address_1"::: SCM_INST:def 3 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ) "st" (Bool (Bool "ex" (Set (Var "mk")) "," (Set (Var "ml")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 9)) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "ml")) ($#k2_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")) ($#k4_scm_inst :::"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))) ")" )) ")" ))); :: deftheorem defines :::"address_2"::: SCM_INST:def 4 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ) "st" (Bool (Bool "ex" (Set (Var "mk")) "," (Set (Var "ml")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 9)) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "ml")) ($#k2_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")) ($#k5_scm_inst :::"address_2"::: ) )) "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 2))) ")" )) ")" ))); theorem :: SCM_INST:5 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ) (Bool "for" (Set (Var "mk")) "," (Set (Var "ml")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 9)) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "ml")) ($#k2_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k4_scm_inst :::"address_1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "mk"))) & (Bool (Set (Set (Var "x")) ($#k5_scm_inst :::"address_2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "ml"))) ")" )))) ; definitionlet "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ); given "mk" being ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), "I" being ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 9)) such that (Bool (Set (Const "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Const "I")) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Const "mk")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )) ; func "x" :::"jump_address"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: SCM_INST:def 5 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "x" ($#k5_xtuple_0 :::"`2_3"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) ")" )); end; :: deftheorem defines :::"jump_address"::: SCM_INST:def 5 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ) "st" (Bool (Bool "ex" (Set (Var "mk")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 9)) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))))) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_scm_inst :::"jump_address"::: ) )) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_xtuple_0 :::"`2_3"::: ) )) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) ")" )) ")" ))); theorem :: SCM_INST:6 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ) (Bool "for" (Set (Var "mk")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 9)) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "x")) ($#k6_scm_inst :::"jump_address"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "mk")))))) ; definitionlet "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ); given "mk" being ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), "ml" being ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), "I" being ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 9)) such that (Bool (Set (Const "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Const "I")) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Const "mk")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Const "ml")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )) ; func "x" :::"cjump_address"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: SCM_INST:def 6 (Bool "ex" (Set (Var "mk")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r1_hidden :::"="::: ) (Set "x" ($#k5_xtuple_0 :::"`2_3"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_partfun1 :::"/."::: ) (Num 1))) ")" )); func "x" :::"cond_address"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) means :: SCM_INST:def 7 (Bool "ex" (Set (Var "ml")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) "st" (Bool "(" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "ml")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r1_hidden :::"="::: ) (Set "x" ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "ml")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_partfun1 :::"/."::: ) (Num 1))) ")" )); end; :: deftheorem defines :::"cjump_address"::: SCM_INST:def 6 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ) "st" (Bool (Bool "ex" (Set (Var "mk")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "ml")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 9)) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "ml")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))))) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k7_scm_inst :::"cjump_address"::: ) )) "iff" (Bool "ex" (Set (Var "mk")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_xtuple_0 :::"`2_3"::: ) )) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_partfun1 :::"/."::: ) (Num 1))) ")" )) ")" ))); :: deftheorem defines :::"cond_address"::: SCM_INST:def 7 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ) "st" (Bool (Bool "ex" (Set (Var "mk")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "ml")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) )(Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 9)) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "ml")) ($#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")) ($#k8_scm_inst :::"cond_address"::: ) )) "iff" (Bool "ex" (Set (Var "ml")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) "st" (Bool "(" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "ml")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "ml")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_partfun1 :::"/."::: ) (Num 1))) ")" )) ")" ))); theorem :: SCM_INST:7 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ) (Bool "for" (Set (Var "mk")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "ml")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 9)) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "ml")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k7_scm_inst :::"cjump_address"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "mk"))) & (Bool (Set (Set (Var "x")) ($#k8_scm_inst :::"cond_address"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "ml"))) ")" ))))) ; theorem :: SCM_INST:8 (Bool (Set ($#k3_scm_inst :::"SCM-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 ($#k3_scm_inst :::"SCM-Instr"::: ) ) ")" ) ($#k3_zfmisc_1 :::":]"::: ) )) ; registration cluster (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set ($#k3_scm_inst :::"SCM-Instr"::: ) )) -> ($#v3_finseq_1 :::"FinSequence-membered"::: ) ; end; theorem :: SCM_INST:9 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k1_scm_inst :::"SCM-Halt"::: ) ) "," (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 :::"["::: ) (Set (Var "J")) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where J "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 9)), a "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "J")) ($#r1_hidden :::"="::: ) (Num 6)) "}" ) & (Bool (Set ($#k4_xtuple_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 6)) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "K")) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "a1")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "b1")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where K "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 9)), a1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), b1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) : (Bool (Set (Var "K")) ($#r2_hidden :::"in"::: ) (Set ($#k7_domain_1 :::"{"::: ) (Num 7) "," (Num 8) ($#k7_domain_1 :::"}"::: ) )) "}" ) & (Bool "(" (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 ($#k2_finseq_4 :::"<*"::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k2_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where I "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 9)), b, c "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) : (Bool (Set (Var "I")) ($#r2_hidden :::"in"::: ) (Set ($#k10_domain_1 :::"{"::: ) (Num 1) "," (Num 2) "," (Num 3) "," (Num 4) "," (Num 5) ($#k10_domain_1 :::"}"::: ) )) "}" ) & (Bool "(" (Bool (Set ($#k4_xtuple_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 1)) "or" (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 (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)) ")" ) ")" ) ")" )) ; begin registration cluster (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ; end; theorem :: SCM_INST:10 (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "l"))) ($#r1_xxreal_0 :::"<="::: ) (Num 8))) ; registration cluster (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compos_0 :::"homogeneous"::: ) ; end; registration cluster (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_compos_0 :::"J/A-independent"::: ) ; end; registration cluster (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v5_compos_0 :::"with_halt"::: ) ; end;