set D = Data-Locations ;
let s1, s2 be State of SCM+FSA; :: thesis: for n being 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 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: ((IC s1) + 1) + n = (k1 + 1) + n
.= (IC s2) + 1 by A1 ;

A4: now :: thesis: ( ( InsCode i < 6 or 8 < InsCode i ) & InsCode i <> 0 implies (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) )

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 = 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 = 8 ) by A5, A6;
then A8: not InsCode i in {0,6,7,8} by ENUMSET1:def 2;
then IC (Exec (i,s1)) = (IC s1) + 1 by Th3;
hence (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A3, A8, A7, Th3; :: thesis: verum

end;

not not InsCode i = 0 & ... & not InsCode i = 12 by SCMFSA_2:16;

per cases then ( 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 ) ;

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 A9: 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, A9, COMPOS_0:4; :: thesis: verum

end;

suppose A10: 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
A11: i = da := db by A10, SCMFSA_2:30;
A12: IncAddr (i,n) = i by A11, COMPOS_0:4;

A13: now :: thesis: for c being Int-Location holds (Exec (i,s1)) . c = (Exec ((IncAddr (i,n)),s2)) . c

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

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

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

hence (Exec (i,s1)) . c = s1 . db by A11, SCMFSA_2:63
.= s2 . db by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A11, A12, A14, SCMFSA_2:63 ;
:: thesis: verum

end;

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

hence (Exec (i,s1)) . c = s1 . c by A11, SCMFSA_2:63
.= s2 . c by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A11, A12, A15, SCMFSA_2:63 ;
:: thesis: verum

end;

end;

end;

now :: thesis: for f being FinSeq-Location holds (Exec (i,s1)) . f = (Exec ((IncAddr (i,n)),s2)) . f

let f be FinSeq-Location ; :: thesis: (Exec (i,s1)) . f = (Exec ((IncAddr (i,n)),s2)) . f
thus (Exec (i,s1)) . f = s1 . f by A11, SCMFSA_2:63
.= s2 . f by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . f by A11, A12, SCMFSA_2:63 ; :: thesis: verum

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A13, SCMFSA_M:2; :: thesis: verum

end;

suppose A16: 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
A17: i = AddTo (da,db) by A16, SCMFSA_2:31;
A18: IncAddr (i,n) = i by A17, COMPOS_0:4;

A19: now :: thesis: for c being Int-Location holds (Exec (i,s1)) . c = (Exec ((IncAddr (i,n)),s2)) . c

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

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

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

( s1 . da = s2 . da & s1 . db = s2 . db ) by A2, SCMFSA_M:2;
hence (Exec (i,s1)) . c = (s2 . da) + (s2 . db) by A17, A20, SCMFSA_2:64
.= (Exec ((IncAddr (i,n)),s2)) . c by A17, A18, A20, SCMFSA_2:64 ;
:: thesis: verum

end;

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

hence (Exec (i,s1)) . c = s1 . c by A17, SCMFSA_2:64
.= s2 . c by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A17, A18, A21, SCMFSA_2:64 ;
:: thesis: verum

end;

end;

end;

now :: thesis: for f being FinSeq-Location holds (Exec (i,s1)) . f = (Exec ((IncAddr (i,n)),s2)) . f

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:64
.= s2 . f by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . f by A17, A18, SCMFSA_2:64 ; :: thesis: verum

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A19, SCMFSA_M:2; :: thesis: verum

end;

suppose A22: 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
A23: i = SubFrom (da,db) by A22, SCMFSA_2:32;
A24: IncAddr (i,n) = i by A23, COMPOS_0:4;

A25: now :: thesis: for c being Int-Location holds (Exec (i,s1)) . c = (Exec ((IncAddr (i,n)),s2)) . c

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

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

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

( s1 . da = s2 . da & s1 . db = s2 . db ) by A2, SCMFSA_M:2;
hence (Exec (i,s1)) . c = (s2 . da) - (s2 . db) by A23, A26, SCMFSA_2:65
.= (Exec ((IncAddr (i,n)),s2)) . c by A23, A24, A26, SCMFSA_2:65 ;
:: thesis: verum

end;

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

hence (Exec (i,s1)) . c = s1 . c by A23, SCMFSA_2:65
.= s2 . c by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A23, A24, A27, SCMFSA_2:65 ;
:: thesis: verum

end;

end;

end;

now :: thesis: for f being FinSeq-Location holds (Exec (i,s1)) . f = (Exec ((IncAddr (i,n)),s2)) . f

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:65
.= s2 . f by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . f by A23, A24, SCMFSA_2:65 ; :: thesis: verum

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A25, SCMFSA_M:2; :: thesis: verum

end;

suppose A28: 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
A29: i = MultBy (da,db) by A28, SCMFSA_2:33;
A30: IncAddr (i,n) = i by A29, COMPOS_0:4;

A31: now :: thesis: for c being Int-Location holds (Exec (i,s1)) . c = (Exec ((IncAddr (i,n)),s2)) . c

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

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

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

( s1 . da = s2 . da & s1 . db = s2 . db ) by A2, SCMFSA_M:2;
hence (Exec (i,s1)) . c = (s2 . da) * (s2 . db) by A29, A32, SCMFSA_2:66
.= (Exec ((IncAddr (i,n)),s2)) . c by A29, A30, A32, SCMFSA_2:66 ;
:: thesis: verum

end;

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

hence (Exec (i,s1)) . c = s1 . c by A29, SCMFSA_2:66
.= s2 . c by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A29, A30, A33, SCMFSA_2:66 ;
:: thesis: verum

end;

end;

end;

now :: thesis: for f being FinSeq-Location holds (Exec (i,s1)) . f = (Exec ((IncAddr (i,n)),s2)) . f

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:66
.= s2 . f by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . f by A29, A30, SCMFSA_2:66 ; :: thesis: verum

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A31, SCMFSA_M:2; :: thesis: verum

end;

suppose A34: 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
A35: i = Divide (da,db) by A34, SCMFSA_2:34;
A36: IncAddr (i,n) = i by A35, COMPOS_0:4;

A37: now :: thesis: for c being Int-Location holds (Exec (i,s1)) . c = (Exec ((IncAddr (i,n)),s2)) . c

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 A38: c = db ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

( s1 . da = s2 . da & s1 . db = s2 . db ) by A2, SCMFSA_M:2;
hence (Exec (i,s1)) . c = (s2 . da) mod (s2 . db) by A35, A38, SCMFSA_2:67
.= (Exec ((IncAddr (i,n)),s2)) . c by A35, A36, A38, SCMFSA_2:67 ;
:: thesis: verum

end;

suppose A39: ( 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, SCMFSA_M:2;
hence (Exec (i,s1)) . c = (s2 . da) div (s2 . db) by A35, A39, SCMFSA_2:67
.= (Exec ((IncAddr (i,n)),s2)) . c by A35, A36, A39, SCMFSA_2:67 ;
:: thesis: verum

end;

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

hence (Exec (i,s1)) . c = s1 . c by A35, SCMFSA_2:67
.= s2 . c by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A35, A36, A40, SCMFSA_2:67 ;
:: thesis: verum

end;

end;

end;

now :: thesis: for f being FinSeq-Location holds (Exec (i,s1)) . f = (Exec ((IncAddr (i,n)),s2)) . f

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:67
.= s2 . f by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . f by A35, A36, SCMFSA_2:67 ; :: thesis: verum

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A37, SCMFSA_M:2; :: 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 Nat such that
A41: i = goto loc by SCMFSA_2:35;
A42: IncAddr (i,n) = goto (loc + n) by A41, SCMFSA_4:1;

A43: now :: thesis: for f being FinSeq-Location holds (Exec (i,s1)) . f = (Exec ((IncAddr (i,n)),s2)) . f

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:69
.= s2 . f by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . f by A42, SCMFSA_2:69 ; :: thesis: verum

end;

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

now :: thesis: for c being Int-Location holds (Exec (i,s1)) . c = (Exec ((IncAddr (i,n)),s2)) . c

let c be Int-Location; :: thesis: (Exec (i,s1)) . c = (Exec ((IncAddr (i,n)),s2)) . c
thus (Exec (i,s1)) . c = s1 . c by A41, SCMFSA_2:69
.= s2 . c by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A42, SCMFSA_2:69 ; :: thesis: verum

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A43, SCMFSA_M:2; :: 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 Nat, da being Int-Location such that
A44: i = da =0_goto loc by SCMFSA_2:36;
A45: IncAddr (i,n) = da =0_goto (loc + n) by A44, SCMFSA_4:2;

A46: now :: thesis: for f being FinSeq-Location holds (Exec (i,s1)) . f = (Exec ((IncAddr (i,n)),s2)) . f

let f be FinSeq-Location ; :: thesis: (Exec (i,s1)) . f = (Exec ((IncAddr (i,n)),s2)) . f
thus (Exec (i,s1)) . f = s1 . f by A44, SCMFSA_2:70
.= s2 . f by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . f by A45, 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, A44, SCMFSA_2:70, SCMFSA_M:2;
hence (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A45, 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)) = (IC s1) + 1 ) by A2, A44, SCMFSA_2:70, SCMFSA_M:2;
hence (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A3, A45, SCMFSA_2:70; :: thesis: verum

end;

end;

end;

now :: thesis: for c being Int-Location holds (Exec (i,s1)) . c = (Exec ((IncAddr (i,n)),s2)) . c

let c be Int-Location; :: thesis: (Exec (i,s1)) . c = (Exec ((IncAddr (i,n)),s2)) . c
thus (Exec (i,s1)) . c = s1 . c by A44, SCMFSA_2:70
.= s2 . c by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A45, SCMFSA_2:70 ; :: thesis: verum

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A46, SCMFSA_M:2; :: 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 Nat, da being Int-Location such that
A47: i = da >0_goto loc by SCMFSA_2:37;
A48: IncAddr (i,n) = da >0_goto (loc + n) by A47, SCMFSA_4:3;

A49: now :: thesis: for f being FinSeq-Location holds (Exec (i,s1)) . f = (Exec ((IncAddr (i,n)),s2)) . f

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:71
.= s2 . f by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . f by A48, 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, A47, SCMFSA_2:71, SCMFSA_M:2;
hence (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A48, 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)) = (IC s1) + 1 ) by A2, A47, SCMFSA_2:71, SCMFSA_M:2;
hence (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A3, A48, SCMFSA_2:71; :: thesis: verum

end;

end;

end;

now :: thesis: for c being Int-Location holds (Exec (i,s1)) . c = (Exec ((IncAddr (i,n)),s2)) . c

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

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A49, SCMFSA_M:2; :: thesis: verum

end;

suppose A50: 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
A51: i = da := (f,db) by A50, SCMFSA_2:38;
A52: IncAddr (i,n) = i by A51, COMPOS_0:4;

A53: now :: thesis: for c being Int-Location holds (Exec (i,s1)) . c = (Exec ((IncAddr (i,n)),s2)) . c

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

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

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

then consider m being Nat such that
A55: m = |.(s1 . db).| and
A56: (Exec ((da := (f,db)),s1)) . c = (s1 . f) /. m by SCMFSA_2:72;
A57: s1 . f = s2 . f by A2, SCMFSA_M:2;
consider m2 being Nat such that
A58: m2 = |.(s2 . db).| and
A59: (Exec ((da := (f,db)),s2)) . c = (s2 . f) /. m2 by A54, SCMFSA_2:72;
m = m2 by A2, A55, A58, SCMFSA_M:2;
hence (Exec (i,s1)) . c = (Exec ((IncAddr (i,n)),s2)) . c by A51, A56, A59, A57, COMPOS_0:4; :: thesis: verum

end;

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

hence (Exec (i,s1)) . c = s1 . c by A51, SCMFSA_2:72
.= s2 . c by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A51, A52, A60, SCMFSA_2:72 ;
:: thesis: verum

end;

end;

end;

now :: thesis: for f being FinSeq-Location holds (Exec (i,s1)) . f = (Exec ((IncAddr (i,n)),s2)) . f

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:72
.= s2 . f by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . f by A51, A52, SCMFSA_2:72 ; :: thesis: verum

end;

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

end;

suppose A61: 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
A62: i = (f,db) := da by A61, SCMFSA_2:39;
A63: IncAddr (i,n) = i by A62, COMPOS_0:4;

A64: now :: thesis: for g being FinSeq-Location holds (Exec (i,s1)) . g = (Exec ((IncAddr (i,n)),s2)) . g

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

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

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

A66: ( s1 . da = s2 . da & s1 . f = s2 . f ) by A2, SCMFSA_M:2;
consider m2 being Nat such that
A67: m2 = |.(s2 . db).| and
A68: (Exec (((f,db) := da),s2)) . f = (s2 . f) +* (m2,(s2 . da)) by SCMFSA_2:73;
consider m1 being Nat such that
A69: m1 = |.(s1 . db).| and
A70: (Exec (((f,db) := da),s1)) . f = (s1 . f) +* (m1,(s1 . da)) by SCMFSA_2:73;
m1 = m2 by A2, A69, A67, SCMFSA_M:2;
hence (Exec (i,s1)) . g = (Exec ((IncAddr (i,n)),s2)) . g by A62, A65, A70, A68, A66, COMPOS_0:4; :: thesis: verum

end;

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

hence (Exec (i,s1)) . g = s1 . g by A62, SCMFSA_2:73
.= s2 . g by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . g by A62, A63, A71, SCMFSA_2:73 ;
:: thesis: verum

end;

end;

end;

now :: thesis: for c being Int-Location holds (Exec (i,s1)) . c = (Exec ((IncAddr (i,n)),s2)) . c

let c be Int-Location; :: thesis: (Exec (i,s1)) . c = (Exec ((IncAddr (i,n)),s2)) . c
thus (Exec (i,s1)) . c = s1 . c by A62, SCMFSA_2:73
.= s2 . c by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A62, A63, SCMFSA_2:73 ; :: thesis: verum

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A64, SCMFSA_M:2; :: thesis: verum

end;

suppose A72: 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
A73: i = da :=len f by A72, SCMFSA_2:40;
A74: IncAddr (i,n) = i by A73, COMPOS_0:4;

A75: now :: thesis: for c being Int-Location holds (Exec (i,s1)) . c = (Exec ((IncAddr (i,n)),s2)) . c

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

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

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

hence (Exec (i,s1)) . c = len (s1 . f) by A73, SCMFSA_2:74
.= len (s2 . f) by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A73, A74, A76, SCMFSA_2:74 ;
:: thesis: verum

end;

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

hence (Exec (i,s1)) . c = s1 . c by A73, SCMFSA_2:74
.= s2 . c by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A73, A74, A77, SCMFSA_2:74 ;
:: thesis: verum

end;

end;

end;

now :: thesis: for f being FinSeq-Location holds (Exec (i,s1)) . f = (Exec ((IncAddr (i,n)),s2)) . f

let f be FinSeq-Location ; :: thesis: (Exec (i,s1)) . f = (Exec ((IncAddr (i,n)),s2)) . f
thus (Exec (i,s1)) . f = s1 . f by A73, SCMFSA_2:74
.= s2 . f by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . f by A73, A74, SCMFSA_2:74 ; :: thesis: verum

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A75, SCMFSA_M:2; :: thesis: verum

end;

suppose A78: 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
A79: i = f :=<0,...,0> da by A78, SCMFSA_2:41;
A80: IncAddr (i,n) = i by A79, COMPOS_0:4;

A81: now :: thesis: for g being FinSeq-Location holds (Exec (i,s1)) . g = (Exec ((IncAddr (i,n)),s2)) . g

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

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

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

( ex m1 being Nat st
( m1 = |.(s1 . da).| & (Exec ((f :=<0,...,0> da),s1)) . f = m1 |-> 0 ) & ex m2 being Nat st
( m2 = |.(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, A79, A80, A82, SCMFSA_M:2; :: thesis: verum

end;

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

hence (Exec (i,s1)) . g = s1 . g by A79, SCMFSA_2:75
.= s2 . g by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . g by A79, A80, A83, SCMFSA_2:75 ;
:: thesis: verum

end;

end;

end;

now :: thesis: for c being Int-Location holds (Exec (i,s1)) . c = (Exec ((IncAddr (i,n)),s2)) . c

let c be Int-Location; :: thesis: (Exec (i,s1)) . c = (Exec ((IncAddr (i,n)),s2)) . c
thus (Exec (i,s1)) . c = s1 . c by A79, SCMFSA_2:75
.= s2 . c by A2, SCMFSA_M:2
.= (Exec ((IncAddr (i,n)),s2)) . c by A79, A80, SCMFSA_2:75 ; :: thesis: verum

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A81, SCMFSA_M:2; :: thesis: verum

end;

end;