let s1, s2 be State of SCMPDS; :: thesis: for n, m being Nat
for i being Instruction of SCMPDS st IC s1 = m & i valid_at m & InsCode i <> 1 & InsCode i <> 3 & (IC s1) + n = IC s2 & DataPart s1 = DataPart s2 holds
( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
let n, m be Nat; :: thesis: for i being Instruction of SCMPDS st IC s1 = m & i valid_at m & InsCode i <> 1 & InsCode i <> 3 & (IC s1) + n = IC s2 & DataPart s1 = DataPart s2 holds
( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
let i be Instruction of SCMPDS; :: thesis: ( IC s1 = m & i valid_at m & InsCode i <> 1 & InsCode i <> 3 & (IC s1) + n = IC s2 & DataPart s1 = DataPart s2 implies ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) ) )
assume that
A1: IC s1 = m and
A2: i valid_at m and
A3: ( InsCode i <> 1 & InsCode i <> 3 ) and
A4: (IC s1) + n = IC s2 and
A5: DataPart s1 = DataPart s2 ; :: thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
A6: now :: thesis: for a being Int_position
for k1 being Integer holds s1 . (DataLoc ((s1 . a),k1)) = s2 . (DataLoc ((s2 . a),k1))
let a be Int_position; :: thesis: for k1 being Integer holds s1 . (DataLoc ((s1 . a),k1)) = s2 . (DataLoc ((s2 . a),k1))
let k1 be Integer; :: thesis: s1 . (DataLoc ((s1 . a),k1)) = s2 . (DataLoc ((s2 . a),k1))
thus s1 . (DataLoc ((s1 . a),k1)) = s1 . (DataLoc ((s2 . a),k1)) by A5, Th7
.= s2 . (DataLoc ((s2 . a),k1)) by A5, Th7 ; :: thesis: verum
end;
reconsider k1 = IC s1 as Nat ;
set Ci = InsCode i;
A7: ((IC s1) + 1) + n = (IC s2) + 1 by A4;
A8: now :: thesis: ( InsCode i <> 0 & InsCode i <> 14 & InsCode i <> 1 & InsCode i <> 4 & InsCode i <> 5 & InsCode i <> 6 implies (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) )
assume ( InsCode i <> 0 & InsCode i <> 14 & InsCode i <> 1 & InsCode i <> 4 & InsCode i <> 5 & InsCode i <> 6 ) ; :: thesis: (IC (Exec (i,s1))) + n = IC (Exec (i,s2))
then A9: not InsCode i in {0,1,4,5,6,14} by ENUMSET1:def 4;
then IC (Exec (i,s1)) = (IC s1) + 1 by Th1;
hence (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) by A7, A9, Th1; :: thesis: verum
end;
not not InsCode i = 0 & ... & not InsCode i = 14 by SCMPDS_2:6;
per cases then ( InsCode i = 0 or InsCode i = 14 or InsCode i = 2 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or InsCode i = 13 ) by A3;
suppose InsCode i = 0 ; :: thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
then A10: ( Exec (i,s1) = s1 & Exec (i,s2) = s2 ) by SCMPDS_2:86;
hence (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) by A4; :: thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
thus DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by A5, A10; :: thesis: verum
end;
suppose InsCode i = 14 ; :: thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
then consider k1 being Integer such that
A11: i = goto k1 and
A12: m + k1 >= 0 by A2;
IC (Exec (i,s1)) = ICplusConst (s1,k1) by A11, SCMPDS_2:54;
hence (IC (Exec (i,s1))) + n = ICplusConst (s2,k1) by A1, A4, A12, Th25
.= IC (Exec (i,s2)) by A11, SCMPDS_2:54 ;
:: thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
now :: thesis: for a being Int_position holds (Exec (i,s1)) . a = (Exec (i,s2)) . a
let a be Int_position; :: thesis: (Exec (i,s1)) . a = (Exec (i,s2)) . a
thus (Exec (i,s1)) . a = s1 . a by A11, SCMPDS_2:54
.= s2 . a by A5, Th7
.= (Exec (i,s2)) . a by A11, SCMPDS_2:54 ; :: thesis: verum
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by Th7; :: thesis: verum
end;
suppose A13: InsCode i = 2 ; :: thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
hence (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) by A8; :: thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
consider a being Int_position, k1 being Integer such that
A14: i = a := k1 by A13, SCMPDS_2:28;
now :: thesis: for b being Int_position holds (Exec (i,s1)) . b = (Exec (i,s2)) . b
let b be Int_position; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
per cases ( a = b or a <> b ) ;
suppose A15: a = b ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
hence (Exec (i,s1)) . b = k1 by A14, SCMPDS_2:45
.= (Exec (i,s2)) . b by A14, A15, SCMPDS_2:45 ;
:: thesis: verum
end;
suppose A16: a <> b ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
hence (Exec (i,s1)) . b = s1 . b by A14, SCMPDS_2:45
.= s2 . b by A5, Th7
.= (Exec (i,s2)) . b by A14, A16, SCMPDS_2:45 ;
:: thesis: verum
end;
end;
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by Th7; :: thesis: verum
end;
suppose InsCode i = 4 ; :: thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
then consider a being Int_position, k1, k2 being Integer such that
A17: i = (a,k1) <>0_goto k2 and
A18: m + k2 >= 0 by A2;
hereby :: thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
per cases ( s1 . (DataLoc ((s1 . a),k1)) <> 0 or s1 . (DataLoc ((s1 . a),k1)) = 0 ) ;
suppose A19: s1 . (DataLoc ((s1 . a),k1)) <> 0 ; :: thesis: (IC (Exec (i,s1))) + n = IC (Exec (i,s2))
then A20: s2 . (DataLoc ((s2 . a),k1)) <> 0 by A6;
IC (Exec (i,s1)) = ICplusConst (s1,k2) by A17, A19, SCMPDS_2:55;
hence (IC (Exec (i,s1))) + n = ICplusConst (s2,k2) by A1, A4, A18, Th25
.= IC (Exec (i,s2)) by A17, A20, SCMPDS_2:55 ;
:: thesis: verum
end;
suppose s1 . (DataLoc ((s1 . a),k1)) = 0 ; :: thesis: (IC (Exec (i,s1))) + n = IC (Exec (i,s2))
then ( s2 . (DataLoc ((s2 . a),k1)) = 0 & IC (Exec (i,s1)) = (IC s1) + 1 ) by A6, A17, SCMPDS_2:55;
hence (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) by A7, A17, SCMPDS_2:55; :: thesis: verum
end;
end;
end;
now :: thesis: for a being Int_position holds (Exec (i,s1)) . a = (Exec (i,s2)) . a
let a be Int_position; :: thesis: (Exec (i,s1)) . a = (Exec (i,s2)) . a
thus (Exec (i,s1)) . a = s1 . a by A17, SCMPDS_2:55
.= s2 . a by A5, Th7
.= (Exec (i,s2)) . a by A17, SCMPDS_2:55 ; :: thesis: verum
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by Th7; :: thesis: verum
end;
suppose InsCode i = 5 ; :: thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
then consider a being Int_position, k1, k2 being Integer such that
A21: i = (a,k1) <=0_goto k2 and
A22: m + k2 >= 0 by A2;
hereby :: thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
per cases ( s1 . (DataLoc ((s1 . a),k1)) <= 0 or s1 . (DataLoc ((s1 . a),k1)) > 0 ) ;
suppose A23: s1 . (DataLoc ((s1 . a),k1)) <= 0 ; :: thesis: (IC (Exec (i,s1))) + n = IC (Exec (i,s2))
then A24: s2 . (DataLoc ((s2 . a),k1)) <= 0 by A6;
IC (Exec (i,s1)) = ICplusConst (s1,k2) by A21, A23, SCMPDS_2:56;
hence (IC (Exec (i,s1))) + n = ICplusConst (s2,k2) by A1, A4, A22, Th25
.= IC (Exec (i,s2)) by A21, A24, SCMPDS_2:56 ;
:: thesis: verum
end;
suppose s1 . (DataLoc ((s1 . a),k1)) > 0 ; :: thesis: (IC (Exec (i,s1))) + n = IC (Exec (i,s2))
then ( s2 . (DataLoc ((s2 . a),k1)) > 0 & IC (Exec (i,s1)) = (IC s1) + 1 ) by A6, A21, SCMPDS_2:56;
hence (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) by A7, A21, SCMPDS_2:56; :: thesis: verum
end;
end;
end;
now :: thesis: for a being Int_position holds (Exec (i,s1)) . a = (Exec (i,s2)) . a
let a be Int_position; :: thesis: (Exec (i,s1)) . a = (Exec (i,s2)) . a
thus (Exec (i,s1)) . a = s1 . a by A21, SCMPDS_2:56
.= s2 . a by A5, Th7
.= (Exec (i,s2)) . a by A21, SCMPDS_2:56 ; :: thesis: verum
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by Th7; :: thesis: verum
end;
suppose InsCode i = 6 ; :: thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
then consider a being Int_position, k1, k2 being Integer such that
A25: i = (a,k1) >=0_goto k2 and
A26: m + k2 >= 0 by A2;
hereby :: thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
per cases ( s1 . (DataLoc ((s1 . a),k1)) >= 0 or s1 . (DataLoc ((s1 . a),k1)) < 0 ) ;
suppose A27: s1 . (DataLoc ((s1 . a),k1)) >= 0 ; :: thesis: (IC (Exec (i,s1))) + n = IC (Exec (i,s2))
then A28: s2 . (DataLoc ((s2 . a),k1)) >= 0 by A6;
IC (Exec (i,s1)) = ICplusConst (s1,k2) by A25, A27, SCMPDS_2:57;
hence (IC (Exec (i,s1))) + n = ICplusConst (s2,k2) by A1, A4, A26, Th25
.= IC (Exec (i,s2)) by A25, A28, SCMPDS_2:57 ;
:: thesis: verum
end;
suppose s1 . (DataLoc ((s1 . a),k1)) < 0 ; :: thesis: (IC (Exec (i,s1))) + n = IC (Exec (i,s2))
then ( s2 . (DataLoc ((s2 . a),k1)) < 0 & IC (Exec (i,s1)) = (IC s1) + 1 ) by A6, A25, SCMPDS_2:57;
hence (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) by A7, A25, SCMPDS_2:57; :: thesis: verum
end;
end;
end;
now :: thesis: for a being Int_position holds (Exec (i,s1)) . a = (Exec (i,s2)) . a
let a be Int_position; :: thesis: (Exec (i,s1)) . a = (Exec (i,s2)) . a
thus (Exec (i,s1)) . a = s1 . a by A25, SCMPDS_2:57
.= s2 . a by A5, Th7
.= (Exec (i,s2)) . a by A25, SCMPDS_2:57 ; :: thesis: verum
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by Th7; :: thesis: verum
end;
suppose A29: InsCode i = 7 ; :: thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
hence (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) by A8; :: thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
consider a being Int_position, k1, k2 being Integer such that
A30: i = (a,k1) := k2 by A29, SCMPDS_2:33;
now :: thesis: for b being Int_position holds (Exec (i,s1)) . b = (Exec (i,s2)) . b
let b be Int_position; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
per cases ( DataLoc ((s1 . a),k1) = b or DataLoc ((s1 . a),k1) <> b ) ;
suppose A31: DataLoc ((s1 . a),k1) = b ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A32: DataLoc ((s2 . a),k1) = b by A5, Th7;
thus (Exec (i,s1)) . b = k2 by A30, A31, SCMPDS_2:46
.= (Exec (i,s2)) . b by A30, A32, SCMPDS_2:46 ; :: thesis: verum
end;
suppose A33: DataLoc ((s1 . a),k1) <> b ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A34: DataLoc ((s2 . a),k1) <> b by A5, Th7;
thus (Exec (i,s1)) . b = s1 . b by A30, A33, SCMPDS_2:46
.= s2 . b by A5, Th7
.= (Exec (i,s2)) . b by A30, A34, SCMPDS_2:46 ; :: thesis: verum
end;
end;
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by Th7; :: thesis: verum
end;
suppose A35: InsCode i = 8 ; :: thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
hence (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) by A8; :: thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
consider a being Int_position, k1, k2 being Integer such that
A36: i = AddTo (a,k1,k2) by A35, SCMPDS_2:34;
now :: thesis: for b being Int_position holds (Exec (i,s1)) . b = (Exec (i,s2)) . b
let b be Int_position; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
per cases ( DataLoc ((s1 . a),k1) = b or DataLoc ((s1 . a),k1) <> b ) ;
suppose A37: DataLoc ((s1 . a),k1) = b ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A38: DataLoc ((s2 . a),k1) = b by A5, Th7;
thus (Exec (i,s1)) . b = (s1 . (DataLoc ((s1 . a),k1))) + k2 by A36, A37, SCMPDS_2:48
.= (s2 . (DataLoc ((s2 . a),k1))) + k2 by A6
.= (Exec (i,s2)) . b by A36, A38, SCMPDS_2:48 ; :: thesis: verum
end;
suppose A39: DataLoc ((s1 . a),k1) <> b ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A40: DataLoc ((s2 . a),k1) <> b by A5, Th7;
thus (Exec (i,s1)) . b = s1 . b by A36, A39, SCMPDS_2:48
.= s2 . b by A5, Th7
.= (Exec (i,s2)) . b by A36, A40, SCMPDS_2:48 ; :: thesis: verum
end;
end;
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by Th7; :: thesis: verum
end;
suppose A41: InsCode i = 9 ; :: thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
hence (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) by A8; :: thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
consider a, b being Int_position, k1, k2 being Integer such that
A42: i = AddTo (a,k1,b,k2) by A41, SCMPDS_2:35;
now :: thesis: for c being Int_position holds (Exec (i,s1)) . c = (Exec (i,s2)) . c
let c be Int_position; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
per cases ( DataLoc ((s1 . a),k1) = c or DataLoc ((s1 . a),k1) <> c ) ;
suppose A43: DataLoc ((s1 . a),k1) = c ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A44: DataLoc ((s2 . a),k1) = c by A5, Th7;
thus (Exec (i,s1)) . c = (s1 . (DataLoc ((s1 . a),k1))) + (s1 . (DataLoc ((s1 . b),k2))) by A42, A43, SCMPDS_2:49
.= (s2 . (DataLoc ((s2 . a),k1))) + (s1 . (DataLoc ((s1 . b),k2))) by A6
.= (s2 . (DataLoc ((s2 . a),k1))) + (s2 . (DataLoc ((s2 . b),k2))) by A6
.= (Exec (i,s2)) . c by A42, A44, SCMPDS_2:49 ; :: thesis: verum
end;
suppose A45: DataLoc ((s1 . a),k1) <> c ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A46: DataLoc ((s2 . a),k1) <> c by A5, Th7;
thus (Exec (i,s1)) . c = s1 . c by A42, A45, SCMPDS_2:49
.= s2 . c by A5, Th7
.= (Exec (i,s2)) . c by A42, A46, SCMPDS_2:49 ; :: thesis: verum
end;
end;
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by Th7; :: thesis: verum
end;
suppose A47: InsCode i = 10 ; :: thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
hence (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) by A8; :: thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
consider a, b being Int_position, k1, k2 being Integer such that
A48: i = SubFrom (a,k1,b,k2) by A47, SCMPDS_2:36;
now :: thesis: for c being Int_position holds (Exec (i,s1)) . c = (Exec (i,s2)) . c
let c be Int_position; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
per cases ( DataLoc ((s1 . a),k1) = c or DataLoc ((s1 . a),k1) <> c ) ;
suppose A49: DataLoc ((s1 . a),k1) = c ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A50: DataLoc ((s2 . a),k1) = c by A5, Th7;
thus (Exec (i,s1)) . c = (s1 . (DataLoc ((s1 . a),k1))) - (s1 . (DataLoc ((s1 . b),k2))) by A48, A49, SCMPDS_2:50
.= (s2 . (DataLoc ((s2 . a),k1))) - (s1 . (DataLoc ((s1 . b),k2))) by A6
.= (s2 . (DataLoc ((s2 . a),k1))) - (s2 . (DataLoc ((s2 . b),k2))) by A6
.= (Exec (i,s2)) . c by A48, A50, SCMPDS_2:50 ; :: thesis: verum
end;
suppose A51: DataLoc ((s1 . a),k1) <> c ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A52: DataLoc ((s2 . a),k1) <> c by A5, Th7;
thus (Exec (i,s1)) . c = s1 . c by A48, A51, SCMPDS_2:50
.= s2 . c by A5, Th7
.= (Exec (i,s2)) . c by A48, A52, SCMPDS_2:50 ; :: thesis: verum
end;
end;
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by Th7; :: thesis: verum
end;
suppose A53: InsCode i = 11 ; :: thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
hence (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) by A8; :: thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
consider a, b being Int_position, k1, k2 being Integer such that
A54: i = MultBy (a,k1,b,k2) by A53, SCMPDS_2:37;
now :: thesis: for c being Int_position holds (Exec (i,s1)) . c = (Exec (i,s2)) . c
let c be Int_position; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
per cases ( DataLoc ((s1 . a),k1) = c or DataLoc ((s1 . a),k1) <> c ) ;
suppose A55: DataLoc ((s1 . a),k1) = c ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A56: DataLoc ((s2 . a),k1) = c by A5, Th7;
thus (Exec (i,s1)) . c = (s1 . (DataLoc ((s1 . a),k1))) * (s1 . (DataLoc ((s1 . b),k2))) by A54, A55, SCMPDS_2:51
.= (s2 . (DataLoc ((s2 . a),k1))) * (s1 . (DataLoc ((s1 . b),k2))) by A6
.= (s2 . (DataLoc ((s2 . a),k1))) * (s2 . (DataLoc ((s2 . b),k2))) by A6
.= (Exec (i,s2)) . c by A54, A56, SCMPDS_2:51 ; :: thesis: verum
end;
suppose A57: DataLoc ((s1 . a),k1) <> c ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A58: DataLoc ((s2 . a),k1) <> c by A5, Th7;
thus (Exec (i,s1)) . c = s1 . c by A54, A57, SCMPDS_2:51
.= s2 . c by A5, Th7
.= (Exec (i,s2)) . c by A54, A58, SCMPDS_2:51 ; :: thesis: verum
end;
end;
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by Th7; :: thesis: verum
end;
suppose A59: InsCode i = 12 ; :: thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
hence (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) by A8; :: thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
consider a, b being Int_position, k1, k2 being Integer such that
A60: i = Divide (a,k1,b,k2) by A59, SCMPDS_2:38;
now :: thesis: for c being Int_position holds (Exec (i,s1)) . c = (Exec (i,s2)) . c
let c be Int_position; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
per cases ( DataLoc ((s1 . b),k2) = c or DataLoc ((s1 . b),k2) <> c ) ;
suppose A61: DataLoc ((s1 . b),k2) = c ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A62: DataLoc ((s2 . b),k2) = c by A5, Th7;
thus (Exec (i,s1)) . c = (s1 . (DataLoc ((s1 . a),k1))) mod (s1 . (DataLoc ((s1 . b),k2))) by A60, A61, SCMPDS_2:52
.= (s2 . (DataLoc ((s2 . a),k1))) mod (s1 . (DataLoc ((s1 . b),k2))) by A6
.= (s2 . (DataLoc ((s2 . a),k1))) mod (s2 . (DataLoc ((s2 . b),k2))) by A6
.= (Exec (i,s2)) . c by A60, A62, SCMPDS_2:52 ; :: thesis: verum
end;
suppose A63: DataLoc ((s1 . b),k2) <> c ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A64: DataLoc ((s2 . b),k2) <> c by A5, Th7;
hereby :: thesis: verum
per cases ( DataLoc ((s1 . a),k1) <> c or DataLoc ((s1 . a),k1) = c ) ;
suppose A65: DataLoc ((s1 . a),k1) <> c ; :: thesis: (Exec (i,s1)) . c = (Exec (i,s2)) . c
then A66: DataLoc ((s2 . a),k1) <> c by A5, Th7;
thus (Exec (i,s1)) . c = s1 . c by A60, A63, A65, SCMPDS_2:52
.= s2 . c by A5, Th7
.= (Exec (i,s2)) . c by A60, A64, A66, SCMPDS_2:52 ; :: thesis: verum
end;
suppose A67: DataLoc ((s1 . a),k1) = c ; :: thesis: (Exec (i,s1)) . c = (Exec (i,s2)) . c
then A68: DataLoc ((s2 . a),k1) = c by A5, Th7;
thus (Exec (i,s1)) . c = (s1 . (DataLoc ((s1 . a),k1))) div (s1 . (DataLoc ((s1 . b),k2))) by A60, A63, A67, SCMPDS_2:52
.= (s2 . (DataLoc ((s2 . a),k1))) div (s1 . (DataLoc ((s1 . b),k2))) by A6
.= (s2 . (DataLoc ((s2 . a),k1))) div (s2 . (DataLoc ((s2 . b),k2))) by A6
.= (Exec (i,s2)) . c by A60, A64, A68, SCMPDS_2:52 ; :: thesis: verum
end;
end;
end;
end;
end;
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by Th7; :: thesis: verum
end;
suppose A69: InsCode i = 13 ; :: thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
hence (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) by A8; :: thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
consider a, b being Int_position, k1, k2 being Integer such that
A70: i = (a,k1) := (b,k2) by A69, SCMPDS_2:39;
now :: thesis: for c being Int_position holds (Exec (i,s1)) . c = (Exec (i,s2)) . c
let c be Int_position; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
per cases ( DataLoc ((s1 . a),k1) = c or DataLoc ((s1 . a),k1) <> c ) ;
suppose A71: DataLoc ((s1 . a),k1) = c ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A72: DataLoc ((s2 . a),k1) = c by A5, Th7;
thus (Exec (i,s1)) . c = s1 . (DataLoc ((s1 . b),k2)) by A70, A71, SCMPDS_2:47
.= s2 . (DataLoc ((s2 . b),k2)) by A6
.= (Exec (i,s2)) . c by A70, A72, SCMPDS_2:47 ; :: thesis: verum
end;
suppose A73: DataLoc ((s1 . a),k1) <> c ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A74: DataLoc ((s2 . a),k1) <> c by A5, Th7;
thus (Exec (i,s1)) . c = s1 . c by A70, A73, SCMPDS_2:47
.= s2 . c by A5, Th7
.= (Exec (i,s2)) . c by A70, A74, SCMPDS_2:47 ; :: thesis: verum
end;
end;
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by Th7; :: thesis: verum
end;
end;