let s be State of SCM; :: thesis: for P being Instruction-Sequence of SCM st Euclid-Algorithm c= P holds
for k being Nat st IC (Comput (P,s,k)) = 0 holds
( IC (Comput (P,s,(k + 1))) = 1 & (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 0) & (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. 1) )
let P be Instruction-Sequence of SCM; :: thesis: ( Euclid-Algorithm c= P implies for k being Nat st IC (Comput (P,s,k)) = 0 holds
( IC (Comput (P,s,(k + 1))) = 1 & (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 0) & (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. 1) ) )
assume A1: Euclid-Algorithm c= P ; :: thesis: for k being Nat st IC (Comput (P,s,k)) = 0 holds
( IC (Comput (P,s,(k + 1))) = 1 & (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 0) & (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. 1) )
let k be Nat; :: thesis: ( IC (Comput (P,s,k)) = 0 implies ( IC (Comput (P,s,(k + 1))) = 1 & (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 0) & (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. 1) ) )
assume A2: IC (Comput (P,s,k)) = 0 ; :: thesis: ( IC (Comput (P,s,(k + 1))) = 1 & (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 0) & (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. 1) )
A3: Comput (P,s,(k + 1)) = Exec ((P . (IC (Comput (P,s,k)))),(Comput (P,s,k))) by EXTPRO_1:6
.= Exec (((dl. 2) := (dl. 1)),(Comput (P,s,k))) by A1, A2, Lm3 ;
hence IC (Comput (P,s,(k + 1))) = (IC (Comput (P,s,k))) + 1 by AMI_3:2
.= 1 by A2 ;
:: thesis: ( (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 0) & (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. 1) )
thus ( (Comput (P,s,(k + 1))) . (dl. 0) = (Comput (P,s,k)) . (dl. 0) & (Comput (P,s,(k + 1))) . (dl. 1) = (Comput (P,s,k)) . (dl. 1) ) by A3, AMI_3:2, AMI_3:10; :: thesis: (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 1)
thus (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 1) by A3, AMI_3:2; :: thesis: verum