let I be Instruction of SCM+FSA ; :: according to AMISTD_2:def 21 :: thesis: I is Exec-preserving
let s1, s2 be State of SCM+FSA ; :: according to AMISTD_2:def 20 :: thesis: ( not s1,s2 equal_outside K37() or Exec I,s1, Exec I,s2 equal_outside K37() )
assume A1: s1,s2 equal_outside NAT ; :: thesis: Exec I,s1, Exec I,s2 equal_outside K37()
A2: ( not InsCode I <= 9 + 1 or InsCode I <= 8 + 1 or InsCode I = 10 ) by NAT_1:8;
A3: ( not InsCode I <= 10 + 1 or InsCode I <= 10 or InsCode I = 11 ) by NAT_1:8;
A4: 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 A4, A3, A2, NAT_1:8, NAT_1:33;

suppose InsCode I = 0 ; :: thesis: Exec I,s1, Exec I,s2 equal_outside K37()

then A5: I = halt SCM+FSA by SCMFSA_2:122;
then Exec I,s1 = s1 by AMI_1:def 8;
hence Exec I,s1, Exec I,s2 equal_outside K37() by A1, A5, AMI_1:def 8; :: thesis: verum

end;

suppose InsCode I = 1 ; :: thesis: Exec I,s1, Exec I,s2 equal_outside K37()

then consider da, db being Int-Location such that
A6: I = da := db by SCMFSA_2:54;

A7: now

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

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

suppose A8: c = da ; :: thesis: (Exec I,s1) . b₁ = (Exec I,s2) . b₁

hence (Exec I,s1) . c = s1 . db by A6, SCMFSA_2:89
.= s2 . db by A1, Th30
.= (Exec I,s2) . c by A6, A8, SCMFSA_2:89 ;
:: thesis: verum

end;

suppose A9: c <> da ; :: thesis: (Exec I,s1) . b₁ = (Exec I,s2) . b₁

hence (Exec I,s1) . c = s1 . c by A6, SCMFSA_2:89
.= s2 . c by A1, Th30
.= (Exec I,s2) . c by A6, A9, SCMFSA_2:89 ;
:: thesis: verum

end;

end;

end;

A10: now

let f be FinSeq-Location ; :: thesis: (Exec I,s1) . f = (Exec I,s2) . f
thus (Exec I,s1) . f = s1 . f by A6, SCMFSA_2:89
.= s2 . f by A1, Th31
.= (Exec I,s2) . f by A6, SCMFSA_2:89 ; :: thesis: verum

end;

IC (Exec I,s1) = succ (IC s1) by A6, SCMFSA_2:89
.= succ (IC s2) by A1, COMPOS_1:24
.= IC (Exec I,s2) by A6, SCMFSA_2:89 ;
hence Exec I,s1, Exec I,s2 equal_outside K37() by A7, A10, Th28; :: thesis: verum

end;

suppose InsCode I = 2 ; :: thesis: Exec I,s1, Exec I,s2 equal_outside K37()

then consider da, db being Int-Location such that
A11: I = AddTo da,db by SCMFSA_2:55;

A12: now

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

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

suppose A13: c = da ; :: thesis: (Exec I,s1) . b₁ = (Exec I,s2) . b₁

( s1 . da = s2 . da & s1 . db = s2 . db ) by A1, Th30;
hence (Exec I,s1) . c = (s2 . da) + (s2 . db) by A11, A13, SCMFSA_2:90
.= (Exec I,s2) . c by A11, A13, SCMFSA_2:90 ;
:: thesis: verum

end;

suppose A14: c <> da ; :: thesis: (Exec I,s1) . b₁ = (Exec I,s2) . b₁

hence (Exec I,s1) . c = s1 . c by A11, SCMFSA_2:90
.= s2 . c by A1, Th30
.= (Exec I,s2) . c by A11, A14, SCMFSA_2:90 ;
:: thesis: verum

end;

end;

end;

A15: now

let f be FinSeq-Location ; :: thesis: (Exec I,s1) . f = (Exec I,s2) . f
thus (Exec I,s1) . f = s1 . f by A11, SCMFSA_2:90
.= s2 . f by A1, Th31
.= (Exec I,s2) . f by A11, SCMFSA_2:90 ; :: thesis: verum

end;

IC (Exec I,s1) = succ (IC s1) by A11, SCMFSA_2:90
.= succ (IC s2) by A1, COMPOS_1:24
.= IC (Exec I,s2) by A11, SCMFSA_2:90 ;
hence Exec I,s1, Exec I,s2 equal_outside K37() by A12, A15, Th28; :: thesis: verum

end;

suppose InsCode I = 3 ; :: thesis: Exec I,s1, Exec I,s2 equal_outside K37()

then consider da, db being Int-Location such that
A16: I = SubFrom da,db by SCMFSA_2:56;

A17: now

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

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

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

( s1 . da = s2 . da & s1 . db = s2 . db ) by A1, Th30;
hence (Exec I,s1) . c = (s2 . da) - (s2 . db) by A16, A18, SCMFSA_2:91
.= (Exec I,s2) . c by A16, A18, SCMFSA_2:91 ;
:: thesis: verum

end;

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

hence (Exec I,s1) . c = s1 . c by A16, SCMFSA_2:91
.= s2 . c by A1, Th30
.= (Exec I,s2) . c by A16, A19, SCMFSA_2:91 ;
:: thesis: verum

end;

end;

end;

A20: now

let f be FinSeq-Location ; :: thesis: (Exec I,s1) . f = (Exec I,s2) . f
thus (Exec I,s1) . f = s1 . f by A16, SCMFSA_2:91
.= s2 . f by A1, Th31
.= (Exec I,s2) . f by A16, SCMFSA_2:91 ; :: thesis: verum

end;

IC (Exec I,s1) = succ (IC s1) by A16, SCMFSA_2:91
.= succ (IC s2) by A1, COMPOS_1:24
.= IC (Exec I,s2) by A16, SCMFSA_2:91 ;
hence Exec I,s1, Exec I,s2 equal_outside K37() by A17, A20, Th28; :: thesis: verum

end;

suppose InsCode I = 4 ; :: thesis: Exec I,s1, Exec I,s2 equal_outside K37()

then consider da, db being Int-Location such that
A21: I = MultBy da,db by SCMFSA_2:57;

A22: now

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

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

suppose A23: c = da ; :: thesis: (Exec I,s1) . b₁ = (Exec I,s2) . b₁

( s1 . da = s2 . da & s1 . db = s2 . db ) by A1, Th30;
hence (Exec I,s1) . c = (s2 . da) * (s2 . db) by A21, A23, SCMFSA_2:92
.= (Exec I,s2) . c by A21, A23, SCMFSA_2:92 ;
:: thesis: verum

end;

suppose A24: c <> da ; :: thesis: (Exec I,s1) . b₁ = (Exec I,s2) . b₁

hence (Exec I,s1) . c = s1 . c by A21, SCMFSA_2:92
.= s2 . c by A1, Th30
.= (Exec I,s2) . c by A21, A24, SCMFSA_2:92 ;
:: thesis: verum

end;

end;

end;

A25: now

let f be FinSeq-Location ; :: thesis: (Exec I,s1) . f = (Exec I,s2) . f
thus (Exec I,s1) . f = s1 . f by A21, SCMFSA_2:92
.= s2 . f by A1, Th31
.= (Exec I,s2) . f by A21, SCMFSA_2:92 ; :: thesis: verum

end;

IC (Exec I,s1) = succ (IC s1) by A21, SCMFSA_2:92
.= succ (IC s2) by A1, COMPOS_1:24
.= IC (Exec I,s2) by A21, SCMFSA_2:92 ;
hence Exec I,s1, Exec I,s2 equal_outside K37() by A22, A25, Th28; :: thesis: verum

end;

suppose InsCode I = 5 ; :: thesis: Exec I,s1, Exec I,s2 equal_outside K37()

then consider da, db being Int-Location such that
A26: I = Divide da,db by SCMFSA_2:58;

A27: now

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

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

suppose A28: c = db ; :: thesis: (Exec I,s1) . b₁ = (Exec I,s2) . b₁

( s1 . da = s2 . da & s1 . db = s2 . db ) by A1, Th30;
hence (Exec I,s1) . c = (s2 . da) mod (s2 . db) by A26, A28, SCMFSA_2:93
.= (Exec I,s2) . c by A26, A28, SCMFSA_2:93 ;
:: thesis: verum

end;

suppose A29: ( c = da & c <> db ) ; :: thesis: (Exec I,s1) . b₁ = (Exec I,s2) . b₁

( s1 . da = s2 . da & s1 . db = s2 . db ) by A1, Th30;
hence (Exec I,s1) . c = (s2 . da) div (s2 . db) by A26, A29, SCMFSA_2:93
.= (Exec I,s2) . c by A26, A29, SCMFSA_2:93 ;
:: thesis: verum

end;

suppose A30: ( c <> da & c <> db ) ; :: thesis: (Exec I,s1) . b₁ = (Exec I,s2) . b₁

hence (Exec I,s1) . c = s1 . c by A26, SCMFSA_2:93
.= s2 . c by A1, Th30
.= (Exec I,s2) . c by A26, A30, SCMFSA_2:93 ;
:: thesis: verum

end;

end;

end;

A31: now

let f be FinSeq-Location ; :: thesis: (Exec I,s1) . f = (Exec I,s2) . f
thus (Exec I,s1) . f = s1 . f by A26, SCMFSA_2:93
.= s2 . f by A1, Th31
.= (Exec I,s2) . f by A26, SCMFSA_2:93 ; :: thesis: verum

end;

IC (Exec I,s1) = succ (IC s1) by A26, SCMFSA_2:93
.= succ (IC s2) by A1, COMPOS_1:24
.= IC (Exec I,s2) by A26, SCMFSA_2:93 ;
hence Exec I,s1, Exec I,s2 equal_outside K37() by A27, A31, Th28; :: thesis: verum

end;

suppose InsCode I = 6 ; :: thesis: Exec I,s1, Exec I,s2 equal_outside K37()

then consider loc being Element of NAT such that
A32: I = goto loc by SCMFSA_2:59;

A33: now

let f be FinSeq-Location ; :: thesis: (Exec I,s1) . f = (Exec I,s2) . f
thus (Exec I,s1) . f = s1 . f by A32, SCMFSA_2:95
.= s2 . f by A1, Th31
.= (Exec I,s2) . f by A32, SCMFSA_2:95 ; :: thesis: verum

end;

A34: now

let c be Int-Location ; :: thesis: (Exec I,s1) . c = (Exec I,s2) . c
thus (Exec I,s1) . c = s1 . c by A32, SCMFSA_2:95
.= s2 . c by A1, Th30
.= (Exec I,s2) . c by A32, SCMFSA_2:95 ; :: thesis: verum

end;

IC (Exec I,s1) = loc by A32, SCMFSA_2:95
.= IC (Exec I,s2) by A32, SCMFSA_2:95 ;
hence Exec I,s1, Exec I,s2 equal_outside K37() by A34, A33, Th28; :: thesis: verum

end;

suppose InsCode I = 7 ; :: thesis: Exec I,s1, Exec I,s2 equal_outside K37()

then consider loc being Element of NAT , da being Int-Location such that
A35: I = da =0_goto loc by SCMFSA_2:60;

A36: now

per cases ( s1 . da = 0 or s1 . da <> 0 ) ;

suppose A37: s1 . da = 0 ; :: thesis: IC (Exec I,s1) = IC (Exec I,s2)

then A38: s2 . da = 0 by A1, Th30;
thus IC (Exec I,s1) = loc by A35, A37, SCMFSA_2:96
.= IC (Exec I,s2) by A35, A38, SCMFSA_2:96 ; :: thesis: verum

end;

suppose A39: s1 . da <> 0 ; :: thesis: IC (Exec I,s1) = IC (Exec I,s2)

then A40: s2 . da <> 0 by A1, Th30;
thus IC (Exec I,s1) = succ (IC s1) by A35, A39, SCMFSA_2:96
.= succ (IC s2) by A1, COMPOS_1:24
.= IC (Exec I,s2) by A35, A40, SCMFSA_2:96 ; :: thesis: verum

end;

end;

end;

A41: now

let f be FinSeq-Location ; :: thesis: (Exec I,s1) . f = (Exec I,s2) . f
thus (Exec I,s1) . f = s1 . f by A35, SCMFSA_2:96
.= s2 . f by A1, Th31
.= (Exec I,s2) . f by A35, SCMFSA_2:96 ; :: thesis: verum

end;

now

let c be Int-Location ; :: thesis: (Exec I,s1) . c = (Exec I,s2) . c
thus (Exec I,s1) . c = s1 . c by A35, SCMFSA_2:96
.= s2 . c by A1, Th30
.= (Exec I,s2) . c by A35, SCMFSA_2:96 ; :: thesis: verum

end;

hence Exec I,s1, Exec I,s2 equal_outside K37() by A41, A36, Th28; :: thesis: verum

end;

suppose InsCode I = 8 ; :: thesis: Exec I,s1, Exec I,s2 equal_outside K37()

then consider loc being Element of NAT , da being Int-Location such that
A42: I = da >0_goto loc by SCMFSA_2:61;

A43: now

per cases ( s1 . da > 0 or s1 . da <= 0 ) ;

suppose A44: s1 . da > 0 ; :: thesis: IC (Exec I,s1) = IC (Exec I,s2)

then A45: s2 . da > 0 by A1, Th30;
thus IC (Exec I,s1) = loc by A42, A44, SCMFSA_2:97
.= IC (Exec I,s2) by A42, A45, SCMFSA_2:97 ; :: thesis: verum

end;

suppose A46: s1 . da <= 0 ; :: thesis: IC (Exec I,s1) = IC (Exec I,s2)

then A47: s2 . da <= 0 by A1, Th30;
thus IC (Exec I,s1) = succ (IC s1) by A42, A46, SCMFSA_2:97
.= succ (IC s2) by A1, COMPOS_1:24
.= IC (Exec I,s2) by A42, A47, SCMFSA_2:97 ; :: thesis: verum

end;

end;

end;

A48: now

let f be FinSeq-Location ; :: thesis: (Exec I,s1) . f = (Exec I,s2) . f
thus (Exec I,s1) . f = s1 . f by A42, SCMFSA_2:97
.= s2 . f by A1, Th31
.= (Exec I,s2) . f by A42, SCMFSA_2:97 ; :: thesis: verum

end;

now

let c be Int-Location ; :: thesis: (Exec I,s1) . c = (Exec I,s2) . c
thus (Exec I,s1) . c = s1 . c by A42, SCMFSA_2:97
.= s2 . c by A1, Th30
.= (Exec I,s2) . c by A42, SCMFSA_2:97 ; :: thesis: verum

end;

hence Exec I,s1, Exec I,s2 equal_outside K37() by A48, A43, Th28; :: thesis: verum

end;

suppose InsCode I = 9 ; :: thesis: Exec I,s1, Exec I,s2 equal_outside K37()

then consider db, da being Int-Location , f being FinSeq-Location such that
A49: I = da := f,db by SCMFSA_2:62;

A50: now

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

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

suppose A51: c = da ; :: thesis: (Exec I,s1) . b₁ = (Exec I,s2) . b₁

then consider n being Element of NAT such that
A52: n = abs (s2 . db) and
A53: (Exec (da := f,db),s2) . c = (s2 . f) /. n by SCMFSA_2:98;
consider m being Element of NAT such that
A54: m = abs (s1 . db) and
A55: (Exec (da := f,db),s1) . c = (s1 . f) /. m by A51, SCMFSA_2:98;
m = n by A1, A54, A52, Th30;
hence (Exec I,s1) . c = (Exec I,s2) . c by A1, A49, A55, A53, Th31; :: thesis: verum

end;

suppose A56: c <> da ; :: thesis: (Exec I,s1) . b₁ = (Exec I,s2) . b₁

hence (Exec I,s1) . c = s1 . c by A49, SCMFSA_2:98
.= s2 . c by A1, Th30
.= (Exec I,s2) . c by A49, A56, SCMFSA_2:98 ;
:: thesis: verum

end;

end;

end;

A57: now

let f be FinSeq-Location ; :: thesis: (Exec I,s1) . f = (Exec I,s2) . f
thus (Exec I,s1) . f = s1 . f by A49, SCMFSA_2:98
.= s2 . f by A1, Th31
.= (Exec I,s2) . f by A49, SCMFSA_2:98 ; :: thesis: verum

end;

IC (Exec I,s1) = succ (IC s1) by A49, SCMFSA_2:98
.= succ (IC s2) by A1, COMPOS_1:24
.= IC (Exec I,s2) by A49, SCMFSA_2:98 ;
hence Exec I,s1, Exec I,s2 equal_outside K37() by A50, A57, Th28; :: thesis: verum

end;

suppose InsCode I = 10 ; :: thesis: Exec I,s1, Exec I,s2 equal_outside K37()

then consider db, da being Int-Location , f being FinSeq-Location such that
A58: I = f,db := da by SCMFSA_2:63;

A59: now

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

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

suppose A60: g = f ; :: thesis: (Exec I,s1) . b₁ = (Exec I,s2) . b₁

A61: s1 . da = s2 . da by A1, Th30;
consider n being Element of NAT such that
A62: n = abs (s2 . db) and
A63: (Exec (f,db := da),s2) . f = (s2 . f) +* n,(s2 . da) by SCMFSA_2:99;
consider m being Element of NAT such that
A64: m = abs (s1 . db) and
A65: (Exec (f,db := da),s1) . f = (s1 . f) +* m,(s1 . da) by SCMFSA_2:99;
m = n by A1, A64, A62, Th30;
hence (Exec I,s1) . g = (Exec I,s2) . g by A1, A58, A60, A65, A63, A61, Th31; :: thesis: verum

end;

suppose A66: g <> f ; :: thesis: (Exec I,s1) . b₁ = (Exec I,s2) . b₁

hence (Exec I,s1) . g = s1 . g by A58, SCMFSA_2:99
.= s2 . g by A1, Th31
.= (Exec I,s2) . g by A58, A66, SCMFSA_2:99 ;
:: thesis: verum

end;

end;

end;

A67: now

let c be Int-Location ; :: thesis: (Exec I,s1) . c = (Exec I,s2) . c
thus (Exec I,s1) . c = s1 . c by A58, SCMFSA_2:99
.= s2 . c by A1, Th30
.= (Exec I,s2) . c by A58, SCMFSA_2:99 ; :: thesis: verum

end;

IC (Exec I,s1) = succ (IC s1) by A58, SCMFSA_2:99
.= succ (IC s2) by A1, COMPOS_1:24
.= IC (Exec I,s2) by A58, SCMFSA_2:99 ;
hence Exec I,s1, Exec I,s2 equal_outside K37() by A67, A59, Th28; :: thesis: verum

end;

suppose InsCode I = 11 ; :: thesis: Exec I,s1, Exec I,s2 equal_outside K37()

then consider da being Int-Location , f being FinSeq-Location such that
A68: I = da :=len f by SCMFSA_2:64;

A69: now

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

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

suppose A70: c = da ; :: thesis: (Exec I,s1) . b₁ = (Exec I,s2) . b₁

hence (Exec I,s1) . c = len (s1 . f) by A68, SCMFSA_2:100
.= len (s2 . f) by A1, Th31
.= (Exec I,s2) . c by A68, A70, SCMFSA_2:100 ;
:: thesis: verum

end;

suppose A71: c <> da ; :: thesis: (Exec I,s1) . b₁ = (Exec I,s2) . b₁

hence (Exec I,s1) . c = s1 . c by A68, SCMFSA_2:100
.= s2 . c by A1, Th30
.= (Exec I,s2) . c by A68, A71, SCMFSA_2:100 ;
:: thesis: verum

end;

end;

end;

A72: now

let f be FinSeq-Location ; :: thesis: (Exec I,s1) . f = (Exec I,s2) . f
thus (Exec I,s1) . f = s1 . f by A68, SCMFSA_2:100
.= s2 . f by A1, Th31
.= (Exec I,s2) . f by A68, SCMFSA_2:100 ; :: thesis: verum

end;

IC (Exec I,s1) = succ (IC s1) by A68, SCMFSA_2:100
.= succ (IC s2) by A1, COMPOS_1:24
.= IC (Exec I,s2) by A68, SCMFSA_2:100 ;
hence Exec I,s1, Exec I,s2 equal_outside K37() by A69, A72, Th28; :: thesis: verum

end;

suppose InsCode I = 12 ; :: thesis: Exec I,s1, Exec I,s2 equal_outside K37()

then consider da being Int-Location , f being FinSeq-Location such that
A73: I = f :=<0,...,0> da by SCMFSA_2:65;

A74: now

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

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

suppose A75: g = f ; :: thesis: (Exec I,s1) . b₁ = (Exec I,s2) . b₁

( ex m being Element of NAT st
( m = abs (s1 . da) & (Exec (f :=<0,...,0> da),s1) . f = m |-> 0 ) & ex n being Element of NAT st
( n = abs (s2 . da) & (Exec (f :=<0,...,0> da),s2) . f = n |-> 0 ) ) by SCMFSA_2:101;
hence (Exec I,s1) . g = (Exec I,s2) . g by A1, A73, A75, Th30; :: thesis: verum

end;

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

hence (Exec I,s1) . g = s1 . g by A73, SCMFSA_2:101
.= s2 . g by A1, Th31
.= (Exec I,s2) . g by A73, A76, SCMFSA_2:101 ;
:: thesis: verum

end;

end;

end;

A77: now

let c be Int-Location ; :: thesis: (Exec I,s1) . c = (Exec I,s2) . c
thus (Exec I,s1) . c = s1 . c by A73, SCMFSA_2:101
.= s2 . c by A1, Th30
.= (Exec I,s2) . c by A73, SCMFSA_2:101 ; :: thesis: verum

end;

IC (Exec I,s1) = succ (IC s1) by A73, SCMFSA_2:101
.= succ (IC s2) by A1, COMPOS_1:24
.= IC (Exec I,s2) by A73, SCMFSA_2:101 ;
hence Exec I,s1, Exec I,s2 equal_outside K37() by A77, A74, Th28; :: thesis: verum

end;

end;