let P1, P2 be Instruction-Sequence of SCMPDS; :: thesis: for s1, s2 being State of SCMPDS
for a being Int_position
for k being Element of 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 Element of 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 Element of 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 Element of 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 )
A9: IC s1 = 0 by A1, MEMSTR_0:39;
A10: P1 /. (IC s1) = P1 . (IC s1) by PBOOLE:143;
A11: 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 A9, Lm1, A10, A3 ;
A12: IC s2 = 0 by A2, MEMSTR_0:39;
A13: P2 /. (IC s2) = P2 . (IC s2) by PBOOLE:143;
A14: 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 A12, Lm1, A13, A4 ;
A15: P1 /. (IC (Comput (P1,s1,1))) = P1 . (IC (Comput (P1,s1,1))) by PBOOLE:143;
A16: IC (Comput (P1,s1,1)) = succ (IC s1) by A11, SCMPDS_2:45
.= 0 + 1 by A9 ;
then A17: CurInstr (P1,(Comput (P1,s1,1))) = P1 . 1 by A15
.= SBP := 7 by Lm1, A3 ;
A19: Comput (P1,s1,(1 + 1)) = Following (P1,(Comput (P1,s1,1))) by EXTPRO_1:3
.= Exec ((SBP := 7),(Comput (P1,s1,1))) by A17 ;
A20: P2 /. (IC (Comput (P2,s2,1))) = P2 . (IC (Comput (P2,s2,1))) by PBOOLE:143;
A21: IC (Comput (P2,s2,1)) = succ (IC s2) by A14, SCMPDS_2:45
.= 0 + 1 by A12 ;
then A22: CurInstr (P2,(Comput (P2,s2,1))) = P2 . 1 by A20
.= SBP := 7 by Lm1, A4 ;
A24: Comput (P2,s2,(1 + 1)) = Following (P2,(Comput (P2,s2,1))) by EXTPRO_1:3
.= Exec ((SBP := 7),(Comput (P2,s2,1))) by A22 ;
A25: P1 /. (IC (Comput (P1,s1,2))) = P1 . (IC (Comput (P1,s1,2))) by PBOOLE:143;
A26: IC (Comput (P1,s1,2)) = succ (IC (Comput (P1,s1,1))) by A19, SCMPDS_2:45
.= 1 + 1 by A16 ;
then A27: CurInstr (P1,(Comput (P1,s1,2))) = P1 . 2 by A25
.= saveIC (SBP,RetIC) by Lm1, A3 ;
A29: Comput (P1,s1,(2 + 1)) = Following (P1,(Comput (P1,s1,2))) by EXTPRO_1:3
.= Exec ((saveIC (SBP,RetIC)),(Comput (P1,s1,2))) by A27 ;
A30: (Comput (P1,s1,2)) . SBP = 7 by A19, SCMPDS_2:45;
A31: P2 /. (IC (Comput (P2,s2,2))) = P2 . (IC (Comput (P2,s2,2))) by PBOOLE:143;
A32: IC (Comput (P2,s2,2)) = succ (IC (Comput (P2,s2,1))) by A24, SCMPDS_2:45
.= 1 + 1 by A21 ;
then A33: CurInstr (P2,(Comput (P2,s2,2))) = P2 . 2 by A31
.= saveIC (SBP,RetIC) by Lm1, A4 ;
A35: Comput (P2,s2,(2 + 1)) = Following (P2,(Comput (P2,s2,2))) by EXTPRO_1:3
.= Exec ((saveIC (SBP,RetIC)),(Comput (P2,s2,2))) by A33 ;
A36: (Comput (P2,s2,2)) . SBP = 7 by A24, SCMPDS_2:45;
A37: P1 /. (IC (Comput (P1,s1,3))) = P1 . (IC (Comput (P1,s1,3))) by PBOOLE:143;
A38: IC (Comput (P1,s1,3)) = succ (IC (Comput (P1,s1,2))) by A29, SCMPDS_2:59
.= 2 + 1 by A26 ;
then A39: CurInstr (P1,(Comput (P1,s1,3))) = P1 . 3 by A37
.= goto 2 by Lm1, A3 ;
A41: Comput (P1,s1,(3 + 1)) = Following (P1,(Comput (P1,s1,3))) by EXTPRO_1:3
.= Exec ((goto 2),(Comput (P1,s1,3))) by A39 ;
A42: P2 /. (IC (Comput (P2,s2,3))) = P2 . (IC (Comput (P2,s2,3))) by PBOOLE:143;
A43: IC (Comput (P2,s2,3)) = succ (IC (Comput (P2,s2,2))) by A35, SCMPDS_2:59
.= 2 + 1 by A32 ;
then A44: CurInstr (P2,(Comput (P2,s2,3))) = P2 . 3 by A42
.= goto 2 by Lm1, A4 ;
A46: Comput (P2,s2,(3 + 1)) = Following (P2,(Comput (P2,s2,3))) by EXTPRO_1:3
.= Exec ((goto 2),(Comput (P2,s2,3))) by A44 ;
A47: now
let b be Int_position ; :: thesis: ( s1 . b = s2 . b implies (Comput (P1,s1,1)) . b1 = (Comput (P2,s2,1)) . b1 )
assume A48: s1 . b = s2 . b ; :: thesis: (Comput (P1,s1,1)) . b1 = (Comput (P2,s2,1)) . b1
per cases ( b = GBP or b <> GBP ) ;
suppose A49: b = GBP ; :: thesis: (Comput (P1,s1,1)) . b1 = (Comput (P2,s2,1)) . b1
hence (Comput (P1,s1,1)) . b = 0 by A11, SCMPDS_2:45
.= (Comput (P2,s2,1)) . b by A14, A49, SCMPDS_2:45 ;
:: thesis: verum
end;
suppose A50: b <> GBP ; :: thesis: (Comput (P1,s1,1)) . b1 = (Comput (P2,s2,1)) . b1
hence (Comput (P1,s1,1)) . b = s1 . b by A11, SCMPDS_2:45
.= (Comput (P2,s2,1)) . b by A14, A48, A50, SCMPDS_2:45 ;
:: thesis: verum
end;
end;
end;
A51: now
let b be Int_position ; :: thesis: ( s1 . b = s2 . b implies (Comput (P1,s1,2)) . b1 = (Comput (P2,s2,2)) . b1 )
assume A52: s1 . b = s2 . b ; :: thesis: (Comput (P1,s1,2)) . b1 = (Comput (P2,s2,2)) . b1
per cases ( b = SBP or b <> SBP ) ;
suppose A53: b = SBP ; :: thesis: (Comput (P1,s1,2)) . b1 = (Comput (P2,s2,2)) . b1
hence (Comput (P1,s1,2)) . b = 7 by A19, SCMPDS_2:45
.= (Comput (P2,s2,2)) . b by A24, A53, SCMPDS_2:45 ;
:: thesis: verum
end;
suppose A54: 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 A19, SCMPDS_2:45
.= (Comput (P2,s2,1)) . b by A47, A52
.= (Comput (P2,s2,2)) . b by A24, A54, SCMPDS_2:45 ;
:: thesis: verum
end;
end;
end;
A55: now
let b be Int_position ; :: thesis: ( s1 . b = s2 . b implies (Comput (P1,s1,3)) . b1 = (Comput (P2,s2,3)) . b1 )
assume A56: 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 A57: 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 A29, SCMPDS_2:59
.= (Comput (P2,s2,3)) . b by A26, A30, A32, A35, A36, A57, SCMPDS_2:59 ;
:: thesis: verum
end;
suppose A58: 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 A29, SCMPDS_2:59
.= (Comput (P2,s2,2)) . b by A51, A56
.= (Comput (P2,s2,3)) . b by A30, A35, A36, A58, SCMPDS_2:59 ;
:: thesis: verum
end;
end;
end;
per cases ( k = 0 or k = 1 or k = 2 or k = 3 or k = 4 ) by A6, NAT_1:28;
suppose A59: 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 A9, A12, A59, EXTPRO_1:2 ;
:: thesis: (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
thus (Comput (P1,s1,k)) . a = s1 . a by A59, EXTPRO_1:2
.= (Comput (P2,s2,k)) . a by A5, A59, EXTPRO_1:2 ; :: thesis: verum
end;
suppose A60: 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 A16, A21; :: 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, A60; :: thesis: verum
end;
suppose A61: 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 A26, A32; :: thesis: (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
thus (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a by A5, A51, A61; :: thesis: verum
end;
suppose A62: 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 A38, A43; :: thesis: (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a
thus (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a by A5, A55, A62; :: thesis: verum
end;
suppose A63: 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 A41, SCMPDS_2:54
.= 3 + 2 by A38, SCMPDS_6:12
.= ICplusConst ((Comput (P2,s2,3)),2) by A43, SCMPDS_6:12
.= IC (Comput (P2,s2,k)) by A46, A63, 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 A41, A63, SCMPDS_2:54
.= (Comput (P2,s2,3)) . a by A5, A55
.= (Comput (P2,s2,k)) . a by A46, A63, SCMPDS_2:54 ; :: thesis: verum
end;
end;