set D = Int-Locations \/ FinSeq-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:39
.= (k1 + n) + 1
.= succ (IC s2) by A1, NAT_1:39 ;

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 in {6,7,8}

proof

assume InsCode i in {6,7,8} ; :: thesis: contradiction
then ( InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) by ENUMSET1:def 1;
hence contradiction by A5; :: thesis: verum

end;

then A8: IncAddr (i,n) = i by SCMFSA_4:30;
A9: not InsCode i in {0,6,7,8}

proof

assume A10: InsCode i in {0,6,7,8} ; :: thesis: contradiction

per cases ( InsCode i = 0 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) by A10, ENUMSET1:def 2;

suppose InsCode i = 0 ; :: thesis: contradiction

hence contradiction by A6; :: thesis: verum

end;

suppose InsCode i = 6 ; :: thesis: contradiction

hence contradiction by A5; :: thesis: verum

end;

suppose InsCode i = 7 ; :: thesis: contradiction

hence contradiction by A5; :: thesis: verum

end;

suppose InsCode i = 8 ; :: thesis: contradiction

hence contradiction by A5; :: thesis: verum

end;

end;

end;

then IC (Exec (i,s1)) = succ (IC s1) by Th23;
hence (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A3, A9, A8, Th23; :: thesis: verum

end;

A11: ( not InsCode i <= 9 + 1 or InsCode i <= 8 + 1 or InsCode i = 10 ) by NAT_1:8;
A12: ( not InsCode i <= 10 + 1 or InsCode i <= 10 or InsCode i = 11 ) by NAT_1:8;
A13: InsCode i <= 11 + 1 by SCMFSA_2:35;

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 A13, A12, A11, 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 A14: i = halt SCM+FSA by SCMFSA_2:122;
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, A14, SCMFSA_4:8; :: thesis: verum

end;

suppose A15: 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
A16: i = da := db by A15, SCMFSA_2:54;
A17: IncAddr (i,n) = i by A16, SCMFSA_4:9;

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

hence (Exec (i,s1)) . c = s1 . db by A16, SCMFSA_2:89
.= s2 . db by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . c by A16, A17, A19, SCMFSA_2:89 ;
:: thesis: verum

end;

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

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

end;

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

end;

suppose A21: 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
A22: i = AddTo (da,db) by A21, SCMFSA_2:55;
A23: IncAddr (i,n) = i by A22, SCMFSA_4:10;

A24: 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 A25: 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 A22, A25, SCMFSA_2:90
.= (Exec ((IncAddr (i,n)),s2)) . c by A22, A23, A25, SCMFSA_2:90 ;
:: thesis: verum

end;

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

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

end;

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

end;

suppose A27: 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
A28: i = SubFrom (da,db) by A27, SCMFSA_2:56;
A29: IncAddr (i,n) = i by A28, SCMFSA_4:11;

A30: 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 A31: 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 A28, A31, SCMFSA_2:91
.= (Exec ((IncAddr (i,n)),s2)) . c by A28, A29, A31, SCMFSA_2:91 ;
:: thesis: verum

end;

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

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

end;

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

end;

suppose A33: 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
A34: i = MultBy (da,db) by A33, SCMFSA_2:57;
A35: IncAddr (i,n) = i by A34, SCMFSA_4:12;

A36: 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 A37: 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 A34, A37, SCMFSA_2:92
.= (Exec ((IncAddr (i,n)),s2)) . c by A34, A35, A37, SCMFSA_2:92 ;
:: thesis: verum

end;

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

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

end;

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

end;

suppose A39: 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
A40: i = Divide (da,db) by A39, SCMFSA_2:58;
A41: IncAddr (i,n) = i by A40, SCMFSA_4:13;

A42: 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 A43: 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 A40, A43, SCMFSA_2:93
.= (Exec ((IncAddr (i,n)),s2)) . c by A40, A41, A43, SCMFSA_2:93 ;
:: thesis: verum

end;

suppose A44: ( 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 A40, A44, SCMFSA_2:93
.= (Exec ((IncAddr (i,n)),s2)) . c by A40, A41, A44, SCMFSA_2:93 ;
:: thesis: verum

end;

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

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

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A42, 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
A46: i = goto loc by SCMFSA_2:59;
A47: IncAddr (i,n) = goto (loc + n) by A46, SCMFSA_4:14;

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

end;

IC (Exec (i,s1)) = loc by A46, SCMFSA_2:95;
hence (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A47, SCMFSA_2:95; :: 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 A46, SCMFSA_2:95
.= s2 . c by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . c by A47, SCMFSA_2:95 ; :: thesis: verum

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A48, 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
A49: i = da =0_goto loc by SCMFSA_2:60;
A50: IncAddr (i,n) = da =0_goto (loc + n) by A49, SCMFSA_4:15;

A51: 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 A49, SCMFSA_2:96
.= s2 . f by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . f by A50, 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 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, A49, Th38, SCMFSA_2:96;
hence (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A50, SCMFSA_2:96; :: 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, A49, Th38, SCMFSA_2:96;
hence (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A3, A50, SCMFSA_2:96; :: 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 A49, SCMFSA_2:96
.= s2 . c by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . c by A50, SCMFSA_2:96 ; :: thesis: verum

end;

hence DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) by A51, 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
A52: i = da >0_goto loc by SCMFSA_2:61;
A53: IncAddr (i,n) = da >0_goto (loc + n) by A52, SCMFSA_4:16;

A54: 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 A52, SCMFSA_2:97
.= s2 . f by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . f by A53, 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 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, A52, Th38, SCMFSA_2:97;
hence (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A53, SCMFSA_2:97; :: 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, A52, Th38, SCMFSA_2:97;
hence (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) by A3, A53, SCMFSA_2:97; :: 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 A52, SCMFSA_2:97
.= s2 . c by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . c by A53, SCMFSA_2:97 ; :: thesis: verum

end;

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

end;

suppose A55: 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
A56: i = da := (f,db) by A55, SCMFSA_2:62;
A57: IncAddr (i,n) = i by A56, SCMFSA_4:17;

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

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

end;

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

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

end;

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

end;

suppose A66: 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
A67: i = (f,db) := da by A66, SCMFSA_2:63;
A68: IncAddr (i,n) = i by A67, SCMFSA_4:18;

A69: 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 A70: g = f ; :: thesis: (Exec (i,s1)) . b₁ = (Exec ((IncAddr (i,n)),s2)) . b₁

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

end;

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

hence (Exec (i,s1)) . g = s1 . g by A67, SCMFSA_2:99
.= s2 . g by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . g by A67, A68, A76, SCMFSA_2:99 ;
:: 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 A67, SCMFSA_2:99
.= s2 . c by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . c by A67, A68, SCMFSA_2:99 ; :: thesis: verum

end;

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

end;

suppose A77: 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
A78: i = da :=len f by A77, SCMFSA_2:64;
A79: IncAddr (i,n) = i by A78, SCMFSA_4:19;

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

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

end;

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

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

end;

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

end;

suppose A83: 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
A84: i = f :=<0,...,0> da by A83, SCMFSA_2:65;
A85: IncAddr (i,n) = i by A84, SCMFSA_4:20;

A86: 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 A87: 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:101;
hence (Exec (i,s1)) . g = (Exec ((IncAddr (i,n)),s2)) . g by A2, A84, A85, A87, Th38; :: thesis: verum

end;

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

hence (Exec (i,s1)) . g = s1 . g by A84, SCMFSA_2:101
.= s2 . g by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . g by A84, A85, A88, SCMFSA_2:101 ;
:: 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 A84, SCMFSA_2:101
.= s2 . c by A2, Th38
.= (Exec ((IncAddr (i,n)),s2)) . c by A84, A85, SCMFSA_2:101 ; :: thesis: verum

end;

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

end;

end;