let n be Element of 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 Element of 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 Element of 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 Element of 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
A3: GCD-Algorithm c= P1 and
A4: 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 Element of 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: 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 Element of 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: 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 Element of 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 A7: 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 Element of 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 A8: 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 Element of 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
A9: IC s2 = IC s1 and
A10: s2 . SBP = s1 . SBP and
A11: 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 Element of 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
A12: s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) and
A13: s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) ; :: thesis: for k being Element of 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 )
A14: P1 /. (IC s1) = P1 . (IC s1) by PBOOLE:143;
A15: 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 A14, A5, Lm1, A3 ;
A16: P2 /. (IC s2) = P2 . (IC s2) by PBOOLE:143;
A17: 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 A5, A9, Lm1, A16, A4 ;
A18: P1 /. (IC (Comput (P1,s1,1))) = P1 . (IC (Comput (P1,s1,1))) by PBOOLE:143;
A19: IC (Comput (P1,s1,1)) = succ (IC s1) by A8, A15, SCMPDS_2:56
.= 5 + 1 by A5 ;
then A20: CurInstr (P1,(Comput (P1,s1,1))) = P1 . 6 by A18
.= (SBP,6) := (SBP,3) by Lm1, A3 ;
A22: 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 A20 ;
A23: (Comput (P1,s1,1)) . SBP = n by A6, A15, SCMPDS_2:56;
A24: (Comput (P1,s1,1)) . GBP = 0 by A7, A15, SCMPDS_2:56;
A25: P2 /. (IC (Comput (P2,s2,1))) = P2 . (IC (Comput (P2,s2,1))) by PBOOLE:143;
A26: IC (Comput (P2,s2,1)) = succ (IC s2) by A8, A10, A13, A17, SCMPDS_2:56
.= 5 + 1 by A5, A9 ;
then A27: CurInstr (P2,(Comput (P2,s2,1))) = P2 . 6 by A25
.= (SBP,6) := (SBP,3) by Lm1, A4 ;
A29: 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 A27 ;
A30: P1 /. (IC (Comput (P1,s1,2))) = P1 . (IC (Comput (P1,s1,2))) by PBOOLE:143;
A31: IC (Comput (P1,s1,2)) = succ (IC (Comput (P1,s1,1))) by A22, SCMPDS_2:47
.= 6 + 1 by A19 ;
then A32: CurInstr (P1,(Comput (P1,s1,2))) = P1 . 7 by A30
.= Divide (SBP,2,SBP,3) by Lm1, A3 ;
A34: 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 A32 ;
A35: DataLoc (((Comput (P1,s1,1)) . SBP),6) = intpos (n + 6) by A23, Th5;
then A36: (Comput (P1,s1,2)) . SBP = n by A22, A23, Lm3, SCMPDS_2:47;
A37: (Comput (P1,s1,2)) . GBP = 0 by A22, A24, A35, Lm2, SCMPDS_2:47;
A38: P2 /. (IC (Comput (P2,s2,2))) = P2 . (IC (Comput (P2,s2,2))) by PBOOLE:143;
A39: IC (Comput (P2,s2,2)) = succ (IC (Comput (P2,s2,1))) by A29, SCMPDS_2:47
.= 6 + 1 by A26 ;
then A40: CurInstr (P2,(Comput (P2,s2,2))) = P2 . 7 by A38
.= Divide (SBP,2,SBP,3) by Lm1, A4 ;
A42: 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 A40 ;
A43: P1 /. (IC (Comput (P1,s1,3))) = P1 . (IC (Comput (P1,s1,3))) by PBOOLE:143;
A44: IC (Comput (P1,s1,3)) = succ (IC (Comput (P1,s1,2))) by A34, SCMPDS_2:52
.= 7 + 1 by A31 ;
then A45: CurInstr (P1,(Comput (P1,s1,3))) = P1 . 8 by A43
.= (SBP,7) := (SBP,3) by Lm1, A3 ;
A47: 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 A45 ;
A48: DataLoc (((Comput (P1,s1,2)) . SBP),2) = intpos (n + 2) by A36, Th5;
then A49: SBP <> DataLoc (((Comput (P1,s1,2)) . SBP),2) by Lm3;
A50: DataLoc (((Comput (P1,s1,2)) . SBP),3) = intpos (n + 3) by A36, Th5;
then SBP <> DataLoc (((Comput (P1,s1,2)) . SBP),3) by Lm3;
then A51: (Comput (P1,s1,3)) . SBP = n by A34, A36, A49, SCMPDS_2:52;
A52: GBP <> DataLoc (((Comput (P1,s1,2)) . SBP),2) by A48, Lm2;
GBP <> DataLoc (((Comput (P1,s1,2)) . SBP),3) by A50, Lm2;
then A53: (Comput (P1,s1,3)) . GBP = 0 by A34, A37, A52, SCMPDS_2:52;
A54: P2 /. (IC (Comput (P2,s2,3))) = P2 . (IC (Comput (P2,s2,3))) by PBOOLE:143;
A55: IC (Comput (P2,s2,3)) = succ (IC (Comput (P2,s2,2))) by A42, SCMPDS_2:52
.= 7 + 1 by A39 ;
then A56: CurInstr (P2,(Comput (P2,s2,3))) = P2 . 8 by A54
.= (SBP,7) := (SBP,3) by Lm1, A4 ;
A58: 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 A56 ;
A59: P1 /. (IC (Comput (P1,s1,4))) = P1 . (IC (Comput (P1,s1,4))) by PBOOLE:143;
A60: IC (Comput (P1,s1,4)) = succ (IC (Comput (P1,s1,3))) by A47, SCMPDS_2:47
.= 8 + 1 by A44 ;
then A61: CurInstr (P1,(Comput (P1,s1,4))) = P1 . 9 by A59
.= (SBP,(4 + RetSP)) := (GBP,1) by Lm1, A3 ;
A63: 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 A61 ;
A64: DataLoc (((Comput (P1,s1,3)) . SBP),7) = intpos (n + 7) by A51, Th5;
then A65: (Comput (P1,s1,4)) . SBP = n by A47, A51, Lm3, SCMPDS_2:47;
A66: (Comput (P1,s1,4)) . GBP = 0 by A47, A53, A64, Lm2, SCMPDS_2:47;
A67: P2 /. (IC (Comput (P2,s2,4))) = P2 . (IC (Comput (P2,s2,4))) by PBOOLE:143;
A68: IC (Comput (P2,s2,4)) = succ (IC (Comput (P2,s2,3))) by A58, SCMPDS_2:47
.= 8 + 1 by A55 ;
then A69: CurInstr (P2,(Comput (P2,s2,4))) = P2 . 9 by A67
.= (SBP,(4 + RetSP)) := (GBP,1) by Lm1, A4 ;
A71: 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 A69 ;
A72: P1 /. (IC (Comput (P1,s1,5))) = P1 . (IC (Comput (P1,s1,5))) by PBOOLE:143;
A73: IC (Comput (P1,s1,5)) = succ (IC (Comput (P1,s1,4))) by A63, SCMPDS_2:47
.= 9 + 1 by A60 ;
then A74: CurInstr (P1,(Comput (P1,s1,5))) = P1 . 10 by A72
.= AddTo (GBP,1,4) by Lm1, A3 ;
A76: 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 A74 ;
DataLoc (((Comput (P1,s1,4)) . SBP),(4 + RetSP)) = intpos (n + (4 + 0)) by A65, Th5, SCMPDS_1:def 20;
then A77: (Comput (P1,s1,5)) . GBP = 0 by A63, A66, Lm2, SCMPDS_2:47;
A78: P2 /. (IC (Comput (P2,s2,5))) = P2 . (IC (Comput (P2,s2,5))) by PBOOLE:143;
A79: IC (Comput (P2,s2,5)) = succ (IC (Comput (P2,s2,4))) by A71, SCMPDS_2:47
.= 9 + 1 by A68 ;
then A80: CurInstr (P2,(Comput (P2,s2,5))) = P2 . 10 by A78
.= AddTo (GBP,1,4) by Lm1, A4 ;
A82: 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 A80 ;
A83: P1 /. (IC (Comput (P1,s1,6))) = P1 . (IC (Comput (P1,s1,6))) by PBOOLE:143;
A84: IC (Comput (P1,s1,6)) = succ (IC (Comput (P1,s1,5))) by A76, SCMPDS_2:48
.= 10 + 1 by A73 ;
then A85: CurInstr (P1,(Comput (P1,s1,6))) = P1 . 11 by A83
.= saveIC (SBP,RetIC) by Lm1, A3 ;
A87: Comput (P1,s1,(6 + 1)) = Following (P1,(Comput (P1,s1,6))) by EXTPRO_1:3
.= Exec ((saveIC (SBP,RetIC)),(Comput (P1,s1,6))) by A85 ;
A88: P2 /. (IC (Comput (P2,s2,6))) = P2 . (IC (Comput (P2,s2,6))) by PBOOLE:143;
A89: IC (Comput (P2,s2,6)) = succ (IC (Comput (P2,s2,5))) by A82, SCMPDS_2:48
.= 10 + 1 by A79 ;
then A90: CurInstr (P2,(Comput (P2,s2,6))) = P2 . 11 by A88
.= saveIC (SBP,RetIC) by Lm1, A4 ;
A92: Comput (P2,s2,(6 + 1)) = Following (P2,(Comput (P2,s2,6))) by EXTPRO_1:3
.= Exec ((saveIC (SBP,RetIC)),(Comput (P2,s2,6))) by A90 ;

A93: now

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 A15, SCMPDS_2:56
.= (Comput (P2,s2,1)) . b by A17, SCMPDS_2:56 ;
:: thesis: verum

end;

A94: 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 A95: 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 A96: b = DataLoc (((Comput (P1,s1,1)) . SBP),6) ; :: thesis: (Comput (P1,s1,2)) . b = (Comput (P2,s2,2)) . b

then A97: b = DataLoc (((Comput (P2,s2,1)) . SBP),6) by A10, A93;
thus (Comput (P1,s1,2)) . b = (Comput (P1,s1,1)) . (DataLoc ((s1 . SBP),3)) by A6, A22, A23, A96, SCMPDS_2:47
.= (Comput (P2,s2,1)) . (DataLoc (((Comput (P1,s1,1)) . SBP),3)) by A6, A13, A23, A93
.= (Comput (P2,s2,1)) . (DataLoc (((Comput (P2,s2,1)) . SBP),3)) by A10, A93
.= (Comput (P2,s2,2)) . b by A29, A97, SCMPDS_2:47 ; :: thesis: verum

end;

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

then A99: b <> DataLoc (((Comput (P2,s2,1)) . SBP),6) by A10, A93;
thus (Comput (P1,s1,2)) . b = (Comput (P1,s1,1)) . b by A22, A98, SCMPDS_2:47
.= (Comput (P2,s2,1)) . b by A93, A95
.= (Comput (P2,s2,2)) . b by A29, A99, SCMPDS_2:47 ; :: thesis: verum

end;

end;

end;

A100: now

let b be Int_position ; :: thesis: ( s1 . b = s2 . b implies (Comput (P1,s1,3)) . b₁ = (Comput (P2,s2,3)) . b₁ )
assume A101: 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);
A102: DataLoc (((Comput (P1,s1,2)) . SBP),2) = DataLoc (((Comput (P2,s2,2)) . SBP),2) by A10, A94;
A103: DataLoc (((Comput (P1,s1,2)) . SBP),3) = DataLoc (((Comput (P2,s2,2)) . SBP),3) by A10, A94;

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 A104: ( 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 A34, SCMPDS_2:52
.= (Comput (P2,s2,2)) . b by A94, A101
.= (Comput (P2,s2,3)) . b by A42, A102, A103, A104, SCMPDS_2:52 ;
:: thesis: verum

end;

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

A106: n + 2 <> n + 3 ;
then A107: DataLoc (((Comput (P1,s1,2)) . SBP),2) <> DataLoc (((Comput (P1,s1,2)) . SBP),3) by A48, A50, AMI_3:10;
A108: DataLoc (((Comput (P2,s2,2)) . SBP),2) <> DataLoc (((Comput (P2,s2,2)) . SBP),3) by A48, A50, A102, A103, A106, 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 A34, A105, A107, 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 A6, A12, A36, A94
.= ((Comput (P2,s2,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),2))) div ((Comput (P2,s2,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),3))) by A6, A13, A36, A94
.= (Comput (P2,s2,3)) . b by A42, A102, A103, A105, A108, SCMPDS_2:52 ; :: thesis: verum

end;

suppose A109: 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 A34, 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 A6, A12, A36, A94
.= ((Comput (P2,s2,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),2))) mod ((Comput (P2,s2,2)) . (DataLoc (((Comput (P1,s1,2)) . SBP),3))) by A6, A13, A36, A94
.= (Comput (P2,s2,3)) . b by A42, A102, A103, A109, SCMPDS_2:52 ;
:: thesis: verum

end;

end;

end;

A110: now

let b be Int_position ; :: thesis: ( s1 . b = s2 . b implies (Comput (P1,s1,4)) . b₁ = (Comput (P2,s2,4)) . b₁ )
assume A111: 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 A112: b = DataLoc (((Comput (P1,s1,3)) . SBP),7) ; :: thesis: (Comput (P1,s1,4)) . b₁ = (Comput (P2,s2,4)) . b₁

then A113: b = DataLoc (((Comput (P2,s2,3)) . SBP),7) by A10, A100;
thus (Comput (P1,s1,4)) . b = (Comput (P1,s1,3)) . (DataLoc (((Comput (P1,s1,3)) . SBP),3)) by A47, A112, SCMPDS_2:47
.= (Comput (P2,s2,3)) . (DataLoc (((Comput (P1,s1,3)) . SBP),3)) by A6, A13, A51, A100
.= (Comput (P2,s2,3)) . (DataLoc (((Comput (P2,s2,3)) . SBP),3)) by A10, A100
.= (Comput (P2,s2,4)) . b by A58, A113, SCMPDS_2:47 ; :: thesis: verum

end;

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

then A115: b <> DataLoc (((Comput (P2,s2,3)) . SBP),7) by A10, A100;
thus (Comput (P1,s1,4)) . b = (Comput (P1,s1,3)) . b by A47, A114, SCMPDS_2:47
.= (Comput (P2,s2,3)) . b by A100, A111
.= (Comput (P2,s2,4)) . b by A58, A115, SCMPDS_2:47 ; :: thesis: verum

end;

end;

end;

A116: now

let b be Int_position ; :: thesis: ( s1 . b = s2 . b implies (Comput (P1,s1,5)) . b₁ = (Comput (P2,s2,5)) . b₁ )
assume A117: s1 . b = s2 . b ; :: thesis: (Comput (P1,s1,5)) . b₁ = (Comput (P2,s2,5)) . b₁
A118: s1 . (DataLoc (((Comput (P1,s1,4)) . GBP),1)) = s2 . (intpos (0 + 1)) by A10, A66, Th5
.= s2 . (DataLoc (((Comput (P1,s1,4)) . GBP),1)) by A66, Th5 ;

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

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

then A120: b = DataLoc (((Comput (P2,s2,4)) . SBP),(4 + RetSP)) by A10, A110;
thus (Comput (P1,s1,5)) . b = (Comput (P1,s1,4)) . (DataLoc (((Comput (P1,s1,4)) . GBP),1)) by A63, A119, SCMPDS_2:47
.= (Comput (P2,s2,4)) . (DataLoc (((Comput (P1,s1,4)) . GBP),1)) by A110, A118
.= (Comput (P2,s2,4)) . (DataLoc (((Comput (P2,s2,4)) . GBP),1)) by A7, A11, A110
.= (Comput (P2,s2,5)) . b by A71, A120, SCMPDS_2:47 ; :: thesis: verum

end;

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

then A122: b <> DataLoc (((Comput (P2,s2,4)) . SBP),(4 + RetSP)) by A10, A110;
thus (Comput (P1,s1,5)) . b = (Comput (P1,s1,4)) . b by A63, A121, SCMPDS_2:47
.= (Comput (P2,s2,4)) . b by A110, A117
.= (Comput (P2,s2,5)) . b by A71, A122, SCMPDS_2:47 ; :: thesis: verum

end;

end;

end;

A123: now

let b be Int_position ; :: thesis: ( s1 . b = s2 . b implies (Comput (P1,s1,6)) . b₁ = (Comput (P2,s2,6)) . b₁ )
assume A124: s1 . b = s2 . b ; :: thesis: (Comput (P1,s1,6)) . b₁ = (Comput (P2,s2,6)) . b₁
A125: s1 . (DataLoc (((Comput (P1,s1,5)) . GBP),1)) = s2 . (intpos (0 + 1)) by A10, A77, Th5
.= s2 . (DataLoc (((Comput (P1,s1,5)) . GBP),1)) by A77, Th5 ;

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

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

then A127: b = DataLoc (((Comput (P2,s2,5)) . GBP),1) by A7, A11, A116;
thus (Comput (P1,s1,6)) . b = ((Comput (P1,s1,5)) . (DataLoc (((Comput (P1,s1,5)) . GBP),1))) + 4 by A76, A126, SCMPDS_2:48
.= ((Comput (P2,s2,5)) . (DataLoc (((Comput (P1,s1,5)) . GBP),1))) + 4 by A116, A125
.= ((Comput (P2,s2,5)) . (DataLoc (((Comput (P2,s2,5)) . GBP),1))) + 4 by A7, A11, A116
.= (Comput (P2,s2,6)) . b by A82, A127, SCMPDS_2:48 ; :: thesis: verum

end;

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

then A129: b <> DataLoc (((Comput (P2,s2,5)) . GBP),1) by A7, A11, A116;
thus (Comput (P1,s1,6)) . b = (Comput (P1,s1,5)) . b by A76, A128, SCMPDS_2:48
.= (Comput (P2,s2,5)) . b by A116, A124
.= (Comput (P2,s2,6)) . b by A82, A129, SCMPDS_2:48 ; :: thesis: verum

end;

end;

end;

A130: now

let b be Int_position ; :: thesis: ( s1 . b = s2 . b implies (Comput (P1,s1,7)) . b₁ = (Comput (P2,s2,7)) . b₁ )
assume A131: 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 A132: b = DataLoc (((Comput (P1,s1,6)) . SBP),RetIC) ; :: thesis: (Comput (P1,s1,7)) . b₁ = (Comput (P2,s2,7)) . b₁

then A133: b = DataLoc (((Comput (P2,s2,6)) . SBP),RetIC) by A10, A123;
thus (Comput (P1,s1,7)) . b = IC (Comput (P1,s1,6)) by A87, A132, SCMPDS_2:59
.= (Comput (P2,s2,7)) . b by A84, A89, A92, A133, SCMPDS_2:59 ; :: thesis: verum

end;

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

then A135: b <> DataLoc (((Comput (P2,s2,6)) . SBP),RetIC) by A10, A123;
thus (Comput (P1,s1,7)) . b = (Comput (P1,s1,6)) . b by A87, A134, SCMPDS_2:59
.= (Comput (P2,s2,6)) . b by A123, A131
.= (Comput (P2,s2,7)) . b by A92, A135, SCMPDS_2:59 ; :: thesis: verum

end;

end;

end;

hereby :: thesis: verum

let k be Element of 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
A136: k <= 7 and
A137: 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₂ )

per cases ( k = 0 or k = 1 or k = 2 or k = 3 or k = 4 or k = 5 or k = 6 or k = 7 ) by A136, NAT_1:31;

suppose A138: 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 A9, A138, EXTPRO_1:2 ;
:: thesis: (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
thus (Comput (P1,s1,k)) . a = s1 . a by A138, EXTPRO_1:2
.= (Comput (P2,s2,k)) . a by A137, A138, EXTPRO_1:2 ; :: thesis: verum

end;

suppose A139: 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 A19, A26; :: thesis: (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
thus (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a by A93, A137, A139; :: thesis: verum

end;

suppose A140: 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 A31, A39; :: thesis: (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
thus (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a by A94, A137, A140; :: thesis: verum

end;

suppose A141: 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 A44, A55; :: thesis: (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
thus (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a by A100, A137, A141; :: thesis: verum

end;

suppose A142: 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 A60, A68; :: thesis: (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
thus (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a by A110, A137, A142; :: thesis: verum

end;

suppose A143: 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 A73, A79; :: thesis: (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
thus (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a by A116, A137, A143; :: thesis: verum

end;

suppose A144: 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 A84, A89; :: thesis: (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
thus (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a by A123, A137, A144; :: thesis: verum

end;

suppose A145: 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)) = succ (IC (Comput (P2,s2,6))) by A84, A87, A89, SCMPDS_2:59
.= IC (Comput (P2,s2,k)) by A92, A145, 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 A130, A137, A145; :: thesis: verum

end;

end;

end;