set GA = GCD-Algorithm ;
defpred S₁[ Element of NAT ] means for s1, s2 being State of SCMPDS st GCD-Algorithm c= s1 & GCD-Algorithm c= s2 & IC s1 = 5 & s1 . SBP > 0 & s1 . GBP = 0 & s1 . (DataLoc ((s1 . SBP),3)) <= $1 & s1 . (DataLoc ((s1 . SBP),3)) >= 0 & s1 . (DataLoc ((s1 . SBP),2)) >= s1 . (DataLoc ((s1 . SBP),3)) & IC s2 = IC s1 & s2 . SBP = s1 . SBP & s2 . GBP = 0 & s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) & s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) holds
ex n being Element of NAT st
( CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,n))),(Comput ((ProgramPart s1),s1,n))) = return SBP & s1 . SBP = (Comput ((ProgramPart s1),s1,n)) . SBP & CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,n))),(Comput ((ProgramPart s2),s2,n))) = return SBP & s2 . SBP = (Comput ((ProgramPart s2),s2,n)) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP) + 1 holds
( s1 . (intpos j) = (Comput ((ProgramPart s1),s1,n)) . (intpos j) & s2 . (intpos j) = (Comput ((ProgramPart s2),s2,n)) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput ((ProgramPart s1),s1,k)) = IC (Comput ((ProgramPart s2),s2,k)) & (Comput ((ProgramPart s1),s1,k)) . a = (Comput ((ProgramPart s2),s2,k)) . a ) ) );
A1: S₁[ 0 ]

proof

hereby :: thesis:

let k be Element of NAT ; :: thesis:
let a be Int_position ; :: thesis:
assume that
A13: k <= n and
A14: s1 . a = s2 . a ; :: thesis:

per cases by A13, NAT_1:26;

suppose A15: k = 0 ; :: thesis:

hence IC (Comput ((ProgramPart s1),s1,k)) = IC s2 by A6, EXTPRO_1:3
.= IC (Comput ((ProgramPart s2),s2,k)) by A15, EXTPRO_1:3 ;
:: thesis:
thus (Comput ((ProgramPart s1),s1,k)) . a = s1 . a by A15, EXTPRO_1:3
.= (Comput ((ProgramPart s2),s2,k)) . a by A14, A15, EXTPRO_1:3 ; :: thesis:

end;

suppose A16: k = 1 ; :: thesis:

hence IC (Comput ((ProgramPart s1),s1,k)) = IC (Comput ((ProgramPart s2),s2,k)) by A11, A12; :: thesis:
thus (Comput ((ProgramPart s1),s1,k)) . a = s1 . a by A9, A16, SCMPDS_2:68
.= (Comput ((ProgramPart s2),s2,k)) . a by A10, A14, A16, SCMPDS_2:68 ; :: thesis:

end;

A17: now

let k be Element of NAT ; :: thesis:
assume A18: S₁[k] ; :: thesis:

now

let s1, s2 be State of SCMPDS; :: thesis:
set x = s1 . (DataLoc ((s1 . SBP),2));
set y = s1 . (DataLoc ((s1 . SBP),3));
assume that
A19: GCD-Algorithm c= s1 and
A20: GCD-Algorithm c= s2 ; :: thesis:
assume A21: IC s1 = 5 ; :: thesis:
assume that
A22: s1 . SBP > 0 and
A23: s1 . GBP = 0 ; :: thesis:
assume A24: s1 . (DataLoc ((s1 . SBP),3)) <= k + 1 ; :: thesis:
assume A25: s1 . (DataLoc ((s1 . SBP),3)) >= 0 ; :: thesis:
assume A26: s1 . (DataLoc ((s1 . SBP),2)) >= s1 . (DataLoc ((s1 . SBP),3)) ; :: thesis:
assume that
A27: IC s2 = IC s1 and
A28: s2 . SBP = s1 . SBP and
A29: s2 . GBP = 0 ; :: thesis:
assume that
A30: s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) and
A31: s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) ; :: thesis:
reconsider y = s1 . (DataLoc ((s1 . SBP),3)) as Element of NAT by A25, INT_1:16;

per cases by A24, NAT_1:8;

suppose y <= k ; :: thesis:

hence ex n being Element of NAT st
( CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,n))),(Comput ((ProgramPart s1),s1,n))) = return SBP & s1 . SBP = (Comput ((ProgramPart s1),s1,n)) . SBP & CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,n))),(Comput ((ProgramPart s2),s2,n))) = return SBP & s2 . SBP = (Comput ((ProgramPart s2),s2,n)) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP) + 1 holds
( s1 . (intpos j) = (Comput ((ProgramPart s1),s1,n)) . (intpos j) & s2 . (intpos j) = (Comput ((ProgramPart s2),s2,n)) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput ((ProgramPart s1),s1,k)) = IC (Comput ((ProgramPart s2),s2,k)) & (Comput ((ProgramPart s1),s1,k)) . a = (Comput ((ProgramPart s2),s2,k)) . a ) ) ) by A18, A19, A20, A21, A22, A23, A25, A26, A27, A28, A29, A30, A31; :: thesis:

end;

suppose A32: y = k + 1 ; :: thesis:

hereby :: thesis:

hereby :: thesis:

end;

hereby :: thesis:

let j be Element of NAT ; :: thesis:
let a be Int_position ; :: thesis:
assume that
A104: j <= nn and
A105: s1 . a = s2 . a ; :: thesis:
nn = (m + 9) + 1 ;
then A106: ( j <= m + 9 or j = nn ) by A104, NAT_1:8;
A107: m + (8 + 1) = (m + 8) + 1 ;

A108: now

assume A109: j <= m + 8 ; :: thesis:

per cases ;

suppose j < 7 + 1 ; :: thesis:

hence ( j <= 7 or ( j >= 8 & j <= m + 8 ) ) by NAT_1:13; :: thesis:

end;

suppose j >= 8 ; :: thesis:

hence ( j <= 7 or ( j >= 8 & j <= m + 8 ) ) by A109; :: thesis:

end;

A110: (Comput ((ProgramPart s1),s1,8)) . a = (Comput ((ProgramPart s1),s1,7)) . a by A36, SCMPDS_2:66
.= (Comput ((ProgramPart s2),s2,7)) . a by A19, A20, A21, A23, A27, A28, A29, A30, A31, A33, A34, A105, Lm7
.= (Comput ((ProgramPart s2),s2,8)) . a by A42, SCMPDS_2:66 ;

A111: now

let b be Int_position ; :: thesis:
assume A112: (Comput ((ProgramPart s1),s1,8)) . b = (Comput ((ProgramPart s2),s2,8)) . b ; :: thesis:

per cases ;

suppose b = SBP ; :: thesis:

hence (Comput ((ProgramPart s1),s1,(m + 9))) . b = (Comput ((ProgramPart s2),s2,(m + 9))) . b by A89, A93; :: thesis:

end;

suppose A113: b <> SBP ; :: thesis:

hence (Comput ((ProgramPart s1),s1,(m + 9))) . b = (Comput ((ProgramPart s1),s1,(m + 8))) . b by A75, SCMPDS_2:70
.= (Comput ((ProgramPart (Comput ((ProgramPart s1),s1,8))),(Comput ((ProgramPart s1),s1,8)),m)) . b by T9, EXTPRO_1:5
.= (Comput ((ProgramPart (Comput ((ProgramPart s2),s2,8))),(Comput ((ProgramPart s2),s2,8)),m)) . b by A73, A112
.= (Comput ((ProgramPart s2),s2,(m + 8))) . b by T8, EXTPRO_1:5
.= (Comput ((ProgramPart s2),s2,(m + 9))) . b by A83, A113, SCMPDS_2:70 ;
:: thesis:

end;

A114: (Comput ((ProgramPart s1),s1,8)) . (DataLoc (((Comput ((ProgramPart s1),s1,(m + 9))) . SBP),6)) = (Comput ((ProgramPart s1),s1,8)) . (DataLoc (((Comput ((ProgramPart s1),s1,8)) . SBP),2)) by A51, A56, A89, Th5
.= (Comput ((ProgramPart s2),s2,8)) . (DataLoc (((Comput ((ProgramPart s1),s1,(m + 9))) . SBP),6)) by A51, A56, A67, A89, Th5 ;

A115: now

per cases ;

suppose A116: a <> DataLoc (((Comput ((ProgramPart s2),s2,(m + 9))) . SBP),2) ; :: thesis:

hence (Comput ((ProgramPart s1),s1,nn)) . a = (Comput ((ProgramPart s1),s1,(m + 9))) . a by A88, A89, A93, SCMPDS_2:59
.= (Comput ((ProgramPart s2),s2,(m + 9))) . a by A110, A111
.= (Comput ((ProgramPart s2),s2,nn)) . a by A92, A116, SCMPDS_2:59 ;
:: thesis:

end;

suppose A117: a = DataLoc (((Comput ((ProgramPart s2),s2,(m + 9))) . SBP),2) ; :: thesis:

hence (Comput ((ProgramPart s1),s1,nn)) . a = (Comput ((ProgramPart s1),s1,(m + 9))) . (DataLoc (((Comput ((ProgramPart s1),s1,(m + 9))) . SBP),6)) by A88, A89, A93, SCMPDS_2:59
.= (Comput ((ProgramPart s2),s2,(m + 9))) . (DataLoc (((Comput ((ProgramPart s2),s2,(m + 9))) . SBP),6)) by A89, A93, A111, A114
.= (Comput ((ProgramPart s2),s2,nn)) . a by A92, A117, SCMPDS_2:59 ;
:: thesis:

end;

per cases by A106, A107, A108, NAT_1:8;

suppose j <= 7 ; :: thesis:

hence ( IC (Comput ((ProgramPart s1),s1,j)) = IC (Comput ((ProgramPart s2),s2,j)) & (Comput ((ProgramPart s1),s1,j)) . a = (Comput ((ProgramPart s2),s2,j)) . a ) by A19, A20, A21, A23, A27, A28, A29, A30, A31, A33, A34, A105, Lm7; :: thesis:

end;

suppose A118: ( j >= 8 & j <= m + 8 ) ; :: thesis:

end;

suppose A121: j = m + 9 ; :: thesis:

hence IC (Comput ((ProgramPart s1),s1,j)) = IC (Comput ((ProgramPart s2),s2,j)) by A86, A90; :: thesis:
thus (Comput ((ProgramPart s1),s1,j)) . a = (Comput ((ProgramPart s2),s2,j)) . a by A110, A111, A121; :: thesis:

end;

suppose A122: j = nn ; :: thesis:

hence IC (Comput ((ProgramPart s1),s1,j)) = IC (Comput ((ProgramPart s2),s2,j)) by A94, A95; :: thesis:
thus (Comput ((ProgramPart s1),s1,j)) . a = (Comput ((ProgramPart s2),s2,j)) . a by A115, A122; :: thesis:

end;

hence S₁[k + 1] ; :: thesis:

end;

A123: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A17);
let s1, s2 be State of SCMPDS; :: thesis:
assume that
A124: GCD-Algorithm c= s1 and
A125: GCD-Algorithm c= s2 and
A126: IC s1 = 5 and
A127: s1 . SBP > 0 and
A128: s1 . GBP = 0 and
A129: s1 . (DataLoc ((s1 . SBP),3)) >= 0 and
A130: s1 . (DataLoc ((s1 . SBP),2)) >= s1 . (DataLoc ((s1 . SBP),3)) and
A131: IC s2 = IC s1 and
A132: s2 . SBP = s1 . SBP and
A133: s2 . GBP = 0 and
A134: s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) and
A135: s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) ; :: thesis:
reconsider m = s1 . (DataLoc ((s1 . SBP),3)) as Element of NAT by A129, INT_1:16;
S₁[m] by A123;
hence ex n being Element of NAT st
( CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,n))),(Comput ((ProgramPart s1),s1,n))) = return SBP & s1 . SBP = (Comput ((ProgramPart s1),s1,n)) . SBP & CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,n))),(Comput ((ProgramPart s2),s2,n))) = return SBP & s2 . SBP = (Comput ((ProgramPart s2),s2,n)) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP) + 1 holds
( s1 . (intpos j) = (Comput ((ProgramPart s1),s1,n)) . (intpos j) & s2 . (intpos j) = (Comput ((ProgramPart s2),s2,n)) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput ((ProgramPart s1),s1,k)) = IC (Comput ((ProgramPart s2),s2,k)) & (Comput ((ProgramPart s1),s1,k)) . a = (Comput ((ProgramPart s2),s2,k)) . a ) ) ) by A124, A125, A126, A127, A128, A129, A130, A131, A132, A133, A134, A135; :: thesis: