let s1, s2 be State of SCMPDS ; :: thesis: for a being Int_position
for k being Element of NAT st Initialized GCD-Algorithm c= s1 & Initialized GCD-Algorithm c= s2 & s1 . a = s2 . a & k <= 4 holds
( IC (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a )
let a be Int_position ; :: thesis: for k being Element of NAT st Initialized GCD-Algorithm c= s1 & Initialized GCD-Algorithm c= s2 & s1 . a = s2 . a & k <= 4 holds
( IC (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a )
let k be Element of NAT ; :: thesis: ( Initialized GCD-Algorithm c= s1 & Initialized GCD-Algorithm c= s2 & s1 . a = s2 . a & k <= 4 implies ( IC (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a ) )
set GA = GCD-Algorithm ;
assume A1: ( Initialized GCD-Algorithm c= s1 & Initialized GCD-Algorithm c= s2 ) ; :: thesis: ( not s1 . a = s2 . a or not k <= 4 or ( IC (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a ) )
assume A2: ( s1 . a = s2 . a & k <= 4 ) ; :: thesis: ( IC (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a )
A3: ( GCD-Algorithm c= s1 & GCD-Algorithm c= s2 ) by A1, SCMPDS_4:57;
A4: IC s1 = inspos 0 by A1, SCMPDS_5:18;
A5: Computation s1,(0 + 1) = Following (Computation s1,0 ) by AMI_1:14
.= Following s1 by AMI_1:13
.= Exec (GBP := 0 ),s1 by A3, A4, Lm1 ;
A6: IC s2 = inspos 0 by A1, SCMPDS_5:18;
A7: Computation s2,(0 + 1) = Following (Computation s2,0 ) by AMI_1:14
.= Following s2 by AMI_1:13
.= Exec (GBP := 0 ),s2 by A3, A6, Lm1 ;
A8: IC (Computation s1,1) = Next (IC s1) by A5, SCMPDS_2:57
.= inspos (0 + 1) by A4 ;
then A9: CurInstr (Computation s1,1) = s1 . (inspos 1) by AMI_1:54
.= SBP := 7 by A3, Lm1 ;
A10: Computation s1,(1 + 1) = Following (Computation s1,1) by AMI_1:14
.= Exec (SBP := 7),(Computation s1,1) by A9 ;
A11: IC (Computation s2,1) = Next (IC s2) by A7, SCMPDS_2:57
.= inspos (0 + 1) by A6 ;
then A12: CurInstr (Computation s2,1) = s2 . (inspos 1) by AMI_1:54
.= SBP := 7 by A3, Lm1 ;
A13: Computation s2,(1 + 1) = Following (Computation s2,1) by AMI_1:14
.= Exec (SBP := 7),(Computation s2,1) by A12 ;
A14: IC (Computation s1,2) = Next (IC (Computation s1,1)) by A10, SCMPDS_2:57
.= inspos (1 + 1) by A8 ;
then A15: CurInstr (Computation s1,2) = s1 . (inspos 2) by AMI_1:54
.= saveIC SBP ,RetIC by A3, Lm1 ;
A16: Computation s1,(2 + 1) = Following (Computation s1,2) by AMI_1:14
.= Exec (saveIC SBP ,RetIC ),(Computation s1,2) by A15 ;
A17: (Computation s1,2) . SBP = 7 by A10, SCMPDS_2:57;
A18: IC (Computation s2,2) = Next (IC (Computation s2,1)) by A13, SCMPDS_2:57
.= inspos (1 + 1) by A11 ;
then A19: CurInstr (Computation s2,2) = s2 . (inspos 2) by AMI_1:54
.= saveIC SBP ,RetIC by A3, Lm1 ;
A20: Computation s2,(2 + 1) = Following (Computation s2,2) by AMI_1:14
.= Exec (saveIC SBP ,RetIC ),(Computation s2,2) by A19 ;
A21: (Computation s2,2) . SBP = 7 by A13, SCMPDS_2:57;
A22: IC (Computation s1,3) = Next (IC (Computation s1,2)) by A16, SCMPDS_2:71
.= inspos (2 + 1) by A14 ;
then A23: CurInstr (Computation s1,3) = s1 . (inspos 3) by AMI_1:54
.= goto 2 by A3, Lm1 ;
A24: Computation s1,(3 + 1) = Following (Computation s1,3) by AMI_1:14
.= Exec (goto 2),(Computation s1,3) by A23 ;
A25: IC (Computation s2,3) = Next (IC (Computation s2,2)) by A20, SCMPDS_2:71
.= inspos (2 + 1) by A18 ;
then A26: CurInstr (Computation s2,3) = s2 . (inspos 3) by AMI_1:54
.= goto 2 by A3, Lm1 ;
A27: Computation s2,(3 + 1) = Following (Computation s2,3) by AMI_1:14
.= Exec (goto 2),(Computation s2,3) by A26 ;
A28: now
let b be Int_position ; :: thesis: ( s1 . b = s2 . b implies (Computation s1,1) . b1 = (Computation s2,1) . b1 )
assume A29: s1 . b = s2 . b ; :: thesis: (Computation s1,1) . b1 = (Computation s2,1) . b1
per cases ( b = GBP or b <> GBP ) ;
suppose A30: b = GBP ; :: thesis: (Computation s1,1) . b1 = (Computation s2,1) . b1
hence (Computation s1,1) . b = 0 by A5, SCMPDS_2:57
.= (Computation s2,1) . b by A7, A30, SCMPDS_2:57 ;
:: thesis: verum
end;
suppose A31: b <> GBP ; :: thesis: (Computation s1,1) . b1 = (Computation s2,1) . b1
hence (Computation s1,1) . b = s1 . b by A5, SCMPDS_2:57
.= (Computation s2,1) . b by A7, A29, A31, SCMPDS_2:57 ;
:: thesis: verum
end;
end;
end;
A32: now
let b be Int_position ; :: thesis: ( s1 . b = s2 . b implies (Computation s1,2) . b1 = (Computation s2,2) . b1 )
assume A33: s1 . b = s2 . b ; :: thesis: (Computation s1,2) . b1 = (Computation s2,2) . b1
per cases ( b = SBP or b <> SBP ) ;
suppose A34: b = SBP ; :: thesis: (Computation s1,2) . b1 = (Computation s2,2) . b1
hence (Computation s1,2) . b = 7 by A10, SCMPDS_2:57
.= (Computation s2,2) . b by A13, A34, SCMPDS_2:57 ;
:: thesis: verum
end;
suppose A35: b <> SBP ; :: thesis: (Computation s1,2) . b1 = (Computation s2,2) . b1
hence (Computation s1,2) . b = (Computation s1,1) . b by A10, SCMPDS_2:57
.= (Computation s2,1) . b by A28, A33
.= (Computation s2,2) . b by A13, A35, SCMPDS_2:57 ;
:: thesis: verum
end;
end;
end;
A36: now
let b be Int_position ; :: thesis: ( s1 . b = s2 . b implies (Computation s1,3) . b1 = (Computation s2,3) . b1 )
assume A37: s1 . b = s2 . b ; :: thesis: (Computation s1,3) . b1 = (Computation s2,3) . b1
per cases ( b = DataLoc ((Computation s1,2) . SBP ),RetIC or b <> DataLoc ((Computation s1,2) . SBP ),RetIC ) ;
suppose A38: b = DataLoc ((Computation s1,2) . SBP ),RetIC ; :: thesis: (Computation s1,3) . b1 = (Computation s2,3) . b1
hence (Computation s1,3) . b = IC (Computation s1,2) by A16, SCMPDS_2:71
.= (Computation s2,3) . b by A14, A17, A18, A20, A21, A38, SCMPDS_2:71 ;
:: thesis: verum
end;
suppose A39: b <> DataLoc ((Computation s1,2) . SBP ),RetIC ; :: thesis: (Computation s1,3) . b1 = (Computation s2,3) . b1
hence (Computation s1,3) . b = (Computation s1,2) . b by A16, SCMPDS_2:71
.= (Computation s2,2) . b by A32, A37
.= (Computation s2,3) . b by A17, A20, A21, A39, 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 A2, NAT_1:29;
suppose A40: k = 0 ; :: thesis: ( IC (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a )
hence IC (Computation s1,k) = IC s1 by AMI_1:13
.= IC (Computation s2,k) by A4, A6, A40, AMI_1:13 ;
:: thesis: (Computation s1,k) . a = (Computation s2,k) . a
thus (Computation s1,k) . a = s1 . a by A40, AMI_1:13
.= (Computation s2,k) . a by A2, A40, AMI_1:13 ; :: thesis: verum
end;
suppose A41: k = 1 ; :: thesis: ( IC (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a )
hence IC (Computation s1,k) = IC (Computation s2,k) by A8, A11; :: thesis: (Computation s1,k) . a = (Computation s2,k) . a
thus (Computation s1,k) . a = (Computation s2,k) . a by A2, A28, A41; :: thesis: verum
end;
suppose A42: k = 2 ; :: thesis: ( IC (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a )
hence IC (Computation s1,k) = IC (Computation s2,k) by A14, A18; :: thesis: (Computation s1,k) . a = (Computation s2,k) . a
thus (Computation s1,k) . a = (Computation s2,k) . a by A2, A32, A42; :: thesis: verum
end;
suppose A43: k = 3 ; :: thesis: ( IC (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a )
hence IC (Computation s1,k) = IC (Computation s2,k) by A22, A25; :: thesis: (Computation s1,k) . a = (Computation s2,k) . a
thus (Computation s1,k) . a = (Computation s2,k) . a by A2, A36, A43; :: thesis: verum
end;
suppose A44: k = 4 ; :: thesis: ( IC (Computation s1,k) = IC (Computation s2,k) & (Computation s1,k) . a = (Computation s2,k) . a )
hence IC (Computation s1,k) = ICplusConst (Computation s1,3),2 by A24, SCMPDS_2:66
.= inspos (3 + 2) by A22, SCMPDS_6:23
.= ICplusConst (Computation s2,3),2 by A25, SCMPDS_6:23
.= IC (Computation s2,k) by A27, A44, SCMPDS_2:66 ;
:: thesis: (Computation s1,k) . a = (Computation s2,k) . a
thus (Computation s1,k) . a = (Computation s1,3) . a by A24, A44, SCMPDS_2:66
.= (Computation s2,3) . a by A2, A36
.= (Computation s2,k) . a by A27, A44, SCMPDS_2:66 ; :: thesis: verum
end;
end;