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 = 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 ((ProgramPart s1),s1,k)) = IC (Comput ((ProgramPart s2),s2,k)) & (Comput ((ProgramPart s1),s1,k)) . a = (Comput ((ProgramPart s2),s2,k)) . a )
let s1, s2 be State of SCMPDS; :: thesis: ( GCD-Algorithm c= s1 & GCD-Algorithm c= s2 & 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 ((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: GCD-Algorithm c= s1 and
A2: GCD-Algorithm c= s2 ; :: 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 ((ProgramPart s1),s1,k)) = IC (Comput ((ProgramPart s2),s2,k)) & (Comput ((ProgramPart s1),s1,k)) . a = (Comput ((ProgramPart s2),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 Element of NAT
for a being Int_position st k <= 7 & s1 . a = s2 . a 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 ) )
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 Element of NAT
for a being Int_position st k <= 7 & s1 . a = s2 . a 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 ) )
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 Element of NAT
for a being Int_position st k <= 7 & s1 . a = s2 . a 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 ) )
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 Element of NAT
for a being Int_position st k <= 7 & s1 . a = s2 . a 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 ) )
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 Element of NAT
for a being Int_position st k <= 7 & s1 . a = s2 . a 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 ) )
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 Element of NAT
for a being Int_position st k <= 7 & s1 . a = s2 . a 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 )
Y: (ProgramPart s1) /. (IC s1) = s1 . (IC s1) by COMPOS_1:38;
A12: Comput ((ProgramPart s1),s1,(1 + 0)) = Following ((ProgramPart s1),(Comput ((ProgramPart s1),s1,0))) by EXTPRO_1:4
.= Following ((ProgramPart s1),s1) by EXTPRO_1:3
.= Exec (((SBP,3) <=0_goto 9),s1) by A1, Y, A3, Lm1 ;
Y: (ProgramPart s2) /. (IC s2) = s2 . (IC s2) by COMPOS_1:38;
A13: Comput ((ProgramPart s2),s2,(1 + 0)) = Following ((ProgramPart s2),(Comput ((ProgramPart s2),s2,0))) by EXTPRO_1:4
.= Following ((ProgramPart s2),s2) by EXTPRO_1:3
.= Exec (((SBP,3) <=0_goto 9),s2) by A2, A3, A7, 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;
A14: IC (Comput ((ProgramPart s1),s1,1)) = succ (IC s1) by A6, A12, SCMPDS_2:68
.= 5 + 1 by A3 ;
then A15: CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,1))),(Comput ((ProgramPart s1),s1,1))) = s1 . 6 by Y, AMI_1:54
.= (SBP,6) := (SBP,3) by A1, Lm1 ;
T: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,1)) by AMI_1:123;
A16: Comput ((ProgramPart s1),s1,(1 + 1)) = Following ((ProgramPart s1),(Comput ((ProgramPart s1),s1,1))) by EXTPRO_1:4
.= Exec (((SBP,6) := (SBP,3)),(Comput ((ProgramPart s1),s1,1))) by A15, T ;
A17: (Comput ((ProgramPart s1),s1,1)) . SBP = n by A4, A12, SCMPDS_2:68;
A18: (Comput ((ProgramPart s1),s1,1)) . GBP = 0 by A5, A12, SCMPDS_2:68;
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;
A19: IC (Comput ((ProgramPart s2),s2,1)) = succ (IC s2) by A6, A8, A11, A13, SCMPDS_2:68
.= 5 + 1 by A3, A7 ;
then A20: CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,1))),(Comput ((ProgramPart s2),s2,1))) = s2 . 6 by Y, AMI_1:54
.= (SBP,6) := (SBP,3) by A2, Lm1 ;
T: ProgramPart s2 = ProgramPart (Comput ((ProgramPart s2),s2,1)) by AMI_1:123;
A21: Comput ((ProgramPart s2),s2,(1 + 1)) = Following ((ProgramPart s2),(Comput ((ProgramPart s2),s2,1))) by EXTPRO_1:4
.= Exec (((SBP,6) := (SBP,3)),(Comput ((ProgramPart s2),s2,1))) by A20, 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;
A22: IC (Comput ((ProgramPart s1),s1,2)) = succ (IC (Comput ((ProgramPart s1),s1,1))) by A16, SCMPDS_2:59
.= 6 + 1 by A14 ;
then A23: CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,2))),(Comput ((ProgramPart s1),s1,2))) = s1 . 7 by Y, AMI_1:54
.= Divide (SBP,2,SBP,3) by A1, Lm1 ;
T: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,2)) by AMI_1:123;
A24: Comput ((ProgramPart s1),s1,(2 + 1)) = Following ((ProgramPart s1),(Comput ((ProgramPart s1),s1,2))) by EXTPRO_1:4
.= Exec ((Divide (SBP,2,SBP,3)),(Comput ((ProgramPart s1),s1,2))) by A23, T ;
A25: DataLoc (((Comput ((ProgramPart s1),s1,1)) . SBP),6) = intpos (n + 6) by A17, Th5;
then A26: (Comput ((ProgramPart s1),s1,2)) . SBP = n by A16, A17, Lm3, SCMPDS_2:59;
A27: (Comput ((ProgramPart s1),s1,2)) . GBP = 0 by A16, A18, A25, Lm2, SCMPDS_2:59;
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;
A28: IC (Comput ((ProgramPart s2),s2,2)) = succ (IC (Comput ((ProgramPart s2),s2,1))) by A21, SCMPDS_2:59
.= 6 + 1 by A19 ;
then A29: CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,2))),(Comput ((ProgramPart s2),s2,2))) = s2 . 7 by Y, AMI_1:54
.= Divide (SBP,2,SBP,3) by A2, Lm1 ;
T: ProgramPart s2 = ProgramPart (Comput ((ProgramPart s2),s2,2)) by AMI_1:123;
A30: Comput ((ProgramPart s2),s2,(2 + 1)) = Following ((ProgramPart s2),(Comput ((ProgramPart s2),s2,2))) by EXTPRO_1:4
.= Exec ((Divide (SBP,2,SBP,3)),(Comput ((ProgramPart s2),s2,2))) by A29, T ;
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;
A31: IC (Comput ((ProgramPart s1),s1,3)) = succ (IC (Comput ((ProgramPart s1),s1,2))) by A24, SCMPDS_2:64
.= 7 + 1 by A22 ;
then A32: CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,3))),(Comput ((ProgramPart s1),s1,3))) = s1 . 8 by Y, AMI_1:54
.= (SBP,7) := (SBP,3) by A1, Lm1 ;
T: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,3)) by AMI_1:123;
A33: Comput ((ProgramPart s1),s1,(3 + 1)) = Following ((ProgramPart s1),(Comput ((ProgramPart s1),s1,3))) by EXTPRO_1:4
.= Exec (((SBP,7) := (SBP,3)),(Comput ((ProgramPart s1),s1,3))) by A32, T ;
A34: DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),2) = intpos (n + 2) by A26, Th5;
then A35: SBP <> DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),2) by Lm3;
A36: DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),3) = intpos (n + 3) by A26, Th5;
then SBP <> DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),3) by Lm3;
then A37: (Comput ((ProgramPart s1),s1,3)) . SBP = n by A24, A26, A35, SCMPDS_2:64;
A38: GBP <> DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),2) by A34, Lm2;
GBP <> DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),3) by A36, Lm2;
then A39: (Comput ((ProgramPart s1),s1,3)) . GBP = 0 by A24, A27, A38, SCMPDS_2:64;
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;
A40: IC (Comput ((ProgramPart s2),s2,3)) = succ (IC (Comput ((ProgramPart s2),s2,2))) by A30, SCMPDS_2:64
.= 7 + 1 by A28 ;
then A41: CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,3))),(Comput ((ProgramPart s2),s2,3))) = s2 . 8 by Y, AMI_1:54
.= (SBP,7) := (SBP,3) by A2, Lm1 ;
T: ProgramPart s2 = ProgramPart (Comput ((ProgramPart s2),s2,3)) by AMI_1:123;
A42: Comput ((ProgramPart s2),s2,(3 + 1)) = Following ((ProgramPart s2),(Comput ((ProgramPart s2),s2,3))) by EXTPRO_1:4
.= Exec (((SBP,7) := (SBP,3)),(Comput ((ProgramPart s2),s2,3))) by A41, T ;
Y: (ProgramPart (Comput ((ProgramPart s1),s1,4))) /. (IC (Comput ((ProgramPart s1),s1,4))) = (Comput ((ProgramPart s1),s1,4)) . (IC (Comput ((ProgramPart s1),s1,4))) by COMPOS_1:38;
A43: IC (Comput ((ProgramPart s1),s1,4)) = succ (IC (Comput ((ProgramPart s1),s1,3))) by A33, SCMPDS_2:59
.= 8 + 1 by A31 ;
then A44: CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4))) = s1 . 9 by Y, AMI_1:54
.= (SBP,(4 + RetSP)) := (GBP,1) by A1, Lm1 ;
T: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,4)) by AMI_1:123;
A45: Comput ((ProgramPart s1),s1,(4 + 1)) = Following ((ProgramPart s1),(Comput ((ProgramPart s1),s1,4))) by EXTPRO_1:4
.= Exec (((SBP,(4 + RetSP)) := (GBP,1)),(Comput ((ProgramPart s1),s1,4))) by A44, T ;
A46: DataLoc (((Comput ((ProgramPart s1),s1,3)) . SBP),7) = intpos (n + 7) by A37, Th5;
then A47: (Comput ((ProgramPart s1),s1,4)) . SBP = n by A33, A37, Lm3, SCMPDS_2:59;
A48: (Comput ((ProgramPart s1),s1,4)) . GBP = 0 by A33, A39, A46, Lm2, SCMPDS_2:59;
Y: (ProgramPart (Comput ((ProgramPart s2),s2,4))) /. (IC (Comput ((ProgramPart s2),s2,4))) = (Comput ((ProgramPart s2),s2,4)) . (IC (Comput ((ProgramPart s2),s2,4))) by COMPOS_1:38;
A49: IC (Comput ((ProgramPart s2),s2,4)) = succ (IC (Comput ((ProgramPart s2),s2,3))) by A42, SCMPDS_2:59
.= 8 + 1 by A40 ;
then A50: CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4))) = s2 . 9 by Y, AMI_1:54
.= (SBP,(4 + RetSP)) := (GBP,1) by A2, Lm1 ;
T: ProgramPart s2 = ProgramPart (Comput ((ProgramPart s2),s2,4)) by AMI_1:123;
A51: Comput ((ProgramPart s2),s2,(4 + 1)) = Following ((ProgramPart s2),(Comput ((ProgramPart s2),s2,4))) by EXTPRO_1:4
.= Exec (((SBP,(4 + RetSP)) := (GBP,1)),(Comput ((ProgramPart s2),s2,4))) by A50, T ;
Y: (ProgramPart (Comput ((ProgramPart s1),s1,5))) /. (IC (Comput ((ProgramPart s1),s1,5))) = (Comput ((ProgramPart s1),s1,5)) . (IC (Comput ((ProgramPart s1),s1,5))) by COMPOS_1:38;
A52: IC (Comput ((ProgramPart s1),s1,5)) = succ (IC (Comput ((ProgramPart s1),s1,4))) by A45, SCMPDS_2:59
.= 9 + 1 by A43 ;
then A53: CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,5))),(Comput ((ProgramPart s1),s1,5))) = s1 . 10 by Y, AMI_1:54
.= AddTo (GBP,1,4) by A1, Lm1 ;
T: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,5)) by AMI_1:123;
A54: Comput ((ProgramPart s1),s1,(5 + 1)) = Following ((ProgramPart s1),(Comput ((ProgramPart s1),s1,5))) by EXTPRO_1:4
.= Exec ((AddTo (GBP,1,4)),(Comput ((ProgramPart s1),s1,5))) by A53, T ;
DataLoc (((Comput ((ProgramPart s1),s1,4)) . SBP),(4 + RetSP)) = intpos (n + (4 + 0)) by A47, Th5, SCMPDS_1:def 22;
then A55: (Comput ((ProgramPart s1),s1,5)) . GBP = 0 by A45, A48, Lm2, SCMPDS_2:59;
Y: (ProgramPart (Comput ((ProgramPart s2),s2,5))) /. (IC (Comput ((ProgramPart s2),s2,5))) = (Comput ((ProgramPart s2),s2,5)) . (IC (Comput ((ProgramPart s2),s2,5))) by COMPOS_1:38;
A56: IC (Comput ((ProgramPart s2),s2,5)) = succ (IC (Comput ((ProgramPart s2),s2,4))) by A51, SCMPDS_2:59
.= 9 + 1 by A49 ;
then A57: CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,5))),(Comput ((ProgramPart s2),s2,5))) = s2 . 10 by Y, AMI_1:54
.= AddTo (GBP,1,4) by A2, Lm1 ;
T: ProgramPart s2 = ProgramPart (Comput ((ProgramPart s2),s2,5)) by AMI_1:123;
A58: Comput ((ProgramPart s2),s2,(5 + 1)) = Following ((ProgramPart s2),(Comput ((ProgramPart s2),s2,5))) by EXTPRO_1:4
.= Exec ((AddTo (GBP,1,4)),(Comput ((ProgramPart s2),s2,5))) by A57, T ;
Y: (ProgramPart (Comput ((ProgramPart s1),s1,6))) /. (IC (Comput ((ProgramPart s1),s1,6))) = (Comput ((ProgramPart s1),s1,6)) . (IC (Comput ((ProgramPart s1),s1,6))) by COMPOS_1:38;
A59: IC (Comput ((ProgramPart s1),s1,6)) = succ (IC (Comput ((ProgramPart s1),s1,5))) by A54, SCMPDS_2:60
.= 10 + 1 by A52 ;
then A60: CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,6))),(Comput ((ProgramPart s1),s1,6))) = s1 . 11 by Y, AMI_1:54
.= saveIC (SBP,RetIC) by A1, Lm1 ;
T: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,6)) by AMI_1:123;
A61: Comput ((ProgramPart s1),s1,(6 + 1)) = Following ((ProgramPart s1),(Comput ((ProgramPart s1),s1,6))) by EXTPRO_1:4
.= Exec ((saveIC (SBP,RetIC)),(Comput ((ProgramPart s1),s1,6))) by A60, T ;
Y: (ProgramPart (Comput ((ProgramPart s2),s2,6))) /. (IC (Comput ((ProgramPart s2),s2,6))) = (Comput ((ProgramPart s2),s2,6)) . (IC (Comput ((ProgramPart s2),s2,6))) by COMPOS_1:38;
A62: IC (Comput ((ProgramPart s2),s2,6)) = succ (IC (Comput ((ProgramPart s2),s2,5))) by A58, SCMPDS_2:60
.= 10 + 1 by A56 ;
then A63: CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,6))),(Comput ((ProgramPart s2),s2,6))) = s2 . 11 by Y, AMI_1:54
.= saveIC (SBP,RetIC) by A2, Lm1 ;
T: ProgramPart s2 = ProgramPart (Comput ((ProgramPart s2),s2,6)) by AMI_1:123;
A64: Comput ((ProgramPart s2),s2,(6 + 1)) = Following ((ProgramPart s2),(Comput ((ProgramPart s2),s2,6))) by EXTPRO_1:4
.= Exec ((saveIC (SBP,RetIC)),(Comput ((ProgramPart s2),s2,6))) by A63, T ;
A65: 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 s1 . b = s2 . b ; :: thesis: (Comput ((ProgramPart s1),s1,1)) . b = (Comput ((ProgramPart s2),s2,1)) . b
hence (Comput ((ProgramPart s1),s1,1)) . b = s2 . b by A12, SCMPDS_2:68
.= (Comput ((ProgramPart s2),s2,1)) . b by A13, SCMPDS_2:68 ;
:: thesis: verum
end;
A66: for b being Int_position st s1 . b = s2 . b holds
(Comput ((ProgramPart s1),s1,2)) . b = (Comput ((ProgramPart s2),s2,2)) . b
proof
let b be Int_position ; :: thesis: ( s1 . b = s2 . b implies (Comput ((ProgramPart s1),s1,2)) . b = (Comput ((ProgramPart s2),s2,2)) . b )
assume A67: s1 . b = s2 . b ; :: thesis: (Comput ((ProgramPart s1),s1,2)) . b = (Comput ((ProgramPart s2),s2,2)) . b
per cases ( b = DataLoc (((Comput ((ProgramPart s1),s1,1)) . SBP),6) or b <> DataLoc (((Comput ((ProgramPart s1),s1,1)) . SBP),6) ) ;
suppose A68: b = DataLoc (((Comput ((ProgramPart s1),s1,1)) . SBP),6) ; :: thesis: (Comput ((ProgramPart s1),s1,2)) . b = (Comput ((ProgramPart s2),s2,2)) . b
then A69: b = DataLoc (((Comput ((ProgramPart s2),s2,1)) . SBP),6) by A8, A65;
thus (Comput ((ProgramPart s1),s1,2)) . b = (Comput ((ProgramPart s1),s1,1)) . (DataLoc ((s1 . SBP),3)) by A4, A16, A17, A68, SCMPDS_2:59
.= (Comput ((ProgramPart s2),s2,1)) . (DataLoc (((Comput ((ProgramPart s1),s1,1)) . SBP),3)) by A4, A11, A17, A65
.= (Comput ((ProgramPart s2),s2,1)) . (DataLoc (((Comput ((ProgramPart s2),s2,1)) . SBP),3)) by A8, A65
.= (Comput ((ProgramPart s2),s2,2)) . b by A21, A69, SCMPDS_2:59 ; :: thesis: verum
end;
suppose A70: b <> DataLoc (((Comput ((ProgramPart s1),s1,1)) . SBP),6) ; :: thesis: (Comput ((ProgramPart s1),s1,2)) . b = (Comput ((ProgramPart s2),s2,2)) . b
then A71: b <> DataLoc (((Comput ((ProgramPart s2),s2,1)) . SBP),6) by A8, A65;
thus (Comput ((ProgramPart s1),s1,2)) . b = (Comput ((ProgramPart s1),s1,1)) . b by A16, A70, SCMPDS_2:59
.= (Comput ((ProgramPart s2),s2,1)) . b by A65, A67
.= (Comput ((ProgramPart s2),s2,2)) . b by A21, A71, SCMPDS_2:59 ; :: thesis: verum
end;
end;
end;
A72: now
let b be Int_position ; :: thesis: ( s1 . b = s2 . b implies (Comput ((ProgramPart s1),s1,3)) . b1 = (Comput ((ProgramPart s2),s2,3)) . b1 )
assume A73: s1 . b = s2 . b ; :: thesis: (Comput ((ProgramPart s1),s1,3)) . b1 = (Comput ((ProgramPart s2),s2,3)) . b1
set x1 = DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),2);
set x2 = DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),3);
set y1 = DataLoc (((Comput ((ProgramPart s2),s2,2)) . SBP),2);
set y2 = DataLoc (((Comput ((ProgramPart s2),s2,2)) . SBP),3);
A74: DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),2) = DataLoc (((Comput ((ProgramPart s2),s2,2)) . SBP),2) by A8, A66;
A75: DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),3) = DataLoc (((Comput ((ProgramPart s2),s2,2)) . SBP),3) by A8, A66;
per cases ( ( b <> DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),2) & b <> DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),3) ) or b = DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),2) or b = DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),3) ) ;
suppose A76: ( b <> DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),2) & b <> DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),3) ) ; :: thesis: (Comput ((ProgramPart s1),s1,3)) . b1 = (Comput ((ProgramPart s2),s2,3)) . b1
hence (Comput ((ProgramPart s1),s1,3)) . b = (Comput ((ProgramPart s1),s1,2)) . b by A24, SCMPDS_2:64
.= (Comput ((ProgramPart s2),s2,2)) . b by A66, A73
.= (Comput ((ProgramPart s2),s2,3)) . b by A30, A74, A75, A76, SCMPDS_2:64 ;
:: thesis: verum
end;
suppose A77: b = DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),2) ; :: thesis: (Comput ((ProgramPart s1),s1,3)) . b1 = (Comput ((ProgramPart s2),s2,3)) . b1
A78: n + 2 <> n + 3 ;
then A79: DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),2) <> DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),3) by A34, A36, AMI_3:52;
A80: DataLoc (((Comput ((ProgramPart s2),s2,2)) . SBP),2) <> DataLoc (((Comput ((ProgramPart s2),s2,2)) . SBP),3) by A34, A36, A74, A75, A78, AMI_3:52;
thus (Comput ((ProgramPart s1),s1,3)) . b = ((Comput ((ProgramPart s1),s1,2)) . (DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),2))) div ((Comput ((ProgramPart s1),s1,2)) . (DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),3))) by A24, A77, A79, SCMPDS_2:64
.= ((Comput ((ProgramPart s2),s2,2)) . (DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),2))) div ((Comput ((ProgramPart s1),s1,2)) . (DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),3))) by A4, A10, A26, A66
.= ((Comput ((ProgramPart s2),s2,2)) . (DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),2))) div ((Comput ((ProgramPart s2),s2,2)) . (DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),3))) by A4, A11, A26, A66
.= (Comput ((ProgramPart s2),s2,3)) . b by A30, A74, A75, A77, A80, SCMPDS_2:64 ; :: thesis: verum
end;
suppose A81: b = DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),3) ; :: thesis: (Comput ((ProgramPart s1),s1,3)) . b1 = (Comput ((ProgramPart s2),s2,3)) . b1
hence (Comput ((ProgramPart s1),s1,3)) . b = ((Comput ((ProgramPart s1),s1,2)) . (DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),2))) mod ((Comput ((ProgramPart s1),s1,2)) . (DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),3))) by A24, SCMPDS_2:64
.= ((Comput ((ProgramPart s2),s2,2)) . (DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),2))) mod ((Comput ((ProgramPart s1),s1,2)) . (DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),3))) by A4, A10, A26, A66
.= ((Comput ((ProgramPart s2),s2,2)) . (DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),2))) mod ((Comput ((ProgramPart s2),s2,2)) . (DataLoc (((Comput ((ProgramPart s1),s1,2)) . SBP),3))) by A4, A11, A26, A66
.= (Comput ((ProgramPart s2),s2,3)) . b by A30, A74, A75, A81, SCMPDS_2:64 ;
:: thesis: verum
end;
end;
end;
A82: now
let b be Int_position ; :: thesis: ( s1 . b = s2 . b implies (Comput ((ProgramPart s1),s1,4)) . b1 = (Comput ((ProgramPart s2),s2,4)) . b1 )
assume A83: s1 . b = s2 . b ; :: thesis: (Comput ((ProgramPart s1),s1,4)) . b1 = (Comput ((ProgramPart s2),s2,4)) . b1
per cases ( b = DataLoc (((Comput ((ProgramPart s1),s1,3)) . SBP),7) or b <> DataLoc (((Comput ((ProgramPart s1),s1,3)) . SBP),7) ) ;
suppose A84: b = DataLoc (((Comput ((ProgramPart s1),s1,3)) . SBP),7) ; :: thesis: (Comput ((ProgramPart s1),s1,4)) . b1 = (Comput ((ProgramPart s2),s2,4)) . b1
then A85: b = DataLoc (((Comput ((ProgramPart s2),s2,3)) . SBP),7) by A8, A72;
thus (Comput ((ProgramPart s1),s1,4)) . b = (Comput ((ProgramPart s1),s1,3)) . (DataLoc (((Comput ((ProgramPart s1),s1,3)) . SBP),3)) by A33, A84, SCMPDS_2:59
.= (Comput ((ProgramPart s2),s2,3)) . (DataLoc (((Comput ((ProgramPart s1),s1,3)) . SBP),3)) by A4, A11, A37, A72
.= (Comput ((ProgramPart s2),s2,3)) . (DataLoc (((Comput ((ProgramPart s2),s2,3)) . SBP),3)) by A8, A72
.= (Comput ((ProgramPart s2),s2,4)) . b by A42, A85, SCMPDS_2:59 ; :: thesis: verum
end;
suppose A86: b <> DataLoc (((Comput ((ProgramPart s1),s1,3)) . SBP),7) ; :: thesis: (Comput ((ProgramPart s1),s1,4)) . b1 = (Comput ((ProgramPart s2),s2,4)) . b1
then A87: b <> DataLoc (((Comput ((ProgramPart s2),s2,3)) . SBP),7) by A8, A72;
thus (Comput ((ProgramPart s1),s1,4)) . b = (Comput ((ProgramPart s1),s1,3)) . b by A33, A86, SCMPDS_2:59
.= (Comput ((ProgramPart s2),s2,3)) . b by A72, A83
.= (Comput ((ProgramPart s2),s2,4)) . b by A42, A87, SCMPDS_2:59 ; :: thesis: verum
end;
end;
end;
A88: now
let b be Int_position ; :: thesis: ( s1 . b = s2 . b implies (Comput ((ProgramPart s1),s1,5)) . b1 = (Comput ((ProgramPart s2),s2,5)) . b1 )
assume A89: s1 . b = s2 . b ; :: thesis: (Comput ((ProgramPart s1),s1,5)) . b1 = (Comput ((ProgramPart s2),s2,5)) . b1
A90: s1 . (DataLoc (((Comput ((ProgramPart s1),s1,4)) . GBP),1)) = s2 . (intpos (0 + 1)) by A8, A48, Th5
.= s2 . (DataLoc (((Comput ((ProgramPart s1),s1,4)) . GBP),1)) by A48, Th5 ;
per cases ( b = DataLoc (((Comput ((ProgramPart s1),s1,4)) . SBP),(4 + RetSP)) or b <> DataLoc (((Comput ((ProgramPart s1),s1,4)) . SBP),(4 + RetSP)) ) ;
suppose A91: b = DataLoc (((Comput ((ProgramPart s1),s1,4)) . SBP),(4 + RetSP)) ; :: thesis: (Comput ((ProgramPart s1),s1,5)) . b1 = (Comput ((ProgramPart s2),s2,5)) . b1
then A92: b = DataLoc (((Comput ((ProgramPart s2),s2,4)) . SBP),(4 + RetSP)) by A8, A82;
thus (Comput ((ProgramPart s1),s1,5)) . b = (Comput ((ProgramPart s1),s1,4)) . (DataLoc (((Comput ((ProgramPart s1),s1,4)) . GBP),1)) by A45, A91, SCMPDS_2:59
.= (Comput ((ProgramPart s2),s2,4)) . (DataLoc (((Comput ((ProgramPart s1),s1,4)) . GBP),1)) by A82, A90
.= (Comput ((ProgramPart s2),s2,4)) . (DataLoc (((Comput ((ProgramPart s2),s2,4)) . GBP),1)) by A5, A9, A82
.= (Comput ((ProgramPart s2),s2,5)) . b by A51, A92, SCMPDS_2:59 ; :: thesis: verum
end;
suppose A93: b <> DataLoc (((Comput ((ProgramPart s1),s1,4)) . SBP),(4 + RetSP)) ; :: thesis: (Comput ((ProgramPart s1),s1,5)) . b1 = (Comput ((ProgramPart s2),s2,5)) . b1
then A94: b <> DataLoc (((Comput ((ProgramPart s2),s2,4)) . SBP),(4 + RetSP)) by A8, A82;
thus (Comput ((ProgramPart s1),s1,5)) . b = (Comput ((ProgramPart s1),s1,4)) . b by A45, A93, SCMPDS_2:59
.= (Comput ((ProgramPart s2),s2,4)) . b by A82, A89
.= (Comput ((ProgramPart s2),s2,5)) . b by A51, A94, SCMPDS_2:59 ; :: thesis: verum
end;
end;
end;
A95: now
let b be Int_position ; :: thesis: ( s1 . b = s2 . b implies (Comput ((ProgramPart s1),s1,6)) . b1 = (Comput ((ProgramPart s2),s2,6)) . b1 )
assume A96: s1 . b = s2 . b ; :: thesis: (Comput ((ProgramPart s1),s1,6)) . b1 = (Comput ((ProgramPart s2),s2,6)) . b1
A97: s1 . (DataLoc (((Comput ((ProgramPart s1),s1,5)) . GBP),1)) = s2 . (intpos (0 + 1)) by A8, A55, Th5
.= s2 . (DataLoc (((Comput ((ProgramPart s1),s1,5)) . GBP),1)) by A55, Th5 ;
per cases ( b = DataLoc (((Comput ((ProgramPart s1),s1,5)) . GBP),1) or b <> DataLoc (((Comput ((ProgramPart s1),s1,5)) . GBP),1) ) ;
suppose A98: b = DataLoc (((Comput ((ProgramPart s1),s1,5)) . GBP),1) ; :: thesis: (Comput ((ProgramPart s1),s1,6)) . b1 = (Comput ((ProgramPart s2),s2,6)) . b1
then A99: b = DataLoc (((Comput ((ProgramPart s2),s2,5)) . GBP),1) by A5, A9, A88;
thus (Comput ((ProgramPart s1),s1,6)) . b = ((Comput ((ProgramPart s1),s1,5)) . (DataLoc (((Comput ((ProgramPart s1),s1,5)) . GBP),1))) + 4 by A54, A98, SCMPDS_2:60
.= ((Comput ((ProgramPart s2),s2,5)) . (DataLoc (((Comput ((ProgramPart s1),s1,5)) . GBP),1))) + 4 by A88, A97
.= ((Comput ((ProgramPart s2),s2,5)) . (DataLoc (((Comput ((ProgramPart s2),s2,5)) . GBP),1))) + 4 by A5, A9, A88
.= (Comput ((ProgramPart s2),s2,6)) . b by A58, A99, SCMPDS_2:60 ; :: thesis: verum
end;
suppose A100: b <> DataLoc (((Comput ((ProgramPart s1),s1,5)) . GBP),1) ; :: thesis: (Comput ((ProgramPart s1),s1,6)) . b1 = (Comput ((ProgramPart s2),s2,6)) . b1
then A101: b <> DataLoc (((Comput ((ProgramPart s2),s2,5)) . GBP),1) by A5, A9, A88;
thus (Comput ((ProgramPart s1),s1,6)) . b = (Comput ((ProgramPart s1),s1,5)) . b by A54, A100, SCMPDS_2:60
.= (Comput ((ProgramPart s2),s2,5)) . b by A88, A96
.= (Comput ((ProgramPart s2),s2,6)) . b by A58, A101, SCMPDS_2:60 ; :: thesis: verum
end;
end;
end;
A102: now
let b be Int_position ; :: thesis: ( s1 . b = s2 . b implies (Comput ((ProgramPart s1),s1,7)) . b1 = (Comput ((ProgramPart s2),s2,7)) . b1 )
assume A103: s1 . b = s2 . b ; :: thesis: (Comput ((ProgramPart s1),s1,7)) . b1 = (Comput ((ProgramPart s2),s2,7)) . b1
per cases ( b = DataLoc (((Comput ((ProgramPart s1),s1,6)) . SBP),RetIC) or b <> DataLoc (((Comput ((ProgramPart s1),s1,6)) . SBP),RetIC) ) ;
suppose A104: b = DataLoc (((Comput ((ProgramPart s1),s1,6)) . SBP),RetIC) ; :: thesis: (Comput ((ProgramPart s1),s1,7)) . b1 = (Comput ((ProgramPart s2),s2,7)) . b1
then A105: b = DataLoc (((Comput ((ProgramPart s2),s2,6)) . SBP),RetIC) by A8, A95;
thus (Comput ((ProgramPart s1),s1,7)) . b = IC (Comput ((ProgramPart s1),s1,6)) by A61, A104, SCMPDS_2:71
.= (Comput ((ProgramPart s2),s2,7)) . b by A59, A62, A64, A105, SCMPDS_2:71 ; :: thesis: verum
end;
suppose A106: b <> DataLoc (((Comput ((ProgramPart s1),s1,6)) . SBP),RetIC) ; :: thesis: (Comput ((ProgramPart s1),s1,7)) . b1 = (Comput ((ProgramPart s2),s2,7)) . b1
then A107: b <> DataLoc (((Comput ((ProgramPart s2),s2,6)) . SBP),RetIC) by A8, A95;
thus (Comput ((ProgramPart s1),s1,7)) . b = (Comput ((ProgramPart s1),s1,6)) . b by A61, A106, SCMPDS_2:71
.= (Comput ((ProgramPart s2),s2,6)) . b by A95, A103
.= (Comput ((ProgramPart s2),s2,7)) . b by A64, A107, 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 (Comput ((ProgramPart s1),s1,b2)) = IC (Comput ((ProgramPart s2),s2,b2)) & (Comput ((ProgramPart s1),s1,b2)) . b3 = (Comput ((ProgramPart s2),s2,b2)) . b3 )
let a be Int_position ; :: thesis: ( k <= 7 & s1 . a = s2 . a implies ( IC (Comput ((ProgramPart s1),s1,b1)) = IC (Comput ((ProgramPart s2),s2,b1)) & (Comput ((ProgramPart s1),s1,b1)) . b2 = (Comput ((ProgramPart s2),s2,b1)) . b2 ) )
assume that
A108: k <= 7 and
A109: s1 . a = s2 . a ; :: thesis: ( IC (Comput ((ProgramPart s1),s1,b1)) = IC (Comput ((ProgramPart s2),s2,b1)) & (Comput ((ProgramPart s1),s1,b1)) . b2 = (Comput ((ProgramPart s2),s2,b1)) . b2 )
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 A108, NAT_1:32;
suppose A110: k = 0 ; :: thesis: ( IC (Comput ((ProgramPart s1),s1,b1)) = IC (Comput ((ProgramPart s2),s2,b1)) & (Comput ((ProgramPart s1),s1,b1)) . b2 = (Comput ((ProgramPart s2),s2,b1)) . b2 )
hence IC (Comput ((ProgramPart s1),s1,k)) = IC s1 by EXTPRO_1:3
.= IC (Comput ((ProgramPart s2),s2,k)) by A7, A110, 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 A110, EXTPRO_1:3
.= (Comput ((ProgramPart s2),s2,k)) . a by A109, A110, EXTPRO_1:3 ; :: thesis: verum
end;
suppose A111: k = 1 ; :: thesis: ( IC (Comput ((ProgramPart s1),s1,b1)) = IC (Comput ((ProgramPart s2),s2,b1)) & (Comput ((ProgramPart s1),s1,b1)) . b2 = (Comput ((ProgramPart s2),s2,b1)) . b2 )
hence IC (Comput ((ProgramPart s1),s1,k)) = IC (Comput ((ProgramPart s2),s2,k)) by A14, A19; :: 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 A65, A109, A111; :: thesis: verum
end;
suppose A112: k = 2 ; :: thesis: ( IC (Comput ((ProgramPart s1),s1,b1)) = IC (Comput ((ProgramPart s2),s2,b1)) & (Comput ((ProgramPart s1),s1,b1)) . b2 = (Comput ((ProgramPart s2),s2,b1)) . b2 )
hence IC (Comput ((ProgramPart s1),s1,k)) = IC (Comput ((ProgramPart s2),s2,k)) by A22, 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 A66, A109, A112; :: thesis: verum
end;
suppose A113: k = 3 ; :: thesis: ( IC (Comput ((ProgramPart s1),s1,b1)) = IC (Comput ((ProgramPart s2),s2,b1)) & (Comput ((ProgramPart s1),s1,b1)) . b2 = (Comput ((ProgramPart s2),s2,b1)) . b2 )
hence IC (Comput ((ProgramPart s1),s1,k)) = IC (Comput ((ProgramPart s2),s2,k)) by A31, A40; :: 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 A72, A109, A113; :: thesis: verum
end;
suppose A114: k = 4 ; :: thesis: ( IC (Comput ((ProgramPart s1),s1,b1)) = IC (Comput ((ProgramPart s2),s2,b1)) & (Comput ((ProgramPart s1),s1,b1)) . b2 = (Comput ((ProgramPart s2),s2,b1)) . b2 )
hence IC (Comput ((ProgramPart s1),s1,k)) = IC (Comput ((ProgramPart s2),s2,k)) by A43, A49; :: 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 A82, A109, A114; :: thesis: verum
end;
suppose A115: k = 5 ; :: thesis: ( IC (Comput ((ProgramPart s1),s1,b1)) = IC (Comput ((ProgramPart s2),s2,b1)) & (Comput ((ProgramPart s1),s1,b1)) . b2 = (Comput ((ProgramPart s2),s2,b1)) . b2 )
hence IC (Comput ((ProgramPart s1),s1,k)) = IC (Comput ((ProgramPart s2),s2,k)) by A52, A56; :: 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 A88, A109, A115; :: thesis: verum
end;
suppose A116: k = 6 ; :: thesis: ( IC (Comput ((ProgramPart s1),s1,b1)) = IC (Comput ((ProgramPart s2),s2,b1)) & (Comput ((ProgramPart s1),s1,b1)) . b2 = (Comput ((ProgramPart s2),s2,b1)) . b2 )
hence IC (Comput ((ProgramPart s1),s1,k)) = IC (Comput ((ProgramPart s2),s2,k)) by A59, A62; :: 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 A95, A109, A116; :: thesis: verum
end;
suppose A117: k = 7 ; :: thesis: ( IC (Comput ((ProgramPart s1),s1,b1)) = IC (Comput ((ProgramPart s2),s2,b1)) & (Comput ((ProgramPart s1),s1,b1)) . b2 = (Comput ((ProgramPart s2),s2,b1)) . b2 )
hence IC (Comput ((ProgramPart s1),s1,k)) = succ (IC (Comput ((ProgramPart s2),s2,6))) by A59, A61, A62, SCMPDS_2:71
.= IC (Comput ((ProgramPart s2),s2,k)) by A64, A117, SCMPDS_2:71 ;
:: 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 A102, A109, A117; :: thesis: verum
end;
end;
end;