let INS be Instruction of SCM+FSA; :: according to AMISTD_5:def 2 :: thesis:
let j, k be Nat; :: according to AMISTD_5:def 1 :: thesis:
reconsider k = k as Element of NAT by ORDINAL1:def 12;
let s be State of SCM+FSA; :: thesis:
A1: IC (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) = (IC (Exec ((IncAddr (INS,j)),s))) + k by MEMSTR_0:53
.= IC (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) by AMISTD_2:def 3 ;

per cases by NAT_1:36, SCMFSA_2:16;

suppose InsCode INS = 0 ; :: thesis:

then A3: INS = halt SCM+FSA by SCMFSA_2:95;
then A4: IncAddr (INS,j) = halt SCM+FSA by COMPOS_1:11;
Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = Exec (INS,(IncIC (s,k))) by A3, COMPOS_1:11
.= IncIC (s,k) by A3, EXTPRO_1:def 3
.= IncIC ((Exec ((IncAddr (INS,j)),s)),k) by A4, EXTPRO_1:def 3 ;
hence R39( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) ; :: thesis:

end;

suppose InsCode INS = 1 ; :: thesis:

then consider da, db being Int-Location such that
A5: INS = da := db by SCMFSA_2:30;

A6: now

let f be FinSeq-Location ; :: thesis:
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (Exec (INS,(IncIC (s,k)))) . f by A5, COMPOS_1:11
.= (IncIC (s,k)) . f by A5, SCMFSA_2:63
.= s . f by SCMFSA_3:4
.= (Exec (INS,s)) . f by A5, SCMFSA_2:63
.= (Exec ((IncAddr (INS,j)),s)) . f by A5, COMPOS_1:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; :: thesis:

end;

now

let d be Int-Location ; :: thesis:

per cases ;

suppose A7: da = d ; :: thesis:

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A5, COMPOS_1:11
.= (IncIC (s,k)) . db by A5, A7, SCMFSA_2:63
.= s . db by SCMFSA_3:3
.= (Exec (INS,s)) . d by A5, A7, SCMFSA_2:63
.= (Exec ((IncAddr (INS,j)),s)) . d by A5, COMPOS_1:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis:

end;

suppose A8: da <> d ; :: thesis:

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A5, COMPOS_1:11
.= (IncIC (s,k)) . d by A5, A8, SCMFSA_2:63
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A5, A8, SCMFSA_2:63
.= (Exec ((IncAddr (INS,j)),s)) . d by A5, COMPOS_1:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis:

end;

hence R39( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A6, A1, SCMFSA_2:104; :: thesis:

end;

suppose InsCode INS = 2 ; :: thesis:

then consider da, db being Int-Location such that
A9: INS = AddTo (da,db) by SCMFSA_2:31;

A10: now

let f be FinSeq-Location ; :: thesis:
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (Exec (INS,(IncIC (s,k)))) . f by A9, COMPOS_1:11
.= (IncIC (s,k)) . f by A9, SCMFSA_2:64
.= s . f by SCMFSA_3:4
.= (Exec (INS,s)) . f by A9, SCMFSA_2:64
.= (Exec ((IncAddr (INS,j)),s)) . f by A9, COMPOS_1:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; :: thesis:

end;

now

let d be Int-Location ; :: thesis:

per cases ;

suppose A11: da = d ; :: thesis:

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A9, COMPOS_1:11
.= ((IncIC (s,k)) . da) + ((IncIC (s,k)) . db) by A11, A9, SCMFSA_2:64
.= (s . da) + ((IncIC (s,k)) . db) by SCMFSA_3:3
.= (s . da) + (s . db) by SCMFSA_3:3
.= (Exec (INS,s)) . d by A9, A11, SCMFSA_2:64
.= (Exec ((IncAddr (INS,j)),s)) . d by A9, COMPOS_1:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis:

end;

suppose A12: da <> d ; :: thesis:

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A9, COMPOS_1:11
.= (IncIC (s,k)) . d by A9, A12, SCMFSA_2:64
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A9, A12, SCMFSA_2:64
.= (Exec ((IncAddr (INS,j)),s)) . d by A9, COMPOS_1:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis:

end;

hence R39( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A10, A1, SCMFSA_2:104; :: thesis:

end;

suppose InsCode INS = 3 ; :: thesis:

then consider da, db being Int-Location such that
A13: INS = SubFrom (da,db) by SCMFSA_2:32;

A14: now

let f be FinSeq-Location ; :: thesis:
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (Exec (INS,(IncIC (s,k)))) . f by A13, COMPOS_1:11
.= (IncIC (s,k)) . f by A13, SCMFSA_2:65
.= s . f by SCMFSA_3:4
.= (Exec (INS,s)) . f by A13, SCMFSA_2:65
.= (Exec ((IncAddr (INS,j)),s)) . f by A13, COMPOS_1:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; :: thesis:

end;

now

let d be Int-Location ; :: thesis:

per cases ;

suppose A15: da = d ; :: thesis:

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A13, COMPOS_1:11
.= ((IncIC (s,k)) . da) - ((IncIC (s,k)) . db) by A15, A13, SCMFSA_2:65
.= (s . da) - ((IncIC (s,k)) . db) by SCMFSA_3:3
.= (s . da) - (s . db) by SCMFSA_3:3
.= (Exec (INS,s)) . d by A13, A15, SCMFSA_2:65
.= (Exec ((IncAddr (INS,j)),s)) . d by A13, COMPOS_1:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis:

end;

suppose A16: da <> d ; :: thesis:

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A13, COMPOS_1:11
.= (IncIC (s,k)) . d by A13, A16, SCMFSA_2:65
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A13, A16, SCMFSA_2:65
.= (Exec ((IncAddr (INS,j)),s)) . d by A13, COMPOS_1:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis:

end;

hence R39( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A14, A1, SCMFSA_2:104; :: thesis:

end;

suppose InsCode INS = 4 ; :: thesis:

then consider da, db being Int-Location such that
A17: INS = MultBy (da,db) by SCMFSA_2:33;

A18: now

let f be FinSeq-Location ; :: thesis:
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (Exec (INS,(IncIC (s,k)))) . f by A17, COMPOS_1:11
.= (IncIC (s,k)) . f by A17, SCMFSA_2:66
.= s . f by SCMFSA_3:4
.= (Exec (INS,s)) . f by A17, SCMFSA_2:66
.= (Exec ((IncAddr (INS,j)),s)) . f by A17, COMPOS_1:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; :: thesis:

end;

now

let d be Int-Location ; :: thesis:

per cases ;

suppose A19: da = d ; :: thesis:

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A17, COMPOS_1:11
.= ((IncIC (s,k)) . da) * ((IncIC (s,k)) . db) by A19, A17, SCMFSA_2:66
.= (s . da) * ((IncIC (s,k)) . db) by SCMFSA_3:3
.= (s . da) * (s . db) by SCMFSA_3:3
.= (Exec (INS,s)) . d by A17, A19, SCMFSA_2:66
.= (Exec ((IncAddr (INS,j)),s)) . d by A17, COMPOS_1:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis:

end;

suppose A20: da <> d ; :: thesis:

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A17, COMPOS_1:11
.= (IncIC (s,k)) . d by A17, A20, SCMFSA_2:66
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A17, A20, SCMFSA_2:66
.= (Exec ((IncAddr (INS,j)),s)) . d by A17, COMPOS_1:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis:

end;

hence R39( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A18, A1, SCMFSA_2:104; :: thesis:

end;

suppose InsCode INS = 5 ; :: thesis:

then consider da, db being Int-Location such that
A21: INS = Divide (da,db) by SCMFSA_2:34;

A22: now

let f be FinSeq-Location ; :: thesis:
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (Exec (INS,(IncIC (s,k)))) . f by A21, COMPOS_1:11
.= (IncIC (s,k)) . f by A21, SCMFSA_2:67
.= s . f by SCMFSA_3:4
.= (Exec (INS,s)) . f by A21, SCMFSA_2:67
.= (Exec ((IncAddr (INS,j)),s)) . f by A21, COMPOS_1:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; :: thesis:

end;

now

let d be Int-Location ; :: thesis:

per cases ;

suppose A23: da <> db ; :: thesis:

hereby :: thesis:

per cases ;

suppose A24: da = d ; :: thesis:

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A21, COMPOS_1:11
.= ((IncIC (s,k)) . da) div ((IncIC (s,k)) . db) by A23, A24, A21, SCMFSA_2:67
.= (s . da) div ((IncIC (s,k)) . db) by SCMFSA_3:3
.= (s . da) div (s . db) by SCMFSA_3:3
.= (Exec (INS,s)) . d by A21, A23, A24, SCMFSA_2:67
.= (Exec ((IncAddr (INS,j)),s)) . d by A21, COMPOS_1:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis:

end;

suppose A25: db = d ; :: thesis:

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A21, COMPOS_1:11
.= ((IncIC (s,k)) . da) mod ((IncIC (s,k)) . db) by A25, A21, SCMFSA_2:67
.= (s . da) mod ((IncIC (s,k)) . db) by SCMFSA_3:3
.= (s . da) mod (s . db) by SCMFSA_3:3
.= (Exec (INS,s)) . d by A21, A25, SCMFSA_2:67
.= (Exec ((IncAddr (INS,j)),s)) . d by A21, COMPOS_1:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis:

end;

suppose A26: ( da <> d & db <> d ) ; :: thesis:

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A21, COMPOS_1:11
.= (IncIC (s,k)) . d by A21, A26, SCMFSA_2:67
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A21, A26, SCMFSA_2:67
.= (Exec ((IncAddr (INS,j)),s)) . d by A21, COMPOS_1:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis:

end;

suppose A27: da = db ; :: thesis:

per cases ;

suppose A28: da = d ; :: thesis:

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A21, COMPOS_1:11
.= ((IncIC (s,k)) . da) mod ((IncIC (s,k)) . db) by A27, A28, A21, SCMFSA_2:67
.= (s . da) mod ((IncIC (s,k)) . db) by SCMFSA_3:3
.= (s . da) mod (s . db) by SCMFSA_3:3
.= (Exec (INS,s)) . d by A21, A27, A28, SCMFSA_2:67
.= (Exec ((IncAddr (INS,j)),s)) . d by A21, COMPOS_1:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis:

end;

suppose A29: da <> d ; :: thesis:

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A21, COMPOS_1:11
.= (IncIC (s,k)) . d by A21, A27, A29, SCMFSA_2:67
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A21, A27, A29, SCMFSA_2:67
.= (Exec ((IncAddr (INS,j)),s)) . d by A21, COMPOS_1:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis:

end;

hence R39( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A22, A1, SCMFSA_2:104; :: thesis:

end;

suppose InsCode INS = 6 ; :: thesis:

then consider loc being Element of NAT such that
A30: INS = goto loc by SCMFSA_2:35;
A31: IncAddr (INS,(j + k)) = goto (loc + (j + k)) by A30, Th14;
reconsider jj = j as Element of NAT by ORDINAL1:def 12;
A32: IncAddr (INS,jj) = goto (loc + jj) by A30, Th14;

A33: now

let f be FinSeq-Location ; :: thesis:
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC (s,k)) . f by A31, SCMFSA_2:69
.= s . f by SCMFSA_3:4
.= (Exec ((IncAddr (INS,j)),s)) . f by A32, SCMFSA_2:69
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; :: thesis:

end;

now

let d be Int-Location ; :: thesis:
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC (s,k)) . d by A31, SCMFSA_2:69
.= s . d by SCMFSA_3:3
.= (Exec ((IncAddr (INS,j)),s)) . d by A32, SCMFSA_2:69
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis:

end;

hence R39( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A33, A1, SCMFSA_2:104; :: thesis:

end;

suppose InsCode INS = 7 ; :: thesis:

then consider loc being Element of NAT , da being Int-Location such that
A34: INS = da =0_goto loc by SCMFSA_2:36;
A35: IncAddr (INS,(j + k)) = da =0_goto (loc + (j + k)) by A34, Th15;
reconsider jj = j as Element of NAT by ORDINAL1:def 12;
A36: IncAddr (INS,jj) = da =0_goto (loc + jj) by A34, Th15;

A37: now

let f be FinSeq-Location ; :: thesis:
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC (s,k)) . f by A35, SCMFSA_2:70
.= s . f by SCMFSA_3:4
.= (Exec ((IncAddr (INS,j)),s)) . f by A36, SCMFSA_2:70
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; :: thesis:

end;

now

let d be Int-Location ; :: thesis:
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC (s,k)) . d by A35, SCMFSA_2:70
.= s . d by SCMFSA_3:3
.= (Exec ((IncAddr (INS,j)),s)) . d by A36, SCMFSA_2:70
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis:

end;

hence R39( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A1, A37, SCMFSA_2:104; :: thesis:

end;

suppose InsCode INS = 8 ; :: thesis:

then consider loc being Element of NAT , da being Int-Location such that
A38: INS = da >0_goto loc by SCMFSA_2:37;
A39: IncAddr (INS,(j + k)) = da >0_goto (loc + (j + k)) by A38, Th16;
reconsider jj = j as Element of NAT by ORDINAL1:def 12;
A40: IncAddr (INS,jj) = da >0_goto (loc + jj) by A38, Th16;

A41: now

let f be FinSeq-Location ; :: thesis:
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC (s,k)) . f by A39, SCMFSA_2:71
.= s . f by SCMFSA_3:4
.= (Exec ((IncAddr (INS,j)),s)) . f by A40, SCMFSA_2:71
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; :: thesis:

end;

now

let d be Int-Location ; :: thesis:
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC (s,k)) . d by A39, SCMFSA_2:71
.= s . d by SCMFSA_3:3
.= (Exec ((IncAddr (INS,j)),s)) . d by A40, SCMFSA_2:71
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis:

end;

hence R39( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A41, A1, SCMFSA_2:104; :: thesis:

end;

suppose InsCode INS = 9 ; :: thesis:

then consider db, da being Int-Location , f being FinSeq-Location such that
A42: INS = da := (f,db) by SCMFSA_2:38;

A43: now

let f be FinSeq-Location ; :: thesis:
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (Exec (INS,(IncIC (s,k)))) . f by A42, COMPOS_1:11
.= (IncIC (s,k)) . f by A42, SCMFSA_2:72
.= s . f by SCMFSA_3:4
.= (Exec (INS,s)) . f by A42, SCMFSA_2:72
.= (Exec ((IncAddr (INS,j)),s)) . f by A42, COMPOS_1:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; :: thesis:

end;

now

let d be Int-Location ; :: thesis:

per cases ;

suppose A44: da = d ; :: thesis:

consider m being Element of NAT such that
A45: m = abs (s . db) and
A46: (Exec (INS,s)) . da = (s . f) /. m by A42, SCMFSA_2:72;
A47: ex m1 being Element of NAT st
( m1 = abs ((IncIC (s,k)) . db) & (Exec (INS,(IncIC (s,k)))) . da = ((IncIC (s,k)) . f) /. m1 ) by A42, SCMFSA_2:72;
A48: (IncIC (s,k)) . db = s . db by SCMFSA_3:3;
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A42, COMPOS_1:11
.= (s . f) /. m by A45, A47, A44, A48, SCMFSA_3:4
.= (IncIC ((Exec (INS,s)),k)) . d by A46, A44, SCMFSA_3:3
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by A42, COMPOS_1:11 ; :: thesis:

end;

suppose A49: da <> d ; :: thesis:

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A42, COMPOS_1:11
.= (IncIC (s,k)) . d by A42, A49, SCMFSA_2:72
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A42, A49, SCMFSA_2:72
.= (Exec ((IncAddr (INS,j)),s)) . d by A42, COMPOS_1:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis:

end;

hence R39( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A43, A1, SCMFSA_2:104; :: thesis:

end;

suppose InsCode INS = 10 ; :: thesis:

then consider db, da being Int-Location , f being FinSeq-Location such that
A50: INS = (f,db) := da by SCMFSA_2:39;

A51: now

let g be FinSeq-Location ; :: thesis:
consider m being Element of NAT such that
A52: m = abs (s . db) and
A53: (Exec (INS,s)) . f = (s . f) +* (m,(s . da)) by A50, SCMFSA_2:73;
A54: ex m1 being Element of NAT st
( m1 = abs ((IncIC (s,k)) . db) & (Exec (INS,(IncIC (s,k)))) . f = ((IncIC (s,k)) . f) +* (m1,((IncIC (s,k)) . da)) ) by A50, SCMFSA_2:73;

per cases ;

suppose A55: f = g ; :: thesis:

A56: ( (IncIC (s,k)) . f = s . f & (IncIC (s,k)) . db = s . db ) by SCMFSA_3:3, SCMFSA_3:4;
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . g = (Exec (INS,(IncIC (s,k)))) . g by A50, COMPOS_1:11
.= (s . f) +* (m,(s . da)) by A52, A54, A55, A56, SCMFSA_3:3
.= (IncIC ((Exec (INS,s)),k)) . g by A53, A55, SCMFSA_3:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . g by A50, COMPOS_1:11 ; :: thesis:

end;

suppose A57: f <> g ; :: thesis:

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . g = (Exec (INS,(IncIC (s,k)))) . g by A50, COMPOS_1:11
.= (IncIC (s,k)) . g by A50, A57, SCMFSA_2:73
.= s . g by SCMFSA_3:4
.= (Exec (INS,s)) . g by A50, A57, SCMFSA_2:73
.= (Exec ((IncAddr (INS,j)),s)) . g by A50, COMPOS_1:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . g by SCMFSA_3:4 ; :: thesis:

end;

now

let d be Int-Location ; :: thesis:
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A50, COMPOS_1:11
.= (IncIC (s,k)) . d by A50, SCMFSA_2:73
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A50, SCMFSA_2:73
.= (Exec ((IncAddr (INS,j)),s)) . d by A50, COMPOS_1:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis:

end;

hence R39( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A51, A1, SCMFSA_2:104; :: thesis:

end;

suppose InsCode INS = 11 ; :: thesis:

then consider da being Int-Location , f being FinSeq-Location such that
A58: INS = da :=len f by SCMFSA_2:40;

A59: now

let f be FinSeq-Location ; :: thesis:
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (Exec (INS,(IncIC (s,k)))) . f by A58, COMPOS_1:11
.= (IncIC (s,k)) . f by A58, SCMFSA_2:74
.= s . f by SCMFSA_3:4
.= (Exec (INS,s)) . f by A58, SCMFSA_2:74
.= (Exec ((IncAddr (INS,j)),s)) . f by A58, COMPOS_1:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; :: thesis:

end;

now

let d be Int-Location ; :: thesis:

per cases ;

suppose A60: da = d ; :: thesis:

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A58, COMPOS_1:11
.= len ((IncIC (s,k)) . f) by A60, A58, SCMFSA_2:74
.= len (s . f) by SCMFSA_3:4
.= (Exec (INS,s)) . d by A58, A60, SCMFSA_2:74
.= (IncIC ((Exec (INS,s)),k)) . d by SCMFSA_3:3
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by A58, COMPOS_1:11 ; :: thesis:

end;

suppose A61: da <> d ; :: thesis:

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A58, COMPOS_1:11
.= (IncIC (s,k)) . d by A58, A61, SCMFSA_2:74
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A58, A61, SCMFSA_2:74
.= (Exec ((IncAddr (INS,j)),s)) . d by A58, COMPOS_1:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis:

end;

hence R39( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A59, A1, SCMFSA_2:104; :: thesis:

end;

suppose InsCode INS = 12 ; :: thesis:

then consider da being Int-Location , f being FinSeq-Location such that
A62: INS = f :=<0,...,0> da by SCMFSA_2:41;

A63: now

let g be FinSeq-Location ; :: thesis:
A64: ( ex m being Element of NAT st
( m = abs (s . da) & (Exec (INS,s)) . f = m |-> 0 ) & ex m being Element of NAT st
( m = abs ((IncIC (s,k)) . da) & (Exec (INS,(IncIC (s,k)))) . f = m |-> 0 ) ) by A62, SCMFSA_2:75;

per cases ;

suppose A65: f = g ; :: thesis:

A66: (IncIC (s,k)) . da = s . da by SCMFSA_3:3;
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . g = (Exec (INS,(IncIC (s,k)))) . g by A62, COMPOS_1:11
.= (IncIC ((Exec (INS,s)),k)) . g by A64, A65, A66, SCMFSA_3:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . g by A62, COMPOS_1:11 ; :: thesis:

end;

suppose A67: f <> g ; :: thesis:

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . g = (Exec (INS,(IncIC (s,k)))) . g by A62, COMPOS_1:11
.= (IncIC (s,k)) . g by A62, A67, SCMFSA_2:75
.= s . g by SCMFSA_3:4
.= (Exec (INS,s)) . g by A62, A67, SCMFSA_2:75
.= (Exec ((IncAddr (INS,j)),s)) . g by A62, COMPOS_1:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . g by SCMFSA_3:4 ; :: thesis:

end;

now

let d be Int-Location ; :: thesis:
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A62, COMPOS_1:11
.= (IncIC (s,k)) . d by A62, SCMFSA_2:75
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A62, SCMFSA_2:75
.= (Exec ((IncAddr (INS,j)),s)) . d by A62, COMPOS_1:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis:

end;

hence R39( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A63, A1, SCMFSA_2:104; :: thesis:

end;