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)) = 1 holds
( IC (Comput (P,s,(k + 1))) = 2 & (Comput (P,s,(k + 1))) . (dl. 0) = ((Comput (P,s,k)) . (dl. 0)) div ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 1) = ((Comput (P,s,k)) . (dl. 0)) mod ((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)) = 1 holds
( IC (Comput (P,s,(k + 1))) = 2 & (Comput (P,s,(k + 1))) . (dl. 0) = ((Comput (P,s,k)) . (dl. 0)) div ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 1) = ((Comput (P,s,k)) . (dl. 0)) mod ((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)) = 1 holds
( IC (Comput (P,s,(k + 1))) = 2 & (Comput (P,s,(k + 1))) . (dl. 0) = ((Comput (P,s,k)) . (dl. 0)) div ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 1) = ((Comput (P,s,k)) . (dl. 0)) mod ((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)) = 1 implies ( IC (Comput (P,s,(k + 1))) = 2 & (Comput (P,s,(k + 1))) . (dl. 0) = ((Comput (P,s,k)) . (dl. 0)) div ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 1) = ((Comput (P,s,k)) . (dl. 0)) mod ((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)) = 1 ; :: thesis: ( IC (Comput (P,s,(k + 1))) = 2 & (Comput (P,s,(k + 1))) . (dl. 0) = ((Comput (P,s,k)) . (dl. 0)) div ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 1) = ((Comput (P,s,k)) . (dl. 0)) mod ((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 EXTPRO_1:7
.= Exec ((Divide ((dl. 0),(dl. 1))),(Comput (P,s,k))) by A1, A2, Lm3 ;
hence IC (Comput (P,s,(k + 1))) = succ (IC (Comput (P,s,k))) by AMI_3:12
.= 2 by A2 ;
:: thesis: ( (Comput (P,s,(k + 1))) . (dl. 0) = ((Comput (P,s,k)) . (dl. 0)) div ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 1) = ((Comput (P,s,k)) . (dl. 0)) mod ((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. 0)) div ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 1) = ((Comput (P,s,k)) . (dl. 0)) mod ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 2) = (Comput (P,s,k)) . (dl. 2) ) by A3, Lm1, Lm2, AMI_3:12; :: thesis: verum