let k be Nat; :: thesis: for s being 0 -started State of SCM
for P being Instruction-Sequence of SCM st Euclid-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 Instruction-Sequence of SCM st Euclid-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 Instruction-Sequence of SCM; :: thesis: ( Euclid-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
A1: Euclid-Algorithm c= P and
A2: ( s . (dl. 0) > 0 & s . (dl. 1) > 0 ) and
A3: (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));
A4: ( ( (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 A1, A2, Lm4;
then A5: ( Comput (P,s,((4 * k) + 2)) = Comput (P,s,(((4 * k) + 1) + 1)) & IC (Comput (P,s,((4 * k) + 1))) = 1 ) by A1, A3, Th2;
then A6: (Comput (P,s,((4 * k) + 2))) . (dl. 2) = (Comput (P,s,((4 * k) + 1))) . (dl. 2) by A1, Th3;
A7: ( Comput (P,s,((4 * k) + 3)) = Comput (P,s,(((4 * k) + 2) + 1)) & IC (Comput (P,s,((4 * k) + 2))) = 2 ) by A1, A5, Th3;
then A8: ( Comput (P,s,((4 * k) + 4)) = Comput (P,s,(((4 * k) + 3) + 1)) & IC (Comput (P,s,((4 * k) + 3))) = 3 ) by A1, Th4;
A9: (Comput (P,s,((4 * k) + 3))) . (dl. 0) = (Comput (P,s,((4 * k) + 2))) . (dl. 2) by A1, A7, Th4;
(Comput (P,s,((4 * k) + 1))) . (dl. 2) = (Comput (P,s,(4 * k))) . (dl. 1) by A1, A3, A4, Th2;
hence (Comput (P,s,(4 * (k + 1)))) . (dl. 0) = (Comput (P,s,(4 * k))) . (dl. 1) by A1, A6, A8, A9, Th5; :: thesis: (Comput (P,s,(4 * (k + 1)))) . (dl. 1) = ((Comput (P,s,(4 * k))) . (dl. 0)) mod ((Comput (P,s,(4 * k))) . (dl. 1))
A10: (Comput (P,s,((4 * k) + 3))) . (dl. 1) = (Comput (P,s,((4 * k) + 2))) . (dl. 1) by A1, A7, Th4;
A11: (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 A1, A5, Th3;
( (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 A1, A3, A4, Th2;
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 A1, A11, A8, A10, Th5; :: thesis: verum