:: AMI_4  semantic presentation begin  




begin  definitionfunc  :::"Euclide-Algorithm":::  -> (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"::: )    ($#m1_hidden :::"Function":::) equals :: AMI_4:def 1 (Set (Set  "(" (Set  ($#k6_numbers :::"0"::: ) )  ($#k16_funcop_1 :::".-->"::: )  (Set  "(" (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 2) ")" )  ($#k2_ami_3 :::":="::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 1) ")" ) ")" ) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k16_funcop_1 :::".-->"::: )  (Set  "("  ($#k6_ami_3 :::"Divide"::: )   "(" (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 1) ")" ) ")"  ")" ) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k16_funcop_1 :::".-->"::: )  (Set  "(" (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k2_ami_3 :::":="::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 2) ")" ) ")" ) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Set  "(" (Num 3)  ($#k16_funcop_1 :::".-->"::: )  (Set  "(" (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 1) ")" )  ($#k9_ami_3 :::">0_goto"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Num 4)  ($#k16_funcop_1 :::".-->"::: )  (Set  "("  ($#k2_compos_1 :::"halt"::: )  (Set  ($#k1_ami_3 :::"SCM"::: ) ) ")" ) ")" ) ")" ) ")" ) ")" )); end; 




:: deftheorem    defines :::"Euclide-Algorithm"::: AMI_4:def 1 :  (Bool (Set   ($#k1_ami_4 :::"Euclide-Algorithm"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k6_numbers :::"0"::: ) )  ($#k16_funcop_1 :::".-->"::: )  (Set  "(" (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 2) ")" )  ($#k2_ami_3 :::":="::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 1) ")" ) ")" ) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k16_funcop_1 :::".-->"::: )  (Set  "("  ($#k6_ami_3 :::"Divide"::: )   "(" (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 1) ")" ) ")"  ")" ) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k16_funcop_1 :::".-->"::: )  (Set  "(" (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k2_ami_3 :::":="::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 2) ")" ) ")" ) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Set  "(" (Num 3)  ($#k16_funcop_1 :::".-->"::: )  (Set  "(" (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 1) ")" )  ($#k9_ami_3 :::">0_goto"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Num 4)  ($#k16_funcop_1 :::".-->"::: )  (Set  "("  ($#k2_compos_1 :::"halt"::: )  (Set  ($#k1_ami_3 :::"SCM"::: ) ) ")" ) ")" ) ")" ) ")" ) ")" ))); 
 
theorem :: AMI_4:1 (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  ($#k1_ami_4 :::"Euclide-Algorithm"::: ) ))  ($#r1_hidden :::"="::: )  (Num 5)) ; 
 begin  
theorem :: AMI_4:2 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )  (Bool  "for" (Set (Var "P")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )  "st" (Bool (Bool (Set   ($#k1_ami_4 :::"Euclide-Algorithm"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Var "P")))) "holds"  (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set   ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 1) ")" ))) & (Bool (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 1) ")" )))  ")" )))) ; 
 
theorem :: AMI_4:3 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )  (Bool  "for" (Set (Var "P")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )  "st" (Bool (Bool (Set   ($#k1_ami_4 :::"Euclide-Algorithm"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Var "P")))) "holds"  (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Num 1))) "holds"  (Bool  "("  (Bool (Set   ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Num 2)) & (Bool (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")" )  ($#k5_int_1 :::"div"::: )  (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 1) ")" ) ")" ))) & (Bool (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ")" )  ($#k6_int_1 :::"mod"::: )  (Set  "(" (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 1) ")" ) ")" ))) & (Bool (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 2) ")" )))  ")" )))) ; 
 
theorem :: AMI_4:4 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )  (Bool  "for" (Set (Var "P")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )  "st" (Bool (Bool (Set   ($#k1_ami_4 :::"Euclide-Algorithm"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Var "P")))) "holds"  (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Num 2))) "holds"  (Bool  "("  (Bool (Set   ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Num 3)) & (Bool (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 2) ")" ))) & (Bool (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 1) ")" ))) & (Bool (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 2) ")" )))  ")" )))) ; 
 
theorem :: AMI_4:5 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )  (Bool  "for" (Set (Var "P")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )  "st" (Bool (Bool (Set   ($#k1_ami_4 :::"Euclide-Algorithm"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Var "P")))) "holds"  (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Num 3))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 1) ")" ))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set   ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"  &  "("  (Bool (Bool (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 1) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set   ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Num 4))  ")"  & (Bool (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 1) ")" )))  ")" )))) ; 
 
theorem :: AMI_4:6 (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"State":::) "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )  (Bool  "for" (Set (Var "P")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )  "st" (Bool (Bool (Set   ($#k1_ami_4 :::"Euclide-Algorithm"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Var "P")))) "holds"  (Bool  "for" (Set (Var "k")) "," (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k5_memstr_0 :::"IC"::: )  (Set  "("  ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Num 4))) "holds"  (Bool (Set   ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "i")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k5_extpro_1 :::"Comput"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) "," (Set (Var "k")) ")" ))))) ; 
 
theorem :: AMI_4:7 (Bool  "for" (Set (Var "s")) "being" (Set   ($#k6_numbers :::"0"::: )  )  ($#v5_memstr_0 :::"-started"::: )    ($#m1_hidden :::"State":::) "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )  (Bool  "for" (Set (Var "P")) "being"   ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set  ($#k1_ami_3 :::"SCM"::: ) )  "st" (Bool (Bool (Set   ($#k1_ami_4 :::"Euclide-Algorithm"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Var "P")))) "holds"  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set (Set (Var "s"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "y"))) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "y"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k6_extpro_1 :::"Result"::: )   "(" (Set (Var "P")) "," (Set (Var "s")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "y"))))))) ; 
 definitionfunc  :::"Euclide-Function":::  ->   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k11_memstr_0 :::"FinPartSt"::: )  (Set  ($#k1_ami_3 :::"SCM"::: ) ) ")" ) "," (Set  "("  ($#k11_memstr_0 :::"FinPartSt"::: )  (Set  ($#k1_ami_3 :::"SCM"::: ) ) ")" ) means :: AMI_4:def 2 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"FinPartState":::) "of" (Set  ($#k1_ami_3 :::"SCM"::: ) ) "holds"   (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "ex" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "y"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set  "(" (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 1) ")" ) ")"   ($#k12_ami_3 :::"-->"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k11_ami_3 :::".-->"::: )  (Set  "(" (Set (Var "x"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "y")) ")" )))  ")" ))  ")" )); end; 




:: deftheorem    defines :::"Euclide-Function"::: AMI_4:def 2 :  (Bool  "for" (Set (Var "b1")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "("  ($#k11_memstr_0 :::"FinPartSt"::: )  (Set  ($#k1_ami_3 :::"SCM"::: ) ) ")" ) "," (Set  "("  ($#k11_memstr_0 :::"FinPartSt"::: )  (Set  ($#k1_ami_3 :::"SCM"::: ) ) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_ami_4 :::"Euclide-Function"::: )  )) "iff" (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"FinPartState":::) "of" (Set  ($#k1_ami_3 :::"SCM"::: ) ) "holds"   (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "b1"))) "iff" (Bool  "ex" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "y"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set  "(" (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 1) ")" ) ")"   ($#k12_ami_3 :::"-->"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k11_ami_3 :::".-->"::: )  (Set  "(" (Set (Var "x"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "y")) ")" )))  ")" ))  ")" ))  ")" )); 
 
theorem :: AMI_4:8 (Bool  "for" (Set (Var "p")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  ($#k2_ami_4 :::"Euclide-Function"::: ) ))) "iff" (Bool  "ex" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "y"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set  "(" (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 1) ")" ) ")"   ($#k12_ami_3 :::"-->"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))  ")" ))  ")" )) ; 
 
theorem :: AMI_4:9 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  ($#k2_ami_4 :::"Euclide-Function"::: ) )  ($#k1_funct_1 :::"."::: )  (Set  "("  "(" (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Num 1) ")" ) ")"   ($#k12_ami_3 :::"-->"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k10_ami_3 :::"dl."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k11_ami_3 :::".-->"::: )  (Set  "(" (Set (Var "i"))  ($#k3_int_2 :::"gcd"::: )  (Set (Var "j")) ")" )))) ; 
 registration
cluster (Set   ($#k1_ami_4 :::"Euclide-Algorithm"::: )  ) -> (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"::: )   ; 
end; registration
cluster (Set   ($#k1_ami_4 :::"Euclide-Algorithm"::: )  ) -> (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"::: )   )  ; 
end; 
theorem :: AMI_4:10 (Bool (Set   ($#k1_ami_4 :::"Euclide-Algorithm"::: )  ) "," (Set   ($#k7_memstr_0 :::"Start-At"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k1_ami_3 :::"SCM"::: ) ) ")" )  ($#r2_extpro_1 :::"computes"::: )  (Set   ($#k2_ami_4 :::"Euclide-Function"::: )  )) ;