let P1, P2 be Instruction-Sequence of SCMPDS; :: thesis: for s1, s2 being State of SCMPDS
for a being Int_position
for k being Nat st Start-At (0,SCMPDS) c= s1 & Start-At (0,SCMPDS) c= s2 & GCD-Algorithm c= P1 & GCD-Algorithm c= P2 & s1 . a = s2 . a & k <= 4 holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a )
let s1, s2 be State of SCMPDS; :: thesis: for a being Int_position
for k being Nat st Start-At (0,SCMPDS) c= s1 & Start-At (0,SCMPDS) c= s2 & GCD-Algorithm c= P1 & GCD-Algorithm c= P2 & s1 . a = s2 . a & k <= 4 holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a )
let a be Int_position; :: thesis: for k being Nat st Start-At (0,SCMPDS) c= s1 & Start-At (0,SCMPDS) c= s2 & GCD-Algorithm c= P1 & GCD-Algorithm c= P2 & s1 . a = s2 . a & k <= 4 holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a )
let k be Nat; :: thesis: ( Start-At (0,SCMPDS) c= s1 & Start-At (0,SCMPDS) c= s2 & GCD-Algorithm c= P1 & GCD-Algorithm c= P2 & s1 . a = s2 . a & k <= 4 implies ( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a ) )
set GA = GCD-Algorithm ;
assume that
A1: Start-At (0,SCMPDS) c= s1 and
A2: Start-At (0,SCMPDS) c= s2 and
A3: GCD-Algorithm c= P1 and
A4: GCD-Algorithm c= P2 ; :: thesis: ( not s1 . a = s2 . a or not k <= 4 or ( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a ) )
assume that
A5: s1 . a = s2 . a and
A6: k <= 4 ; :: thesis: ( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a )
A7: IC s1 = 0 by A1, MEMSTR_0:39;
A8: P1 /. (IC s1) = P1 . (IC s1) by PBOOLE:143;
A9: Comput (P1,s1,(0 + 1)) = Following (P1,(Comput (P1,s1,0))) by EXTPRO_1:3
.= Following (P1,s1) by EXTPRO_1:2
.= Exec ((GBP := 0),s1) by A7, Lm1, A8, A3 ;
A10: IC s2 = 0 by A2, MEMSTR_0:39;
A11: P2 /. (IC s2) = P2 . (IC s2) by PBOOLE:143;
A12: Comput (P2,s2,(0 + 1)) = Following (P2,(Comput (P2,s2,0))) by EXTPRO_1:3
.= Following (P2,s2) by EXTPRO_1:2
.= Exec ((GBP := 0),s2) by A10, Lm1, A11, A4 ;
A13: P1 /. (IC (Comput (P1,s1,1))) = P1 . (IC (Comput (P1,s1,1))) by PBOOLE:143;
A14: IC (Comput (P1,s1,1)) = (IC s1) + 1 by A9, SCMPDS_2:45
.= 0 + 1 by A7 ;
then A15: CurInstr (P1,(Comput (P1,s1,1))) = P1 . 1 by A13
.= SBP := 7 by Lm1, A3 ;
A16: Comput (P1,s1,(1 + 1)) = Following (P1,(Comput (P1,s1,1))) by EXTPRO_1:3
.= Exec ((SBP := 7),(Comput (P1,s1,1))) by A15 ;
A17: P2 /. (IC (Comput (P2,s2,1))) = P2 . (IC (Comput (P2,s2,1))) by PBOOLE:143;
A18: IC (Comput (P2,s2,1)) = (IC s2) + 1 by A12, SCMPDS_2:45
.= 0 + 1 by A10 ;
then A19: CurInstr (P2,(Comput (P2,s2,1))) = P2 . 1 by A17
.= SBP := 7 by Lm1, A4 ;
A20: Comput (P2,s2,(1 + 1)) = Following (P2,(Comput (P2,s2,1))) by EXTPRO_1:3
.= Exec ((SBP := 7),(Comput (P2,s2,1))) by A19 ;
A21: P1 /. (IC (Comput (P1,s1,2))) = P1 . (IC (Comput (P1,s1,2))) by PBOOLE:143;
A22: IC (Comput (P1,s1,2)) = (IC (Comput (P1,s1,1))) + 1 by A16, SCMPDS_2:45
.= 1 + 1 by A14 ;
then A23: CurInstr (P1,(Comput (P1,s1,2))) = P1 . 2 by A21
.= saveIC (SBP,RetIC) by Lm1, A3 ;
A24: Comput (P1,s1,(2 + 1)) = Following (P1,(Comput (P1,s1,2))) by EXTPRO_1:3
.= Exec ((saveIC (SBP,RetIC)),(Comput (P1,s1,2))) by A23 ;
A25: (Comput (P1,s1,2)) . SBP = 7 by A16, SCMPDS_2:45;
A26: P2 /. (IC (Comput (P2,s2,2))) = P2 . (IC (Comput (P2,s2,2))) by PBOOLE:143;
A27: IC (Comput (P2,s2,2)) = (IC (Comput (P2,s2,1))) + 1 by A20, SCMPDS_2:45
.= 1 + 1 by A18 ;
then A28: CurInstr (P2,(Comput (P2,s2,2))) = P2 . 2 by A26
.= saveIC (SBP,RetIC) by Lm1, A4 ;
A29: Comput (P2,s2,(2 + 1)) = Following (P2,(Comput (P2,s2,2))) by EXTPRO_1:3
.= Exec ((saveIC (SBP,RetIC)),(Comput (P2,s2,2))) by A28 ;
A30: (Comput (P2,s2,2)) . SBP = 7 by A20, SCMPDS_2:45;
A31: P1 /. (IC (Comput (P1,s1,3))) = P1 . (IC (Comput (P1,s1,3))) by PBOOLE:143;
A32: IC (Comput (P1,s1,3)) = (IC (Comput (P1,s1,2))) + 1 by A24, SCMPDS_2:59
.= 2 + 1 by A22 ;
then A33: CurInstr (P1,(Comput (P1,s1,3))) = P1 . 3 by A31
.= goto 2 by Lm1, A3 ;
A34: Comput (P1,s1,(3 + 1)) = Following (P1,(Comput (P1,s1,3))) by EXTPRO_1:3
.= Exec ((goto 2),(Comput (P1,s1,3))) by A33 ;
A35: P2 /. (IC (Comput (P2,s2,3))) = P2 . (IC (Comput (P2,s2,3))) by PBOOLE:143;
A36: IC (Comput (P2,s2,3)) = (IC (Comput (P2,s2,2))) + 1 by A29, SCMPDS_2:59
.= 2 + 1 by A27 ;
then A37: CurInstr (P2,(Comput (P2,s2,3))) = P2 . 3 by A35
.= goto 2 by Lm1, A4 ;
A38: Comput (P2,s2,(3 + 1)) = Following (P2,(Comput (P2,s2,3))) by EXTPRO_1:3
.= Exec ((goto 2),(Comput (P2,s2,3))) by A37 ;
A39: now :: thesis: for b being Int_position st s1 . b = s2 . b holds
(Comput (P1,s1,1)) . b = (Comput (P2,s2,1)) . b
let b be Int_position; :: thesis: ( s1 . b = s2 . b implies (Comput (P1,s1,1)) . b1 = (Comput (P2,s2,1)) . b1 )
assume A40: s1 . b = s2 . b ; :: thesis: (Comput (P1,s1,1)) . b1 = (Comput (P2,s2,1)) . b1
per cases ( b = GBP or b <> GBP ) ;
suppose A41: b = GBP ; :: thesis: (Comput (P1,s1,1)) . b1 = (Comput (P2,s2,1)) . b1
hence (Comput (P1,s1,1)) . b = 0 by A9, SCMPDS_2:45
.= (Comput (P2,s2,1)) . b by A12, A41, SCMPDS_2:45 ;
:: thesis: verum
end;
suppose A42: b <> GBP ; :: thesis: (Comput (P1,s1,1)) . b1 = (Comput (P2,s2,1)) . b1
hence (Comput (P1,s1,1)) . b = s1 . b by A9, SCMPDS_2:45
.= (Comput (P2,s2,1)) . b by A12, A40, A42, SCMPDS_2:45 ;
:: thesis: verum
end;
end;
end;
A43: now :: thesis: for b being Int_position st s1 . b = s2 . b holds
(Comput (P1,s1,2)) . b = (Comput (P2,s2,2)) . b
let b be Int_position; :: thesis: ( s1 . b = s2 . b implies (Comput (P1,s1,2)) . b1 = (Comput (P2,s2,2)) . b1 )
assume A44: s1 . b = s2 . b ; :: thesis: (Comput (P1,s1,2)) . b1 = (Comput (P2,s2,2)) . b1
per cases ( b = SBP or b <> SBP ) ;
suppose A45: b = SBP ; :: thesis: (Comput (P1,s1,2)) . b1 = (Comput (P2,s2,2)) . b1
hence (Comput (P1,s1,2)) . b = 7 by A16, SCMPDS_2:45
.= (Comput (P2,s2,2)) . b by A20, A45, SCMPDS_2:45 ;
:: thesis: verum
end;
suppose A46: b <> SBP ; :: thesis: (Comput (P1,s1,2)) . b1 = (Comput (P2,s2,2)) . b1
hence (Comput (P1,s1,2)) . b = (Comput (P1,s1,1)) . b by A16, SCMPDS_2:45
.= (Comput (P2,s2,1)) . b by A39, A44
.= (Comput (P2,s2,2)) . b by A20, A46, SCMPDS_2:45 ;
:: thesis: verum
end;
end;
end;
A47: now :: thesis: for b being Int_position st s1 . b = s2 . b holds
(Comput (P1,s1,3)) . b = (Comput (P2,s2,3)) . b
let b be Int_position; :: thesis: ( s1 . b = s2 . b implies (Comput (P1,s1,3)) . b1 = (Comput (P2,s2,3)) . b1 )
assume A48: s1 . b = s2 . b ; :: thesis: (Comput (P1,s1,3)) . b1 = (Comput (P2,s2,3)) . b1
per cases ( b = DataLoc (((Comput (P1,s1,2)) . SBP),RetIC) or b <> DataLoc (((Comput (P1,s1,2)) . SBP),RetIC) ) ;
suppose A49: b = DataLoc (((Comput (P1,s1,2)) . SBP),RetIC) ; :: thesis: (Comput (P1,s1,3)) . b1 = (Comput (P2,s2,3)) . b1
hence (Comput (P1,s1,3)) . b = IC (Comput (P1,s1,2)) by A24, SCMPDS_2:59
.= (Comput (P2,s2,3)) . b by A22, A25, A27, A29, A30, A49, SCMPDS_2:59 ;
:: thesis: verum
end;
suppose A50: b <> DataLoc (((Comput (P1,s1,2)) . SBP),RetIC) ; :: thesis: (Comput (P1,s1,3)) . b1 = (Comput (P2,s2,3)) . b1
hence (Comput (P1,s1,3)) . b = (Comput (P1,s1,2)) . b by A24, SCMPDS_2:59
.= (Comput (P2,s2,2)) . b by A43, A48
.= (Comput (P2,s2,3)) . b by A25, A29, A30, A50, SCMPDS_2:59 ;
:: thesis: verum
end;
end;
end;
not not k = 0 & ... & not k = 4 by A6;
per cases then ( k = 0 or k = 1 or k = 2 or k = 3 or k = 4 ) ;
suppose A51: k = 0 ; :: thesis: ( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a )
hence IC (Comput (P1,s1,k)) = IC s1 by EXTPRO_1:2
.= IC (Comput (P2,s2,k)) by A7, A10, A51, EXTPRO_1:2 ;
:: thesis: (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
thus (Comput (P1,s1,k)) . a = s1 . a by A51, EXTPRO_1:2
.= (Comput (P2,s2,k)) . a by A5, A51, EXTPRO_1:2 ; :: thesis: verum
end;
suppose A52: k = 1 ; :: thesis: ( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a )
hence IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) by A14, A18; :: thesis: (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
thus (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a by A5, A39, A52; :: thesis: verum
end;
suppose A53: k = 2 ; :: thesis: ( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a )
hence IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) by A22, A27; :: thesis: (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
thus (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a by A5, A43, A53; :: thesis: verum
end;
suppose A54: k = 3 ; :: thesis: ( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a )
hence IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) by A32, A36; :: thesis: (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
thus (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a by A5, A47, A54; :: thesis: verum
end;
suppose A55: k = 4 ; :: thesis: ( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a )
hence IC (Comput (P1,s1,k)) = ICplusConst ((Comput (P1,s1,3)),2) by A34, SCMPDS_2:54
.= 3 + 2 by A32, SCMPDS_6:12
.= ICplusConst ((Comput (P2,s2,3)),2) by A36, SCMPDS_6:12
.= IC (Comput (P2,s2,k)) by A38, A55, SCMPDS_2:54 ;
:: thesis: (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
thus (Comput (P1,s1,k)) . a = (Comput (P1,s1,3)) . a by A34, A55, SCMPDS_2:54
.= (Comput (P2,s2,3)) . a by A5, A47
.= (Comput (P2,s2,k)) . a by A38, A55, SCMPDS_2:54 ; :: thesis: verum
end;
end;