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