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 holds
( (Comput (P,s,(4 * k))) . (dl. 0) > 0 & ( ( (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 ) ) )
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 holds
( (Comput (P,s,(4 * k))) . (dl. 0) > 0 & ( ( (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 ) ) )
let P be Instruction-Sequence of SCM; :: thesis: ( Euclid-Algorithm c= P & s . (dl. 0) > 0 & s . (dl. 1) > 0 implies ( (Comput (P,s,(4 * k))) . (dl. 0) > 0 & ( ( (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 ) ) ) )
assume that
A1: Euclid-Algorithm c= P and
A2: ( s . (dl. 0) > 0 & s . (dl. 1) > 0 ) ; :: thesis: ( (Comput (P,s,(4 * k))) . (dl. 0) > 0 & ( ( (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 ) ) )
A3: IC s = 0 by MEMSTR_0:def 12;
defpred S₂[ Nat] means ( (Comput (P,s,(4 * $1))) . (dl. 0) > 0 & ( ( (Comput (P,s,(4 * $1))) . (dl. 1) > 0 & IC (Comput (P,s,(4 * $1))) = 0 ) or ( (Comput (P,s,(4 * $1))) . (dl. 1) = 0 & IC (Comput (P,s,(4 * $1))) = 4 ) ) );
A4: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 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));
set c8 = Comput (P,s,((4 * k) + 4));
A5: Comput (P,s,((4 * k) + 3)) = Comput (P,s,(((4 * k) + 2) + 1)) ;
A6: Comput (P,s,((4 * k) + 4)) = Comput (P,s,(((4 * k) + 3) + 1)) ;
assume A7: (Comput (P,s,(4 * k))) . (dl. 0) > 0 ; :: thesis: ( ( not ( (Comput (P,s,(4 * k))) . (dl. 1) > 0 & IC (Comput (P,s,(4 * k))) = 0 ) & not ( (Comput (P,s,(4 * k))) . (dl. 1) = 0 & IC (Comput (P,s,(4 * k))) = 4 ) ) or S₂[k + 1] )
assume A8: ( ( (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 ) ) ; :: thesis: S₂[k + 1]
A9: Comput (P,s,((4 * k) + 2)) = Comput (P,s,(((4 * k) + 1) + 1)) ;

now :: thesis: ( ( (Comput (P,s,(4 * k))) . (dl. 1) > 0 & (Comput (P,s,((4 * k) + 4))) . (dl. 0) > 0 & ( ( (Comput (P,s,((4 * k) + 4))) . (dl. 1) > 0 & IC (Comput (P,s,((4 * k) + 4))) = 0 ) or ( (Comput (P,s,((4 * k) + 4))) . (dl. 1) = 0 & IC (Comput (P,s,((4 * k) + 4))) = 4 ) ) ) or ( (Comput (P,s,(4 * k))) . (dl. 1) = 0 & (Comput (P,s,((4 * k) + 4))) . (dl. 0) > 0 & (Comput (P,s,((4 * k) + 4))) . (dl. 1) = 0 & IC (Comput (P,s,((4 * k) + 4))) = 4 ) )

per cases ( (Comput (P,s,(4 * k))) . (dl. 1) > 0 or (Comput (P,s,(4 * k))) . (dl. 1) = 0 ) by A8;

case A10: (Comput (P,s,(4 * k))) . (dl. 1) > 0 ; :: thesis: ( (Comput (P,s,((4 * k) + 4))) . (dl. 0) > 0 & ( ( (Comput (P,s,((4 * k) + 4))) . (dl. 1) > 0 & IC (Comput (P,s,((4 * k) + 4))) = 0 ) or ( (Comput (P,s,((4 * k) + 4))) . (dl. 1) = 0 & IC (Comput (P,s,((4 * k) + 4))) = 4 ) ) )

then A11: IC (Comput (P,s,((4 * k) + 1))) = 1 by A1, A8, Th2;
then A12: IC (Comput (P,s,((4 * k) + 2))) = 2 by A1, A9, Th3;
then A13: IC (Comput (P,s,((4 * k) + 3))) = 3 by A1, A5, Th4;
then A14: (Comput (P,s,((4 * k) + 4))) . (dl. 1) = (Comput (P,s,((4 * k) + 3))) . (dl. 1) by A1, A6, Th5;
A15: ( (Comput (P,s,((4 * k) + 3))) . (dl. 0) = (Comput (P,s,((4 * k) + 2))) . (dl. 2) & (Comput (P,s,((4 * k) + 3))) . (dl. 1) = (Comput (P,s,((4 * k) + 2))) . (dl. 1) ) by A1, A5, A12, Th4;
A16: ( (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)) & (Comput (P,s,((4 * k) + 2))) . (dl. 2) = (Comput (P,s,((4 * k) + 1))) . (dl. 2) ) by A1, A9, A11, Th3;
A17: ( (Comput (P,s,((4 * k) + 1))) . (dl. 1) = (Comput (P,s,(4 * k))) . (dl. 1) & (Comput (P,s,((4 * k) + 1))) . (dl. 2) = (Comput (P,s,(4 * k))) . (dl. 1) ) by A1, A8, A10, Th2;
thus (Comput (P,s,((4 * k) + 4))) . (dl. 0) > 0 by A1, A6, A10, A17, A16, A13, A15, Th5; :: thesis: ( ( (Comput (P,s,((4 * k) + 4))) . (dl. 1) > 0 & IC (Comput (P,s,((4 * k) + 4))) = 0 ) or ( (Comput (P,s,((4 * k) + 4))) . (dl. 1) = 0 & IC (Comput (P,s,((4 * k) + 4))) = 4 ) )
( (Comput (P,s,((4 * k) + 4))) . (dl. 1) is positive or (Comput (P,s,((4 * k) + 4))) . (dl. 1) is zero ) by A10, A17, A16, A15, A14, NEWTON:64;
hence ( ( (Comput (P,s,((4 * k) + 4))) . (dl. 1) > 0 & IC (Comput (P,s,((4 * k) + 4))) = 0 ) or ( (Comput (P,s,((4 * k) + 4))) . (dl. 1) = 0 & IC (Comput (P,s,((4 * k) + 4))) = 4 ) ) by A1, A6, A13, A14, Th5; :: thesis: verum

end;

case (Comput (P,s,(4 * k))) . (dl. 1) = 0 ; :: thesis: ( (Comput (P,s,((4 * k) + 4))) . (dl. 0) > 0 & (Comput (P,s,((4 * k) + 4))) . (dl. 1) = 0 & IC (Comput (P,s,((4 * k) + 4))) = 4 )

hence ( (Comput (P,s,((4 * k) + 4))) . (dl. 0) > 0 & (Comput (P,s,((4 * k) + 4))) . (dl. 1) = 0 & IC (Comput (P,s,((4 * k) + 4))) = 4 ) by A1, A7, A8, Th6; :: thesis: verum

end;

end;

end;

hence S₂[k + 1] ; :: thesis: verum

end;

A18: S₂[ 0 ] by A3, A2, EXTPRO_1:2;
for k being Nat holds S₂[k] from NAT_1:sch 2(A18, A4);
hence ( (Comput (P,s,(4 * k))) . (dl. 0) > 0 & ( ( (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 ) ) ) ; :: thesis: verum