let n be Nat; :: thesis: for s1, s2 being State of SCMPDS
for P1, P2 being Instruction-Sequence of SCMPDS st GCD-Algorithm c= P1 & GCD-Algorithm c= P2 & IC s1 = 5 & n = s1 . SBP & s1 . GBP = 0 & s1 . (DataLoc ((s1 . SBP),3)) > 0 & 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
for k being Nat
for a being Int_position st k <= 7 & s1 . a = s2 . a holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a )
let s1, s2 be State of SCMPDS; :: thesis: for P1, P2 being Instruction-Sequence of SCMPDS st GCD-Algorithm c= P1 & GCD-Algorithm c= P2 & IC s1 = 5 & n = s1 . SBP & s1 . GBP = 0 & s1 . (DataLoc ((s1 . SBP),3)) > 0 & 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
for k being Nat
for a being Int_position st k <= 7 & s1 . a = s2 . a holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a )
let P1, P2 be Instruction-Sequence of SCMPDS; :: thesis: ( GCD-Algorithm c= P1 & GCD-Algorithm c= P2 & IC s1 = 5 & n = s1 . SBP & s1 . GBP = 0 & s1 . (DataLoc ((s1 . SBP),3)) > 0 & 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)) implies for k being Nat
for a being Int_position st k <= 7 & s1 . a = s2 . a holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a ) )
set GA = GCD-Algorithm ;
assume that
A1: GCD-Algorithm c= P1 and
A2: GCD-Algorithm c= P2 ; :: thesis: ( not IC s1 = 5 or not n = s1 . SBP or not s1 . GBP = 0 or not s1 . (DataLoc ((s1 . SBP),3)) > 0 or not IC s2 = IC s1 or not s2 . SBP = s1 . SBP or not s2 . GBP = 0 or not s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) or not s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) or for k being Nat
for a being Int_position st k <= 7 & s1 . a = s2 . a holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a ) )
assume A3: IC s1 = 5 ; :: thesis: ( not n = s1 . SBP or not s1 . GBP = 0 or not s1 . (DataLoc ((s1 . SBP),3)) > 0 or not IC s2 = IC s1 or not s2 . SBP = s1 . SBP or not s2 . GBP = 0 or not s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) or not s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) or for k being Nat
for a being Int_position st k <= 7 & s1 . a = s2 . a holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a ) )
assume A4: n = s1 . SBP ; :: thesis: ( not s1 . GBP = 0 or not s1 . (DataLoc ((s1 . SBP),3)) > 0 or not IC s2 = IC s1 or not s2 . SBP = s1 . SBP or not s2 . GBP = 0 or not s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) or not s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) or for k being Nat
for a being Int_position st k <= 7 & s1 . a = s2 . a holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a ) )
assume A5: s1 . GBP = 0 ; :: thesis: ( not s1 . (DataLoc ((s1 . SBP),3)) > 0 or not IC s2 = IC s1 or not s2 . SBP = s1 . SBP or not s2 . GBP = 0 or not s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) or not s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) or for k being Nat
for a being Int_position st k <= 7 & s1 . a = s2 . a holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a ) )
assume A6: s1 . (DataLoc ((s1 . SBP),3)) > 0 ; :: thesis: ( not IC s2 = IC s1 or not s2 . SBP = s1 . SBP or not s2 . GBP = 0 or not s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) or not s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) or for k being Nat
for a being Int_position st k <= 7 & s1 . a = s2 . a holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a ) )
assume that
A7: IC s2 = IC s1 and
A8: s2 . SBP = s1 . SBP and
A9: s2 . GBP = 0 ; :: thesis: ( not s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) or not s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) or for k being Nat
for a being Int_position st k <= 7 & s1 . a = s2 . a holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a ) )
assume that
A10: s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) and
A11: s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) ; :: thesis: for k being Nat
for a being Int_position st k <= 7 & s1 . a = s2 . a holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a )
A12: P1 /. (IC s1) = P1 . (IC s1) by PBOOLE:143;
A13: Comput (P1,s1,(1 + 0)) = Following (P1,(Comput (P1,s1,0))) by EXTPRO_1:3
.= Following (P1,s1) by EXTPRO_1:2
.= Exec (((SBP,3) <=0_goto 9),s1) by A12, A3, Lm1, A1 ;
A14: P2 /. (IC s2) = P2 . (IC s2) by PBOOLE:143;
A15: Comput (P2,s2,(1 + 0)) = Following (P2,(Comput (P2,s2,0))) by EXTPRO_1:3
.= Following (P2,s2) by EXTPRO_1:2
.= Exec (((SBP,3) <=0_goto 9),s2) by A3, A7, Lm1, A14, A2 ;
A16: P1 /. (IC (Comput (P1,s1,1))) = P1 . (IC (Comput (P1,s1,1))) by PBOOLE:143;
A17: IC (Comput (P1,s1,1)) = (IC s1) + 1 by A6, A13, SCMPDS_2:56
.= 5 + 1 by A3 ;
then A18: CurInstr (P1,(Comput (P1,s1,1))) = P1 . 6 by A16
.= (SBP,6) := (SBP,3) by Lm1, A1 ;
A19: Comput (P1,s1,(1 + 1)) = Following (P1,(Comput (P1,s1,1))) by EXTPRO_1:3
.= Exec (((SBP,6) := (SBP,3)),(Comput (P1,s1,1))) by A18 ;
A20: (Comput (P1,s1,1)) . SBP = n by A4, A13, SCMPDS_2:56;
A21: (Comput (P1,s1,1)) . GBP = 0 by A5, A13, SCMPDS_2:56;
A22: P2 /. (IC (Comput (P2,s2,1))) = P2 . (IC (Comput (P2,s2,1))) by PBOOLE:143;
A23: IC (Comput (P2,s2,1)) = (IC s2) + 1 by A6, A8, A11, A15, SCMPDS_2:56
.= 5 + 1 by A3, A7 ;
then A24: CurInstr (P2,(Comput (P2,s2,1))) = P2 . 6 by A22
.= (SBP,6) := (SBP,3) by Lm1, A2 ;
A25: Comput (P2,s2,(1 + 1)) = Following (P2,(Comput (P2,s2,1))) by EXTPRO_1:3
.= Exec (((SBP,6) := (SBP,3)),(Comput (P2,s2,1))) by A24 ;
A26: P1 /. (IC (Comput (P1,s1,2))) = P1 . (IC (Comput (P1,s1,2))) by PBOOLE:143;
A27: IC (Comput (P1,s1,2)) = (IC (Comput (P1,s1,1))) + 1 by A19, SCMPDS_2:47
.= 6 + 1 by A17 ;
then A28: CurInstr (P1,(Comput (P1,s1,2))) = P1 . 7 by A26
.= Divide (SBP,2,SBP,3) by Lm1, A1 ;
A29: Comput (P1,s1,(2 + 1)) = Following (P1,(Comput (P1,s1,2))) by EXTPRO_1:3
.= Exec ((Divide (SBP,2,SBP,3)),(Comput (P1,s1,2))) by A28 ;
A30: DataLoc (((Comput (P1,s1,1)) . SBP),6) = intpos (n + 6) by A20, Th1;
then A31: (Comput (P1,s1,2)) . SBP = n by A19, A20, Lm3, SCMPDS_2:47;
A32: (Comput (P1,s1,2)) . GBP = 0 by A19, A21, A30, Lm2, SCMPDS_2:47;
A33: P2 /. (IC (Comput (P2,s2,2))) = P2 . (IC (Comput (P2,s2,2))) by PBOOLE:143;
A34: IC (Comput (P2,s2,2)) = (IC (Comput (P2,s2,1))) + 1 by A25, SCMPDS_2:47
.= 6 + 1 by A23 ;
then A35: CurInstr (P2,(Comput (P2,s2,2))) = P2 . 7 by A33
.= Divide (SBP,2,SBP,3) by Lm1, A2 ;
A36: Comput (P2,s2,(2 + 1)) = Following (P2,(Comput (P2,s2,2))) by EXTPRO_1:3
.= Exec ((Divide (SBP,2,SBP,3)),(Comput (P2,s2,2))) by A35 ;
A37: P1 /. (IC (Comput (P1,s1,3))) = P1 . (IC (Comput (P1,s1,3))) by PBOOLE:143;
A38: IC (Comput (P1,s1,3)) = (IC (Comput (P1,s1,2))) + 1 by A29, SCMPDS_2:52
.= 7 + 1 by A27 ;
then A39: CurInstr (P1,(Comput (P1,s1,3))) = P1 . 8 by A37
.= (SBP,7) := (SBP,3) by Lm1, A1 ;
A40: Comput (P1,s1,(3 + 1)) = Following (P1,(Comput (P1,s1,3))) by EXTPRO_1:3
.= Exec (((SBP,7) := (SBP,3)),(Comput (P1,s1,3))) by A39 ;
A41: DataLoc (((Comput (P1,s1,2)) . SBP),2) = intpos (n + 2) by A31, Th1;
then A42: SBP <> DataLoc (((Comput (P1,s1,2)) . SBP),2) by Lm3;
A43: DataLoc (((Comput (P1,s1,2)) . SBP),3) = intpos (n + 3) by A31, Th1;
then SBP <> DataLoc (((Comput (P1,s1,2)) . SBP),3) by Lm3;
then A44: (Comput (P1,s1,3)) . SBP = n by A29, A31, A42, SCMPDS_2:52;
A45: GBP <> DataLoc (((Comput (P1,s1,2)) . SBP),2) by A41, Lm2;
GBP <> DataLoc (((Comput (P1,s1,2)) . SBP),3) by A43, Lm2;
then A46: (Comput (P1,s1,3)) . GBP = 0 by A29, A32, A45, SCMPDS_2:52;
A47: P2 /. (IC (Comput (P2,s2,3))) = P2 . (IC (Comput (P2,s2,3))) by PBOOLE:143;
A48: IC (Comput (P2,s2,3)) = (IC (Comput (P2,s2,2))) + 1 by A36, SCMPDS_2:52
.= 7 + 1 by A34 ;
then A49: CurInstr (P2,(Comput (P2,s2,3))) = P2 . 8 by A47
.= (SBP,7) := (SBP,3) by Lm1, A2 ;
A50: Comput (P2,s2,(3 + 1)) = Following (P2,(Comput (P2,s2,3))) by EXTPRO_1:3
.= Exec (((SBP,7) := (SBP,3)),(Comput (P2,s2,3))) by A49 ;
A51: P1 /. (IC (Comput (P1,s1,4))) = P1 . (IC (Comput (P1,s1,4))) by PBOOLE:143;
A52: IC (Comput (P1,s1,4)) = (IC (Comput (P1,s1,3))) + 1 by A40, SCMPDS_2:47
.= 8 + 1 by A38 ;
then A53: CurInstr (P1,(Comput (P1,s1,4))) = P1 . 9 by A51
.= (SBP,(4 + RetSP)) := (GBP,1) by Lm1, A1 ;
A54: Comput (P1,s1,(4 + 1)) = Following (P1,(Comput (P1,s1,4))) by EXTPRO_1:3
.= Exec (((SBP,(4 + RetSP)) := (GBP,1)),(Comput (P1,s1,4))) by A53 ;
A55: DataLoc (((Comput (P1,s1,3)) . SBP),7) = intpos (n + 7) by A44, Th1;
then A56: (Comput (P1,s1,4)) . SBP = n by A40, A44, Lm3, SCMPDS_2:47;
A57: (Comput (P1,s1,4)) . GBP = 0 by A40, A46, A55, Lm2, SCMPDS_2:47;
A58: P2 /. (IC (Comput (P2,s2,4))) = P2 . (IC (Comput (P2,s2,4))) by PBOOLE:143;
A59: IC (Comput (P2,s2,4)) = (IC (Comput (P2,s2,3))) + 1 by A50, SCMPDS_2:47
.= 8 + 1 by A48 ;
then A60: CurInstr (P2,(Comput (P2,s2,4))) = P2 . 9 by A58
.= (SBP,(4 + RetSP)) := (GBP,1) by Lm1, A2 ;
A61: Comput (P2,s2,(4 + 1)) = Following (P2,(Comput (P2,s2,4))) by EXTPRO_1:3
.= Exec (((SBP,(4 + RetSP)) := (GBP,1)),(Comput (P2,s2,4))) by A60 ;
A62: P1 /. (IC (Comput (P1,s1,5))) = P1 . (IC (Comput (P1,s1,5))) by PBOOLE:143;
A63: IC (Comput (P1,s1,5)) = (IC (Comput (P1,s1,4))) + 1 by A54, SCMPDS_2:47
.= 9 + 1 by A52 ;
then A64: CurInstr (P1,(Comput (P1,s1,5))) = P1 . 10 by A62
.= AddTo (GBP,1,4) by Lm1, A1 ;
A65: Comput (P1,s1,(5 + 1)) = Following (P1,(Comput (P1,s1,5))) by EXTPRO_1:3
.= Exec ((AddTo (GBP,1,4)),(Comput (P1,s1,5))) by A64 ;
DataLoc (((Comput (P1,s1,4)) . SBP),(4 + RetSP)) = intpos (n + (4 + 0)) by A56, Th1, SCMPDS_I:def 13;
then A66: (Comput (P1,s1,5)) . GBP = 0 by A54, A57, Lm2, SCMPDS_2:47;
A67: P2 /. (IC (Comput (P2,s2,5))) = P2 . (IC (Comput (P2,s2,5))) by PBOOLE:143;
A68: IC (Comput (P2,s2,5)) = (IC (Comput (P2,s2,4))) + 1 by A61, SCMPDS_2:47
.= 9 + 1 by A59 ;
then A69: CurInstr (P2,(Comput (P2,s2,5))) = P2 . 10 by A67
.= AddTo (GBP,1,4) by Lm1, A2 ;
A70: Comput (P2,s2,(5 + 1)) = Following (P2,(Comput (P2,s2,5))) by EXTPRO_1:3
.= Exec ((AddTo (GBP,1,4)),(Comput (P2,s2,5))) by A69 ;
A71: P1 /. (IC (Comput (P1,s1,6))) = P1 . (IC (Comput (P1,s1,6))) by PBOOLE:143;
A72: IC (Comput (P1,s1,6)) = (IC (Comput (P1,s1,5))) + 1 by A65, SCMPDS_2:48
.= 10 + 1 by A63 ;
then A73: CurInstr (P1,(Comput (P1,s1,6))) = P1 . 11 by A71
.= saveIC (SBP,RetIC) by Lm1, A1 ;
A74: Comput (P1,s1,(6 + 1)) = Following (P1,(Comput (P1,s1,6))) by EXTPRO_1:3
.= Exec ((saveIC (SBP,RetIC)),(Comput (P1,s1,6))) by A73 ;
A75: P2 /. (IC (Comput (P2,s2,6))) = P2 . (IC (Comput (P2,s2,6))) by PBOOLE:143;
A76: IC (Comput (P2,s2,6)) = (IC (Comput (P2,s2,5))) + 1 by A70, SCMPDS_2:48
.= 10 + 1 by A68 ;
then A77: CurInstr (P2,(Comput (P2,s2,6))) = P2 . 11 by A75
.= saveIC (SBP,RetIC) by Lm1, A2 ;
A78: Comput (P2,s2,(6 + 1)) = Following (P2,(Comput (P2,s2,6))) by EXTPRO_1:3
.= Exec ((saveIC (SBP,RetIC)),(Comput (P2,s2,6))) by A77 ;

A79: now :: thesis: for b being Int_position st s1 . b = s2 . b holds
(Comput (P1,s1,1)) . b = (Comput (P2,s2,1)) . b

let b be Int_position; :: thesis: ( s1 . b = s2 . b implies (Comput (P1,s1,1)) . b = (Comput (P2,s2,1)) . b )
assume s1 . b = s2 . b ; :: thesis: (Comput (P1,s1,1)) . b = (Comput (P2,s2,1)) . b
hence (Comput (P1,s1,1)) . b = s2 . b by A13, SCMPDS_2:56
.= (Comput (P2,s2,1)) . b by A15, SCMPDS_2:56 ;
:: thesis: verum

end;

A80: for b being Int_position st s1 . b = s2 . b holds
(Comput (P1,s1,2)) . b = (Comput (P2,s2,2)) . b

proof

let b be Int_position; :: thesis: ( s1 . b = s2 . b implies (Comput (P1,s1,2)) . b = (Comput (P2,s2,2)) . b )
assume A81: s1 . b = s2 . b ; :: thesis: (Comput (P1,s1,2)) . b = (Comput (P2,s2,2)) . b

per cases ( b = DataLoc (((Comput (P1,s1,1)) . SBP),6) or b <> DataLoc (((Comput (P1,s1,1)) . SBP),6) ) ;

suppose A82: b = DataLoc (((Comput (P1,s1,1)) . SBP),6) ; :: thesis: (Comput (P1,s1,2)) . b = (Comput (P2,s2,2)) . b

then A83: b = DataLoc (((Comput (P2,s2,1)) . SBP),6) by A8, A79;
thus (Comput (P1,s1,2)) . b = (Comput (P1,s1,1)) . (DataLoc ((s1 . SBP),3)) by A4, A19, A20, A82, SCMPDS_2:47
.= (Comput (P2,s2,1)) . (DataLoc (((Comput (P1,s1,1)) . SBP),3)) by A4, A11, A20, A79
.= (Comput (P2,s2,1)) . (DataLoc (((Comput (P2,s2,1)) . SBP),3)) by A8, A79
.= (Comput (P2,s2,2)) . b by A25, A83, SCMPDS_2:47 ; :: thesis: verum

end;

suppose A84: b <> DataLoc (((Comput (P1,s1,1)) . SBP),6) ; :: thesis: (Comput (P1,s1,2)) . b = (Comput (P2,s2,2)) . b

then A85: b <> DataLoc (((Comput (P2,s2,1)) . SBP),6) by A8, A79;
thus (Comput (P1,s1,2)) . b = (Comput (P1,s1,1)) . b by A19, A84, SCMPDS_2:47
.= (Comput (P2,s2,1)) . b by A79, A81
.= (Comput (P2,s2,2)) . b by A25, A85, SCMPDS_2:47 ; :: thesis: verum

end;

end;

end;

A86: now :: thesis: for b being Int_position st s1 . b = s2 . b holds
(Comput (P1,s1,3)) . b = (Comput (P2,s2,3)) . b

let b be Int_position; :: thesis: ( s1 . b = s2 . b implies (Comput (P1,s1,3)) . b₁ = (Comput (P2,s2,3)) . b₁ )
assume A87: s1 . b = s2 . b ; :: thesis: (Comput (P1,s1,3)) . b₁ = (Comput (P2,s2,3)) . b₁
set x1 = DataLoc (((Comput (P1,s1,2)) . SBP),2);
set x2 = DataLoc (((Comput (P1,s1,2)) . SBP),3);
set y1 = DataLoc (((Comput (P2,s2,2)) . SBP),2);
set y2 = DataLoc (((Comput (P2,s2,2)) . SBP),3);
A88: DataLoc (((Comput (P1,s1,2)) . SBP),2) = DataLoc (((Comput (P2,s2,2)) . SBP),2) by A8, A80;
A89: DataLoc (((Comput (P1,s1,2)) . SBP),3) = DataLoc (((Comput (P2,s2,2)) . SBP),3) by A8, A80;

per cases ( ( b <> DataLoc (((Comput (P1,s1,2)) . SBP),2) & b <> DataLoc (((Comput (P1,s1,2)) . SBP),3) ) or b = DataLoc (((Comput (P1,s1,2)) . SBP),2) or b = DataLoc (((Comput (P1,s1,2)) . SBP),3) ) ;

suppose A90: ( b <> DataLoc (((Comput (P1,s1,2)) . SBP),2) & b <> DataLoc (((Comput (P1,s1,2)) . SBP),3) ) ; :: thesis: (Comput (P1,s1,3)) . b₁ = (Comput (P2,s2,3)) . b₁

hence (Comput (P1,s1,3)) . b = (Comput (P1,s1,2)) . b by A29, SCMPDS_2:52
.= (Comput (P2,s2,2)) . b by A80, A87
.= (Comput (P2,s2,3)) . b by A36, A88, A89, A90, SCMPDS_2:52 ;
:: thesis: verum

end;

suppose A91: b = DataLoc (((Comput (P1,s1,2)) . SBP),2) ; :: thesis: (Comput (P1,s1,3)) . b₁ = (Comput (P2,s2,3)) . b₁

A92: n + 2 <> n + 3 ;
then A93: DataLoc (((Comput (P1,s1,2)) . SBP),2) <> DataLoc (((Comput (P1,s1,2)) . SBP),3) by A41, A43, AMI_3:10;
A94: DataLoc (((Comput (P2,s2,2)) . SBP),2) <> DataLoc (((Comput (P2,s2,2)) . SBP),3) by A41, A43, A88, A89, A92, AMI_3:10;
thus (Comput (P1,s1,3)) . b = ((Comput (P1,s1,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),2))) div ((Comput (P1,s1,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),3))) by A29, A91, A93, SCMPDS_2:52
.= ((Comput (P2,s2,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),2))) div ((Comput (P1,s1,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),3))) by A4, A10, A31, A80
.= ((Comput (P2,s2,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),2))) div ((Comput (P2,s2,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),3))) by A4, A11, A31, A80
.= (Comput (P2,s2,3)) . b by A36, A88, A89, A91, A94, SCMPDS_2:52 ; :: thesis: verum

end;

suppose A95: b = DataLoc (((Comput (P1,s1,2)) . SBP),3) ; :: thesis: (Comput (P1,s1,3)) . b₁ = (Comput (P2,s2,3)) . b₁

hence (Comput (P1,s1,3)) . b = ((Comput (P1,s1,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),2))) mod ((Comput (P1,s1,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),3))) by A29, SCMPDS_2:52
.= ((Comput (P2,s2,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),2))) mod ((Comput (P1,s1,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),3))) by A4, A10, A31, A80
.= ((Comput (P2,s2,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),2))) mod ((Comput (P2,s2,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),3))) by A4, A11, A31, A80
.= (Comput (P2,s2,3)) . b by A36, A88, A89, A95, SCMPDS_2:52 ;
:: thesis: verum

end;

end;

end;

A96: now :: thesis: for b being Int_position st s1 . b = s2 . b holds
(Comput (P1,s1,4)) . b = (Comput (P2,s2,4)) . b

let b be Int_position; :: thesis: ( s1 . b = s2 . b implies (Comput (P1,s1,4)) . b₁ = (Comput (P2,s2,4)) . b₁ )
assume A97: s1 . b = s2 . b ; :: thesis: (Comput (P1,s1,4)) . b₁ = (Comput (P2,s2,4)) . b₁

per cases ( b = DataLoc (((Comput (P1,s1,3)) . SBP),7) or b <> DataLoc (((Comput (P1,s1,3)) . SBP),7) ) ;

suppose A98: b = DataLoc (((Comput (P1,s1,3)) . SBP),7) ; :: thesis: (Comput (P1,s1,4)) . b₁ = (Comput (P2,s2,4)) . b₁

then A99: b = DataLoc (((Comput (P2,s2,3)) . SBP),7) by A8, A86;
thus (Comput (P1,s1,4)) . b = (Comput (P1,s1,3)) . (DataLoc (((Comput (P1,s1,3)) . SBP),3)) by A40, A98, SCMPDS_2:47
.= (Comput (P2,s2,3)) . (DataLoc (((Comput (P1,s1,3)) . SBP),3)) by A4, A11, A44, A86
.= (Comput (P2,s2,3)) . (DataLoc (((Comput (P2,s2,3)) . SBP),3)) by A8, A86
.= (Comput (P2,s2,4)) . b by A50, A99, SCMPDS_2:47 ; :: thesis: verum

end;

suppose A100: b <> DataLoc (((Comput (P1,s1,3)) . SBP),7) ; :: thesis: (Comput (P1,s1,4)) . b₁ = (Comput (P2,s2,4)) . b₁

then A101: b <> DataLoc (((Comput (P2,s2,3)) . SBP),7) by A8, A86;
thus (Comput (P1,s1,4)) . b = (Comput (P1,s1,3)) . b by A40, A100, SCMPDS_2:47
.= (Comput (P2,s2,3)) . b by A86, A97
.= (Comput (P2,s2,4)) . b by A50, A101, SCMPDS_2:47 ; :: thesis: verum

end;

end;

end;

A102: now :: thesis: for b being Int_position st s1 . b = s2 . b holds
(Comput (P1,s1,5)) . b = (Comput (P2,s2,5)) . b

let b be Int_position; :: thesis: ( s1 . b = s2 . b implies (Comput (P1,s1,5)) . b₁ = (Comput (P2,s2,5)) . b₁ )
assume A103: s1 . b = s2 . b ; :: thesis: (Comput (P1,s1,5)) . b₁ = (Comput (P2,s2,5)) . b₁
A104: s1 . (DataLoc (((Comput (P1,s1,4)) . GBP),1)) = s2 . (intpos (0 + 1)) by A8, A57, Th1
.= s2 . (DataLoc (((Comput (P1,s1,4)) . GBP),1)) by A57, Th1 ;

per cases ( b = DataLoc (((Comput (P1,s1,4)) . SBP),(4 + RetSP)) or b <> DataLoc (((Comput (P1,s1,4)) . SBP),(4 + RetSP)) ) ;

suppose A105: b = DataLoc (((Comput (P1,s1,4)) . SBP),(4 + RetSP)) ; :: thesis: (Comput (P1,s1,5)) . b₁ = (Comput (P2,s2,5)) . b₁

then A106: b = DataLoc (((Comput (P2,s2,4)) . SBP),(4 + RetSP)) by A8, A96;
thus (Comput (P1,s1,5)) . b = (Comput (P1,s1,4)) . (DataLoc (((Comput (P1,s1,4)) . GBP),1)) by A54, A105, SCMPDS_2:47
.= (Comput (P2,s2,4)) . (DataLoc (((Comput (P1,s1,4)) . GBP),1)) by A96, A104
.= (Comput (P2,s2,4)) . (DataLoc (((Comput (P2,s2,4)) . GBP),1)) by A5, A9, A96
.= (Comput (P2,s2,5)) . b by A61, A106, SCMPDS_2:47 ; :: thesis: verum

end;

suppose A107: b <> DataLoc (((Comput (P1,s1,4)) . SBP),(4 + RetSP)) ; :: thesis: (Comput (P1,s1,5)) . b₁ = (Comput (P2,s2,5)) . b₁

then A108: b <> DataLoc (((Comput (P2,s2,4)) . SBP),(4 + RetSP)) by A8, A96;
thus (Comput (P1,s1,5)) . b = (Comput (P1,s1,4)) . b by A54, A107, SCMPDS_2:47
.= (Comput (P2,s2,4)) . b by A96, A103
.= (Comput (P2,s2,5)) . b by A61, A108, SCMPDS_2:47 ; :: thesis: verum

end;

end;

end;

A109: now :: thesis: for b being Int_position st s1 . b = s2 . b holds
(Comput (P1,s1,6)) . b = (Comput (P2,s2,6)) . b

let b be Int_position; :: thesis: ( s1 . b = s2 . b implies (Comput (P1,s1,6)) . b₁ = (Comput (P2,s2,6)) . b₁ )
assume A110: s1 . b = s2 . b ; :: thesis: (Comput (P1,s1,6)) . b₁ = (Comput (P2,s2,6)) . b₁
A111: s1 . (DataLoc (((Comput (P1,s1,5)) . GBP),1)) = s2 . (intpos (0 + 1)) by A8, A66, Th1
.= s2 . (DataLoc (((Comput (P1,s1,5)) . GBP),1)) by A66, Th1 ;

per cases ( b = DataLoc (((Comput (P1,s1,5)) . GBP),1) or b <> DataLoc (((Comput (P1,s1,5)) . GBP),1) ) ;

suppose A112: b = DataLoc (((Comput (P1,s1,5)) . GBP),1) ; :: thesis: (Comput (P1,s1,6)) . b₁ = (Comput (P2,s2,6)) . b₁

then A113: b = DataLoc (((Comput (P2,s2,5)) . GBP),1) by A5, A9, A102;
thus (Comput (P1,s1,6)) . b = ((Comput (P1,s1,5)) . (DataLoc (((Comput (P1,s1,5)) . GBP),1))) + 4 by A65, A112, SCMPDS_2:48
.= ((Comput (P2,s2,5)) . (DataLoc (((Comput (P1,s1,5)) . GBP),1))) + 4 by A102, A111
.= ((Comput (P2,s2,5)) . (DataLoc (((Comput (P2,s2,5)) . GBP),1))) + 4 by A5, A9, A102
.= (Comput (P2,s2,6)) . b by A70, A113, SCMPDS_2:48 ; :: thesis: verum

end;

suppose A114: b <> DataLoc (((Comput (P1,s1,5)) . GBP),1) ; :: thesis: (Comput (P1,s1,6)) . b₁ = (Comput (P2,s2,6)) . b₁

then A115: b <> DataLoc (((Comput (P2,s2,5)) . GBP),1) by A5, A9, A102;
thus (Comput (P1,s1,6)) . b = (Comput (P1,s1,5)) . b by A65, A114, SCMPDS_2:48
.= (Comput (P2,s2,5)) . b by A102, A110
.= (Comput (P2,s2,6)) . b by A70, A115, SCMPDS_2:48 ; :: thesis: verum

end;

end;

end;

A116: now :: thesis: for b being Int_position st s1 . b = s2 . b holds
(Comput (P1,s1,7)) . b = (Comput (P2,s2,7)) . b

let b be Int_position; :: thesis: ( s1 . b = s2 . b implies (Comput (P1,s1,7)) . b₁ = (Comput (P2,s2,7)) . b₁ )
assume A117: s1 . b = s2 . b ; :: thesis: (Comput (P1,s1,7)) . b₁ = (Comput (P2,s2,7)) . b₁

per cases ( b = DataLoc (((Comput (P1,s1,6)) . SBP),RetIC) or b <> DataLoc (((Comput (P1,s1,6)) . SBP),RetIC) ) ;

suppose A118: b = DataLoc (((Comput (P1,s1,6)) . SBP),RetIC) ; :: thesis: (Comput (P1,s1,7)) . b₁ = (Comput (P2,s2,7)) . b₁

then A119: b = DataLoc (((Comput (P2,s2,6)) . SBP),RetIC) by A8, A109;
thus (Comput (P1,s1,7)) . b = IC (Comput (P1,s1,6)) by A74, A118, SCMPDS_2:59
.= (Comput (P2,s2,7)) . b by A72, A76, A78, A119, SCMPDS_2:59 ; :: thesis: verum

end;

suppose A120: b <> DataLoc (((Comput (P1,s1,6)) . SBP),RetIC) ; :: thesis: (Comput (P1,s1,7)) . b₁ = (Comput (P2,s2,7)) . b₁

then A121: b <> DataLoc (((Comput (P2,s2,6)) . SBP),RetIC) by A8, A109;
thus (Comput (P1,s1,7)) . b = (Comput (P1,s1,6)) . b by A74, A120, SCMPDS_2:59
.= (Comput (P2,s2,6)) . b by A109, A117
.= (Comput (P2,s2,7)) . b by A78, A121, SCMPDS_2:59 ; :: thesis: verum

end;

end;

end;

hereby :: thesis: verum

let k be Nat; :: thesis: for a being Int_position st k <= 7 & s1 . a = s2 . a holds
( IC (Comput (P1,s1,b₂)) = IC (Comput (P2,s2,b₂)) & (Comput (P1,s1,b₂)) . b₃ = (Comput (P2,s2,b₂)) . b₃ )
let a be Int_position; :: thesis: ( k <= 7 & s1 . a = s2 . a implies ( IC (Comput (P1,s1,b₁)) = IC (Comput (P2,s2,b₁)) & (Comput (P1,s1,b₁)) . b₂ = (Comput (P2,s2,b₁)) . b₂ ) )
assume that
A122: k <= 7 and
A123: s1 . a = s2 . a ; :: thesis: ( IC (Comput (P1,s1,b₁)) = IC (Comput (P2,s2,b₁)) & (Comput (P1,s1,b₁)) . b₂ = (Comput (P2,s2,b₁)) . b₂ )
not not k = 0 & ... & not k = 7 by A122;

per cases then ( k = 0 or k = 1 or k = 2 or k = 3 or k = 4 or k = 5 or k = 6 or k = 7 ) ;

suppose A124: k = 0 ; :: thesis: ( IC (Comput (P1,s1,b₁)) = IC (Comput (P2,s2,b₁)) & (Comput (P1,s1,b₁)) . b₂ = (Comput (P2,s2,b₁)) . b₂ )

hence IC (Comput (P1,s1,k)) = IC s1 by EXTPRO_1:2
.= IC (Comput (P2,s2,k)) by A7, A124, EXTPRO_1:2 ;
:: thesis: (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
thus (Comput (P1,s1,k)) . a = s1 . a by A124, EXTPRO_1:2
.= (Comput (P2,s2,k)) . a by A123, A124, EXTPRO_1:2 ; :: thesis: verum

end;

suppose A125: k = 1 ; :: thesis: ( IC (Comput (P1,s1,b₁)) = IC (Comput (P2,s2,b₁)) & (Comput (P1,s1,b₁)) . b₂ = (Comput (P2,s2,b₁)) . b₂ )

hence IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) by A17, A23; :: thesis: (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
thus (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a by A79, A123, A125; :: thesis: verum

end;

suppose A126: k = 2 ; :: thesis: ( IC (Comput (P1,s1,b₁)) = IC (Comput (P2,s2,b₁)) & (Comput (P1,s1,b₁)) . b₂ = (Comput (P2,s2,b₁)) . b₂ )

hence IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) by A27, A34; :: thesis: (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
thus (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a by A80, A123, A126; :: thesis: verum

end;

suppose A127: k = 3 ; :: thesis: ( IC (Comput (P1,s1,b₁)) = IC (Comput (P2,s2,b₁)) & (Comput (P1,s1,b₁)) . b₂ = (Comput (P2,s2,b₁)) . b₂ )

hence IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) by A38, A48; :: thesis: (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
thus (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a by A86, A123, A127; :: thesis: verum

end;

suppose A128: k = 4 ; :: thesis: ( IC (Comput (P1,s1,b₁)) = IC (Comput (P2,s2,b₁)) & (Comput (P1,s1,b₁)) . b₂ = (Comput (P2,s2,b₁)) . b₂ )

hence IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) by A52, A59; :: thesis: (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
thus (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a by A96, A123, A128; :: thesis: verum

end;

suppose A129: k = 5 ; :: thesis: ( IC (Comput (P1,s1,b₁)) = IC (Comput (P2,s2,b₁)) & (Comput (P1,s1,b₁)) . b₂ = (Comput (P2,s2,b₁)) . b₂ )

hence IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) by A63, A68; :: thesis: (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
thus (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a by A102, A123, A129; :: thesis: verum

end;

suppose A130: k = 6 ; :: thesis: ( IC (Comput (P1,s1,b₁)) = IC (Comput (P2,s2,b₁)) & (Comput (P1,s1,b₁)) . b₂ = (Comput (P2,s2,b₁)) . b₂ )

hence IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) by A72, A76; :: thesis: (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
thus (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a by A109, A123, A130; :: thesis: verum

end;

suppose A131: k = 7 ; :: thesis: ( IC (Comput (P1,s1,b₁)) = IC (Comput (P2,s2,b₁)) & (Comput (P1,s1,b₁)) . b₂ = (Comput (P2,s2,b₁)) . b₂ )

hence IC (Comput (P1,s1,k)) = (IC (Comput (P2,s2,6))) + 1 by A72, A74, A76, SCMPDS_2:59
.= IC (Comput (P2,s2,k)) by A78, A131, SCMPDS_2:59 ;
:: thesis: (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
thus (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a by A116, A123, A131; :: thesis: verum

end;

end;

end;