set GA = GCD-Algorithm ;
defpred S₁[ Element of NAT ] means for s1, s2 being State of st GCD-Algorithm c= s1 & GCD-Algorithm c= s2 & IC s1 = inspos 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 (Computation s1,n) = return SBP & s1 . SBP = (Computation s1,n) . SBP & CurInstr (Computation s2,n) = return SBP & s2 . SBP = (Computation s2,n) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Computation s1,n) . (intpos j) & s2 . (intpos j) = (Computation s2,n) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a ) ) );
A1: S₁[ 0 ]

proof

let s1, s2 be State of ; :: thesis:
set x = s1 . (DataLoc (s1 . SBP ),2);
set y = s1 . (DataLoc (s1 . SBP ),3);
set y2 = s2 . (DataLoc (s1 . SBP ),3);
assume that
A2: GCD-Algorithm c= s1 and
A3: GCD-Algorithm c= s2 ; :: thesis:
assume A4: IC s1 = inspos 5 ; :: thesis:
assume that
s1 . SBP > 0 and
s1 . GBP = 0 ; :: thesis:
assume A5: s1 . (DataLoc (s1 . SBP ),3) <= 0 ; :: thesis:
assume s1 . (DataLoc (s1 . SBP ),3) >= 0 ; :: thesis:
assume s1 . (DataLoc (s1 . SBP ),2) >= s1 . (DataLoc (s1 . SBP ),3) ; :: thesis:
assume that
A6: IC s2 = IC s1 and
A7: s2 . SBP = s1 . SBP and
s2 . GBP = 0 ; :: thesis:
assume that
s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) and
A8: s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) ; :: thesis:
A9: Computation s1,(1 + 0 ) = Following (Computation s1,0 ) by AMI_1:14
.= Following s1 by AMI_1:13
.= Exec (SBP ,3 <=0_goto 9),s1 by A2, A4, Lm1 ;
A10: Computation s2,(1 + 0 ) = Following (Computation s2,0 ) by AMI_1:14
.= Following s2 by AMI_1:13
.= Exec (SBP ,3 <=0_goto 9),s2 by A3, A4, A6, Lm1 ;
A11: IC (Computation s1,1) = ICplusConst s1,9 by A5, A9, SCMPDS_2:68
.= inspos (5 + 9) by A4, SCMPDS_6:23 ;
A12: IC (Computation s2,1) = ICplusConst s2,9 by A5, A7, A8, A10, SCMPDS_2:68
.= inspos (5 + 9) by A4, A6, SCMPDS_6:23 ;
take n = 1; :: thesis:
thus CurInstr (Computation s1,n) = s1 . (inspos 14) by A11, AMI_1:54
.= return SBP by A2, Lm1 ; :: thesis:
thus (Computation s1,n) . SBP = s1 . SBP by A9, SCMPDS_2:68; :: thesis:
thus CurInstr (Computation s2,n) = s2 . (inspos 14) by A12, AMI_1:54
.= return SBP by A3, Lm1 ; :: thesis:
thus (Computation s2,n) . SBP = s2 . SBP by A10, SCMPDS_2:68; :: thesis:
thus for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Computation s1,n) . (intpos j) & s2 . (intpos j) = (Computation s2,n) . (intpos j) ) by A9, A10, SCMPDS_2:68; :: thesis:

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 (Computation s1,k) = IC s2 by A6, AMI_1:13
.= IC (Computation s2,k) by A15, AMI_1:13 ;
:: thesis:
thus (Computation s1,k) . a = s1 . a by A15, AMI_1:13
.= (Computation s2,k) . a by A14, A15, AMI_1:13 ; :: thesis:

end;

suppose A16: k = 1 ; :: thesis:

hence IC (Computation s1,k) = IC (Computation s2,k) by A11, A12; :: thesis:
thus (Computation s1,k) . a = s1 . a by A9, A16, SCMPDS_2:68
.= (Computation 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 ; :: 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 = inspos 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 (Computation s1,n) = return SBP & s1 . SBP = (Computation s1,n) . SBP & CurInstr (Computation s2,n) = return SBP & s2 . SBP = (Computation s2,n) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Computation s1,n) . (intpos j) & s2 . (intpos j) = (Computation s2,n) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation 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:

take nn = m + 10; :: thesis:
thus CurInstr (Computation s1,nn) = s1 . (inspos 14) by A94, AMI_1:54
.= return SBP by A19, Lm1 ; :: thesis:
A96: DataLoc ((Computation s1,(m + 9)) . SBP ),2 = intpos (n + 2) by A89, Th5;
hence (Computation s1,nn) . SBP = s1 . SBP by A88, A89, Lm3, SCMPDS_2:59; :: thesis:
thus CurInstr (Computation s2,nn) = s2 . (inspos 14) by A95, AMI_1:54
.= return SBP by A20, Lm1 ; :: thesis:
A97: DataLoc ((Computation s2,(m + 9)) . SBP ),2 = intpos (n + 2) by A93, Th5;
hence (Computation s2,nn) . SBP = s2 . SBP by A28, A92, A93, Lm3, SCMPDS_2:59; :: thesis:

hereby :: thesis:

let j be Element of NAT ; :: thesis:
assume that
A98: 1 < j and
A99: j <= (s1 . SBP ) + 1 ; :: thesis:
s1 . SBP <= (Computation s1,8) . SBP by A56, NAT_1:11;
then (s1 . SBP ) + 1 <= ((Computation s1,8) . SBP ) + 1 by XREAL_1:8;
then A100: j <= ((Computation s1,8) . SBP ) + 1 by A99, XXREAL_0:2;
A101: (Computation s1,(m + 9)) . (intpos j) = (Computation s1,(m + 8)) . (intpos j) by A75, A98, AMI_3:52, SCMPDS_2:70
.= (Computation (Computation s1,8),m) . (intpos j) by AMI_1:51
.= (Computation s1,8) . (intpos j) by A72, A98, A100 ;
A102: n + 1 < n + 2 by XREAL_1:8;
(Computation s1,7) . (intpos j) = s1 . (intpos j) by A19, A21, A23, A32, A34, A98, A99, Lm5, NAT_1:5;
hence s1 . (intpos j) = (Computation s1,8) . (intpos j) by A36, SCMPDS_2:66
.= (Computation s1,nn) . (intpos j) by A88, A96, A99, A101, A102, AMI_3:52, SCMPDS_2:59 ;
:: thesis:
A103: (Computation s2,(m + 9)) . (intpos j) = (Computation s2,(m + 8)) . (intpos j) by A83, A98, AMI_3:52, SCMPDS_2:70
.= (Computation (Computation s2,8),m) . (intpos j) by AMI_1:51
.= (Computation s2,8) . (intpos j) by A72, A98, A100 ;
j <= n + 1 by A99;
then (Computation s2,7) . (intpos j) = s2 . (intpos j) by A20, A21, A27, A28, A29, A31, A32, A98, Lm5, NAT_1:5;
hence s2 . (intpos j) = (Computation s2,8) . (intpos j) by A42, SCMPDS_2:66
.= (Computation s2,nn) . (intpos j) by A92, A97, A99, A102, A103, AMI_3:52, SCMPDS_2:59 ;
:: 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: (Computation s1,8) . a = (Computation s1,7) . a by A36, SCMPDS_2:66
.= (Computation s2,7) . a by A19, A20, A21, A23, A27, A28, A29, A30, A31, A33, A34, A105, Lm7
.= (Computation s2,8) . a by A42, SCMPDS_2:66 ;

A111: now

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

per cases ;

suppose b = SBP ; :: thesis:

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

end;

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

hence (Computation s1,(m + 9)) . b = (Computation s1,(m + 8)) . b by A75, SCMPDS_2:70
.= (Computation (Computation s1,8),m) . b by AMI_1:51
.= (Computation (Computation s2,8),m) . b by A73, A112
.= (Computation s2,(m + 8)) . b by AMI_1:51
.= (Computation s2,(m + 9)) . b by A83, A113, SCMPDS_2:70 ;
:: thesis:

end;

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

A115: now

per cases ;

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

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

end;

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

hence (Computation s1,nn) . a = (Computation s1,(m + 9)) . (DataLoc ((Computation s1,(m + 9)) . SBP ),6) by A88, A89, A93, SCMPDS_2:59
.= (Computation s2,(m + 9)) . (DataLoc ((Computation s2,(m + 9)) . SBP ),6) by A89, A93, A111, A114
.= (Computation 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 (Computation s1,j) = IC (Computation s2,j) & (Computation s1,j) . a = (Computation 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:

then consider j1 being Nat such that
A119: j = 8 + j1 by NAT_1:10;
reconsider j1 = j1 as Element of NAT by ORDINAL1:def 13;
A120: j1 <= m by A118, A119, XREAL_1:8;
thus IC (Computation s1,j) = IC (Computation (Computation s1,8),j1) by A119, AMI_1:51
.= IC (Computation (Computation s2,8),j1) by A73, A110, A120
.= IC (Computation s2,j) by A119, AMI_1:51 ; :: thesis:
thus (Computation s1,j) . a = (Computation (Computation s1,8),j1) . a by A119, AMI_1:51
.= (Computation (Computation s2,8),j1) . a by A73, A110, A120
.= (Computation s2,j) . a by A119, AMI_1:51 ; :: thesis:

end;

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

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

end;

suppose A122: j = nn ; :: thesis:

hence IC (Computation s1,j) = IC (Computation s2,j) by A94, A95; :: thesis:
thus (Computation s1,j) . a = (Computation 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 ; :: thesis:
assume that
A124: GCD-Algorithm c= s1 and
A125: GCD-Algorithm c= s2 and
A126: IC s1 = inspos 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 (Computation s1,n) = return SBP & s1 . SBP = (Computation s1,n) . SBP & CurInstr (Computation s2,n) = return SBP & s2 . SBP = (Computation s2,n) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Computation s1,n) . (intpos j) & s2 . (intpos j) = (Computation s2,n) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a ) ) ) by A124, A125, A126, A127, A128, A129, A130, A131, A132, A133, A134, A135; :: thesis: