A65: now

let b be Int_position ; :: thesis:
assume s1 . b = s2 . b ; :: thesis:
hence (Computation s1,1) . b = s2 . b by A12, SCMPDS_2:68
.= (Computation s2,1) . b by A13, SCMPDS_2:68 ;
:: thesis:

end;

A66: for b being Int_position st s1 . b = s2 . b holds
(Computation s1,2) . b = (Computation s2,2) . b

proof

let b be Int_position ; :: thesis:
assume A67: s1 . b = s2 . b ; :: thesis:

per cases ;

suppose A68: b = DataLoc ((Computation s1,1) . SBP ),6 ; :: thesis:

then A69: b = DataLoc ((Computation s2,1) . SBP ),6 by A8, A65;
thus (Computation s1,2) . b = (Computation s1,1) . (DataLoc (s1 . SBP ),3) by A4, A16, A17, A68, SCMPDS_2:59
.= (Computation s2,1) . (DataLoc ((Computation s1,1) . SBP ),3) by A4, A11, A17, A65
.= (Computation s2,1) . (DataLoc ((Computation s2,1) . SBP ),3) by A8, A65
.= (Computation s2,2) . b by A21, A69, SCMPDS_2:59 ; :: thesis:

end;

suppose A70: b <> DataLoc ((Computation s1,1) . SBP ),6 ; :: thesis:

then A71: b <> DataLoc ((Computation s2,1) . SBP ),6 by A8, A65;
thus (Computation s1,2) . b = (Computation s1,1) . b by A16, A70, SCMPDS_2:59
.= (Computation s2,1) . b by A65, A67
.= (Computation s2,2) . b by A21, A71, SCMPDS_2:59 ; :: thesis:

end;

A72: now

let b be Int_position ; :: thesis:
assume A73: s1 . b = s2 . b ; :: thesis:
set x1 = DataLoc ((Computation s1,2) . SBP ),2;
set x2 = DataLoc ((Computation s1,2) . SBP ),3;
set y1 = DataLoc ((Computation s2,2) . SBP ),2;
set y2 = DataLoc ((Computation s2,2) . SBP ),3;
A74: DataLoc ((Computation s1,2) . SBP ),2 = DataLoc ((Computation s2,2) . SBP ),2 by A8, A66;
A75: DataLoc ((Computation s1,2) . SBP ),3 = DataLoc ((Computation s2,2) . SBP ),3 by A8, A66;

per cases ;

suppose A76: ( b <> DataLoc ((Computation s1,2) . SBP ),2 & b <> DataLoc ((Computation s1,2) . SBP ),3 ) ; :: thesis:

hence (Computation s1,3) . b = (Computation s1,2) . b by A24, SCMPDS_2:64
.= (Computation s2,2) . b by A66, A73
.= (Computation s2,3) . b by A30, A74, A75, A76, SCMPDS_2:64 ;
:: thesis:

end;

suppose A77: b = DataLoc ((Computation s1,2) . SBP ),2 ; :: thesis:

end;

suppose A81: b = DataLoc ((Computation s1,2) . SBP ),3 ; :: thesis:

end;

A82: now

let b be Int_position ; :: thesis:
assume A83: s1 . b = s2 . b ; :: thesis:

per cases ;

suppose A84: b = DataLoc ((Computation s1,3) . SBP ),7 ; :: thesis:

then A85: b = DataLoc ((Computation s2,3) . SBP ),7 by A8, A72;
thus (Computation s1,4) . b = (Computation s1,3) . (DataLoc ((Computation s1,3) . SBP ),3) by A33, A84, SCMPDS_2:59
.= (Computation s2,3) . (DataLoc ((Computation s1,3) . SBP ),3) by A4, A11, A37, A72
.= (Computation s2,3) . (DataLoc ((Computation s2,3) . SBP ),3) by A8, A72
.= (Computation s2,4) . b by A42, A85, SCMPDS_2:59 ; :: thesis:

end;

suppose A86: b <> DataLoc ((Computation s1,3) . SBP ),7 ; :: thesis:

then A87: b <> DataLoc ((Computation s2,3) . SBP ),7 by A8, A72;
thus (Computation s1,4) . b = (Computation s1,3) . b by A33, A86, SCMPDS_2:59
.= (Computation s2,3) . b by A72, A83
.= (Computation s2,4) . b by A42, A87, SCMPDS_2:59 ; :: thesis:

end;

A88: now

let b be Int_position ; :: thesis:
assume A89: s1 . b = s2 . b ; :: thesis:
A90: s1 . (DataLoc ((Computation s1,4) . GBP ),1) = s2 . (intpos (0 + 1)) by A8, A48, Th5
.= s2 . (DataLoc ((Computation s1,4) . GBP ),1) by A48, Th5 ;

per cases ;

suppose A91: b = DataLoc ((Computation s1,4) . SBP ),(4 + RetSP ) ; :: thesis:

then A92: b = DataLoc ((Computation s2,4) . SBP ),(4 + RetSP ) by A8, A82;
thus (Computation s1,5) . b = (Computation s1,4) . (DataLoc ((Computation s1,4) . GBP ),1) by A45, A91, SCMPDS_2:59
.= (Computation s2,4) . (DataLoc ((Computation s1,4) . GBP ),1) by A82, A90
.= (Computation s2,4) . (DataLoc ((Computation s2,4) . GBP ),1) by A5, A9, A82
.= (Computation s2,5) . b by A51, A92, SCMPDS_2:59 ; :: thesis:

end;

suppose A93: b <> DataLoc ((Computation s1,4) . SBP ),(4 + RetSP ) ; :: thesis:

then A94: b <> DataLoc ((Computation s2,4) . SBP ),(4 + RetSP ) by A8, A82;
thus (Computation s1,5) . b = (Computation s1,4) . b by A45, A93, SCMPDS_2:59
.= (Computation s2,4) . b by A82, A89
.= (Computation s2,5) . b by A51, A94, SCMPDS_2:59 ; :: thesis:

end;

A95: now

let b be Int_position ; :: thesis:
assume A96: s1 . b = s2 . b ; :: thesis:
A97: s1 . (DataLoc ((Computation s1,5) . GBP ),1) = s2 . (intpos (0 + 1)) by A8, A55, Th5
.= s2 . (DataLoc ((Computation s1,5) . GBP ),1) by A55, Th5 ;

per cases ;

suppose A98: b = DataLoc ((Computation s1,5) . GBP ),1 ; :: thesis:

then A99: b = DataLoc ((Computation s2,5) . GBP ),1 by A5, A9, A88;
thus (Computation s1,6) . b = ((Computation s1,5) . (DataLoc ((Computation s1,5) . GBP ),1)) + 4 by A54, A98, SCMPDS_2:60
.= ((Computation s2,5) . (DataLoc ((Computation s1,5) . GBP ),1)) + 4 by A88, A97
.= ((Computation s2,5) . (DataLoc ((Computation s2,5) . GBP ),1)) + 4 by A5, A9, A88
.= (Computation s2,6) . b by A58, A99, SCMPDS_2:60 ; :: thesis:

end;

suppose A100: b <> DataLoc ((Computation s1,5) . GBP ),1 ; :: thesis:

then A101: b <> DataLoc ((Computation s2,5) . GBP ),1 by A5, A9, A88;
thus (Computation s1,6) . b = (Computation s1,5) . b by A54, A100, SCMPDS_2:60
.= (Computation s2,5) . b by A88, A96
.= (Computation s2,6) . b by A58, A101, SCMPDS_2:60 ; :: thesis:

end;

A102: now

let b be Int_position ; :: thesis:
assume A103: s1 . b = s2 . b ; :: thesis:

per cases ;

suppose A104: b = DataLoc ((Computation s1,6) . SBP ),RetIC ; :: thesis:

then A105: b = DataLoc ((Computation s2,6) . SBP ),RetIC by A8, A95;
thus (Computation s1,7) . b = IC (Computation s1,6) by A61, A104, SCMPDS_2:71
.= (Computation s2,7) . b by A59, A62, A64, A105, SCMPDS_2:71 ; :: thesis:

end;

suppose A106: b <> DataLoc ((Computation s1,6) . SBP ),RetIC ; :: thesis:

then A107: b <> DataLoc ((Computation s2,6) . SBP ),RetIC by A8, A95;
thus (Computation s1,7) . b = (Computation s1,6) . b by A61, A106, SCMPDS_2:71
.= (Computation s2,6) . b by A95, A103
.= (Computation s2,7) . b by A64, A107, SCMPDS_2:71 ; :: thesis:

end;

hereby :: thesis:

let k be Element of NAT ; :: thesis:
let a be Int_position ; :: thesis:
assume that
A108: k <= 7 and
A109: s1 . a = s2 . a ; :: thesis:

per cases by A108, NAT_1:32;

suppose A110: k = 0 ; :: thesis:

hence IC (Computation s1,k) = IC s1 by AMI_1:13
.= IC (Computation s2,k) by A7, A110, AMI_1:13 ;
:: thesis:
thus (Computation s1,k) . a = s1 . a by A110, AMI_1:13
.= (Computation s2,k) . a by A109, A110, AMI_1:13 ; :: thesis:

end;

suppose A111: k = 1 ; :: thesis:

hence IC (Computation s1,k) = IC (Computation s2,k) by A14, A19; :: thesis:
thus (Computation s1,k) . a = (Computation s2,k) . a by A65, A109, A111; :: thesis:

end;

suppose A112: k = 2 ; :: thesis:

hence IC (Computation s1,k) = IC (Computation s2,k) by A22, A28; :: thesis:
thus (Computation s1,k) . a = (Computation s2,k) . a by A66, A109, A112; :: thesis:

end;

suppose A113: k = 3 ; :: thesis:

hence IC (Computation s1,k) = IC (Computation s2,k) by A31, A40; :: thesis:
thus (Computation s1,k) . a = (Computation s2,k) . a by A72, A109, A113; :: thesis:

end;

suppose A114: k = 4 ; :: thesis:

hence IC (Computation s1,k) = IC (Computation s2,k) by A43, A49; :: thesis:
thus (Computation s1,k) . a = (Computation s2,k) . a by A82, A109, A114; :: thesis:

end;

suppose A115: k = 5 ; :: thesis:

hence IC (Computation s1,k) = IC (Computation s2,k) by A52, A56; :: thesis:
thus (Computation s1,k) . a = (Computation s2,k) . a by A88, A109, A115; :: thesis:

end;

suppose A116: k = 6 ; :: thesis:

hence IC (Computation s1,k) = IC (Computation s2,k) by A59, A62; :: thesis:
thus (Computation s1,k) . a = (Computation s2,k) . a by A95, A109, A116; :: thesis:

end;

suppose A117: k = 7 ; :: thesis:

hence IC (Computation s1,k) = Next (IC (Computation s2,6)) by A59, A61, A62, SCMPDS_2:71
.= IC (Computation s2,k) by A64, A117, SCMPDS_2:71 ;
:: thesis:
thus (Computation s1,k) . a = (Computation s2,k) . a by A102, A109, A117; :: thesis:

end;