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) = 3 holds
( ( (Comput (ProgramPart s),s,k) . (dl. 1) > 0 implies IC (Comput (ProgramPart s),s,(k + 1)) = 0 ) & ( (Comput (ProgramPart s),s,k) . (dl. 1) <= 0 implies IC (Comput (ProgramPart s),s,(k + 1)) = 4 ) & (Comput (ProgramPart s),s,(k + 1)) . (dl. 0 ) = (Comput (ProgramPart s),s,k) . (dl. 0 ) & (Comput (ProgramPart s),s,(k + 1)) . (dl. 1) = (Comput (ProgramPart s),s,k) . (dl. 1) ) )
assume A1: Euclide-Algorithm c= s ; :: thesis: for k being Element of NAT st IC (Comput (ProgramPart s),s,k) = 3 holds
( ( (Comput (ProgramPart s),s,k) . (dl. 1) > 0 implies IC (Comput (ProgramPart s),s,(k + 1)) = 0 ) & ( (Comput (ProgramPart s),s,k) . (dl. 1) <= 0 implies IC (Comput (ProgramPart s),s,(k + 1)) = 4 ) & (Comput (ProgramPart s),s,(k + 1)) . (dl. 0 ) = (Comput (ProgramPart s),s,k) . (dl. 0 ) & (Comput (ProgramPart s),s,(k + 1)) . (dl. 1) = (Comput (ProgramPart s),s,k) . (dl. 1) )
let k be Element of NAT ; :: thesis: ( IC (Comput (ProgramPart s),s,k) = 3 implies ( ( (Comput (ProgramPart s),s,k) . (dl. 1) > 0 implies IC (Comput (ProgramPart s),s,(k + 1)) = 0 ) & ( (Comput (ProgramPart s),s,k) . (dl. 1) <= 0 implies IC (Comput (ProgramPart s),s,(k + 1)) = 4 ) & (Comput (ProgramPart s),s,(k + 1)) . (dl. 0 ) = (Comput (ProgramPart s),s,k) . (dl. 0 ) & (Comput (ProgramPart s),s,(k + 1)) . (dl. 1) = (Comput (ProgramPart s),s,k) . (dl. 1) ) )
assume A2: IC (Comput (ProgramPart s),s,k) = 3 ; :: thesis: ( ( (Comput (ProgramPart s),s,k) . (dl. 1) > 0 implies IC (Comput (ProgramPart s),s,(k + 1)) = 0 ) & ( (Comput (ProgramPart s),s,k) . (dl. 1) <= 0 implies IC (Comput (ProgramPart s),s,(k + 1)) = 4 ) & (Comput (ProgramPart s),s,(k + 1)) . (dl. 0 ) = (Comput (ProgramPart s),s,k) . (dl. 0 ) & (Comput (ProgramPart s),s,(k + 1)) . (dl. 1) = (Comput (ProgramPart s),s,k) . (dl. 1) )
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 ((dl. 1) >0_goto 0 ),(Comput (ProgramPart s),s,k) by A1, A2, Lm3 ;
hence ( (Comput (ProgramPart s),s,k) . (dl. 1) > 0 implies IC (Comput (ProgramPart s),s,(k + 1)) = 0 ) by AMI_3:15; :: thesis: ( ( (Comput (ProgramPart s),s,k) . (dl. 1) <= 0 implies IC (Comput (ProgramPart s),s,(k + 1)) = 4 ) & (Comput (ProgramPart s),s,(k + 1)) . (dl. 0 ) = (Comput (ProgramPart s),s,k) . (dl. 0 ) & (Comput (ProgramPart s),s,(k + 1)) . (dl. 1) = (Comput (ProgramPart s),s,k) . (dl. 1) )
thus ( (Comput (ProgramPart s),s,k) . (dl. 1) <= 0 implies IC (Comput (ProgramPart s),s,(k + 1)) = 4 ) :: thesis: ( (Comput (ProgramPart s),s,(k + 1)) . (dl. 0 ) = (Comput (ProgramPart s),s,k) . (dl. 0 ) & (Comput (ProgramPart s),s,(k + 1)) . (dl. 1) = (Comput (ProgramPart s),s,k) . (dl. 1) )

proof

assume (Comput (ProgramPart s),s,k) . (dl. 1) <= 0 ; :: thesis: IC (Comput (ProgramPart s),s,(k + 1)) = 4
hence IC (Comput (ProgramPart s),s,(k + 1)) = succ (IC (Comput (ProgramPart s),s,k)) by A3, AMI_3:15
.= 3 + 1 by A2
.= 4 ;
:: thesis: verum

end;

thus ( (Comput (ProgramPart s),s,(k + 1)) . (dl. 0 ) = (Comput (ProgramPart s),s,k) . (dl. 0 ) & (Comput (ProgramPart s),s,(k + 1)) . (dl. 1) = (Comput (ProgramPart s),s,k) . (dl. 1) ) by A3, AMI_3:15; :: thesis: verum