let k be Element of NAT ; :: thesis: for s being 0 -started State of SCM
for P being the Instructions of SCM -valued ManySortedSet of NAT st Euclide-Algorithm c= P & s . (dl. 0 ) > 0 & s . (dl. 1) > 0 & (Comput P,s,(4 * k)) . (dl. 1) > 0 holds
( (Comput P,s,(4 * (k + 1))) . (dl. 0 ) = (Comput P,s,(4 * k)) . (dl. 1) & (Comput P,s,(4 * (k + 1))) . (dl. 1) = ((Comput P,s,(4 * k)) . (dl. 0 )) mod ((Comput P,s,(4 * k)) . (dl. 1)) )
let s be 0 -started State of SCM ; :: thesis: for P being the Instructions of SCM -valued ManySortedSet of NAT st Euclide-Algorithm c= P & s . (dl. 0 ) > 0 & s . (dl. 1) > 0 & (Comput P,s,(4 * k)) . (dl. 1) > 0 holds
( (Comput P,s,(4 * (k + 1))) . (dl. 0 ) = (Comput P,s,(4 * k)) . (dl. 1) & (Comput P,s,(4 * (k + 1))) . (dl. 1) = ((Comput P,s,(4 * k)) . (dl. 0 )) mod ((Comput P,s,(4 * k)) . (dl. 1)) )
let P be the Instructions of SCM -valued ManySortedSet of NAT ; :: thesis: ( Euclide-Algorithm c= P & s . (dl. 0 ) > 0 & s . (dl. 1) > 0 & (Comput P,s,(4 * k)) . (dl. 1) > 0 implies ( (Comput P,s,(4 * (k + 1))) . (dl. 0 ) = (Comput P,s,(4 * k)) . (dl. 1) & (Comput P,s,(4 * (k + 1))) . (dl. 1) = ((Comput P,s,(4 * k)) . (dl. 0 )) mod ((Comput P,s,(4 * k)) . (dl. 1)) ) )
assume that
A2: Euclide-Algorithm c= P and
A3: ( s . (dl. 0 ) > 0 & s . (dl. 1) > 0 ) and
A4: (Comput P,s,(4 * k)) . (dl. 1) > 0 ; :: thesis: ( (Comput P,s,(4 * (k + 1))) . (dl. 0 ) = (Comput P,s,(4 * k)) . (dl. 1) & (Comput P,s,(4 * (k + 1))) . (dl. 1) = ((Comput P,s,(4 * k)) . (dl. 0 )) mod ((Comput P,s,(4 * k)) . (dl. 1)) )
set c4 = Comput P,s,(4 * k);
set c5 = Comput P,s,((4 * k) + 1);
set c6 = Comput P,s,((4 * k) + 2);
set c7 = Comput P,s,((4 * k) + 3);
A5: ( ( (Comput P,s,(4 * k)) . (dl. 1) > 0 & IC (Comput P,s,(4 * k)) = 0 ) or ( (Comput P,s,(4 * k)) . (dl. 1) = 0 & IC (Comput P,s,(4 * k)) = 4 ) ) by A2, A3, Lm4;
then A6: ( Comput P,s,((4 * k) + 2) = Comput P,s,(((4 * k) + 1) + 1) & IC (Comput P,s,((4 * k) + 1)) = 1 ) by A2, A4, Th5;
then A7: (Comput P,s,((4 * k) + 2)) . (dl. 2) = (Comput P,s,((4 * k) + 1)) . (dl. 2) by A2, Th6;
A8: ( Comput P,s,((4 * k) + 3) = Comput P,s,(((4 * k) + 2) + 1) & IC (Comput P,s,((4 * k) + 2)) = 2 ) by A2, A6, Th6;
then A9: ( Comput P,s,((4 * k) + 4) = Comput P,s,(((4 * k) + 3) + 1) & IC (Comput P,s,((4 * k) + 3)) = 3 ) by A2, Th7;
A10: (Comput P,s,((4 * k) + 3)) . (dl. 0 ) = (Comput P,s,((4 * k) + 2)) . (dl. 2) by A2, A8, Th7;
(Comput P,s,((4 * k) + 1)) . (dl. 2) = (Comput P,s,(4 * k)) . (dl. 1) by A2, A4, A5, Th5;
hence (Comput P,s,(4 * (k + 1))) . (dl. 0 ) = (Comput P,s,(4 * k)) . (dl. 1) by A2, A7, A9, A10, Th8; :: thesis: (Comput P,s,(4 * (k + 1))) . (dl. 1) = ((Comput P,s,(4 * k)) . (dl. 0 )) mod ((Comput P,s,(4 * k)) . (dl. 1))
A11: (Comput P,s,((4 * k) + 3)) . (dl. 1) = (Comput P,s,((4 * k) + 2)) . (dl. 1) by A2, A8, Th7;
A12: (Comput P,s,((4 * k) + 2)) . (dl. 1) = ((Comput P,s,((4 * k) + 1)) . (dl. 0 )) mod ((Comput P,s,((4 * k) + 1)) . (dl. 1)) by A2, A6, Th6;
( (Comput P,s,((4 * k) + 1)) . (dl. 0 ) = (Comput P,s,(4 * k)) . (dl. 0 ) & (Comput P,s,((4 * k) + 1)) . (dl. 1) = (Comput P,s,(4 * k)) . (dl. 1) ) by A2, A4, A5, Th5;
hence (Comput P,s,(4 * (k + 1))) . (dl. 1) = ((Comput P,s,(4 * k)) . (dl. 0 )) mod ((Comput P,s,(4 * k)) . (dl. 1)) by A2, A12, A9, A11, Th8; :: thesis: verum