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