let i be Instruction of SCM+FSA; :: thesis: for a being Int-Location

for s being State of SCM+FSA st not i destroys a holds

(Exec (i,s)) . a = s . a

let a be Int-Location; :: thesis: for s being State of SCM+FSA st not i destroys a holds

(Exec (i,s)) . a = s . a

let s be State of SCM+FSA; :: thesis: ( not i destroys a implies (Exec (i,s)) . a = s . a )

assume A1: not i destroys a ; :: thesis: (Exec (i,s)) . a = s . a

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

for s being State of SCM+FSA st not i destroys a holds

(Exec (i,s)) . a = s . a

let a be Int-Location; :: thesis: for s being State of SCM+FSA st not i destroys a holds

(Exec (i,s)) . a = s . a

let s be State of SCM+FSA; :: thesis: ( not i destroys a implies (Exec (i,s)) . a = s . a )

assume A1: not i destroys a ; :: thesis: (Exec (i,s)) . a = s . a

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 )
;

end;

suppose
InsCode i = 0
; :: thesis: (Exec (i,s)) . a = s . a

then
i = halt SCM+FSA
by SCMFSA_2:95;

hence (Exec (i,s)) . a = s . a by EXTPRO_1:def 3; :: thesis: verum

end;hence (Exec (i,s)) . a = s . a by EXTPRO_1:def 3; :: thesis: verum

suppose
InsCode i = 1
; :: thesis: (Exec (i,s)) . a = s . a

then consider da, db being Int-Location such that

A2: i = da := db by SCMFSA_2:30;

da <> a by A1, A2;

hence (Exec (i,s)) . a = s . a by A2, SCMFSA_2:63; :: thesis: verum

end;A2: i = da := db by SCMFSA_2:30;

da <> a by A1, A2;

hence (Exec (i,s)) . a = s . a by A2, SCMFSA_2:63; :: thesis: verum

suppose
InsCode i = 2
; :: thesis: (Exec (i,s)) . a = s . a

then consider da, db being Int-Location such that

A3: i = AddTo (da,db) by SCMFSA_2:31;

da <> a by A1, A3;

hence (Exec (i,s)) . a = s . a by A3, SCMFSA_2:64; :: thesis: verum

end;A3: i = AddTo (da,db) by SCMFSA_2:31;

da <> a by A1, A3;

hence (Exec (i,s)) . a = s . a by A3, SCMFSA_2:64; :: thesis: verum

suppose
InsCode i = 3
; :: thesis: (Exec (i,s)) . a = s . a

then consider da, db being Int-Location such that

A4: i = SubFrom (da,db) by SCMFSA_2:32;

da <> a by A1, A4;

hence (Exec (i,s)) . a = s . a by A4, SCMFSA_2:65; :: thesis: verum

end;A4: i = SubFrom (da,db) by SCMFSA_2:32;

da <> a by A1, A4;

hence (Exec (i,s)) . a = s . a by A4, SCMFSA_2:65; :: thesis: verum

suppose
InsCode i = 4
; :: thesis: (Exec (i,s)) . a = s . a

then consider da, db being Int-Location such that

A5: i = MultBy (da,db) by SCMFSA_2:33;

da <> a by A1, A5;

hence (Exec (i,s)) . a = s . a by A5, SCMFSA_2:66; :: thesis: verum

end;A5: i = MultBy (da,db) by SCMFSA_2:33;

da <> a by A1, A5;

hence (Exec (i,s)) . a = s . a by A5, SCMFSA_2:66; :: thesis: verum

suppose
InsCode i = 5
; :: thesis: (Exec (i,s)) . a = s . a

then consider da, db being Int-Location such that

A6: i = Divide (da,db) by SCMFSA_2:34;

( da <> a & db <> a ) by A1, A6;

hence (Exec (i,s)) . a = s . a by A6, SCMFSA_2:67; :: thesis: verum

end;A6: i = Divide (da,db) by SCMFSA_2:34;

( da <> a & db <> a ) by A1, A6;

hence (Exec (i,s)) . a = s . a by A6, SCMFSA_2:67; :: thesis: verum

suppose
InsCode i = 6
; :: thesis: (Exec (i,s)) . a = s . a

then
ex loc being Nat st i = goto loc
by SCMFSA_2:35;

hence (Exec (i,s)) . a = s . a by SCMFSA_2:69; :: thesis: verum

end;hence (Exec (i,s)) . a = s . a by SCMFSA_2:69; :: thesis: verum

suppose
InsCode i = 7
; :: thesis: (Exec (i,s)) . a = s . a

then
ex loc being Nat ex da being Int-Location st i = da =0_goto loc
by SCMFSA_2:36;

hence (Exec (i,s)) . a = s . a by SCMFSA_2:70; :: thesis: verum

end;hence (Exec (i,s)) . a = s . a by SCMFSA_2:70; :: thesis: verum

suppose
InsCode i = 8
; :: thesis: (Exec (i,s)) . a = s . a

then
ex loc being Nat ex da being Int-Location st i = da >0_goto loc
by SCMFSA_2:37;

hence (Exec (i,s)) . a = s . a by SCMFSA_2:71; :: thesis: verum

end;hence (Exec (i,s)) . a = s . a by SCMFSA_2:71; :: thesis: verum

suppose
InsCode i = 9
; :: thesis: (Exec (i,s)) . a = s . a

then consider db, da being Int-Location, g being FinSeq-Location such that

A7: i = da := (g,db) by SCMFSA_2:38;

da <> a by A1, A7;

hence (Exec (i,s)) . a = s . a by A7, SCMFSA_2:72; :: thesis: verum

end;A7: i = da := (g,db) by SCMFSA_2:38;

da <> a by A1, A7;

hence (Exec (i,s)) . a = s . a by A7, SCMFSA_2:72; :: thesis: verum

suppose
InsCode i = 10
; :: thesis: (Exec (i,s)) . a = s . a

then
ex db, da being Int-Location ex g being FinSeq-Location st i = (g,db) := da
by SCMFSA_2:39;

hence (Exec (i,s)) . a = s . a by SCMFSA_2:73; :: thesis: verum

end;hence (Exec (i,s)) . a = s . a by SCMFSA_2:73; :: thesis: verum

suppose
InsCode i = 11
; :: thesis: (Exec (i,s)) . a = s . a

then consider da being Int-Location, g being FinSeq-Location such that

A8: i = da :=len g by SCMFSA_2:40;

da <> a by A1, A8;

hence (Exec (i,s)) . a = s . a by A8, SCMFSA_2:74; :: thesis: verum

end;A8: i = da :=len g by SCMFSA_2:40;

da <> a by A1, A8;

hence (Exec (i,s)) . a = s . a by A8, SCMFSA_2:74; :: thesis: verum

suppose
InsCode i = 12
; :: thesis: (Exec (i,s)) . a = s . a

then
ex da being Int-Location ex g being FinSeq-Location st i = g :=<0,...,0> da
by SCMFSA_2:41;

hence (Exec (i,s)) . a = s . a by SCMFSA_2:75; :: thesis: verum

end;hence (Exec (i,s)) . a = s . a by SCMFSA_2:75; :: thesis: verum