let s1, s2 be State of SCM+FSA ; :: thesis: for i being Instruction of SCM+FSA
for a being Int-Location st ( for b being Int-Location st a <> b holds
s1 . b = s2 . b ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & i does_not_refer a & IC s1 = IC s2 holds
( ( for b being Int-Location st a <> b holds
(Exec i,s1) . b = (Exec i,s2) . b ) & ( for f being FinSeq-Location holds (Exec i,s1) . f = (Exec i,s2) . f ) & IC (Exec i,s1) = IC (Exec i,s2) )
let i be Instruction of SCM+FSA ; :: thesis: for a being Int-Location st ( for b being Int-Location st a <> b holds
s1 . b = s2 . b ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & i does_not_refer a & IC s1 = IC s2 holds
( ( for b being Int-Location st a <> b holds
(Exec i,s1) . b = (Exec i,s2) . b ) & ( for f being FinSeq-Location holds (Exec i,s1) . f = (Exec i,s2) . f ) & IC (Exec i,s1) = IC (Exec i,s2) )
let a be Int-Location ; :: thesis: ( ( for b being Int-Location st a <> b holds
s1 . b = s2 . b ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & i does_not_refer a & IC s1 = IC s2 implies ( ( for b being Int-Location st a <> b holds
(Exec i,s1) . b = (Exec i,s2) . b ) & ( for f being FinSeq-Location holds (Exec i,s1) . f = (Exec i,s2) . f ) & IC (Exec i,s1) = IC (Exec i,s2) ) )
defpred S₁[ State of SCM+FSA , State of SCM+FSA ] means ( ( for b being Int-Location st a <> b holds
$1 . b = $2 . b ) & ( for f being FinSeq-Location holds $1 . f = $2 . f ) );
assume A1: S₁[s1,s2] ; :: thesis: ( not i does_not_refer a or not IC s1 = IC s2 or ( ( for b being Int-Location st a <> b holds
(Exec i,s1) . b = (Exec i,s2) . b ) & ( for f being FinSeq-Location holds (Exec i,s1) . f = (Exec i,s2) . f ) & IC (Exec i,s1) = IC (Exec i,s2) ) )
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;
assume A4: i does_not_refer a ; :: thesis: ( not IC s1 = IC s2 or ( ( for b being Int-Location st a <> b holds
(Exec i,s1) . b = (Exec i,s2) . b ) & ( for f being FinSeq-Location holds (Exec i,s1) . f = (Exec i,s2) . f ) & IC (Exec i,s1) = IC (Exec i,s2) ) )
A5: InsCode i <= 11 + 1 by SCMFSA_2:35;

A6: now

let b be Int-Location ; :: thesis: ( a <> b implies (Exec i,s1) . b₁ = (Exec i,s2) . b₁ )
assume A7: a <> b ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

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 A5, A3, A2, NAT_1:8, NAT_1:33;

suppose InsCode i = 0 ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then A8: i = halt SCM+FSA by SCMFSA_2:122;
hence (Exec i,s1) . b = s1 . b by AMI_1:def 8
.= s2 . b by A1, A7
.= (Exec i,s2) . b by A8, AMI_1:def 8 ;
:: thesis: verum

end;

suppose InsCode i = 1 ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then consider da, db being Int-Location such that
A9: i = da := db by SCMFSA_2:54;
A10: a <> db by A4, A9, SCMFSA7B:def 1;

hereby :: thesis: verum

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

suppose A11: b = da ; :: thesis: (Exec i,s1) . b = (Exec i,s2) . b

hence (Exec i,s1) . b = s1 . db by A9, SCMFSA_2:89
.= s2 . db by A1, A10
.= (Exec i,s2) . b by A9, A11, SCMFSA_2:89 ;
:: thesis: verum

end;

suppose A12: b <> da ; :: thesis: (Exec i,s1) . b = (Exec i,s2) . b

hence (Exec i,s1) . b = s1 . b by A9, SCMFSA_2:89
.= s2 . b by A1, A7
.= (Exec i,s2) . b by A9, A12, SCMFSA_2:89 ;
:: thesis: verum

end;

end;

end;

end;

suppose InsCode i = 2 ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then consider da, db being Int-Location such that
A13: i = AddTo da,db by SCMFSA_2:55;
A14: a <> db by A4, A13, SCMFSA7B:def 1;

hereby :: thesis: verum

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

suppose A15: b = da ; :: thesis: (Exec i,s1) . b = (Exec i,s2) . b

hence (Exec i,s1) . b = (s1 . b) + (s1 . db) by A13, SCMFSA_2:90
.= (s2 . b) + (s1 . db) by A1, A7
.= (s2 . b) + (s2 . db) by A1, A14
.= (Exec i,s2) . b by A13, A15, SCMFSA_2:90 ;
:: thesis: verum

end;

suppose A16: b <> da ; :: thesis: (Exec i,s1) . b = (Exec i,s2) . b

hence (Exec i,s1) . b = s1 . b by A13, SCMFSA_2:90
.= s2 . b by A1, A7
.= (Exec i,s2) . b by A13, A16, SCMFSA_2:90 ;
:: thesis: verum

end;

end;

end;

end;

suppose InsCode i = 3 ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then consider da, db being Int-Location such that
A17: i = SubFrom da,db by SCMFSA_2:56;
A18: a <> db by A4, A17, SCMFSA7B:def 1;

hereby :: thesis: verum

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

suppose A19: b = da ; :: thesis: (Exec i,s1) . b = (Exec i,s2) . b

hence (Exec i,s1) . b = (s1 . b) - (s1 . db) by A17, SCMFSA_2:91
.= (s2 . b) - (s1 . db) by A1, A7
.= (s2 . b) - (s2 . db) by A1, A18
.= (Exec i,s2) . b by A17, A19, SCMFSA_2:91 ;
:: thesis: verum

end;

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

hence (Exec i,s1) . b = s1 . b by A17, SCMFSA_2:91
.= s2 . b by A1, A7
.= (Exec i,s2) . b by A17, A20, SCMFSA_2:91 ;
:: thesis: verum

end;

end;

end;

end;

suppose InsCode i = 4 ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then consider da, db being Int-Location such that
A21: i = MultBy da,db by SCMFSA_2:57;
A22: a <> db by A4, A21, SCMFSA7B:def 1;

hereby :: thesis: verum

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

suppose A23: b = da ; :: thesis: (Exec i,s1) . b = (Exec i,s2) . b

hence (Exec i,s1) . b = (s1 . b) * (s1 . db) by A21, SCMFSA_2:92
.= (s2 . b) * (s1 . db) by A1, A7
.= (s2 . b) * (s2 . db) by A1, A22
.= (Exec i,s2) . b by A21, A23, SCMFSA_2:92 ;
:: thesis: verum

end;

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

hence (Exec i,s1) . b = s1 . b by A21, SCMFSA_2:92
.= s2 . b by A1, A7
.= (Exec i,s2) . b by A21, A24, SCMFSA_2:92 ;
:: thesis: verum

end;

end;

end;

end;

suppose InsCode i = 5 ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then consider da, db being Int-Location such that
A25: i = Divide da,db by SCMFSA_2:58;
A26: a <> db by A4, A25, SCMFSA7B:def 1;
A27: a <> da by A4, A25, SCMFSA7B:def 1;

hereby :: thesis: verum

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

suppose A28: b = db ; :: thesis: (Exec i,s1) . b = (Exec i,s2) . b

hence (Exec i,s1) . b = (s1 . da) mod (s1 . db) by A25, SCMFSA_2:93
.= (s2 . da) mod (s1 . db) by A1, A27
.= (s2 . da) mod (s2 . db) by A1, A26
.= (Exec i,s2) . b by A25, A28, SCMFSA_2:93 ;
:: thesis: verum

end;

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

hence (Exec i,s1) . b = (s1 . da) div (s1 . db) by A25, SCMFSA_2:93
.= (s1 . da) div (s2 . db) by A1, A26
.= (s2 . da) div (s2 . db) by A1, A27
.= (Exec i,s2) . b by A25, A29, SCMFSA_2:93 ;
:: thesis: verum

end;

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

hence (Exec i,s1) . b = s1 . b by A25, SCMFSA_2:93
.= s2 . b by A1, A7
.= (Exec i,s2) . b by A25, A30, SCMFSA_2:93 ;
:: thesis: verum

end;

end;

end;

end;

suppose InsCode i = 6 ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then A31: ex loc being Element of NAT st i = goto loc by SCMFSA_2:59;
hence (Exec i,s1) . b = s1 . b by SCMFSA_2:95
.= s2 . b by A1, A7
.= (Exec i,s2) . b by A31, SCMFSA_2:95 ;
:: thesis: verum

end;

suppose InsCode i = 7 ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then A32: ex loc being Element of NAT ex da being Int-Location st i = da =0_goto loc by SCMFSA_2:60;
hence (Exec i,s1) . b = s1 . b by SCMFSA_2:96
.= s2 . b by A1, A7
.= (Exec i,s2) . b by A32, SCMFSA_2:96 ;
:: thesis: verum

end;

suppose InsCode i = 8 ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then A33: ex loc being Element of NAT ex da being Int-Location st i = da >0_goto loc by SCMFSA_2:61;
hence (Exec i,s1) . b = s1 . b by SCMFSA_2:97
.= s2 . b by A1, A7
.= (Exec i,s2) . b by A33, SCMFSA_2:97 ;
:: thesis: verum

end;

suppose InsCode i = 9 ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then consider db, da being Int-Location , g being FinSeq-Location such that
A34: i = da := g,db by SCMFSA_2:62;
A35: a <> db by A4, A34, SCMFSA7B:def 1;

hereby :: thesis: verum

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

suppose A36: b = da ; :: thesis: (Exec i,s1) . b = (Exec i,s2) . b

then consider m2 being Element of NAT such that
A37: m2 = abs (s2 . db) and
A38: (Exec (da := g,db),s2) . b = (s2 . g) /. m2 by SCMFSA_2:98;
consider m1 being Element of NAT such that
A39: m1 = abs (s1 . db) and
A40: (Exec (da := g,db),s1) . b = (s1 . g) /. m1 by A36, SCMFSA_2:98;
m1 = m2 by A1, A35, A39, A37;
hence (Exec i,s1) . b = (Exec i,s2) . b by A1, A34, A40, A38; :: thesis: verum

end;

suppose A41: b <> da ; :: thesis: (Exec i,s1) . b = (Exec i,s2) . b

hence (Exec i,s1) . b = s1 . b by A34, SCMFSA_2:98
.= s2 . b by A1, A7
.= (Exec i,s2) . b by A34, A41, SCMFSA_2:98 ;
:: thesis: verum

end;

end;

end;

end;

suppose InsCode i = 10 ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then A42: ex db, da being Int-Location ex g being FinSeq-Location st i = g,db := da by SCMFSA_2:63;
hence (Exec i,s1) . b = s1 . b by SCMFSA_2:99
.= s2 . b by A1, A7
.= (Exec i,s2) . b by A42, SCMFSA_2:99 ;
:: thesis: verum

end;

suppose InsCode i = 11 ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then consider da being Int-Location , g being FinSeq-Location such that
A43: i = da :=len g by SCMFSA_2:64;

hereby :: thesis: verum

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

suppose A44: b = da ; :: thesis: (Exec i,s1) . b = (Exec i,s2) . b

hence (Exec i,s1) . b = len (s1 . g) by A43, SCMFSA_2:100
.= len (s2 . g) by A1
.= (Exec i,s2) . b by A43, A44, SCMFSA_2:100 ;
:: thesis: verum

end;

suppose A45: b <> da ; :: thesis: (Exec i,s1) . b = (Exec i,s2) . b

hence (Exec i,s1) . b = s1 . b by A43, SCMFSA_2:100
.= s2 . b by A1, A7
.= (Exec i,s2) . b by A43, A45, SCMFSA_2:100 ;
:: thesis: verum

end;

end;

end;

end;

suppose InsCode i = 12 ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then A46: ex da being Int-Location ex g being FinSeq-Location st i = g :=<0,...,0> da by SCMFSA_2:65;
hence (Exec i,s1) . b = s1 . b by SCMFSA_2:101
.= s2 . b by A1, A7
.= (Exec i,s2) . b by A46, SCMFSA_2:101 ;
:: thesis: verum

end;

end;

end;

assume A47: IC s1 = IC s2 ; :: thesis: ( ( for b being Int-Location st a <> b holds
(Exec i,s1) . b = (Exec i,s2) . b ) & ( for f being FinSeq-Location holds (Exec i,s1) . f = (Exec i,s2) . f ) & IC (Exec i,s1) = IC (Exec i,s2) )

now

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

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 A5, A3, A2, NAT_1:8, NAT_1:33;

suppose InsCode i = 0 ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then A48: i = halt SCM+FSA by SCMFSA_2:122;
hence (Exec i,s1) . f = s1 . f by AMI_1:def 8
.= s2 . f by A1
.= (Exec i,s2) . f by A48, AMI_1:def 8 ;
:: thesis: verum

end;

suppose InsCode i = 1 ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then A49: ex da, db being Int-Location st i = da := db by SCMFSA_2:54;
hence (Exec i,s1) . f = s1 . f by SCMFSA_2:89
.= s2 . f by A1
.= (Exec i,s2) . f by A49, SCMFSA_2:89 ;
:: thesis: verum

end;

suppose InsCode i = 2 ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then A50: ex da, db being Int-Location st i = AddTo da,db by SCMFSA_2:55;
hence (Exec i,s1) . f = s1 . f by SCMFSA_2:90
.= s2 . f by A1
.= (Exec i,s2) . f by A50, SCMFSA_2:90 ;
:: thesis: verum

end;

suppose InsCode i = 3 ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then A51: ex da, db being Int-Location st i = SubFrom da,db by SCMFSA_2:56;
hence (Exec i,s1) . f = s1 . f by SCMFSA_2:91
.= s2 . f by A1
.= (Exec i,s2) . f by A51, SCMFSA_2:91 ;
:: thesis: verum

end;

suppose InsCode i = 4 ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then A52: ex da, db being Int-Location st i = MultBy da,db by SCMFSA_2:57;
hence (Exec i,s1) . f = s1 . f by SCMFSA_2:92
.= s2 . f by A1
.= (Exec i,s2) . f by A52, SCMFSA_2:92 ;
:: thesis: verum

end;

suppose InsCode i = 5 ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then A53: ex da, db being Int-Location st i = Divide da,db by SCMFSA_2:58;
hence (Exec i,s1) . f = s1 . f by SCMFSA_2:93
.= s2 . f by A1
.= (Exec i,s2) . f by A53, SCMFSA_2:93 ;
:: thesis: verum

end;

suppose InsCode i = 6 ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then A54: ex loc being Element of NAT st i = goto loc by SCMFSA_2:59;
hence (Exec i,s1) . f = s1 . f by SCMFSA_2:95
.= s2 . f by A1
.= (Exec i,s2) . f by A54, SCMFSA_2:95 ;
:: thesis: verum

end;

suppose InsCode i = 7 ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then A55: ex loc being Element of NAT ex da being Int-Location st i = da =0_goto loc by SCMFSA_2:60;
hence (Exec i,s1) . f = s1 . f by SCMFSA_2:96
.= s2 . f by A1
.= (Exec i,s2) . f by A55, SCMFSA_2:96 ;
:: thesis: verum

end;

suppose InsCode i = 8 ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then A56: ex loc being Element of NAT ex da being Int-Location st i = da >0_goto loc by SCMFSA_2:61;
hence (Exec i,s1) . f = s1 . f by SCMFSA_2:97
.= s2 . f by A1
.= (Exec i,s2) . f by A56, SCMFSA_2:97 ;
:: thesis: verum

end;

suppose InsCode i = 9 ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then A57: ex db, da being Int-Location ex g being FinSeq-Location st i = da := g,db by SCMFSA_2:62;
hence (Exec i,s1) . f = s1 . f by SCMFSA_2:98
.= s2 . f by A1
.= (Exec i,s2) . f by A57, SCMFSA_2:98 ;
:: thesis: verum

end;

suppose InsCode i = 10 ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then consider db, da being Int-Location , g being FinSeq-Location such that
A58: i = g,db := da by SCMFSA_2:63;
A59: a <> db by A4, A58, SCMFSA7B:def 1;
A60: a <> da by A4, A58, SCMFSA7B:def 1;

hereby :: thesis: verum

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

suppose A61: f = g ; :: thesis: (Exec i,s1) . f = (Exec i,s2) . f

A62: s1 . da = s2 . da by A1, A60;
consider m2 being Element of NAT such that
A63: m2 = abs (s2 . db) and
A64: (Exec (g,db := da),s2) . g = (s2 . g) +* m2,(s2 . da) by SCMFSA_2:99;
consider m1 being Element of NAT such that
A65: m1 = abs (s1 . db) and
A66: (Exec (g,db := da),s1) . g = (s1 . g) +* m1,(s1 . da) by SCMFSA_2:99;
m1 = m2 by A1, A59, A65, A63;
hence (Exec i,s1) . f = (Exec i,s2) . f by A1, A58, A61, A66, A64, A62; :: thesis: verum

end;

suppose A67: f <> g ; :: thesis: (Exec i,s1) . f = (Exec i,s2) . f

hence (Exec i,s1) . f = s1 . f by A58, SCMFSA_2:99
.= s2 . f by A1
.= (Exec i,s2) . f by A58, A67, SCMFSA_2:99 ;
:: thesis: verum

end;

end;

end;

end;

suppose InsCode i = 11 ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then A68: ex da being Int-Location ex g being FinSeq-Location st i = da :=len g by SCMFSA_2:64;
hence (Exec i,s1) . f = s1 . f by SCMFSA_2:100
.= s2 . f by A1
.= (Exec i,s2) . f by A68, SCMFSA_2:100 ;
:: thesis: verum

end;

suppose InsCode i = 12 ; :: thesis: (Exec i,s1) . b₁ = (Exec i,s2) . b₁

then consider da being Int-Location , g being FinSeq-Location such that
A69: i = g :=<0,...,0> da by SCMFSA_2:65;
A70: a <> da by A4, A69, SCMFSA7B:def 1;

hereby :: thesis: verum

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

suppose A71: f = g ; :: thesis: (Exec i,s1) . f = (Exec i,s2) . f

A72: ex m2 being Element of NAT st
( m2 = abs (s2 . da) & (Exec (g :=<0,...,0> da),s2) . g = m2 |-> 0 ) by SCMFSA_2:101;
ex m1 being Element of NAT st
( m1 = abs (s1 . da) & (Exec (g :=<0,...,0> da),s1) . g = m1 |-> 0 ) by SCMFSA_2:101;
hence (Exec i,s1) . f = (Exec i,s2) . f by A1, A69, A70, A71, A72; :: thesis: verum

end;

suppose A73: f <> g ; :: thesis: (Exec i,s1) . f = (Exec i,s2) . f

hence (Exec i,s1) . f = s1 . f by A69, SCMFSA_2:101
.= s2 . f by A1
.= (Exec i,s2) . f by A69, A73, SCMFSA_2:101 ;
:: thesis: verum

end;

end;

end;

end;

end;

end;

hence S₁[ Exec i,s1, Exec i,s2] by A6; :: thesis: IC (Exec i,s1) = IC (Exec i,s2)

now

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 A5, A3, A2, NAT_1:8, NAT_1:33;

suppose InsCode i = 0 ; :: thesis: (Exec i,s1) . (IC SCM+FSA ) = (Exec i,s2) . (IC SCM+FSA )

then A74: i = halt SCM+FSA by SCMFSA_2:122;
hence (Exec i,s1) . (IC SCM+FSA ) = IC s1 by AMI_1:def 8
.= (Exec i,s2) . (IC SCM+FSA ) by A47, A74, AMI_1:def 8 ;
:: thesis: verum

end;

suppose InsCode i = 1 ; :: thesis: (Exec i,s1) . (IC SCM+FSA ) = (Exec i,s2) . (IC SCM+FSA )

then A75: ex da, db being Int-Location st i = da := db by SCMFSA_2:54;
hence (Exec i,s1) . (IC SCM+FSA ) = succ (IC s1) by SCMFSA_2:89
.= (Exec i,s2) . (IC SCM+FSA ) by A47, A75, SCMFSA_2:89 ;
:: thesis: verum

end;

suppose InsCode i = 2 ; :: thesis: (Exec i,s1) . (IC SCM+FSA ) = (Exec i,s2) . (IC SCM+FSA )

then A76: ex da, db being Int-Location st i = AddTo da,db by SCMFSA_2:55;
hence (Exec i,s1) . (IC SCM+FSA ) = succ (IC s1) by SCMFSA_2:90
.= (Exec i,s2) . (IC SCM+FSA ) by A47, A76, SCMFSA_2:90 ;
:: thesis: verum

end;

suppose InsCode i = 3 ; :: thesis: (Exec i,s1) . (IC SCM+FSA ) = (Exec i,s2) . (IC SCM+FSA )

then A77: ex da, db being Int-Location st i = SubFrom da,db by SCMFSA_2:56;
hence (Exec i,s1) . (IC SCM+FSA ) = succ (IC s1) by SCMFSA_2:91
.= (Exec i,s2) . (IC SCM+FSA ) by A47, A77, SCMFSA_2:91 ;
:: thesis: verum

end;

suppose InsCode i = 4 ; :: thesis: (Exec i,s1) . (IC SCM+FSA ) = (Exec i,s2) . (IC SCM+FSA )

then A78: ex da, db being Int-Location st i = MultBy da,db by SCMFSA_2:57;
hence (Exec i,s1) . (IC SCM+FSA ) = succ (IC s1) by SCMFSA_2:92
.= (Exec i,s2) . (IC SCM+FSA ) by A47, A78, SCMFSA_2:92 ;
:: thesis: verum

end;

suppose InsCode i = 5 ; :: thesis: (Exec i,s1) . (IC SCM+FSA ) = (Exec i,s2) . (IC SCM+FSA )

then A79: ex da, db being Int-Location st i = Divide da,db by SCMFSA_2:58;
hence (Exec i,s1) . (IC SCM+FSA ) = succ (IC s1) by SCMFSA_2:93
.= (Exec i,s2) . (IC SCM+FSA ) by A47, A79, SCMFSA_2:93 ;
:: thesis: verum

end;

suppose InsCode i = 6 ; :: thesis: (Exec i,s1) . (IC SCM+FSA ) = (Exec i,s2) . (IC SCM+FSA )

then consider loc being Element of NAT such that
A80: i = goto loc by SCMFSA_2:59;
thus (Exec i,s1) . (IC SCM+FSA ) = loc by A80, SCMFSA_2:95
.= (Exec i,s2) . (IC SCM+FSA ) by A80, SCMFSA_2:95 ; :: thesis: verum

end;

suppose InsCode i = 7 ; :: thesis: (Exec i,s1) . (IC SCM+FSA ) = (Exec i,s2) . (IC SCM+FSA )

then consider loc being Element of NAT , da being Int-Location such that
A81: i = da =0_goto loc by SCMFSA_2:60;
a <> da by A4, A81, SCMFSA7B:def 1;
then A82: s1 . da = s2 . da by A1;

hereby :: thesis: verum

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

suppose A83: s1 . da = 0 ; :: thesis: (Exec i,s1) . (IC SCM+FSA ) = (Exec i,s2) . (IC SCM+FSA )

hence (Exec i,s1) . (IC SCM+FSA ) = loc by A81, SCMFSA_2:96
.= (Exec i,s2) . (IC SCM+FSA ) by A81, A82, A83, SCMFSA_2:96 ;
:: thesis: verum

end;

suppose A84: s1 . da <> 0 ; :: thesis: (Exec i,s1) . (IC SCM+FSA ) = (Exec i,s2) . (IC SCM+FSA )

hence (Exec i,s1) . (IC SCM+FSA ) = succ (IC s1) by A81, SCMFSA_2:96
.= (Exec i,s2) . (IC SCM+FSA ) by A47, A81, A82, A84, SCMFSA_2:96 ;
:: thesis: verum

end;

end;

end;

end;

suppose InsCode i = 8 ; :: thesis: (Exec i,s1) . (IC SCM+FSA ) = (Exec i,s2) . (IC SCM+FSA )

then consider loc being Element of NAT , da being Int-Location such that
A85: i = da >0_goto loc by SCMFSA_2:61;
a <> da by A4, A85, SCMFSA7B:def 1;
then A86: s1 . da = s2 . da by A1;

hereby :: thesis: verum

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

suppose A87: s1 . da > 0 ; :: thesis: (Exec i,s1) . (IC SCM+FSA ) = (Exec i,s2) . (IC SCM+FSA )

hence (Exec i,s1) . (IC SCM+FSA ) = loc by A85, SCMFSA_2:97
.= (Exec i,s2) . (IC SCM+FSA ) by A85, A86, A87, SCMFSA_2:97 ;
:: thesis: verum

end;

suppose A88: s1 . da <= 0 ; :: thesis: (Exec i,s1) . (IC SCM+FSA ) = (Exec i,s2) . (IC SCM+FSA )

hence (Exec i,s1) . (IC SCM+FSA ) = succ (IC s1) by A85, SCMFSA_2:97
.= (Exec i,s2) . (IC SCM+FSA ) by A47, A85, A86, A88, SCMFSA_2:97 ;
:: thesis: verum

end;

end;

end;

end;

suppose InsCode i = 9 ; :: thesis: (Exec i,s1) . (IC SCM+FSA ) = (Exec i,s2) . (IC SCM+FSA )

then A89: ex db, da being Int-Location ex g being FinSeq-Location st i = da := g,db by SCMFSA_2:62;
hence (Exec i,s1) . (IC SCM+FSA ) = succ (IC s1) by SCMFSA_2:98
.= (Exec i,s2) . (IC SCM+FSA ) by A47, A89, SCMFSA_2:98 ;
:: thesis: verum

end;

suppose InsCode i = 10 ; :: thesis: (Exec i,s1) . (IC SCM+FSA ) = (Exec i,s2) . (IC SCM+FSA )

then A90: ex db, da being Int-Location ex g being FinSeq-Location st i = g,db := da by SCMFSA_2:63;
hence (Exec i,s1) . (IC SCM+FSA ) = succ (IC s1) by SCMFSA_2:99
.= (Exec i,s2) . (IC SCM+FSA ) by A47, A90, SCMFSA_2:99 ;
:: thesis: verum

end;

suppose InsCode i = 11 ; :: thesis: (Exec i,s1) . (IC SCM+FSA ) = (Exec i,s2) . (IC SCM+FSA )

then A91: ex da being Int-Location ex g being FinSeq-Location st i = da :=len g by SCMFSA_2:64;
hence (Exec i,s1) . (IC SCM+FSA ) = succ (IC s1) by SCMFSA_2:100
.= (Exec i,s2) . (IC SCM+FSA ) by A47, A91, SCMFSA_2:100 ;
:: thesis: verum

end;

suppose InsCode i = 12 ; :: thesis: (Exec i,s1) . (IC SCM+FSA ) = (Exec i,s2) . (IC SCM+FSA )

then A92: ex da being Int-Location ex g being FinSeq-Location st i = g :=<0,...,0> da by SCMFSA_2:65;
hence (Exec i,s1) . (IC SCM+FSA ) = succ (IC s1) by SCMFSA_2:101
.= (Exec i,s2) . (IC SCM+FSA ) by A47, A92, SCMFSA_2:101 ;
:: thesis: verum

end;

end;

end;

hence IC (Exec i,s1) = IC (Exec i,s2) ; :: thesis: verum