let s1, s2 be State of SCM+FSA ; :: thesis: for n being Element of NAT
for i being Instruction of SCM+FSA st (IC s1) + n = IC s2 & DataPart s1 = DataPart s2 holds
( (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) & DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) )
let n be Element of NAT ; :: thesis: for i being Instruction of SCM+FSA st (IC s1) + n = IC s2 & DataPart s1 = DataPart s2 holds
( (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) & DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) )
let i be Instruction of SCM+FSA ; :: thesis: ( (IC s1) + n = IC s2 & DataPart s1 = DataPart s2 implies ( (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) & DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) ) )
assume that
A1: (IC s1) + n = IC s2 and
A2: DataPart s1 = DataPart s2 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) & DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) )
set D = Int-Locations \/ FinSeq-Locations ;
reconsider k1 = IC s1 as Element of NAT by ORDINAL1:def 13;
A4: (Next (IC s1)) + n = Next (IC s2)
proof
thus (Next (IC s1)) + n = (insloc (k1 + 1)) + n by NAT_1:39
.= insloc ((k1 + n) + 1)
.= Next (IC s2) by A1, NAT_1:39 ; :: thesis: verum
end;
A5: now
assume that
A6: ( InsCode i < 6 or 8 < InsCode i ) and
A7: InsCode i <> 0 ; :: thesis: (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2)
set I = InsCode i;
A8: not InsCode i in {0 ,6,7,8}
proof
assume A9: InsCode i in {0 ,6,7,8} ; :: thesis: contradiction
end;
not InsCode i in {6,7,8}
proof
assume A10: InsCode i in {6,7,8} ; :: thesis: contradiction
end;
then A11: IncAddr i,n = i by SCMFSA_4:def 3;
IC (Exec i,s1) = Next (IC s1) by A8, Th23;
hence (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) by A4, A8, A11, Th23; :: thesis: verum
end;
A12: InsCode i <= 11 + 1 by SCMFSA_2:35;
A13: ( not InsCode i <= 10 + 1 or InsCode i <= 10 or InsCode i = 11 ) by NAT_1:8;
A14: ( not InsCode i <= 9 + 1 or InsCode i <= 8 + 1 or InsCode i = 10 ) by NAT_1:8;
per cases ( InsCode i = 0 or InsCode i = 1 or InsCode i = 2 or InsCode i = 3 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 ) by A12, A13, A14, NAT_1:8, NAT_1:33;
suppose InsCode i = 0 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) & DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) )
then A15: i = halt SCM+FSA by SCMFSA_2:122;
then ( Exec i,s1 = s1 & Exec i,s2 = s2 ) by AMI_1:def 8;
hence ( (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) & DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) ) by A1, A2, A15, SCMFSA_4:8; :: thesis: verum
end;
suppose A16: InsCode i = 1 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) & DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) )
then consider da, db being Int-Location such that
A17: i = da := db by SCMFSA_2:54;
A18: IncAddr i,n = i by A17, SCMFSA_4:9;
thus (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) by A5, A16; :: thesis: DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2)
A19: now
let c be Int-Location ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
per cases ( c = da or c <> da ) ;
suppose A20: c = da ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
hence (Exec i,s1) . c = s1 . db by A17, SCMFSA_2:89
.= s2 . db by A2, Th38
.= (Exec (IncAddr i,n),s2) . c by A17, A18, A20, SCMFSA_2:89 ;
:: thesis: verum
end;
suppose A21: c <> da ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
hence (Exec i,s1) . c = s1 . c by A17, SCMFSA_2:89
.= s2 . c by A2, Th38
.= (Exec (IncAddr i,n),s2) . c by A17, A18, A21, SCMFSA_2:89 ;
:: thesis: verum
end;
end;
end;
now
let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec (IncAddr i,n),s2) . f
thus (Exec i,s1) . f = s1 . f by A17, SCMFSA_2:89
.= s2 . f by A2, Th38
.= (Exec (IncAddr i,n),s2) . f by A17, A18, SCMFSA_2:89 ; :: thesis: verum
end;
hence DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) by A19, Th38; :: thesis: verum
end;
suppose A22: InsCode i = 2 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) & DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) )
then consider da, db being Int-Location such that
A23: i = AddTo da,db by SCMFSA_2:55;
A24: IncAddr i,n = i by A23, SCMFSA_4:10;
thus (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) by A5, A22; :: thesis: DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2)
A25: now
let c be Int-Location ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
per cases ( c = da or c <> da ) ;
suppose A26: c = da ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
( s1 . da = s2 . da & s1 . db = s2 . db ) by A2, Th38;
hence (Exec i,s1) . c = (s2 . da) + (s2 . db) by A23, A26, SCMFSA_2:90
.= (Exec (IncAddr i,n),s2) . c by A23, A24, A26, SCMFSA_2:90 ;
:: thesis: verum
end;
suppose A27: c <> da ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
hence (Exec i,s1) . c = s1 . c by A23, SCMFSA_2:90
.= s2 . c by A2, Th38
.= (Exec (IncAddr i,n),s2) . c by A23, A24, A27, SCMFSA_2:90 ;
:: thesis: verum
end;
end;
end;
now
let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec (IncAddr i,n),s2) . f
thus (Exec i,s1) . f = s1 . f by A23, SCMFSA_2:90
.= s2 . f by A2, Th38
.= (Exec (IncAddr i,n),s2) . f by A23, A24, SCMFSA_2:90 ; :: thesis: verum
end;
hence DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) by A25, Th38; :: thesis: verum
end;
suppose A28: InsCode i = 3 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) & DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) )
then consider da, db being Int-Location such that
A29: i = SubFrom da,db by SCMFSA_2:56;
A30: IncAddr i,n = i by A29, SCMFSA_4:11;
thus (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) by A5, A28; :: thesis: DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2)
A31: now
let c be Int-Location ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
per cases ( c = da or c <> da ) ;
suppose A32: c = da ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
( s1 . da = s2 . da & s1 . db = s2 . db ) by A2, Th38;
hence (Exec i,s1) . c = (s2 . da) - (s2 . db) by A29, A32, SCMFSA_2:91
.= (Exec (IncAddr i,n),s2) . c by A29, A30, A32, SCMFSA_2:91 ;
:: thesis: verum
end;
suppose A33: c <> da ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
hence (Exec i,s1) . c = s1 . c by A29, SCMFSA_2:91
.= s2 . c by A2, Th38
.= (Exec (IncAddr i,n),s2) . c by A29, A30, A33, SCMFSA_2:91 ;
:: thesis: verum
end;
end;
end;
now
let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec (IncAddr i,n),s2) . f
thus (Exec i,s1) . f = s1 . f by A29, SCMFSA_2:91
.= s2 . f by A2, Th38
.= (Exec (IncAddr i,n),s2) . f by A29, A30, SCMFSA_2:91 ; :: thesis: verum
end;
hence DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) by A31, Th38; :: thesis: verum
end;
suppose A34: InsCode i = 4 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) & DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) )
then consider da, db being Int-Location such that
A35: i = MultBy da,db by SCMFSA_2:57;
thus (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) by A5, A34; :: thesis: DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2)
A36: IncAddr i,n = i by A35, SCMFSA_4:12;
A37: now
let c be Int-Location ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
per cases ( c = da or c <> da ) ;
suppose A38: c = da ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
( s1 . da = s2 . da & s1 . db = s2 . db ) by A2, Th38;
hence (Exec i,s1) . c = (s2 . da) * (s2 . db) by A35, A38, SCMFSA_2:92
.= (Exec (IncAddr i,n),s2) . c by A35, A36, A38, SCMFSA_2:92 ;
:: thesis: verum
end;
suppose A39: c <> da ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
hence (Exec i,s1) . c = s1 . c by A35, SCMFSA_2:92
.= s2 . c by A2, Th38
.= (Exec (IncAddr i,n),s2) . c by A35, A36, A39, SCMFSA_2:92 ;
:: thesis: verum
end;
end;
end;
now
let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec (IncAddr i,n),s2) . f
thus (Exec i,s1) . f = s1 . f by A35, SCMFSA_2:92
.= s2 . f by A2, Th38
.= (Exec (IncAddr i,n),s2) . f by A35, A36, SCMFSA_2:92 ; :: thesis: verum
end;
hence DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) by A37, Th38; :: thesis: verum
end;
suppose A40: InsCode i = 5 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) & DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) )
then consider da, db being Int-Location such that
A41: i = Divide da,db by SCMFSA_2:58;
A42: IncAddr i,n = i by A41, SCMFSA_4:13;
thus (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) by A5, A40; :: thesis: DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2)
A43: now
let c be Int-Location ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
per cases ( c = db or ( c = da & c <> db ) or ( c <> da & c <> db ) ) ;
suppose A44: c = db ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
( s1 . da = s2 . da & s1 . db = s2 . db ) by A2, Th38;
hence (Exec i,s1) . c = (s2 . da) mod (s2 . db) by A41, A44, SCMFSA_2:93
.= (Exec (IncAddr i,n),s2) . c by A41, A42, A44, SCMFSA_2:93 ;
:: thesis: verum
end;
suppose A45: ( c = da & c <> db ) ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
( s1 . da = s2 . da & s1 . db = s2 . db ) by A2, Th38;
hence (Exec i,s1) . c = (s2 . da) div (s2 . db) by A41, A45, SCMFSA_2:93
.= (Exec (IncAddr i,n),s2) . c by A41, A42, A45, SCMFSA_2:93 ;
:: thesis: verum
end;
suppose A46: ( c <> da & c <> db ) ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
hence (Exec i,s1) . c = s1 . c by A41, SCMFSA_2:93
.= s2 . c by A2, Th38
.= (Exec (IncAddr i,n),s2) . c by A41, A42, A46, SCMFSA_2:93 ;
:: thesis: verum
end;
end;
end;
now
let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec (IncAddr i,n),s2) . f
thus (Exec i,s1) . f = s1 . f by A41, SCMFSA_2:93
.= s2 . f by A2, Th38
.= (Exec (IncAddr i,n),s2) . f by A41, A42, SCMFSA_2:93 ; :: thesis: verum
end;
hence DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) by A43, Th38; :: thesis: verum
end;
suppose InsCode i = 6 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) & DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) )
then consider loc being Instruction-Location of SCM+FSA such that
A47: i = goto loc by SCMFSA_2:59;
A48: IncAddr i,n = goto (loc + n) by A47, SCMFSA_4:14;
IC (Exec i,s1) = loc by A47, SCMFSA_2:95;
hence (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) by A48, SCMFSA_2:95; :: thesis: DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2)
A49: now
let c be Int-Location ; :: thesis: (Exec i,s1) . c = (Exec (IncAddr i,n),s2) . c
thus (Exec i,s1) . c = s1 . c by A47, SCMFSA_2:95
.= s2 . c by A2, Th38
.= (Exec (IncAddr i,n),s2) . c by A48, SCMFSA_2:95 ; :: thesis: verum
end;
now
let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec (IncAddr i,n),s2) . f
thus (Exec i,s1) . f = s1 . f by A47, SCMFSA_2:95
.= s2 . f by A2, Th38
.= (Exec (IncAddr i,n),s2) . f by A48, SCMFSA_2:95 ; :: thesis: verum
end;
hence DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) by A49, Th38; :: thesis: verum
end;
suppose InsCode i = 7 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) & DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) )
then consider loc being Instruction-Location of SCM+FSA , da being Int-Location such that
A50: i = da =0_goto loc by SCMFSA_2:60;
A51: IncAddr i,n = da =0_goto (loc + n) by A50, SCMFSA_4:15;
A52: now
let c be Int-Location ; :: thesis: (Exec i,s1) . c = (Exec (IncAddr i,n),s2) . c
thus (Exec i,s1) . c = s1 . c by A50, SCMFSA_2:96
.= s2 . c by A2, Th38
.= (Exec (IncAddr i,n),s2) . c by A51, SCMFSA_2:96 ; :: thesis: verum
end;
A53: now
let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec (IncAddr i,n),s2) . f
thus (Exec i,s1) . f = s1 . f by A50, SCMFSA_2:96
.= s2 . f by A2, Th38
.= (Exec (IncAddr i,n),s2) . f by A51, SCMFSA_2:96 ; :: thesis: verum
end;
hereby :: thesis: DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2)
per cases ( s1 . da = 0 or s1 . da <> 0 ) ;
suppose A54: s1 . da = 0 ; :: thesis: (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2)
then A55: s2 . da = 0 by A2, Th38;
IC (Exec i,s1) = loc by A50, A54, SCMFSA_2:96;
hence (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) by A51, A55, SCMFSA_2:96; :: thesis: verum
end;
suppose A56: s1 . da <> 0 ; :: thesis: (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2)
then A57: s2 . da <> 0 by A2, Th38;
IC (Exec i,s1) = Next (IC s1) by A50, A56, SCMFSA_2:96;
hence (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) by A4, A51, A57, SCMFSA_2:96; :: thesis: verum
end;
end;
end;
thus DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) by A52, A53, Th38; :: thesis: verum
end;
suppose InsCode i = 8 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) & DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) )
then consider loc being Instruction-Location of SCM+FSA , da being Int-Location such that
A58: i = da >0_goto loc by SCMFSA_2:61;
A59: IncAddr i,n = da >0_goto (loc + n) by A58, SCMFSA_4:16;
A60: now
let c be Int-Location ; :: thesis: (Exec i,s1) . c = (Exec (IncAddr i,n),s2) . c
thus (Exec i,s1) . c = s1 . c by A58, SCMFSA_2:97
.= s2 . c by A2, Th38
.= (Exec (IncAddr i,n),s2) . c by A59, SCMFSA_2:97 ; :: thesis: verum
end;
A61: now
let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec (IncAddr i,n),s2) . f
thus (Exec i,s1) . f = s1 . f by A58, SCMFSA_2:97
.= s2 . f by A2, Th38
.= (Exec (IncAddr i,n),s2) . f by A59, SCMFSA_2:97 ; :: thesis: verum
end;
hereby :: thesis: DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2)
per cases ( s1 . da > 0 or s1 . da <= 0 ) ;
suppose A62: s1 . da > 0 ; :: thesis: (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2)
then A63: s2 . da > 0 by A2, Th38;
IC (Exec i,s1) = loc by A58, A62, SCMFSA_2:97;
hence (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) by A59, A63, SCMFSA_2:97; :: thesis: verum
end;
suppose A64: s1 . da <= 0 ; :: thesis: (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2)
then A65: s2 . da <= 0 by A2, Th38;
IC (Exec i,s1) = Next (IC s1) by A58, A64, SCMFSA_2:97;
hence (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) by A4, A59, A65, SCMFSA_2:97; :: thesis: verum
end;
end;
end;
thus DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) by A60, A61, Th38; :: thesis: verum
end;
suppose A66: InsCode i = 9 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) & DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) )
then consider db, da being Int-Location , f being FinSeq-Location such that
A67: i = da := f,db by SCMFSA_2:62;
A68: IncAddr i,n = i by A67, SCMFSA_4:17;
thus (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) by A5, A66; :: thesis: DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2)
A69: now
let c be Int-Location ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
per cases ( c = da or c <> da ) ;
suppose A70: c = da ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
then consider m being Element of NAT such that
A71: m = abs (s1 . db) and
A72: (Exec (da := f,db),s1) . c = (s1 . f) /. m by SCMFSA_2:98;
consider m2 being Element of NAT such that
A73: m2 = abs (s2 . db) and
A74: (Exec (da := f,db),s2) . c = (s2 . f) /. m2 by A70, SCMFSA_2:98;
( m = m2 & s1 . f = s2 . f ) by A2, A71, A73, Th38;
hence (Exec i,s1) . c = (Exec (IncAddr i,n),s2) . c by A67, A72, A74, SCMFSA_4:17; :: thesis: verum
end;
suppose A75: c <> da ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
hence (Exec i,s1) . c = s1 . c by A67, SCMFSA_2:98
.= s2 . c by A2, Th38
.= (Exec (IncAddr i,n),s2) . c by A67, A68, A75, SCMFSA_2:98 ;
:: thesis: verum
end;
end;
end;
now
let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec (IncAddr i,n),s2) . f
thus (Exec i,s1) . f = s1 . f by A67, SCMFSA_2:98
.= s2 . f by A2, Th38
.= (Exec (IncAddr i,n),s2) . f by A67, A68, SCMFSA_2:98 ; :: thesis: verum
end;
hence DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) by A69, Th38; :: thesis: verum
end;
suppose A76: InsCode i = 10 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) & DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) )
then consider db, da being Int-Location , f being FinSeq-Location such that
A77: i = f,db := da by SCMFSA_2:63;
A78: IncAddr i,n = i by A77, SCMFSA_4:18;
thus (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) by A5, A76; :: thesis: DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2)
A79: now
let c be Int-Location ; :: thesis: (Exec i,s1) . c = (Exec (IncAddr i,n),s2) . c
thus (Exec i,s1) . c = s1 . c by A77, SCMFSA_2:99
.= s2 . c by A2, Th38
.= (Exec (IncAddr i,n),s2) . c by A77, A78, SCMFSA_2:99 ; :: thesis: verum
end;
now
let g be FinSeq-Location ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
per cases ( g = f or g <> f ) ;
suppose A80: g = f ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
consider m1 being Element of NAT such that
A81: m1 = abs (s1 . db) and
A82: (Exec (f,db := da),s1) . f = (s1 . f) +* m1,(s1 . da) by SCMFSA_2:99;
consider m2 being Element of NAT such that
A83: m2 = abs (s2 . db) and
A84: (Exec (f,db := da),s2) . f = (s2 . f) +* m2,(s2 . da) by SCMFSA_2:99;
( m1 = m2 & s1 . da = s2 . da & s1 . f = s2 . f ) by A2, A81, A83, Th38;
hence (Exec i,s1) . g = (Exec (IncAddr i,n),s2) . g by A77, A80, A82, A84, SCMFSA_4:18; :: thesis: verum
end;
suppose A85: g <> f ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
hence (Exec i,s1) . g = s1 . g by A77, SCMFSA_2:99
.= s2 . g by A2, Th38
.= (Exec (IncAddr i,n),s2) . g by A77, A78, A85, SCMFSA_2:99 ;
:: thesis: verum
end;
end;
end;
hence DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) by A79, Th38; :: thesis: verum
end;
suppose A86: InsCode i = 11 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) & DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) )
then consider da being Int-Location , f being FinSeq-Location such that
A87: i = da :=len f by SCMFSA_2:64;
A88: IncAddr i,n = i by A87, SCMFSA_4:19;
thus (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) by A5, A86; :: thesis: DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2)
A89: now
let c be Int-Location ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
per cases ( c = da or c <> da ) ;
suppose A90: c = da ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
hence (Exec i,s1) . c = len (s1 . f) by A87, SCMFSA_2:100
.= len (s2 . f) by A2, Th38
.= (Exec (IncAddr i,n),s2) . c by A87, A88, A90, SCMFSA_2:100 ;
:: thesis: verum
end;
suppose A91: c <> da ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
hence (Exec i,s1) . c = s1 . c by A87, SCMFSA_2:100
.= s2 . c by A2, Th38
.= (Exec (IncAddr i,n),s2) . c by A87, A88, A91, SCMFSA_2:100 ;
:: thesis: verum
end;
end;
end;
now
let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec (IncAddr i,n),s2) . f
thus (Exec i,s1) . f = s1 . f by A87, SCMFSA_2:100
.= s2 . f by A2, Th38
.= (Exec (IncAddr i,n),s2) . f by A87, A88, SCMFSA_2:100 ; :: thesis: verum
end;
hence DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) by A89, Th38; :: thesis: verum
end;
suppose A92: InsCode i = 12 ; :: thesis: ( (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) & DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) )
then consider da being Int-Location , f being FinSeq-Location such that
A93: i = f :=<0,...,0> da by SCMFSA_2:65;
A94: IncAddr i,n = i by A93, SCMFSA_4:20;
thus (IC (Exec i,s1)) + n = IC (Exec (IncAddr i,n),s2) by A5, A92; :: thesis: DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2)
A95: now
let c be Int-Location ; :: thesis: (Exec i,s1) . c = (Exec (IncAddr i,n),s2) . c
thus (Exec i,s1) . c = s1 . c by A93, SCMFSA_2:101
.= s2 . c by A2, Th38
.= (Exec (IncAddr i,n),s2) . c by A93, A94, SCMFSA_2:101 ; :: thesis: verum
end;
now
let g be FinSeq-Location ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
per cases ( g = f or g <> f ) ;
suppose A96: g = f ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
consider m1 being Element of NAT such that
A97: m1 = abs (s1 . da) and
A98: (Exec (f :=<0,...,0> da),s1) . f = m1 |-> 0 by SCMFSA_2:101;
consider m2 being Element of NAT such that
A99: m2 = abs (s2 . da) and
A100: (Exec (f :=<0,...,0> da),s2) . f = m2 |-> 0 by SCMFSA_2:101;
thus (Exec i,s1) . g = (Exec (IncAddr i,n),s2) . g by A2, A93, A94, A96, A97, A98, A99, A100, Th38; :: thesis: verum
end;
suppose A101: g <> f ; :: thesis: (Exec i,s1) . b1 = (Exec (IncAddr i,n),s2) . b1
hence (Exec i,s1) . g = s1 . g by A93, SCMFSA_2:101
.= s2 . g by A2, Th38
.= (Exec (IncAddr i,n),s2) . g by A93, A94, A101, SCMFSA_2:101 ;
:: thesis: verum
end;
end;
end;
hence DataPart (Exec i,s1) = DataPart (Exec (IncAddr i,n),s2) by A95, Th38; :: thesis: verum
end;
end;