let s be State of ; :: thesis: ( Euclide-Algorithm c= s implies for k being Element of NAT st IC (Computation s,k) = 0 holds
( IC (Computation s,(k + 1)) = 1 & (Computation s,(k + 1)) . (dl. 0 ) = (Computation s,k) . (dl. 0 ) & (Computation s,(k + 1)) . (dl. 1) = (Computation s,k) . (dl. 1) & (Computation s,(k + 1)) . (dl. 2) = (Computation s,k) . (dl. 1) ) )
assume A1: Euclide-Algorithm c= s ; :: thesis: for k being Element of NAT st IC (Computation s,k) = 0 holds
( IC (Computation s,(k + 1)) = 1 & (Computation s,(k + 1)) . (dl. 0 ) = (Computation s,k) . (dl. 0 ) & (Computation s,(k + 1)) . (dl. 1) = (Computation s,k) . (dl. 1) & (Computation s,(k + 1)) . (dl. 2) = (Computation s,k) . (dl. 1) )
let k be Element of NAT ; :: thesis: ( IC (Computation s,k) = 0 implies ( IC (Computation s,(k + 1)) = 1 & (Computation s,(k + 1)) . (dl. 0 ) = (Computation s,k) . (dl. 0 ) & (Computation s,(k + 1)) . (dl. 1) = (Computation s,k) . (dl. 1) & (Computation s,(k + 1)) . (dl. 2) = (Computation s,k) . (dl. 1) ) )
assume A2: IC (Computation s,k) = 0 ; :: thesis: ( IC (Computation s,(k + 1)) = 1 & (Computation s,(k + 1)) . (dl. 0 ) = (Computation s,k) . (dl. 0 ) & (Computation s,(k + 1)) . (dl. 1) = (Computation s,k) . (dl. 1) & (Computation s,(k + 1)) . (dl. 2) = (Computation s,k) . (dl. 1) )
A3: Computation s,(k + 1) = Exec (s . (IC (Computation s,k))),(Computation s,k) by AMI_1:55
.= Exec ((dl. 2) := (dl. 1)),(Computation s,k) by A1, A2, Lm3 ;
hence IC (Computation s,(k + 1)) = Next by AMI_3:8
.= 0 + 1 by A2
.= 1 ;
:: thesis: ( (Computation s,(k + 1)) . (dl. 0 ) = (Computation s,k) . (dl. 0 ) & (Computation s,(k + 1)) . (dl. 1) = (Computation s,k) . (dl. 1) & (Computation s,(k + 1)) . (dl. 2) = (Computation s,k) . (dl. 1) )
thus ( (Computation s,(k + 1)) . (dl. 0 ) = (Computation s,k) . (dl. 0 ) & (Computation s,(k + 1)) . (dl. 1) = (Computation s,k) . (dl. 1) ) by A3, AMI_3:8, AMI_3:52; :: thesis: (Computation s,(k + 1)) . (dl. 2) = (Computation s,k) . (dl. 1)
thus (Computation s,(k + 1)) . (dl. 2) = (Computation s,k) . (dl. 1) by A3, AMI_3:8; :: thesis: verum