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, SCMPDS_4:57;
A6: GCD-Algorithm c= s2 by A2, SCMPDS_4:57;
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 AMI_1:14
.= Following (ProgramPart s1),s1 by AMI_1:13
.= 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 AMI_1:14
.= Following (ProgramPart s2),s2 by AMI_1:13
.= 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 AMI_1:14
.= 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 AMI_1:14
.= 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 AMI_1:14
.= 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 AMI_1:14
.= 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 AMI_1:14
.= 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 AMI_1:14
.= 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) . b1 = (Comput (ProgramPart s2),s2,1) . b1 )
assume A32: s1 . b = s2 . b ; :: thesis: (Comput (ProgramPart s1),s1,1) . b1 = (Comput (ProgramPart s2),s2,1) . b1
per cases ( b = GBP or b <> GBP ) ;
suppose A33: b = GBP ; :: thesis: (Comput (ProgramPart s1),s1,1) . b1 = (Comput (ProgramPart s2),s2,1) . b1
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) . b1 = (Comput (ProgramPart s2),s2,1) . b1
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) . b1 = (Comput (ProgramPart s2),s2,2) . b1 )
assume A36: s1 . b = s2 . b ; :: thesis: (Comput (ProgramPart s1),s1,2) . b1 = (Comput (ProgramPart s2),s2,2) . b1
per cases ( b = SBP or b <> SBP ) ;
suppose A37: b = SBP ; :: thesis: (Comput (ProgramPart s1),s1,2) . b1 = (Comput (ProgramPart s2),s2,2) . b1
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) . b1 = (Comput (ProgramPart s2),s2,2) . b1
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) . b1 = (Comput (ProgramPart s2),s2,3) . b1 )
assume A40: s1 . b = s2 . b ; :: thesis: (Comput (ProgramPart s1),s1,3) . b1 = (Comput (ProgramPart s2),s2,3) . b1
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) . b1 = (Comput (ProgramPart s2),s2,3) . b1
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) . b1 = (Comput (ProgramPart s2),s2,3) . b1
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 AMI_1:13
.= IC (Comput (ProgramPart s2),s2,k) by A7, A9, A43, AMI_1:13 ;
:: thesis: (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a
thus (Comput (ProgramPart s1),s1,k) . a = s1 . a by A43, AMI_1:13
.= (Comput (ProgramPart s2),s2,k) . a by A3, A43, AMI_1:13 ; :: 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;