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