set D = Data-Locations ;
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)) )
reconsider k1 = IC s1 as Element of NAT ;
A3: (succ (IC s1)) + n = (k1 + 1) + n by NAT_1:38
.= (k1 + n) + 1
.= succ (IC s2) by A1, NAT_1:38 ;

A4: now

set I = InsCode i;
assume that
A5: ( InsCode i < 6 or 8 < InsCode i ) and
A6: InsCode i <> 0 ; :: thesis: (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2))
( not InsCode i = 6 & not InsCode i = 7 & not InsCode i = 8 ) by A5;
then not InsCode i in {6,7,8} by ENUMSET1:def 1;
then A7: IncAddr (i,n) = i by SCMFSA_4:4;
( not InsCode i = 0 & not InsCode i = 6 & not InsCode i = 7 & not InsCode i = 8 ) by A5, A6;
then A8: not InsCode i in {0,6,7,8} by ENUMSET1:def 2;
then IC (Exec (i,s1)) = succ (IC s1) by Th23;
hence (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A3, A8, A7, Th23; :: thesis: verum

end;

A12: InsCode i <= 12 by SCMFSA_2:16;

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, NAT_1:36;

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 A13: i = halt SCM+FSA by SCMFSA_2:95;
then ( Exec (i,s1) = s1 & Exec (i,s2) = s2 ) by EXTPRO_1:def 3;
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, A13, COMPOS_1:11; :: thesis: verum

end;

suppose A14: 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)) )

hence (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A4; :: thesis: DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2))
consider da, db being Int-Location such that
A15: i = da := db by A14, SCMFSA_2:30;
A16: IncAddr (i,n) = i by A15, COMPOS_1:11;

A17: now

let c be Int-Location ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

per cases ( c = da or c <> da ) ;

suppose A18: c = da ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

hence (Exec (i,s1)) . c = s1 . db by A15, SCMFSA_2:63
.= s2 . db by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . c by A15, A16, A18, SCMFSA_2:63 ;
:: thesis: verum

end;

suppose A19: c <> da ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

hence (Exec (i,s1)) . c = s1 . c by A15, SCMFSA_2:63
.= s2 . c by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . c by A15, A16, A19, SCMFSA_2:63 ;
:: 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 A15, SCMFSA_2:63
.= s2 . f by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . f by A15, A16, SCMFSA_2:63 ; :: thesis: verum

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A17, Th38; :: thesis: verum

end;

suppose A20: 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)) )

hence (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A4; :: thesis: DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2))
consider da, db being Int-Location such that
A21: i = AddTo (da,db) by A20, SCMFSA_2:31;
A22: IncAddr (i,n) = i by A21, COMPOS_1:11;

A23: now

let c be Int-Location ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

per cases ( c = da or c <> da ) ;

suppose A24: c = da ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

( s1 . da = s2 . da & s1 . db = s2 . db ) by A2, Th38;
hence (Exec (i,s1)) . c = (s2 . da) + (s2 . db) by A21, A24, SCMFSA_2:64
.= (Exec ((IncAddr (i,n)),s2)) . c by A21, A22, A24, SCMFSA_2:64 ;
:: thesis: verum

end;

suppose A25: c <> da ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

hence (Exec (i,s1)) . c = s1 . c by A21, SCMFSA_2:64
.= s2 . c by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . c by A21, A22, A25, SCMFSA_2:64 ;
:: 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 A21, SCMFSA_2:64
.= s2 . f by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . f by A21, A22, SCMFSA_2:64 ; :: thesis: verum

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A23, Th38; :: thesis: verum

end;

suppose A26: 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)) )

hence (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A4; :: thesis: DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2))
consider da, db being Int-Location such that
A27: i = SubFrom (da,db) by A26, SCMFSA_2:32;
A28: IncAddr (i,n) = i by A27, COMPOS_1:11;

A29: now

let c be Int-Location ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

per cases ( c = da or c <> da ) ;

suppose A30: c = da ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

( s1 . da = s2 . da & s1 . db = s2 . db ) by A2, Th38;
hence (Exec (i,s1)) . c = (s2 . da) - (s2 . db) by A27, A30, SCMFSA_2:65
.= (Exec ((IncAddr (i,n)),s2)) . c by A27, A28, A30, SCMFSA_2:65 ;
:: thesis: verum

end;

suppose A31: c <> da ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

hence (Exec (i,s1)) . c = s1 . c by A27, SCMFSA_2:65
.= s2 . c by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . c by A27, A28, A31, SCMFSA_2:65 ;
:: 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 A27, SCMFSA_2:65
.= s2 . f by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . f by A27, A28, SCMFSA_2:65 ; :: thesis: verum

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A29, Th38; :: thesis: verum

end;

suppose A32: 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)) )

hence (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A4; :: thesis: DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2))
consider da, db being Int-Location such that
A33: i = MultBy (da,db) by A32, SCMFSA_2:33;
A34: IncAddr (i,n) = i by A33, COMPOS_1:11;

A35: now

let c be Int-Location ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

per cases ( c = da or c <> da ) ;

suppose A36: c = da ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

( s1 . da = s2 . da & s1 . db = s2 . db ) by A2, Th38;
hence (Exec (i,s1)) . c = (s2 . da) * (s2 . db) by A33, A36, SCMFSA_2:66
.= (Exec ((IncAddr (i,n)),s2)) . c by A33, A34, A36, SCMFSA_2:66 ;
:: thesis: verum

end;

suppose A37: c <> da ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

hence (Exec (i,s1)) . c = s1 . c by A33, SCMFSA_2:66
.= s2 . c by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . c by A33, A34, A37, SCMFSA_2:66 ;
:: 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 A33, SCMFSA_2:66
.= s2 . f by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . f by A33, A34, SCMFSA_2:66 ; :: thesis: verum

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A35, Th38; :: thesis: verum

end;

suppose A38: 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)) )

hence (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A4; :: thesis: DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2))
consider da, db being Int-Location such that
A39: i = Divide (da,db) by A38, SCMFSA_2:34;
A40: IncAddr (i,n) = i by A39, COMPOS_1:11;

A41: now

let c be Int-Location ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

per cases ( c = db or ( c = da & c <> db ) or ( c <> da & c <> db ) ) ;

suppose A42: c = db ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

( s1 . da = s2 . da & s1 . db = s2 . db ) by A2, Th38;
hence (Exec (i,s1)) . c = (s2 . da) mod (s2 . db) by A39, A42, SCMFSA_2:67
.= (Exec ((IncAddr (i,n)),s2)) . c by A39, A40, A42, SCMFSA_2:67 ;
:: thesis: verum

end;

suppose A43: ( c = da & c <> db ) ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

( s1 . da = s2 . da & s1 . db = s2 . db ) by A2, Th38;
hence (Exec (i,s1)) . c = (s2 . da) div (s2 . db) by A39, A43, SCMFSA_2:67
.= (Exec ((IncAddr (i,n)),s2)) . c by A39, A40, A43, SCMFSA_2:67 ;
:: thesis: verum

end;

suppose A44: ( c <> da & c <> db ) ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

hence (Exec (i,s1)) . c = s1 . c by A39, SCMFSA_2:67
.= s2 . c by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . c by A39, A40, A44, SCMFSA_2:67 ;
:: 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 A39, SCMFSA_2:67
.= s2 . f by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . f by A39, A40, SCMFSA_2:67 ; :: thesis: verum

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A41, 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 Element of NAT such that
A45: i = goto loc by SCMFSA_2:35;
A46: IncAddr (i,n) = goto (loc + n) by A45, SCMFSA_4:1;

A47: 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 A45, SCMFSA_2:69
.= s2 . f by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . f by A46, SCMFSA_2:69 ; :: thesis: verum

end;

IC (Exec (i,s1)) = loc by A45, SCMFSA_2:69;
hence (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A46, SCMFSA_2:69; :: thesis: DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2))

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 A45, SCMFSA_2:69
.= s2 . c by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . c by A46, SCMFSA_2:69 ; :: thesis: verum

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A47, 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 Element of NAT , da being Int-Location such that
A48: i = da =0_goto loc by SCMFSA_2:36;
A49: IncAddr (i,n) = da =0_goto (loc + n) by A48, SCMFSA_4:2;

A50: 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 A48, SCMFSA_2:70
.= s2 . f by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . f by A49, SCMFSA_2:70 ; :: 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 s1 . da = 0 ; :: thesis: (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2))

then ( s2 . da = 0 & IC (Exec (i,s1)) = loc ) by A2, A48, Th38, SCMFSA_2:70;
hence (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A49, SCMFSA_2:70; :: thesis: verum

end;

suppose s1 . da <> 0 ; :: thesis: (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2))

then ( s2 . da <> 0 & IC (Exec (i,s1)) = succ (IC s1) ) by A2, A48, Th38, SCMFSA_2:70;
hence (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A3, A49, SCMFSA_2:70; :: thesis: verum

end;

end;

end;

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 A48, SCMFSA_2:70
.= s2 . c by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . c by A49, SCMFSA_2:70 ; :: thesis: verum

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A50, 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 Element of NAT , da being Int-Location such that
A51: i = da >0_goto loc by SCMFSA_2:37;
A52: IncAddr (i,n) = da >0_goto (loc + n) by A51, SCMFSA_4:3;

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 A51, SCMFSA_2:71
.= s2 . f by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . f by A52, SCMFSA_2:71 ; :: 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 s1 . da > 0 ; :: thesis: (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2))

then ( s2 . da > 0 & IC (Exec (i,s1)) = loc ) by A2, A51, Th38, SCMFSA_2:71;
hence (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A52, SCMFSA_2:71; :: thesis: verum

end;

suppose s1 . da <= 0 ; :: thesis: (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2))

then ( s2 . da <= 0 & IC (Exec (i,s1)) = succ (IC s1) ) by A2, A51, Th38, SCMFSA_2:71;
hence (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A3, A52, SCMFSA_2:71; :: thesis: verum

end;

end;

end;

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 A51, SCMFSA_2:71
.= s2 . c by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . c by A52, SCMFSA_2:71 ; :: thesis: verum

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A53, Th38; :: thesis: verum

end;

suppose A54: 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)) )

hence (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A4; :: thesis: DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2))
consider db, da being Int-Location , f being FinSeq-Location such that
A55: i = da := (f,db) by A54, SCMFSA_2:38;
A56: IncAddr (i,n) = i by A55, COMPOS_1:11;

A57: now

let c be Int-Location ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

per cases ( c = da or c <> da ) ;

suppose A58: c = da ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

then consider m being Element of NAT such that
A59: m = abs (s1 . db) and
A60: (Exec ((da := (f,db)),s1)) . c = (s1 . f) /. m by SCMFSA_2:72;
A61: s1 . f = s2 . f by A2, Th38;
consider m2 being Element of NAT such that
A62: m2 = abs (s2 . db) and
A63: (Exec ((da := (f,db)),s2)) . c = (s2 . f) /. m2 by A58, SCMFSA_2:72;
m = m2 by A2, A59, A62, Th38;
hence (Exec (i,s1)) . c = (Exec ((IncAddr (i,n)),s2)) . c by A55, A60, A63, A61, COMPOS_1:11; :: thesis: verum

end;

suppose A64: c <> da ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

hence (Exec (i,s1)) . c = s1 . c by A55, SCMFSA_2:72
.= s2 . c by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . c by A55, A56, A64, SCMFSA_2:72 ;
:: 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 A55, SCMFSA_2:72
.= s2 . f by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . f by A55, A56, SCMFSA_2:72 ; :: thesis: verum

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A57, Th38; :: thesis: verum

end;

suppose A65: 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)) )

hence (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A4; :: thesis: DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2))
consider db, da being Int-Location , f being FinSeq-Location such that
A66: i = (f,db) := da by A65, SCMFSA_2:39;
A67: IncAddr (i,n) = i by A66, COMPOS_1:11;

A68: now

let g be FinSeq-Location ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

per cases ( g = f or g <> f ) ;

suppose A69: g = f ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

A70: ( s1 . da = s2 . da & s1 . f = s2 . f ) by A2, Th38;
consider m2 being Element of NAT such that
A71: m2 = abs (s2 . db) and
A72: (Exec (((f,db) := da),s2)) . f = (s2 . f) +* (m2,(s2 . da)) by SCMFSA_2:73;
consider m1 being Element of NAT such that
A73: m1 = abs (s1 . db) and
A74: (Exec (((f,db) := da),s1)) . f = (s1 . f) +* (m1,(s1 . da)) by SCMFSA_2:73;
m1 = m2 by A2, A73, A71, Th38;
hence (Exec (i,s1)) . g = (Exec ((IncAddr (i,n)),s2)) . g by A66, A69, A74, A72, A70, COMPOS_1:11; :: thesis: verum

end;

suppose A75: g <> f ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

hence (Exec (i,s1)) . g = s1 . g by A66, SCMFSA_2:73
.= s2 . g by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . g by A66, A67, A75, SCMFSA_2:73 ;
:: thesis: verum

end;

end;

end;

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 A66, SCMFSA_2:73
.= s2 . c by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . c by A66, A67, SCMFSA_2:73 ; :: thesis: verum

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A68, Th38; :: thesis: verum

end;

suppose A76: 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)) )

hence (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A4; :: thesis: DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2))
consider da being Int-Location , f being FinSeq-Location such that
A77: i = da :=len f by A76, SCMFSA_2:40;
A78: IncAddr (i,n) = i by A77, COMPOS_1:11;

A79: now

let c be Int-Location ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

per cases ( c = da or c <> da ) ;

suppose A80: c = da ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

hence (Exec (i,s1)) . c = len (s1 . f) by A77, SCMFSA_2:74
.= len (s2 . f) by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . c by A77, A78, A80, SCMFSA_2:74 ;
:: thesis: verum

end;

suppose A81: c <> da ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

hence (Exec (i,s1)) . c = s1 . c by A77, SCMFSA_2:74
.= s2 . c by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . c by A77, A78, A81, SCMFSA_2:74 ;
:: 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 A77, SCMFSA_2:74
.= s2 . f by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . f by A77, A78, SCMFSA_2:74 ; :: thesis: verum

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A79, Th38; :: thesis: verum

end;

suppose A82: 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)) )

hence (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A4; :: thesis: DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2))
consider da being Int-Location , f being FinSeq-Location such that
A83: i = f :=<0,...,0> da by A82, SCMFSA_2:41;
A84: IncAddr (i,n) = i by A83, COMPOS_1:11;

A85: now

let g be FinSeq-Location ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

per cases ( g = f or g <> f ) ;

suppose A86: g = f ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

( ex m1 being Element of NAT st
( m1 = abs (s1 . da) & (Exec ((f :=<0,...,0> da),s1)) . f = m1 |-> 0 ) & ex m2 being Element of NAT st
( m2 = abs (s2 . da) & (Exec ((f :=<0,...,0> da),s2)) . f = m2 |-> 0 ) ) by SCMFSA_2:75;
hence (Exec (i,s1)) . g = (Exec ((IncAddr (i,n)),s2)) . g by A2, A83, A84, A86, Th38; :: thesis: verum

end;

suppose A87: g <> f ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

hence (Exec (i,s1)) . g = s1 . g by A83, SCMFSA_2:75
.= s2 . g by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . g by A83, A84, A87, SCMFSA_2:75 ;
:: thesis: verum

end;

end;

end;

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 A83, SCMFSA_2:75
.= s2 . c by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . c by A83, A84, SCMFSA_2:75 ; :: thesis: verum

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A85, Th38; :: thesis: verum

end;

end;