let s be State of SCM ; :: thesis: ( Euclide-Algorithm c= s implies for k being Element of NAT st IC (Comput (ProgramPart s),s,k) = 1 holds
( IC (Comput (ProgramPart s),s,(k + 1)) = 2 & (Comput (ProgramPart s),s,(k + 1)) . (dl. 0 ) = ((Comput (ProgramPart s),s,k) . (dl. 0 )) div ((Comput (ProgramPart s),s,k) . (dl. 1)) & (Comput (ProgramPart s),s,(k + 1)) . (dl. 1) = ((Comput (ProgramPart s),s,k) . (dl. 0 )) mod ((Comput (ProgramPart s),s,k) . (dl. 1)) & (Comput (ProgramPart s),s,(k + 1)) . (dl. 2) = (Comput (ProgramPart s),s,k) . (dl. 2) ) )
assume A1: Euclide-Algorithm c= s ; :: thesis: for k being Element of NAT st IC (Comput (ProgramPart s),s,k) = 1 holds
( IC (Comput (ProgramPart s),s,(k + 1)) = 2 & (Comput (ProgramPart s),s,(k + 1)) . (dl. 0 ) = ((Comput (ProgramPart s),s,k) . (dl. 0 )) div ((Comput (ProgramPart s),s,k) . (dl. 1)) & (Comput (ProgramPart s),s,(k + 1)) . (dl. 1) = ((Comput (ProgramPart s),s,k) . (dl. 0 )) mod ((Comput (ProgramPart s),s,k) . (dl. 1)) & (Comput (ProgramPart s),s,(k + 1)) . (dl. 2) = (Comput (ProgramPart s),s,k) . (dl. 2) )
let k be Element of NAT ; :: thesis: ( IC (Comput (ProgramPart s),s,k) = 1 implies ( IC (Comput (ProgramPart s),s,(k + 1)) = 2 & (Comput (ProgramPart s),s,(k + 1)) . (dl. 0 ) = ((Comput (ProgramPart s),s,k) . (dl. 0 )) div ((Comput (ProgramPart s),s,k) . (dl. 1)) & (Comput (ProgramPart s),s,(k + 1)) . (dl. 1) = ((Comput (ProgramPart s),s,k) . (dl. 0 )) mod ((Comput (ProgramPart s),s,k) . (dl. 1)) & (Comput (ProgramPart s),s,(k + 1)) . (dl. 2) = (Comput (ProgramPart s),s,k) . (dl. 2) ) )
assume A2: IC (Comput (ProgramPart s),s,k) = 1 ; :: thesis: ( IC (Comput (ProgramPart s),s,(k + 1)) = 2 & (Comput (ProgramPart s),s,(k + 1)) . (dl. 0 ) = ((Comput (ProgramPart s),s,k) . (dl. 0 )) div ((Comput (ProgramPart s),s,k) . (dl. 1)) & (Comput (ProgramPart s),s,(k + 1)) . (dl. 1) = ((Comput (ProgramPart s),s,k) . (dl. 0 )) mod ((Comput (ProgramPart s),s,k) . (dl. 1)) & (Comput (ProgramPart s),s,(k + 1)) . (dl. 2) = (Comput (ProgramPart s),s,k) . (dl. 2) )
A3: Comput (ProgramPart s),s,(k + 1) = Exec (s . (IC (Comput (ProgramPart s),s,k))),(Comput (ProgramPart s),s,k) by AMI_1:55
.= Exec (Divide (dl. 0 ),(dl. 1)),(Comput (ProgramPart s),s,k) by A1, A2, Lm3 ;
hence IC (Comput (ProgramPart s),s,(k + 1)) = succ (IC (Comput (ProgramPart s),s,k)) by AMI_3:12
.= 1 + 1 by A2
.= 2 ;
:: thesis: ( (Comput (ProgramPart s),s,(k + 1)) . (dl. 0 ) = ((Comput (ProgramPart s),s,k) . (dl. 0 )) div ((Comput (ProgramPart s),s,k) . (dl. 1)) & (Comput (ProgramPart s),s,(k + 1)) . (dl. 1) = ((Comput (ProgramPart s),s,k) . (dl. 0 )) mod ((Comput (ProgramPart s),s,k) . (dl. 1)) & (Comput (ProgramPart s),s,(k + 1)) . (dl. 2) = (Comput (ProgramPart s),s,k) . (dl. 2) )
thus ( (Comput (ProgramPart s),s,(k + 1)) . (dl. 0 ) = ((Comput (ProgramPart s),s,k) . (dl. 0 )) div ((Comput (ProgramPart s),s,k) . (dl. 1)) & (Comput (ProgramPart s),s,(k + 1)) . (dl. 1) = ((Comput (ProgramPart s),s,k) . (dl. 0 )) mod ((Comput (ProgramPart s),s,k) . (dl. 1)) & (Comput (ProgramPart s),s,(k + 1)) . (dl. 2) = (Comput (ProgramPart s),s,k) . (dl. 2) ) by A3, Lm1, Lm2, AMI_3:12; :: thesis: verum