:: AMI_3 semantic presentation begin registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#v7_ordinal1 :::"natural"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#v1_setfam_1 :::"with_zero"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionfunc :::"SCM"::: -> ($#v1_extpro_1 :::"strict"::: ) ($#l1_extpro_1 :::"AMI-Struct"::: ) "over" (Num 2) equals :: AMI_3:def 1 (Set ($#g1_extpro_1 :::"AMI-Struct"::: ) "(#" (Set ($#k1_ami_2 :::"SCM-Memory"::: ) ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_ami_2 :::"SCM-Memory"::: ) ) ")" ")" ) "," (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ) "," (Set ($#k3_ami_2 :::"SCM-OK"::: ) ) "," (Set ($#k4_ami_2 :::"SCM-VAL"::: ) ) "," (Set ($#k9_ami_2 :::"SCM-Exec"::: ) ) "#)" ); end; :: deftheorem defines :::"SCM"::: AMI_3:def 1 : (Bool (Set ($#k1_ami_3 :::"SCM"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_extpro_1 :::"AMI-Struct"::: ) "(#" (Set ($#k1_ami_2 :::"SCM-Memory"::: ) ) "," (Set "(" ($#k1_funct_7 :::"In"::: ) "(" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k1_ami_2 :::"SCM-Memory"::: ) ) ")" ")" ) "," (Set ($#k3_scm_inst :::"SCM-Instr"::: ) ) "," (Set ($#k3_ami_2 :::"SCM-OK"::: ) ) "," (Set ($#k4_ami_2 :::"SCM-VAL"::: ) ) "," (Set ($#k9_ami_2 :::"SCM-Exec"::: ) ) "#)" )); registration cluster (Set ($#k1_ami_3 :::"SCM"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_extpro_1 :::"strict"::: ) ; end; registration cluster (Set ($#k1_ami_3 :::"SCM"::: ) ) -> ($#v2_memstr_0 :::"with_non-empty_values"::: ) ($#v1_extpro_1 :::"strict"::: ) ; end; registration cluster (Set ($#k1_ami_3 :::"SCM"::: ) ) -> ($#v3_memstr_0 :::"IC-Ins-separated"::: ) ($#v1_extpro_1 :::"strict"::: ) ; end; registration cluster ($#v1_ami_2 :::"Int-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )); end; definitionmode Data-Location is ($#v1_ami_2 :::"Int-like"::: ) ($#m1_subset_1 :::"Object":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ); end; registrationlet "s" be ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ); let "d" be ($#m1_subset_1 :::"Data-Location":::); cluster (Set "s" ($#k1_funct_1 :::"."::: ) "d") -> ($#v1_int_1 :::"integer"::: ) ; end; definitioncanceled; let "a", "b" be ($#m1_subset_1 :::"Data-Location":::); func "a" :::":="::: "b" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) equals :: AMI_3:def 3 (Set ($#k3_xtuple_0 :::"["::: ) (Num 1) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) "a" "," "b" ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); func :::"AddTo"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) equals :: AMI_3:def 4 (Set ($#k3_xtuple_0 :::"["::: ) (Num 2) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) "a" "," "b" ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); func :::"SubFrom"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) equals :: AMI_3:def 5 (Set ($#k3_xtuple_0 :::"["::: ) (Num 3) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) "a" "," "b" ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); func :::"MultBy"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) equals :: AMI_3:def 6 (Set ($#k3_xtuple_0 :::"["::: ) (Num 4) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) "a" "," "b" ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); func :::"Divide"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) equals :: AMI_3:def 7 (Set ($#k3_xtuple_0 :::"["::: ) (Num 5) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) "a" "," "b" ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); end; :: deftheorem AMI_3:def 2 : canceled; :: deftheorem defines :::":="::: AMI_3:def 3 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Set (Set (Var "a")) ($#k2_ami_3 :::":="::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 1) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))); :: deftheorem defines :::"AddTo"::: AMI_3:def 4 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Set ($#k3_ami_3 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 2) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))); :: deftheorem defines :::"SubFrom"::: AMI_3:def 5 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Set ($#k4_ami_3 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 3) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))); :: deftheorem defines :::"MultBy"::: AMI_3:def 6 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Set ($#k5_ami_3 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 4) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))); :: deftheorem defines :::"Divide"::: AMI_3:def 7 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Set ($#k6_ami_3 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 5) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))); definitionlet "loc" be ($#m1_hidden :::"Nat":::); func :::"SCM-goto"::: "loc" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) equals :: AMI_3:def 8 (Set ($#k3_xtuple_0 :::"["::: ) (Num 6) "," (Set ($#k9_finseq_1 :::"<*"::: ) "loc" ($#k9_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); let "a" be ($#m1_subset_1 :::"Data-Location":::); func "a" :::"=0_goto"::: "loc" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) equals :: AMI_3:def 9 (Set ($#k3_xtuple_0 :::"["::: ) (Num 7) "," (Set ($#k9_finseq_1 :::"<*"::: ) "loc" ($#k9_finseq_1 :::"*>"::: ) ) "," (Set ($#k9_finseq_1 :::"<*"::: ) "a" ($#k9_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); func "a" :::">0_goto"::: "loc" -> ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) equals :: AMI_3:def 10 (Set ($#k3_xtuple_0 :::"["::: ) (Num 8) "," (Set ($#k9_finseq_1 :::"<*"::: ) "loc" ($#k9_finseq_1 :::"*>"::: ) ) "," (Set ($#k9_finseq_1 :::"<*"::: ) "a" ($#k9_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ); end; :: deftheorem defines :::"SCM-goto"::: AMI_3:def 8 : (Bool "for" (Set (Var "loc")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k7_ami_3 :::"SCM-goto"::: ) (Set (Var "loc"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 6) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "loc")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))); :: deftheorem defines :::"=0_goto"::: AMI_3:def 9 : (Bool "for" (Set (Var "loc")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Set (Set (Var "a")) ($#k8_ami_3 :::"=0_goto"::: ) (Set (Var "loc"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 7) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "loc")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))); :: deftheorem defines :::">0_goto"::: AMI_3:def 10 : (Bool "for" (Set (Var "loc")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Set (Set (Var "a")) ($#k9_ami_3 :::">0_goto"::: ) (Set (Var "loc"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Num 8) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "loc")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )))); theorem :: AMI_3:1 (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ; begin theorem :: AMI_3:2 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_ami_3 :::":="::: ) (Set (Var "b")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_ami_3 :::":="::: ) (Set (Var "b")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_ami_3 :::":="::: ) (Set (Var "b")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" ) ")" ))) ; theorem :: AMI_3:3 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k3_ami_3 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k3_ami_3 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k3_ami_3 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" ) ")" ))) ; theorem :: AMI_3:4 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k4_ami_3 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k4_ami_3 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k4_ami_3 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" ) ")" ))) ; theorem :: AMI_3:5 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k5_ami_3 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k5_ami_3 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k5_ami_3 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" ) ")" ))) ; theorem :: AMI_3:6 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k6_ami_3 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) & "(" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "implies" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k6_ami_3 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k5_int_1 :::"div"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ))) ")" & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k6_ami_3 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "b")) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "a"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k6_ami_3 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" ) ")" ))) ; theorem :: AMI_3:7 (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Data-Location":::) (Bool "for" (Set (Var "loc")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k7_ami_3 :::"SCM-goto"::: ) (Set (Var "loc")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "loc"))) & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" ($#k7_ami_3 :::"SCM-goto"::: ) (Set (Var "loc")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" )))) ; theorem :: AMI_3:8 (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Data-Location":::) (Bool "for" (Set (Var "loc")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k8_ami_3 :::"=0_goto"::: ) (Set (Var "loc")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "loc"))) ")" & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k8_ami_3 :::"=0_goto"::: ) (Set (Var "loc")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) ")" & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k8_ami_3 :::"=0_goto"::: ) (Set (Var "loc")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" )))) ; theorem :: AMI_3:9 (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Data-Location":::) (Bool "for" (Set (Var "loc")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k9_ami_3 :::">0_goto"::: ) (Set (Var "loc")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "loc"))) ")" & "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k9_ami_3 :::">0_goto"::: ) (Set (Var "loc")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))) ")" & (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set "(" (Set (Var "a")) ($#k9_ami_3 :::">0_goto"::: ) (Set (Var "loc")) ")" ) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" )))) ; registration cluster (Set ($#k1_ami_3 :::"SCM"::: ) ) -> ($#v1_extpro_1 :::"strict"::: ) ($#v3_extpro_1 :::"halting"::: ) ; end; begin definitionlet "k" be ($#m1_hidden :::"Nat":::); func :::"dl."::: "k" -> ($#m1_subset_1 :::"Data-Location":::) equals :: AMI_3:def 11 (Set ($#k4_tarski :::"["::: ) (Num 1) "," "k" ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"dl."::: AMI_3:def 11 : (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k10_ami_3 :::"dl."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Num 1) "," (Set (Var "k")) ($#k4_tarski :::"]"::: ) ))); theorem :: AMI_3:10 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j")))) "holds" (Bool (Set ($#k10_ami_3 :::"dl."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set ($#k10_ami_3 :::"dl."::: ) (Set (Var "j"))))) ; theorem :: AMI_3:11 (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Set ($#k4_memstr_0 :::"Values"::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set ($#k4_numbers :::"INT"::: ) ))) ; definitionlet "la" be ($#m1_subset_1 :::"Data-Location":::); let "a" be ($#m1_hidden :::"Integer":::); :: original: :::".-->"::: redefine func "la" :::".-->"::: "a" -> ($#m1_hidden :::"PartState":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ); end; definitionlet "la", "lb" be ($#m1_subset_1 :::"Data-Location":::); let "a", "b" be ($#m1_hidden :::"Integer":::); :: original: :::"-->"::: redefine func "(" "la" "," "lb" ")" :::"-->"::: "(" "a" "," "b" ")" -> ($#m1_hidden :::"PartState":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ); end; theorem :: AMI_3:12 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k10_ami_3 :::"dl."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set (Var "j")))) ; theorem :: AMI_3:13 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k10_ami_3 :::"dl."::: ) (Set (Var "i")))) & (Bool (Set ($#k4_struct_0 :::"IC"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Var "i"))) ")" )) ; begin theorem :: AMI_3:14 (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool "ex" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Set (Set "(" ($#k2_extpro_1 :::"Exec"::: ) "(" (Set (Var "I")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_struct_0 :::"IC"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s")) ")" ))))) "holds" (Bool "not" (Bool (Set (Var "I")) "is" ($#v2_extpro_1 :::"halting"::: ) ))) ; theorem :: AMI_3:15 (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) ))) "holds" (Bool (Set (Var "I")) "is" ($#v2_extpro_1 :::"halting"::: ) )) ; theorem :: AMI_3:16 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Bool "not" (Set (Set (Var "a")) ($#k2_ami_3 :::":="::: ) (Set (Var "b"))) "is" ($#v2_extpro_1 :::"halting"::: ) ))) ; theorem :: AMI_3:17 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Bool "not" (Set ($#k3_ami_3 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v2_extpro_1 :::"halting"::: ) ))) ; theorem :: AMI_3:18 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Bool "not" (Set ($#k4_ami_3 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v2_extpro_1 :::"halting"::: ) ))) ; theorem :: AMI_3:19 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Bool "not" (Set ($#k5_ami_3 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v2_extpro_1 :::"halting"::: ) ))) ; theorem :: AMI_3:20 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Bool "not" (Set ($#k6_ami_3 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v2_extpro_1 :::"halting"::: ) ))) ; theorem :: AMI_3:21 (Bool "for" (Set (Var "loc")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Bool "not" (Set ($#k7_ami_3 :::"SCM-goto"::: ) (Set (Var "loc"))) "is" ($#v2_extpro_1 :::"halting"::: ) ))) ; theorem :: AMI_3:22 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Data-Location":::) (Bool "for" (Set (Var "loc")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Bool "not" (Set (Set (Var "a")) ($#k8_ami_3 :::"=0_goto"::: ) (Set (Var "loc"))) "is" ($#v2_extpro_1 :::"halting"::: ) )))) ; theorem :: AMI_3:23 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Data-Location":::) (Bool "for" (Set (Var "loc")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Bool "not" (Set (Set (Var "a")) ($#k9_ami_3 :::">0_goto"::: ) (Set (Var "loc"))) "is" ($#v2_extpro_1 :::"halting"::: ) )))) ; theorem :: AMI_3:24 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) "iff" (Bool "(" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )) "or" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k2_ami_3 :::":="::: ) (Set (Var "b"))))) "or" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k3_ami_3 :::"AddTo"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "or" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k4_ami_3 :::"SubFrom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "or" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k5_ami_3 :::"MultBy"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "or" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k6_ami_3 :::"Divide"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "or" (Bool "ex" (Set (Var "loc")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k7_ami_3 :::"SCM-goto"::: ) (Set (Var "loc"))))) "or" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Data-Location":::)(Bool "ex" (Set (Var "loc")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_ami_3 :::"=0_goto"::: ) (Set (Var "loc")))))) "or" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Data-Location":::)(Bool "ex" (Set (Var "loc")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k9_ami_3 :::">0_goto"::: ) (Set (Var "loc")))))) ")" ) ")" )) ; theorem :: AMI_3:25 (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set (Var "I")) "is" ($#v2_extpro_1 :::"halting"::: ) )) "holds" (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_ami_3 :::"SCM"::: ) )))) ; theorem :: AMI_3:26 (Bool (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k3_xtuple_0 :::"]"::: ) )) ; theorem :: AMI_3:27 (Bool (Set ($#k8_struct_0 :::"Data-Locations"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) )) ; theorem :: AMI_3:28 (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k8_struct_0 :::"Data-Locations"::: ) ))) ; theorem :: AMI_3:29 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SCM-State":::) "holds" (Bool (Set (Var "s")) "is" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ))) ; theorem :: AMI_3:30 (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))) ;