let n be Element of NAT ; :: thesis: for s1, s2 being State of SCMPDS st GCD-Algorithm c= s1 & GCD-Algorithm c= s2 & IC s1 = inspos 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 (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a )
let s1, s2 be State of SCMPDS ; :: thesis: ( GCD-Algorithm c= s1 & GCD-Algorithm c= s2 & IC s1 = inspos 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 (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a ) )
set GA = GCD-Algorithm ;
assume A1: ( GCD-Algorithm c= s1 & GCD-Algorithm c= s2 ) ; :: thesis: ( not IC s1 = inspos 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 (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a ) )
assume A2: IC s1 = inspos 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 (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a ) )
assume A3: 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 (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a ) )
assume A4: 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 (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a ) )
assume A5: 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 (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a ) )
assume A6: ( IC s2 = IC s1 & s2 . SBP = s1 . SBP & 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 (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a ) )
assume A7: ( s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) & 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 (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a )
A8: 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 A1, A2, Lm1 ;
A9: 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 A1, A2, A6, Lm1 ;
A10: IC (Computation s1,1) = Next (IC s1) by A5, A8, SCMPDS_2:68
.= inspos (5 + 1) by A2 ;
then A11: CurInstr (Computation s1,1) = s1 . (inspos 6) by AMI_1:54
.= SBP ,6 := SBP ,3 by A1, Lm1 ;
A12: Computation s1,(1 + 1) = Following (Computation s1,1) by AMI_1:14
.= Exec (SBP ,6 := SBP ,3),(Computation s1,1) by A11 ;
A13: (Computation s1,1) . SBP = n by A3, A8, SCMPDS_2:68;
A14: (Computation s1,1) . GBP = 0 by A4, A8, SCMPDS_2:68;
A15: IC (Computation s2,1) = Next (IC s2) by A5, A6, A7, A9, SCMPDS_2:68
.= inspos (5 + 1) by A2, A6 ;
then A16: CurInstr (Computation s2,1) = s2 . (inspos 6) by AMI_1:54
.= SBP ,6 := SBP ,3 by A1, Lm1 ;
A17: Computation s2,(1 + 1) = Following (Computation s2,1) by AMI_1:14
.= Exec (SBP ,6 := SBP ,3),(Computation s2,1) by A16 ;
A18: IC (Computation s1,2) = Next (IC (Computation s1,1)) by A12, SCMPDS_2:59
.= inspos (6 + 1) by A10 ;
then A19: CurInstr (Computation s1,2) = s1 . (inspos 7) by AMI_1:54
.= Divide SBP ,2,SBP ,3 by A1, Lm1 ;
A20: Computation s1,(2 + 1) = Following (Computation s1,2) by AMI_1:14
.= Exec (Divide SBP ,2,SBP ,3),(Computation s1,2) by A19 ;
A21: DataLoc ((Computation s1,1) . SBP ),6 = intpos (n + 6) by A13, Th5;
then SBP <> DataLoc ((Computation s1,1) . SBP ),6 by Lm3;
then A22: (Computation s1,2) . SBP = n by A12, A13, SCMPDS_2:59;
GBP <> DataLoc ((Computation s1,1) . SBP ),6 by A21, Lm2;
then A23: (Computation s1,2) . GBP = 0 by A12, A14, SCMPDS_2:59;
A24: IC (Computation s2,2) = Next (IC (Computation s2,1)) by A17, SCMPDS_2:59
.= inspos (6 + 1) by A15 ;
then A25: CurInstr (Computation s2,2) = s2 . (inspos 7) by AMI_1:54
.= Divide SBP ,2,SBP ,3 by A1, Lm1 ;
A26: Computation s2,(2 + 1) = Following (Computation s2,2) by AMI_1:14
.= Exec (Divide SBP ,2,SBP ,3),(Computation s2,2) by A25 ;
A27: IC (Computation s1,3) = Next (IC (Computation s1,2)) by A20, SCMPDS_2:64
.= inspos (7 + 1) by A18 ;
then A28: CurInstr (Computation s1,3) = s1 . (inspos 8) by AMI_1:54
.= SBP ,7 := SBP ,3 by A1, Lm1 ;
A29: Computation s1,(3 + 1) = Following (Computation s1,3) by AMI_1:14
.= Exec (SBP ,7 := SBP ,3),(Computation s1,3) by A28 ;
A30: DataLoc ((Computation s1,2) . SBP ),2 = intpos (n + 2) by A22, Th5;
then A31: SBP <> DataLoc ((Computation s1,2) . SBP ),2 by Lm3;
A32: DataLoc ((Computation s1,2) . SBP ),3 = intpos (n + 3) by A22, Th5;
then SBP <> DataLoc ((Computation s1,2) . SBP ),3 by Lm3;
then A33: (Computation s1,3) . SBP = n by A20, A22, A31, SCMPDS_2:64;
A34: GBP <> DataLoc ((Computation s1,2) . SBP ),2 by A30, Lm2;
GBP <> DataLoc ((Computation s1,2) . SBP ),3 by A32, Lm2;
then A35: (Computation s1,3) . GBP = 0 by A20, A23, A34, SCMPDS_2:64;
A36: IC (Computation s2,3) = Next (IC (Computation s2,2)) by A26, SCMPDS_2:64
.= inspos (7 + 1) by A24 ;
then A37: CurInstr (Computation s2,3) = s2 . (inspos 8) by AMI_1:54
.= SBP ,7 := SBP ,3 by A1, Lm1 ;
A38: Computation s2,(3 + 1) = Following (Computation s2,3) by AMI_1:14
.= Exec (SBP ,7 := SBP ,3),(Computation s2,3) by A37 ;
A39: IC (Computation s1,4) = Next (IC (Computation s1,3)) by A29, SCMPDS_2:59
.= inspos (8 + 1) by A27 ;
then A40: CurInstr (Computation s1,4) = s1 . (inspos 9) by AMI_1:54
.= SBP ,(4 + RetSP ) := GBP ,1 by A1, Lm1 ;
A41: Computation s1,(4 + 1) = Following (Computation s1,4) by AMI_1:14
.= Exec (SBP ,(4 + RetSP ) := GBP ,1),(Computation s1,4) by A40 ;
A42: DataLoc ((Computation s1,3) . SBP ),7 = intpos (n + 7) by A33, Th5;
then SBP <> DataLoc ((Computation s1,3) . SBP ),7 by Lm3;
then A43: (Computation s1,4) . SBP = n by A29, A33, SCMPDS_2:59;
GBP <> DataLoc ((Computation s1,3) . SBP ),7 by A42, Lm2;
then A44: (Computation s1,4) . GBP = 0 by A29, A35, SCMPDS_2:59;
A45: IC (Computation s2,4) = Next (IC (Computation s2,3)) by A38, SCMPDS_2:59
.= inspos (8 + 1) by A36 ;
then A46: CurInstr (Computation s2,4) = s2 . (inspos 9) by AMI_1:54
.= SBP ,(4 + RetSP ) := GBP ,1 by A1, Lm1 ;
A47: Computation s2,(4 + 1) = Following (Computation s2,4) by AMI_1:14
.= Exec (SBP ,(4 + RetSP ) := GBP ,1),(Computation s2,4) by A46 ;
A48: IC (Computation s1,5) = Next (IC (Computation s1,4)) by A41, SCMPDS_2:59
.= inspos (9 + 1) by A39 ;
then A49: CurInstr (Computation s1,5) = s1 . (inspos 10) by AMI_1:54
.= AddTo GBP ,1,4 by A1, Lm1 ;
A50: Computation s1,(5 + 1) = Following (Computation s1,5) by AMI_1:14
.= Exec (AddTo GBP ,1,4),(Computation s1,5) by A49 ;
DataLoc ((Computation s1,4) . SBP ),(4 + RetSP ) = intpos (n + (4 + 0 )) by A43, Th5, SCMPDS_1:def 22;
then GBP <> DataLoc ((Computation s1,4) . SBP ),(4 + RetSP ) by Lm2;
then A51: (Computation s1,5) . GBP = 0 by A41, A44, SCMPDS_2:59;
A52: IC (Computation s2,5) = Next (IC (Computation s2,4)) by A47, SCMPDS_2:59
.= inspos (9 + 1) by A45 ;
then A53: CurInstr (Computation s2,5) = s2 . (inspos 10) by AMI_1:54
.= AddTo GBP ,1,4 by A1, Lm1 ;
A54: Computation s2,(5 + 1) = Following (Computation s2,5) by AMI_1:14
.= Exec (AddTo GBP ,1,4),(Computation s2,5) by A53 ;
A55: IC (Computation s1,6) = Next (IC (Computation s1,5)) by A50, SCMPDS_2:60
.= inspos (10 + 1) by A48 ;
then A56: CurInstr (Computation s1,6) = s1 . (inspos 11) by AMI_1:54
.= saveIC SBP ,RetIC by A1, Lm1 ;
A57: Computation s1,(6 + 1) = Following (Computation s1,6) by AMI_1:14
.= Exec (saveIC SBP ,RetIC ),(Computation s1,6) by A56 ;
A58: IC (Computation s2,6) = Next (IC (Computation s2,5)) by A54, SCMPDS_2:60
.= inspos (10 + 1) by A52 ;
then A59: CurInstr (Computation s2,6) = s2 . (inspos 11) by AMI_1:54
.= saveIC SBP ,RetIC by A1, Lm1 ;
A60: Computation s2,(6 + 1) = Following (Computation s2,6) by AMI_1:14
.= Exec (saveIC SBP ,RetIC ),(Computation s2,6) by A59 ;

A61: now

let b be Int_position ; :: thesis: ( s1 . b = s2 . b implies (Computation s1,1) . b = (Computation s2,1) . b )
assume s1 . b = s2 . b ; :: thesis: (Computation s1,1) . b = (Computation s2,1) . b
hence (Computation s1,1) . b = s2 . b by A8, SCMPDS_2:68
.= (Computation s2,1) . b by A9, SCMPDS_2:68 ;
:: thesis: verum

end;

A62: 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: ( s1 . b = s2 . b implies (Computation s1,2) . b = (Computation s2,2) . b )
assume A63: s1 . b = s2 . b ; :: thesis: (Computation s1,2) . b = (Computation s2,2) . b

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

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

then A65: b = DataLoc ((Computation s2,1) . SBP ),6 by A6, A61;
thus (Computation s1,2) . b = (Computation s1,1) . (DataLoc (s1 . SBP ),3) by A3, A12, A13, A64, SCMPDS_2:59
.= (Computation s2,1) . (DataLoc ((Computation s1,1) . SBP ),3) by A3, A7, A13, A61
.= (Computation s2,1) . (DataLoc ((Computation s2,1) . SBP ),3) by A6, A61
.= (Computation s2,2) . b by A17, A65, SCMPDS_2:59 ; :: thesis: verum

end;

suppose A66: b <> DataLoc ((Computation s1,1) . SBP ),6 ; :: thesis: (Computation s1,2) . b = (Computation s2,2) . b

then A67: b <> DataLoc ((Computation s2,1) . SBP ),6 by A6, A61;
thus (Computation s1,2) . b = (Computation s1,1) . b by A12, A66, SCMPDS_2:59
.= (Computation s2,1) . b by A61, A63
.= (Computation s2,2) . b by A17, A67, SCMPDS_2:59 ; :: thesis: verum

end;

end;

end;

A68: now

let b be Int_position ; :: thesis: ( s1 . b = s2 . b implies (Computation s1,3) . b₁ = (Computation s2,3) . b₁ )
assume A69: s1 . b = s2 . b ; :: thesis: (Computation s1,3) . b₁ = (Computation s2,3) . b₁
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;
A70: DataLoc ((Computation s1,2) . SBP ),2 = DataLoc ((Computation s2,2) . SBP ),2 by A6, A62;
A71: DataLoc ((Computation s1,2) . SBP ),3 = DataLoc ((Computation s2,2) . SBP ),3 by A6, A62;

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

suppose A72: ( b <> DataLoc ((Computation s1,2) . SBP ),2 & b <> DataLoc ((Computation s1,2) . SBP ),3 ) ; :: thesis: (Computation s1,3) . b₁ = (Computation s2,3) . b₁

hence (Computation s1,3) . b = (Computation s1,2) . b by A20, SCMPDS_2:64
.= (Computation s2,2) . b by A62, A69
.= (Computation s2,3) . b by A26, A70, A71, A72, SCMPDS_2:64 ;
:: thesis: verum

end;

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

A74: n + 2 <> n + 3 ;
then A75: DataLoc ((Computation s1,2) . SBP ),2 <> DataLoc ((Computation s1,2) . SBP ),3 by A30, A32, AMI_3:52;
A76: DataLoc ((Computation s2,2) . SBP ),2 <> DataLoc ((Computation s2,2) . SBP ),3 by A30, A32, A70, A71, A74, AMI_3:52;
thus (Computation s1,3) . b = ((Computation s1,2) . (DataLoc ((Computation s1,2) . SBP ),2)) div ((Computation s1,2) . (DataLoc ((Computation s1,2) . SBP ),3)) by A20, A73, A75, SCMPDS_2:64
.= ((Computation s2,2) . (DataLoc ((Computation s1,2) . SBP ),2)) div ((Computation s1,2) . (DataLoc ((Computation s1,2) . SBP ),3)) by A3, A7, A22, A62
.= ((Computation s2,2) . (DataLoc ((Computation s1,2) . SBP ),2)) div ((Computation s2,2) . (DataLoc ((Computation s1,2) . SBP ),3)) by A3, A7, A22, A62
.= (Computation s2,3) . b by A26, A70, A71, A73, A76, SCMPDS_2:64 ; :: thesis: verum

end;

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

hence (Computation s1,3) . b = ((Computation s1,2) . (DataLoc ((Computation s1,2) . SBP ),2)) mod ((Computation s1,2) . (DataLoc ((Computation s1,2) . SBP ),3)) by A20, SCMPDS_2:64
.= ((Computation s2,2) . (DataLoc ((Computation s1,2) . SBP ),2)) mod ((Computation s1,2) . (DataLoc ((Computation s1,2) . SBP ),3)) by A3, A7, A22, A62
.= ((Computation s2,2) . (DataLoc ((Computation s1,2) . SBP ),2)) mod ((Computation s2,2) . (DataLoc ((Computation s1,2) . SBP ),3)) by A3, A7, A22, A62
.= (Computation s2,3) . b by A26, A70, A71, A77, SCMPDS_2:64 ;
:: thesis: verum

end;

end;

end;

A78: now

let b be Int_position ; :: thesis: ( s1 . b = s2 . b implies (Computation s1,4) . b₁ = (Computation s2,4) . b₁ )
assume A79: s1 . b = s2 . b ; :: thesis: (Computation s1,4) . b₁ = (Computation s2,4) . b₁

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

suppose A80: b = DataLoc ((Computation s1,3) . SBP ),7 ; :: thesis: (Computation s1,4) . b₁ = (Computation s2,4) . b₁

then A81: b = DataLoc ((Computation s2,3) . SBP ),7 by A6, A68;
thus (Computation s1,4) . b = (Computation s1,3) . (DataLoc ((Computation s1,3) . SBP ),3) by A29, A80, SCMPDS_2:59
.= (Computation s2,3) . (DataLoc ((Computation s1,3) . SBP ),3) by A3, A7, A33, A68
.= (Computation s2,3) . (DataLoc ((Computation s2,3) . SBP ),3) by A6, A68
.= (Computation s2,4) . b by A38, A81, SCMPDS_2:59 ; :: thesis: verum

end;

suppose A82: b <> DataLoc ((Computation s1,3) . SBP ),7 ; :: thesis: (Computation s1,4) . b₁ = (Computation s2,4) . b₁

then A83: b <> DataLoc ((Computation s2,3) . SBP ),7 by A6, A68;
thus (Computation s1,4) . b = (Computation s1,3) . b by A29, A82, SCMPDS_2:59
.= (Computation s2,3) . b by A68, A79
.= (Computation s2,4) . b by A38, A83, SCMPDS_2:59 ; :: thesis: verum

end;

end;

end;

A84: now

let b be Int_position ; :: thesis: ( s1 . b = s2 . b implies (Computation s1,5) . b₁ = (Computation s2,5) . b₁ )
assume A85: s1 . b = s2 . b ; :: thesis: (Computation s1,5) . b₁ = (Computation s2,5) . b₁
A86: s1 . (DataLoc ((Computation s1,4) . GBP ),1) = s2 . (intpos (0 + 1)) by A6, A44, Th5
.= s2 . (DataLoc ((Computation s1,4) . GBP ),1) by A44, Th5 ;

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

suppose A87: b = DataLoc ((Computation s1,4) . SBP ),(4 + RetSP ) ; :: thesis: (Computation s1,5) . b₁ = (Computation s2,5) . b₁

then A88: b = DataLoc ((Computation s2,4) . SBP ),(4 + RetSP ) by A6, A78;
thus (Computation s1,5) . b = (Computation s1,4) . (DataLoc ((Computation s1,4) . GBP ),1) by A41, A87, SCMPDS_2:59
.= (Computation s2,4) . (DataLoc ((Computation s1,4) . GBP ),1) by A78, A86
.= (Computation s2,4) . (DataLoc ((Computation s2,4) . GBP ),1) by A4, A6, A78
.= (Computation s2,5) . b by A47, A88, SCMPDS_2:59 ; :: thesis: verum

end;

suppose A89: b <> DataLoc ((Computation s1,4) . SBP ),(4 + RetSP ) ; :: thesis: (Computation s1,5) . b₁ = (Computation s2,5) . b₁

then A90: b <> DataLoc ((Computation s2,4) . SBP ),(4 + RetSP ) by A6, A78;
thus (Computation s1,5) . b = (Computation s1,4) . b by A41, A89, SCMPDS_2:59
.= (Computation s2,4) . b by A78, A85
.= (Computation s2,5) . b by A47, A90, SCMPDS_2:59 ; :: thesis: verum

end;

end;

end;

A91: now

let b be Int_position ; :: thesis: ( s1 . b = s2 . b implies (Computation s1,6) . b₁ = (Computation s2,6) . b₁ )
assume A92: s1 . b = s2 . b ; :: thesis: (Computation s1,6) . b₁ = (Computation s2,6) . b₁
A93: s1 . (DataLoc ((Computation s1,5) . GBP ),1) = s2 . (intpos (0 + 1)) by A6, A51, Th5
.= s2 . (DataLoc ((Computation s1,5) . GBP ),1) by A51, Th5 ;

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

suppose A94: b = DataLoc ((Computation s1,5) . GBP ),1 ; :: thesis: (Computation s1,6) . b₁ = (Computation s2,6) . b₁

then A95: b = DataLoc ((Computation s2,5) . GBP ),1 by A4, A6, A84;
thus (Computation s1,6) . b = ((Computation s1,5) . (DataLoc ((Computation s1,5) . GBP ),1)) + 4 by A50, A94, SCMPDS_2:60
.= ((Computation s2,5) . (DataLoc ((Computation s1,5) . GBP ),1)) + 4 by A84, A93
.= ((Computation s2,5) . (DataLoc ((Computation s2,5) . GBP ),1)) + 4 by A4, A6, A84
.= (Computation s2,6) . b by A54, A95, SCMPDS_2:60 ; :: thesis: verum

end;

suppose A96: b <> DataLoc ((Computation s1,5) . GBP ),1 ; :: thesis: (Computation s1,6) . b₁ = (Computation s2,6) . b₁

then A97: b <> DataLoc ((Computation s2,5) . GBP ),1 by A4, A6, A84;
thus (Computation s1,6) . b = (Computation s1,5) . b by A50, A96, SCMPDS_2:60
.= (Computation s2,5) . b by A84, A92
.= (Computation s2,6) . b by A54, A97, SCMPDS_2:60 ; :: thesis: verum

end;

end;

end;

A98: now

let b be Int_position ; :: thesis: ( s1 . b = s2 . b implies (Computation s1,7) . b₁ = (Computation s2,7) . b₁ )
assume A99: s1 . b = s2 . b ; :: thesis: (Computation s1,7) . b₁ = (Computation s2,7) . b₁

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

suppose A100: b = DataLoc ((Computation s1,6) . SBP ),RetIC ; :: thesis: (Computation s1,7) . b₁ = (Computation s2,7) . b₁

then A101: b = DataLoc ((Computation s2,6) . SBP ),RetIC by A6, A91;
thus (Computation s1,7) . b = IC (Computation s1,6) by A57, A100, SCMPDS_2:71
.= (Computation s2,7) . b by A55, A58, A60, A101, SCMPDS_2:71 ; :: thesis: verum

end;

suppose A102: b <> DataLoc ((Computation s1,6) . SBP ),RetIC ; :: thesis: (Computation s1,7) . b₁ = (Computation s2,7) . b₁

then A103: b <> DataLoc ((Computation s2,6) . SBP ),RetIC by A6, A91;
thus (Computation s1,7) . b = (Computation s1,6) . b by A57, A102, SCMPDS_2:71
.= (Computation s2,6) . b by A91, A99
.= (Computation s2,7) . b by A60, A103, SCMPDS_2:71 ; :: 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 (Computation s1,b₂) = IC (Computation s2,b₂) & (Computation s1,b₂) . b₃ = (Computation s2,b₂) . b₃ )
let a be Int_position ; :: thesis: ( k <= 7 & s1 . a = s2 . a implies ( IC (Computation s1,b₁) = IC (Computation s2,b₁) & (Computation s1,b₁) . b₂ = (Computation s2,b₁) . b₂ ) )
assume A104: ( k <= 7 & s1 . a = s2 . a ) ; :: thesis: ( IC (Computation s1,b₁) = IC (Computation s2,b₁) & (Computation s1,b₁) . b₂ = (Computation 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 A104, NAT_1:32;

suppose A105: k = 0 ; :: thesis: ( IC (Computation s1,b₁) = IC (Computation s2,b₁) & (Computation s1,b₁) . b₂ = (Computation s2,b₁) . b₂ )

hence IC (Computation s1,k) = IC s1 by AMI_1:13
.= IC (Computation s2,k) by A6, A105, AMI_1:13 ;
:: thesis: (Computation s1,k) . a = (Computation s2,k) . a
thus (Computation s1,k) . a = s1 . a by A105, AMI_1:13
.= (Computation s2,k) . a by A104, A105, AMI_1:13 ; :: thesis: verum

end;

suppose A106: k = 1 ; :: thesis: ( IC (Computation s1,b₁) = IC (Computation s2,b₁) & (Computation s1,b₁) . b₂ = (Computation s2,b₁) . b₂ )

hence IC (Computation s1,k) = IC (Computation s2,k) by A10, A15; :: thesis: (Computation s1,k) . a = (Computation s2,k) . a
thus (Computation s1,k) . a = (Computation s2,k) . a by A61, A104, A106; :: thesis: verum

end;

suppose A107: k = 2 ; :: thesis: ( IC (Computation s1,b₁) = IC (Computation s2,b₁) & (Computation s1,b₁) . b₂ = (Computation s2,b₁) . b₂ )

hence IC (Computation s1,k) = IC (Computation s2,k) by A18, A24; :: thesis: (Computation s1,k) . a = (Computation s2,k) . a
thus (Computation s1,k) . a = (Computation s2,k) . a by A62, A104, A107; :: thesis: verum

end;

suppose A108: k = 3 ; :: thesis: ( IC (Computation s1,b₁) = IC (Computation s2,b₁) & (Computation s1,b₁) . b₂ = (Computation s2,b₁) . b₂ )

hence IC (Computation s1,k) = IC (Computation s2,k) by A27, A36; :: thesis: (Computation s1,k) . a = (Computation s2,k) . a
thus (Computation s1,k) . a = (Computation s2,k) . a by A68, A104, A108; :: thesis: verum

end;

suppose A109: k = 4 ; :: thesis: ( IC (Computation s1,b₁) = IC (Computation s2,b₁) & (Computation s1,b₁) . b₂ = (Computation s2,b₁) . b₂ )

hence IC (Computation s1,k) = IC (Computation s2,k) by A39, A45; :: thesis: (Computation s1,k) . a = (Computation s2,k) . a
thus (Computation s1,k) . a = (Computation s2,k) . a by A78, A104, A109; :: thesis: verum

end;

suppose A110: k = 5 ; :: thesis: ( IC (Computation s1,b₁) = IC (Computation s2,b₁) & (Computation s1,b₁) . b₂ = (Computation s2,b₁) . b₂ )

hence IC (Computation s1,k) = IC (Computation s2,k) by A48, A52; :: thesis: (Computation s1,k) . a = (Computation s2,k) . a
thus (Computation s1,k) . a = (Computation s2,k) . a by A84, A104, A110; :: thesis: verum

end;

suppose A111: k = 6 ; :: thesis: ( IC (Computation s1,b₁) = IC (Computation s2,b₁) & (Computation s1,b₁) . b₂ = (Computation s2,b₁) . b₂ )

hence IC (Computation s1,k) = IC (Computation s2,k) by A55, A58; :: thesis: (Computation s1,k) . a = (Computation s2,k) . a
thus (Computation s1,k) . a = (Computation s2,k) . a by A91, A104, A111; :: thesis: verum

end;

suppose A112: k = 7 ; :: thesis: ( IC (Computation s1,b₁) = IC (Computation s2,b₁) & (Computation s1,b₁) . b₂ = (Computation s2,b₁) . b₂ )

hence IC (Computation s1,k) = Next (IC (Computation s2,6)) by A55, A57, A58, SCMPDS_2:71
.= IC (Computation s2,k) by A60, A112, SCMPDS_2:71 ;
:: thesis: (Computation s1,k) . a = (Computation s2,k) . a
thus (Computation s1,k) . a = (Computation s2,k) . a by A98, A104, A112; :: thesis: verum

end;

end;

end;