let k be Element of NAT ; :: thesis: for s being State of st s starts_at 0 & Euclide-Algorithm c= s & s . (dl. 0 ) > 0 & s . (dl. 1) > 0 holds
( (Computation s,(4 * k)) . (dl. 0 ) > 0 & ( ( (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 ) ) )
let s be State of ; :: thesis: ( s starts_at 0 & Euclide-Algorithm c= s & s . (dl. 0 ) > 0 & s . (dl. 1) > 0 implies ( (Computation s,(4 * k)) . (dl. 0 ) > 0 & ( ( (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 ) ) ) )
assume that
A1: IC s = 0 and
A2: Euclide-Algorithm c= s and
A3: ( s . (dl. 0 ) > 0 & s . (dl. 1) > 0 ) ; :: according to AMI_1:def 41 :: thesis: ( (Computation s,(4 * k)) . (dl. 0 ) > 0 & ( ( (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 ) ) )
defpred S2[ Element of NAT ] means ( (Computation s,(4 * $1)) . (dl. 0 ) > 0 & ( ( (Computation s,(4 * $1)) . (dl. 1) > 0 & IC (Computation s,(4 * $1)) = 0 ) or ( (Computation s,(4 * $1)) . (dl. 1) = 0 & IC (Computation s,(4 * $1)) = 4 ) ) );
A4: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S2[k] implies S2[k + 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);
set c8 = Computation s,((4 * k) + 4);
A5: Computation s,((4 * k) + 3) = Computation s,(((4 * k) + 2) + 1) ;
A6: Computation s,((4 * k) + 4) = Computation s,(((4 * k) + 3) + 1) ;
assume A7: (Computation s,(4 * k)) . (dl. 0 ) > 0 ; :: thesis: ( ( not ( (Computation s,(4 * k)) . (dl. 1) > 0 & IC (Computation s,(4 * k)) = 0 ) & not ( (Computation s,(4 * k)) . (dl. 1) = 0 & IC (Computation s,(4 * k)) = 4 ) ) or S2[k + 1] )
assume A8: ( ( (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 ) ) ; :: thesis: S2[k + 1]
A9: Computation s,((4 * k) + 2) = Computation s,(((4 * k) + 1) + 1) ;
now
per cases ( (Computation s,(4 * k)) . (dl. 1) > 0 or (Computation s,(4 * k)) . (dl. 1) = 0 ) by A8;
case A10: (Computation s,(4 * k)) . (dl. 1) > 0 ; :: thesis: ( (Computation s,((4 * k) + 4)) . (dl. 0 ) > 0 & ( ( (Computation s,((4 * k) + 4)) . (dl. 1) > 0 & IC (Computation s,((4 * k) + 4)) = 0 ) or ( (Computation s,((4 * k) + 4)) . (dl. 1) = 0 & IC (Computation s,((4 * k) + 4)) = 4 ) ) )
then A11: IC (Computation s,((4 * k) + 1)) = 1 by A2, A8, Th5;
then A12: IC (Computation s,((4 * k) + 2)) = 2 by A2, A9, Th6;
then A13: IC (Computation s,((4 * k) + 3)) = 3 by A2, A5, Th7;
then A14: (Computation s,((4 * k) + 4)) . (dl. 1) = (Computation s,((4 * k) + 3)) . (dl. 1) by A2, A6, Th8;
A15: ( (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) ) by A2, A5, A12, Th7;
A16: ( (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, A9, A11, Th6;
A17: ( (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, A8, A10, Th5;
( (Computation s,((4 * k) + 3)) . (dl. 1) > 0 implies IC (Computation s,((4 * k) + 4)) = 0 ) by A2, A6, A13, Th8;
hence ( (Computation s,((4 * k) + 4)) . (dl. 0 ) > 0 & ( ( (Computation s,((4 * k) + 4)) . (dl. 1) > 0 & IC (Computation s,((4 * k) + 4)) = 0 ) or ( (Computation s,((4 * k) + 4)) . (dl. 1) = 0 & IC (Computation s,((4 * k) + 4)) = 4 ) ) ) by A2, A6, A10, A17, A16, A13, A15, A14, Th8, NEWTON:78; :: thesis: verum
end;
case (Computation s,(4 * k)) . (dl. 1) = 0 ; :: thesis: ( (Computation s,((4 * k) + 4)) . (dl. 0 ) > 0 & (Computation s,((4 * k) + 4)) . (dl. 1) = 0 & IC (Computation s,((4 * k) + 4)) = 4 )
hence ( (Computation s,((4 * k) + 4)) . (dl. 0 ) > 0 & (Computation s,((4 * k) + 4)) . (dl. 1) = 0 & IC (Computation s,((4 * k) + 4)) = 4 ) by A2, A7, A8, Th9; :: thesis: verum
end;
end;
end;
hence S2[k + 1] ; :: thesis: verum
end;
A18: S2[ 0 ] by A1, A3, AMI_1:13;
for k being Element of NAT holds S2[k] from NAT_1:sch 1(A18, A4);
 hence ( (Computation s,(4 * k)) . (dl. 0 ) > 0 & ( ( (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 ) ) ) ; :: thesis: verum