let s1, s2 be State of SCMPDS; :: thesis: for a being Int_position
for k being Element of NAT st Initialize GCD-Algorithm c= s1 & Initialize GCD-Algorithm c= s2 & s1 . a = s2 . a & k <= 4 holds
( IC (Comput ((ProgramPart s1),s1,k)) = IC (Comput ((ProgramPart s2),s2,k)) & (Comput ((ProgramPart s1),s1,k)) . a = (Comput ((ProgramPart s2),s2,k)) . a )
let a be Int_position ; :: thesis: for k being Element of NAT st Initialize GCD-Algorithm c= s1 & Initialize GCD-Algorithm c= s2 & s1 . a = s2 . a & k <= 4 holds
( IC (Comput ((ProgramPart s1),s1,k)) = IC (Comput ((ProgramPart s2),s2,k)) & (Comput ((ProgramPart s1),s1,k)) . a = (Comput ((ProgramPart s2),s2,k)) . a )
let k be Element of NAT ; :: thesis: ( Initialize GCD-Algorithm c= s1 & Initialize GCD-Algorithm c= s2 & s1 . a = s2 . a & k <= 4 implies ( IC (Comput ((ProgramPart s1),s1,k)) = IC (Comput ((ProgramPart s2),s2,k)) & (Comput ((ProgramPart s1),s1,k)) . a = (Comput ((ProgramPart s2),s2,k)) . a ) )
set GA = GCD-Algorithm ;
assume that
A1: Initialize GCD-Algorithm c= s1 and
A2: Initialize GCD-Algorithm c= s2 ; :: thesis: ( not s1 . a = s2 . a or not k <= 4 or ( IC (Comput ((ProgramPart s1),s1,k)) = IC (Comput ((ProgramPart s2),s2,k)) & (Comput ((ProgramPart s1),s1,k)) . a = (Comput ((ProgramPart s2),s2,k)) . a ) )
assume that
A3: s1 . a = s2 . a and
A4: k <= 4 ; :: thesis: ( IC (Comput ((ProgramPart s1),s1,k)) = IC (Comput ((ProgramPart s2),s2,k)) & (Comput ((ProgramPart s1),s1,k)) . a = (Comput ((ProgramPart s2),s2,k)) . a )
A5: GCD-Algorithm c= s1 by A1, COMPOS_1:132;
A6: GCD-Algorithm c= s2 by A2, COMPOS_1:132;
A7: IC s1 = 0 by A1, SCMPDS_5:18;
Y: (ProgramPart s1) /. (IC s1) = s1 . (IC s1) by COMPOS_1:38;
A8: Comput ((ProgramPart s1),s1,(0 + 1)) = Following ((ProgramPart s1),(Comput ((ProgramPart s1),s1,0))) by EXTPRO_1:4
.= Following ((ProgramPart s1),s1) by EXTPRO_1:3
.= Exec ((GBP := 0),s1) by A5, A7, Lm1, Y ;
A9: IC s2 = 0 by A2, SCMPDS_5:18;
Y: (ProgramPart s2) /. (IC s2) = s2 . (IC s2) by COMPOS_1:38;
A10: Comput ((ProgramPart s2),s2,(0 + 1)) = Following ((ProgramPart s2),(Comput ((ProgramPart s2),s2,0))) by EXTPRO_1:4
.= Following ((ProgramPart s2),s2) by EXTPRO_1:3
.= Exec ((GBP := 0),s2) by A6, A9, Lm1, Y ;
Y: (ProgramPart (Comput ((ProgramPart s1),s1,1))) /. (IC (Comput ((ProgramPart s1),s1,1))) = (Comput ((ProgramPart s1),s1,1)) . (IC (Comput ((ProgramPart s1),s1,1))) by COMPOS_1:38;
A11: IC (Comput ((ProgramPart s1),s1,1)) = succ (IC s1) by A8, SCMPDS_2:57
.= 0 + 1 by A7 ;
then A12: CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,1))),(Comput ((ProgramPart s1),s1,1))) = s1 . 1 by Y, AMI_1:54
.= SBP := 7 by A5, Lm1 ;
T: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,1)) by AMI_1:123;
A13: Comput ((ProgramPart s1),s1,(1 + 1)) = Following ((ProgramPart s1),(Comput ((ProgramPart s1),s1,1))) by EXTPRO_1:4
.= Exec ((SBP := 7),(Comput ((ProgramPart s1),s1,1))) by A12, T ;
Y: (ProgramPart (Comput ((ProgramPart s2),s2,1))) /. (IC (Comput ((ProgramPart s2),s2,1))) = (Comput ((ProgramPart s2),s2,1)) . (IC (Comput ((ProgramPart s2),s2,1))) by COMPOS_1:38;
A14: IC (Comput ((ProgramPart s2),s2,1)) = succ (IC s2) by A10, SCMPDS_2:57
.= 0 + 1 by A9 ;
then A15: CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,1))),(Comput ((ProgramPart s2),s2,1))) = s2 . 1 by Y, AMI_1:54
.= SBP := 7 by A6, Lm1 ;
T: ProgramPart s2 = ProgramPart (Comput ((ProgramPart s2),s2,1)) by AMI_1:123;
A16: Comput ((ProgramPart s2),s2,(1 + 1)) = Following ((ProgramPart s2),(Comput ((ProgramPart s2),s2,1))) by EXTPRO_1:4
.= Exec ((SBP := 7),(Comput ((ProgramPart s2),s2,1))) by A15, T ;
Y: (ProgramPart (Comput ((ProgramPart s1),s1,2))) /. (IC (Comput ((ProgramPart s1),s1,2))) = (Comput ((ProgramPart s1),s1,2)) . (IC (Comput ((ProgramPart s1),s1,2))) by COMPOS_1:38;
A17: IC (Comput ((ProgramPart s1),s1,2)) = succ (IC (Comput ((ProgramPart s1),s1,1))) by A13, SCMPDS_2:57
.= 1 + 1 by A11 ;
then A18: CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,2))),(Comput ((ProgramPart s1),s1,2))) = s1 . 2 by Y, AMI_1:54
.= saveIC (SBP,RetIC) by A5, Lm1 ;
T: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,2)) by AMI_1:123;
A19: Comput ((ProgramPart s1),s1,(2 + 1)) = Following ((ProgramPart s1),(Comput ((ProgramPart s1),s1,2))) by EXTPRO_1:4
.= Exec ((saveIC (SBP,RetIC)),(Comput ((ProgramPart s1),s1,2))) by A18, T ;
A20: (Comput ((ProgramPart s1),s1,2)) . SBP = 7 by A13, SCMPDS_2:57;
Y: (ProgramPart (Comput ((ProgramPart s2),s2,2))) /. (IC (Comput ((ProgramPart s2),s2,2))) = (Comput ((ProgramPart s2),s2,2)) . (IC (Comput ((ProgramPart s2),s2,2))) by COMPOS_1:38;
A21: IC (Comput ((ProgramPart s2),s2,2)) = succ (IC (Comput ((ProgramPart s2),s2,1))) by A16, SCMPDS_2:57
.= 1 + 1 by A14 ;
then A22: CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,2))),(Comput ((ProgramPart s2),s2,2))) = s2 . 2 by Y, AMI_1:54
.= saveIC (SBP,RetIC) by A6, Lm1 ;
T: ProgramPart s2 = ProgramPart (Comput ((ProgramPart s2),s2,2)) by AMI_1:123;
A23: Comput ((ProgramPart s2),s2,(2 + 1)) = Following ((ProgramPart s2),(Comput ((ProgramPart s2),s2,2))) by EXTPRO_1:4
.= Exec ((saveIC (SBP,RetIC)),(Comput ((ProgramPart s2),s2,2))) by A22, T ;
A24: (Comput ((ProgramPart s2),s2,2)) . SBP = 7 by A16, SCMPDS_2:57;
Y: (ProgramPart (Comput ((ProgramPart s1),s1,3))) /. (IC (Comput ((ProgramPart s1),s1,3))) = (Comput ((ProgramPart s1),s1,3)) . (IC (Comput ((ProgramPart s1),s1,3))) by COMPOS_1:38;
A25: IC (Comput ((ProgramPart s1),s1,3)) = succ (IC (Comput ((ProgramPart s1),s1,2))) by A19, SCMPDS_2:71
.= 2 + 1 by A17 ;
then A26: CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,3))),(Comput ((ProgramPart s1),s1,3))) = s1 . 3 by Y, AMI_1:54
.= goto 2 by A5, Lm1 ;
T: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,3)) by AMI_1:123;
A27: Comput ((ProgramPart s1),s1,(3 + 1)) = Following ((ProgramPart s1),(Comput ((ProgramPart s1),s1,3))) by EXTPRO_1:4
.= Exec ((goto 2),(Comput ((ProgramPart s1),s1,3))) by A26, T ;
Y: (ProgramPart (Comput ((ProgramPart s2),s2,3))) /. (IC (Comput ((ProgramPart s2),s2,3))) = (Comput ((ProgramPart s2),s2,3)) . (IC (Comput ((ProgramPart s2),s2,3))) by COMPOS_1:38;
A28: IC (Comput ((ProgramPart s2),s2,3)) = succ (IC (Comput ((ProgramPart s2),s2,2))) by A23, SCMPDS_2:71
.= 2 + 1 by A21 ;
then A29: CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,3))),(Comput ((ProgramPart s2),s2,3))) = s2 . 3 by Y, AMI_1:54
.= goto 2 by A6, Lm1 ;
T: ProgramPart s2 = ProgramPart (Comput ((ProgramPart s2),s2,3)) by AMI_1:123;
A30: Comput ((ProgramPart s2),s2,(3 + 1)) = Following ((ProgramPart s2),(Comput ((ProgramPart s2),s2,3))) by EXTPRO_1:4
.= Exec ((goto 2),(Comput ((ProgramPart s2),s2,3))) by A29, T ;

A31: now

let b be Int_position ; :: thesis: ( s1 . b = s2 . b implies (Comput ((ProgramPart s1),s1,1)) . b₁ = (Comput ((ProgramPart s2),s2,1)) . b₁ )
assume A32: s1 . b = s2 . b ; :: thesis: (Comput ((ProgramPart s1),s1,1)) . b₁ = (Comput ((ProgramPart s2),s2,1)) . b₁

per cases ( b = GBP or b <> GBP ) ;

suppose A33: b = GBP ; :: thesis: (Comput ((ProgramPart s1),s1,1)) . b₁ = (Comput ((ProgramPart s2),s2,1)) . b₁

hence (Comput ((ProgramPart s1),s1,1)) . b = 0 by A8, SCMPDS_2:57
.= (Comput ((ProgramPart s2),s2,1)) . b by A10, A33, SCMPDS_2:57 ;
:: thesis: verum

end;

suppose A34: b <> GBP ; :: thesis: (Comput ((ProgramPart s1),s1,1)) . b₁ = (Comput ((ProgramPart s2),s2,1)) . b₁

hence (Comput ((ProgramPart s1),s1,1)) . b = s1 . b by A8, SCMPDS_2:57
.= (Comput ((ProgramPart s2),s2,1)) . b by A10, A32, A34, SCMPDS_2:57 ;
:: thesis: verum

end;

end;

end;

A35: now

let b be Int_position ; :: thesis: ( s1 . b = s2 . b implies (Comput ((ProgramPart s1),s1,2)) . b₁ = (Comput ((ProgramPart s2),s2,2)) . b₁ )
assume A36: s1 . b = s2 . b ; :: thesis: (Comput ((ProgramPart s1),s1,2)) . b₁ = (Comput ((ProgramPart s2),s2,2)) . b₁

per cases ( b = SBP or b <> SBP ) ;

suppose A37: b = SBP ; :: thesis: (Comput ((ProgramPart s1),s1,2)) . b₁ = (Comput ((ProgramPart s2),s2,2)) . b₁

hence (Comput ((ProgramPart s1),s1,2)) . b = 7 by A13, SCMPDS_2:57
.= (Comput ((ProgramPart s2),s2,2)) . b by A16, A37, SCMPDS_2:57 ;
:: thesis: verum

end;

suppose A38: b <> SBP ; :: thesis: (Comput ((ProgramPart s1),s1,2)) . b₁ = (Comput ((ProgramPart s2),s2,2)) . b₁

hence (Comput ((ProgramPart s1),s1,2)) . b = (Comput ((ProgramPart s1),s1,1)) . b by A13, SCMPDS_2:57
.= (Comput ((ProgramPart s2),s2,1)) . b by A31, A36
.= (Comput ((ProgramPart s2),s2,2)) . b by A16, A38, SCMPDS_2:57 ;
:: thesis: verum

end;

end;

end;

A39: now

let b be Int_position ; :: thesis: ( s1 . b = s2 . b implies (Comput ((ProgramPart s1),s1,3)) . b₁ = (Comput ((ProgramPart s2),s2,3)) . b₁ )
assume A40: s1 . b = s2 . b ; :: thesis: (Comput ((ProgramPart s1),s1,3)) . b₁ = (Comput ((ProgramPart s2),s2,3)) . b₁

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

suppose A41: b = DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),RetIC) ; :: thesis: (Comput ((ProgramPart s1),s1,3)) . b₁ = (Comput ((ProgramPart s2),s2,3)) . b₁

hence (Comput ((ProgramPart s1),s1,3)) . b = IC (Comput ((ProgramPart s1),s1,2)) by A19, SCMPDS_2:71
.= (Comput ((ProgramPart s2),s2,3)) . b by A17, A20, A21, A23, A24, A41, SCMPDS_2:71 ;
:: thesis: verum

end;

suppose A42: b <> DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),RetIC) ; :: thesis: (Comput ((ProgramPart s1),s1,3)) . b₁ = (Comput ((ProgramPart s2),s2,3)) . b₁

hence (Comput ((ProgramPart s1),s1,3)) . b = (Comput ((ProgramPart s1),s1,2)) . b by A19, SCMPDS_2:71
.= (Comput ((ProgramPart s2),s2,2)) . b by A35, A40
.= (Comput ((ProgramPart s2),s2,3)) . b by A20, A23, A24, A42, SCMPDS_2:71 ;
:: thesis: verum

end;

end;

end;

per cases ( k = 0 or k = 1 or k = 2 or k = 3 or k = 4 ) by A4, NAT_1:29;

suppose A43: k = 0 ; :: thesis: ( IC (Comput ((ProgramPart s1),s1,k)) = IC (Comput ((ProgramPart s2),s2,k)) & (Comput ((ProgramPart s1),s1,k)) . a = (Comput ((ProgramPart s2),s2,k)) . a )

hence IC (Comput ((ProgramPart s1),s1,k)) = IC s1 by EXTPRO_1:3
.= IC (Comput ((ProgramPart s2),s2,k)) by A7, A9, A43, EXTPRO_1:3 ;
:: thesis: (Comput ((ProgramPart s1),s1,k)) . a = (Comput ((ProgramPart s2),s2,k)) . a
thus (Comput ((ProgramPart s1),s1,k)) . a = s1 . a by A43, EXTPRO_1:3
.= (Comput ((ProgramPart s2),s2,k)) . a by A3, A43, EXTPRO_1:3 ; :: thesis: verum

end;

suppose A44: k = 1 ; :: thesis: ( IC (Comput ((ProgramPart s1),s1,k)) = IC (Comput ((ProgramPart s2),s2,k)) & (Comput ((ProgramPart s1),s1,k)) . a = (Comput ((ProgramPart s2),s2,k)) . a )

hence IC (Comput ((ProgramPart s1),s1,k)) = IC (Comput ((ProgramPart s2),s2,k)) by A11, A14; :: thesis: (Comput ((ProgramPart s1),s1,k)) . a = (Comput ((ProgramPart s2),s2,k)) . a
thus (Comput ((ProgramPart s1),s1,k)) . a = (Comput ((ProgramPart s2),s2,k)) . a by A3, A31, A44; :: thesis: verum

end;

suppose A45: k = 2 ; :: thesis: ( IC (Comput ((ProgramPart s1),s1,k)) = IC (Comput ((ProgramPart s2),s2,k)) & (Comput ((ProgramPart s1),s1,k)) . a = (Comput ((ProgramPart s2),s2,k)) . a )

hence IC (Comput ((ProgramPart s1),s1,k)) = IC (Comput ((ProgramPart s2),s2,k)) by A17, A21; :: thesis: (Comput ((ProgramPart s1),s1,k)) . a = (Comput ((ProgramPart s2),s2,k)) . a
thus (Comput ((ProgramPart s1),s1,k)) . a = (Comput ((ProgramPart s2),s2,k)) . a by A3, A35, A45; :: thesis: verum

end;

suppose A46: k = 3 ; :: thesis: ( IC (Comput ((ProgramPart s1),s1,k)) = IC (Comput ((ProgramPart s2),s2,k)) & (Comput ((ProgramPart s1),s1,k)) . a = (Comput ((ProgramPart s2),s2,k)) . a )

hence IC (Comput ((ProgramPart s1),s1,k)) = IC (Comput ((ProgramPart s2),s2,k)) by A25, A28; :: thesis: (Comput ((ProgramPart s1),s1,k)) . a = (Comput ((ProgramPart s2),s2,k)) . a
thus (Comput ((ProgramPart s1),s1,k)) . a = (Comput ((ProgramPart s2),s2,k)) . a by A3, A39, A46; :: thesis: verum

end;

suppose A47: k = 4 ; :: thesis: ( IC (Comput ((ProgramPart s1),s1,k)) = IC (Comput ((ProgramPart s2),s2,k)) & (Comput ((ProgramPart s1),s1,k)) . a = (Comput ((ProgramPart s2),s2,k)) . a )

hence IC (Comput ((ProgramPart s1),s1,k)) = ICplusConst ((Comput ((ProgramPart s1),s1,3)),2) by A27, SCMPDS_2:66
.= 3 + 2 by A25, SCMPDS_6:23
.= ICplusConst ((Comput ((ProgramPart s2),s2,3)),2) by A28, SCMPDS_6:23
.= IC (Comput ((ProgramPart s2),s2,k)) by A30, A47, SCMPDS_2:66 ;
:: thesis: (Comput ((ProgramPart s1),s1,k)) . a = (Comput ((ProgramPart s2),s2,k)) . a
thus (Comput ((ProgramPart s1),s1,k)) . a = (Comput ((ProgramPart s1),s1,3)) . a by A27, A47, SCMPDS_2:66
.= (Comput ((ProgramPart s2),s2,3)) . a by A3, A39
.= (Comput ((ProgramPart s2),s2,k)) . a by A30, A47, SCMPDS_2:66 ; :: thesis: verum

end;

end;