:: SCMRINGI semantic presentation begin registration cluster (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ) -> ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ; end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; func :::"SCM-Instr"::: "S" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) equals :: SCMRINGI:def 1 (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 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where I "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 8)), a, b "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) : (Bool (Set (Var "I")) ($#r2_hidden :::"in"::: ) (Set ($#k2_enumset1 :::"{"::: ) (Num 1) "," (Num 2) "," (Num 3) "," (Num 4) ($#k2_enumset1 :::"}"::: ) )) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Num 6) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "i")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool verum) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Num 7) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "i")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), a "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) : (Bool verum) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Num 5) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "r")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where a "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), r "is" ($#m1_subset_1 :::"Element":::) "of" "S" : (Bool verum) "}" ); end; :: deftheorem defines :::"SCM-Instr"::: SCMRINGI:def 1 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) "holds" (Bool (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (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 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where I "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 8)), a, b "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) : (Bool (Set (Var "I")) ($#r2_hidden :::"in"::: ) (Set ($#k2_enumset1 :::"{"::: ) (Num 1) "," (Num 2) "," (Num 3) "," (Num 4) ($#k2_enumset1 :::"}"::: ) )) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Num 6) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "i")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool verum) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Num 7) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "i")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), a "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) : (Bool verum) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Num 5) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "r")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where a "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), r "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) : (Bool verum) "}" ))); registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; cluster (Set ($#k1_scmringi :::"SCM-Instr"::: ) "S") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ; end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Const "S"))); given "mk", "ml" 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 8)) 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 :: SCMRINGI: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))) ")" )); func "x" :::"address_2"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) means :: SCMRINGI: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 2))) ")" )); end; :: deftheorem defines :::"address_1"::: SCMRINGI:def 2 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "S"))) "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" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 8)) "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 "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_scmringi :::"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 "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) ")" )) ")" )))); :: deftheorem defines :::"address_2"::: SCMRINGI:def 3 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "S"))) "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" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 8)) "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 "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_scmringi :::"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 "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2))) ")" )) ")" )))); theorem :: SCMRINGI:1 (Bool "for" (Set (Var "I")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 8)) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "S"))) (Bool "for" (Set (Var "mk")) "," (Set (Var "ml")) "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 ($#k2_finseq_4 :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "ml")) ($#k2_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k2_scmringi :::"address_1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "mk"))) & (Bool (Set (Set (Var "x")) ($#k3_scmringi :::"address_2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "ml"))) ")" ))))) ; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Const "R"))); given "mk" being ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), "I" being ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 8)) 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 :: SCMRINGI:def 4 (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"::: SCMRINGI:def 4 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "R"))) "st" (Bool (Bool "ex" (Set (Var "mk")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "I")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 8)) "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 "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_scmringi :::"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 "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) ")" )) ")" )))); theorem :: SCMRINGI:2 (Bool "for" (Set (Var "I")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 8)) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "S"))) (Bool "for" (Set (Var "mk")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "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")) ($#k4_scmringi :::"jump_address"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "mk"))))))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Const "S"))); 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 ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 8)) 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 :: SCMRINGI:def 5 (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 :: SCMRINGI:def 6 (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"::: SCMRINGI:def 5 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "S"))) "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" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 8)) "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 "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_scmringi :::"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 "b3")) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "mk")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_partfun1 :::"/."::: ) (Num 1))) ")" )) ")" )))); :: deftheorem defines :::"cond_address"::: SCMRINGI:def 6 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "S"))) "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" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 8)) "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 "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_scmringi :::"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 "b3")) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "ml")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_partfun1 :::"/."::: ) (Num 1))) ")" )) ")" )))); theorem :: SCMRINGI:3 (Bool "for" (Set (Var "I")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 8)) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "S"))) (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"::: ) ) "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")) ($#k5_scmringi :::"cjump_address"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "mk"))) & (Bool (Set (Set (Var "x")) ($#k6_scmringi :::"cond_address"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "ml"))) ")" )))))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ); let "s" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); :: original: :::"<*"::: redefine func :::"<*":::"d" "," "s":::"*>"::: -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S")); end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Const "S"))); given "mk" being ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), "r" being ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")), "I" being ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 8)) such that (Bool (Set (Const "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Const "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k7_scmringi :::"<*"::: ) (Set (Const "mk")) "," (Set (Const "r")) ($#k7_scmringi :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )) ; func "x" :::"const_address"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) means :: SCMRINGI: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 "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S")) "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" :::"const_value"::: -> ($#m1_subset_1 :::"Element":::) "of" "S" means :: SCMRINGI: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 "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S")) "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 :::"const_address"::: SCMRINGI:def 7 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "S"))) "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_subset_1 :::"Element":::) "of" (Set (Var "S"))(Bool "ex" (Set (Var "I")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 8)) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k7_scmringi :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "r")) ($#k7_scmringi :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k8_scmringi :::"const_address"::: ) )) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1))) ")" )) ")" )))); :: deftheorem defines :::"const_value"::: SCMRINGI:def 8 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "S"))) "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_subset_1 :::"Element":::) "of" (Set (Var "S"))(Bool "ex" (Set (Var "I")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 8)) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k7_scmringi :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "r")) ($#k7_scmringi :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k9_scmringi :::"const_value"::: ) )) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xtuple_0 :::"`3_3"::: ) )) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2))) ")" )) ")" )))); theorem :: SCMRINGI:4 (Bool "for" (Set (Var "I")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 8)) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "S"))) (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_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k7_scmringi :::"<*"::: ) (Set (Var "mk")) "," (Set (Var "r")) ($#k7_scmringi :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k8_scmringi :::"const_address"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "mk"))) & (Bool (Set (Set (Var "x")) ($#k9_scmringi :::"const_value"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "r"))) ")" )))))) ; theorem :: SCMRINGI:5 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) "holds" (Bool (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "S"))) ($#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 "(" ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "S")) ")" ) ")" ) ($#k3_zfmisc_1 :::":]"::: ) ))) ; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; cluster (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" ($#k1_scmringi :::"SCM-Instr"::: ) "S" ")" )) -> ($#v3_finseq_1 :::"FinSequence-membered"::: ) ; end; theorem :: SCMRINGI:6 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) "holds" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "S"))))) ; theorem :: SCMRINGI:7 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "S"))) "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 :::"["::: ) (Set (Var "I")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where I "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k7_card_1 :::"Segm"::: ) (Num 8)), a, b "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) : (Bool (Set (Var "I")) ($#r2_hidden :::"in"::: ) (Set ($#k2_enumset1 :::"{"::: ) (Num 1) "," (Num 2) "," (Num 3) "," (Num 4) ($#k2_enumset1 :::"}"::: ) )) "}" ) & (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 "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Num 6) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "i")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool verum) "}" ) & (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 :::"["::: ) (Num 7) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "i")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), a "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 7)) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "{" (Set ($#k3_xtuple_0 :::"["::: ) (Num 5) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k7_scmringi :::"<*"::: ) (Set (Var "a")) "," (Set (Var "r")) ($#k7_scmringi :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) where a "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ), r "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) : (Bool verum) "}" ) & (Bool (Set ($#k4_xtuple_0 :::"InsCode"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Num 5)) ")" ) ")" ))) ; begin registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_struct_0 :::"trivial"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v36_algstr_0 :::"strict"::: ) bbbadV2_RLVECT_1() bbbadV3_RLVECT_1() bbbadV4_RLVECT_1() bbbadV3_GROUP_1() bbbadV4_VECTSP_1() bbbadV5_VECTSP_1() for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); cluster (Set ($#k1_scmringi :::"SCM-Instr"::: ) "R") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_compos_0 :::"standard-ins"::: ) ; end; registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); cluster (Set ($#k1_scmringi :::"SCM-Instr"::: ) "R") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compos_0 :::"homogeneous"::: ) ; end; registrationlet "R" be ($#l6_algstr_0 :::"Ring":::); cluster (Set ($#k1_scmringi :::"SCM-Instr"::: ) "R") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_compos_0 :::"J/A-independent"::: ) ; end; theorem :: SCMRINGI:8 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_enumset1 :::"{"::: ) (Num 1) "," (Num 2) "," (Num 3) "," (Num 4) ($#k2_enumset1 :::"}"::: ) ))) "holds" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "x")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "d1")) "," (Set (Var "d2")) ($#k2_finseq_4 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "S"))))))) ; theorem :: SCMRINGI:9 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "d1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) "holds" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Num 5) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k7_scmringi :::"<*"::: ) (Set (Var "d1")) "," (Set (Var "t")) ($#k7_scmringi :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "S"))))))) ; theorem :: SCMRINGI:10 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "i1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Num 6) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "i1")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "S")))))) ; theorem :: SCMRINGI:11 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "d1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_scm_inst :::"SCM-Data-Loc"::: ) ) (Bool "for" (Set (Var "i1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_xtuple_0 :::"["::: ) (Num 7) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "i1")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d1")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_scmringi :::"SCM-Instr"::: ) (Set (Var "S"))))))) ; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; cluster (Set ($#k1_scmringi :::"SCM-Instr"::: ) "S") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v5_compos_0 :::"with_halt"::: ) ; end;