:: AMI_5 semantic presentation begin theorem :: AMI_5:1 (Bool "for" (Set (Var "dl")) "being" ($#m1_subset_1 :::"Data-Location":::) (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "dl")) ($#r1_hidden :::"="::: ) (Set ($#k10_ami_3 :::"dl."::: ) (Set (Var "i")))))) ; theorem :: AMI_5:2 (Bool "for" (Set (Var "dl")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Set (Var "dl")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"IC"::: ) ))) ; theorem :: AMI_5:3 (Bool "for" (Set (Var "il")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "dl")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Set (Var "il")) ($#r1_hidden :::"<>"::: ) (Set (Var "dl"))))) ; theorem :: AMI_5:4 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "s")))))) ; registration cluster (Set ($#k8_struct_0 :::"NonZero"::: ) (Set ($#k1_ami_3 :::"SCM"::: ) )) -> ($#v1_finset_1 :::"infinite"::: ) ; end; theorem :: AMI_5:5 (Bool "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "holds" (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "l"))) ($#r1_xxreal_0 :::"<="::: ) (Num 8))) ; theorem :: AMI_5:6 canceled; theorem :: AMI_5:7 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_ami_3 :::"SCM"::: ) )))) ; theorem :: AMI_5:8 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "ex" (Set (Var "da")) "," (Set (Var "db")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set (Set (Var "da")) ($#k2_ami_3 :::":="::: ) (Set (Var "db")))))) ; theorem :: AMI_5:9 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 2))) "holds" (Bool "ex" (Set (Var "da")) "," (Set (Var "db")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set ($#k3_ami_3 :::"AddTo"::: ) "(" (Set (Var "da")) "," (Set (Var "db")) ")" )))) ; theorem :: AMI_5:10 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 3))) "holds" (Bool "ex" (Set (Var "da")) "," (Set (Var "db")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set ($#k4_ami_3 :::"SubFrom"::: ) "(" (Set (Var "da")) "," (Set (Var "db")) ")" )))) ; theorem :: AMI_5:11 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 4))) "holds" (Bool "ex" (Set (Var "da")) "," (Set (Var "db")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set ($#k5_ami_3 :::"MultBy"::: ) "(" (Set (Var "da")) "," (Set (Var "db")) ")" )))) ; theorem :: AMI_5:12 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 5))) "holds" (Bool "ex" (Set (Var "da")) "," (Set (Var "db")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set ($#k6_ami_3 :::"Divide"::: ) "(" (Set (Var "da")) "," (Set (Var "db")) ")" )))) ; theorem :: AMI_5:13 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 6))) "holds" (Bool "ex" (Set (Var "loc")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set ($#k7_ami_3 :::"SCM-goto"::: ) (Set (Var "loc")))))) ; theorem :: AMI_5:14 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 7))) "holds" (Bool "ex" (Set (Var "loc")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "da")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set (Set (Var "da")) ($#k8_ami_3 :::"=0_goto"::: ) (Set (Var "loc"))))))) ; theorem :: AMI_5:15 (Bool "for" (Set (Var "ins")) "being" ($#m1_subset_1 :::"Instruction":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set ($#k2_compos_0 :::"InsCode"::: ) (Set (Var "ins"))) ($#r1_hidden :::"="::: ) (Num 8))) "holds" (Bool "ex" (Set (Var "loc")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "da")) "being" ($#m1_subset_1 :::"Data-Location":::) "st" (Bool (Set (Var "ins")) ($#r1_hidden :::"="::: ) (Set (Set (Var "da")) ($#k9_ami_3 :::">0_goto"::: ) (Set (Var "loc"))))))) ; begin theorem :: AMI_5:16 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "iloc")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k7_memstr_0 :::"Start-At"::: ) "(" (Set (Var "iloc")) "," (Set ($#k1_ami_3 :::"SCM"::: ) ) ")" ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))))) ; begin registration cluster (Set ($#k1_ami_3 :::"SCM"::: ) ) -> ($#v3_amistd_5 :::"IC-recognized"::: ) ; end; registration cluster (Set ($#k1_ami_3 :::"SCM"::: ) ) -> ($#v4_amistd_5 :::"CurIns-recognized"::: ) ; end; theorem :: AMI_5:17 (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b1")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s2")))) "holds" (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "da")) "," (Set (Var "db")) "being" ($#m1_subset_1 :::"Data-Location":::) (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_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" )) & (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Set (Var "da")) ($#k2_ami_3 :::":="::: ) (Set (Var "db")))) & (Bool (Set (Var "da")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "db"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "db"))))))))))) ; theorem :: AMI_5:18 (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b1")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s2")))) "holds" (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "da")) "," (Set (Var "db")) "being" ($#m1_subset_1 :::"Data-Location":::) (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_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" )) & (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k3_ami_3 :::"AddTo"::: ) "(" (Set (Var "da")) "," (Set (Var "db")) ")" )) & (Bool (Set (Var "da")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "da")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "db")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "da")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "db")) ")" )))))))))) ; theorem :: AMI_5:19 (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b1")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s2")))) "holds" (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "da")) "," (Set (Var "db")) "being" ($#m1_subset_1 :::"Data-Location":::) (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_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" )) & (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k4_ami_3 :::"SubFrom"::: ) "(" (Set (Var "da")) "," (Set (Var "db")) ")" )) & (Bool (Set (Var "da")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "da")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "db")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "da")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "db")) ")" )))))))))) ; theorem :: AMI_5:20 (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b1")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s2")))) "holds" (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "da")) "," (Set (Var "db")) "being" ($#m1_subset_1 :::"Data-Location":::) (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_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" )) & (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k5_ami_3 :::"MultBy"::: ) "(" (Set (Var "da")) "," (Set (Var "db")) ")" )) & (Bool (Set (Var "da")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "da")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "db")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "da")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "db")) ")" )))))))))) ; theorem :: AMI_5:21 (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b1")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s2")))) "holds" (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "da")) "," (Set (Var "db")) "being" ($#m1_subset_1 :::"Data-Location":::) (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_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" )) & (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k6_ami_3 :::"Divide"::: ) "(" (Set (Var "da")) "," (Set (Var "db")) ")" )) & (Bool (Set (Var "da")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "da")) ($#r1_hidden :::"<>"::: ) (Set (Var "db")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "da")) ")" ) ($#k5_int_1 :::"div"::: ) (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "db")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "da")) ")" ) ($#k5_int_1 :::"div"::: ) (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "db")) ")" )))))))))) ; theorem :: AMI_5:22 (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b1")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s2")))) "holds" (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "da")) "," (Set (Var "db")) "being" ($#m1_subset_1 :::"Data-Location":::) (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_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" )) & (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set ($#k6_ami_3 :::"Divide"::: ) "(" (Set (Var "da")) "," (Set (Var "db")) ")" )) & (Bool (Set (Var "db")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "da")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "db")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "da")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "db")) ")" )))))))))) ; theorem :: AMI_5:23 (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b1")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s2")))) "holds" (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "da")) "being" ($#m1_subset_1 :::"Data-Location":::) (Bool "for" (Set (Var "loc")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" )) & (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Set (Var "da")) ($#k8_ami_3 :::"=0_goto"::: ) (Set (Var "loc")))) & (Bool (Set (Var "loc")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "da"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "da"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))))))))) ; theorem :: AMI_5:24 (Bool "for" (Set (Var "q")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_finset_1 :::"finite"::: ) ($#~v2_compos_1 "non" ($#v2_compos_1 :::"halt-free"::: ) ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "p")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Var "b1")) ($#v4_extpro_1 :::"-autonomic"::: ) ($#m1_hidden :::"FinPartState":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s1"))) & (Bool (Set (Var "p")) ($#r1_tarski :::"c="::: ) (Set (Var "s2")))) "holds" (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P1"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"c="::: ) (Set (Var "P2")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "da")) "being" ($#m1_subset_1 :::"Data-Location":::) (Bool "for" (Set (Var "loc")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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_extpro_1 :::"CurInstr"::: ) "(" (Set (Var "P1")) "," (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" )) & (Bool (Set (Var "I")) ($#r1_hidden :::"="::: ) (Set (Set (Var "da")) ($#k9_ami_3 :::">0_goto"::: ) (Set (Var "loc")))) & (Bool (Set (Var "loc")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P1")) "," (Set (Var "s1")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "da"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "P2")) "," (Set (Var "s2")) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "da"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))))))))) ; theorem :: AMI_5:25 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "s2")))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Data-Location":::) "holds" (Bool (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) ")" )) "holds" (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Var "s2")))) ;