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 ) & not i refers 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 ) & not i refers 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 ) & not i refers 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 S1[ 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: S1[s1,s2] ; :: thesis: ( i refers 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)) ) )
assume A4: not i refers 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 <= 12 by SCMFSA_2:16;
A6: now
let b be Int-Location ; :: thesis: ( a <> b implies (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1 )
assume A7: a <> b ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
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, NAT_1:36;
suppose InsCode i = 0 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A8: i = halt SCM+FSA by SCMFSA_2:95;
hence (Exec (i,s1)) . b = s1 . b by EXTPRO_1:def 3
.= s2 . b by A1, A7
.= (Exec (i,s2)) . b by A8, EXTPRO_1:def 3 ;
:: thesis: verum
end;
suppose InsCode i = 1 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then consider da, db being Int-Location such that
A9: i = da := db by SCMFSA_2:30;
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:63
.= s2 . db by A1, A10
.= (Exec (i,s2)) . b by A9, A11, SCMFSA_2:63 ;
:: 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:63
.= s2 . b by A1, A7
.= (Exec (i,s2)) . b by A9, A12, SCMFSA_2:63 ;
:: thesis: verum
end;
end;
end;
end;
suppose InsCode i = 2 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then consider da, db being Int-Location such that
A13: i = AddTo (da,db) by SCMFSA_2:31;
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:64
.= (s2 . b) + (s1 . db) by A1, A7
.= (s2 . b) + (s2 . db) by A1, A14
.= (Exec (i,s2)) . b by A13, A15, SCMFSA_2:64 ;
:: 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:64
.= s2 . b by A1, A7
.= (Exec (i,s2)) . b by A13, A16, SCMFSA_2:64 ;
:: thesis: verum
end;
end;
end;
end;
suppose InsCode i = 3 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then consider da, db being Int-Location such that
A17: i = SubFrom (da,db) by SCMFSA_2:32;
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:65
.= (s2 . b) - (s1 . db) by A1, A7
.= (s2 . b) - (s2 . db) by A1, A18
.= (Exec (i,s2)) . b by A17, A19, SCMFSA_2:65 ;
:: 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:65
.= s2 . b by A1, A7
.= (Exec (i,s2)) . b by A17, A20, SCMFSA_2:65 ;
:: thesis: verum
end;
end;
end;
end;
suppose InsCode i = 4 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then consider da, db being Int-Location such that
A21: i = MultBy (da,db) by SCMFSA_2:33;
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:66
.= (s2 . b) * (s1 . db) by A1, A7
.= (s2 . b) * (s2 . db) by A1, A22
.= (Exec (i,s2)) . b by A21, A23, SCMFSA_2:66 ;
:: 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:66
.= s2 . b by A1, A7
.= (Exec (i,s2)) . b by A21, A24, SCMFSA_2:66 ;
:: thesis: verum
end;
end;
end;
end;
suppose InsCode i = 5 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then consider da, db being Int-Location such that
A25: i = Divide (da,db) by SCMFSA_2:34;
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:67
.= (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:67 ;
:: 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:67
.= (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:67 ;
:: 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:67
.= s2 . b by A1, A7
.= (Exec (i,s2)) . b by A25, A30, SCMFSA_2:67 ;
:: thesis: verum
end;
end;
end;
end;
suppose InsCode i = 6 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A31: ex loc being Element of NAT st i = goto loc by SCMFSA_2:35;
hence (Exec (i,s1)) . b = s1 . b by SCMFSA_2:69
.= s2 . b by A1, A7
.= (Exec (i,s2)) . b by A31, SCMFSA_2:69 ;
:: thesis: verum
end;
suppose InsCode i = 7 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A32: ex loc being Element of NAT ex da being Int-Location st i = da =0_goto loc by SCMFSA_2:36;
hence (Exec (i,s1)) . b = s1 . b by SCMFSA_2:70
.= s2 . b by A1, A7
.= (Exec (i,s2)) . b by A32, SCMFSA_2:70 ;
:: thesis: verum
end;
suppose InsCode i = 8 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A33: ex loc being Element of NAT ex da being Int-Location st i = da >0_goto loc by SCMFSA_2:37;
hence (Exec (i,s1)) . b = s1 . b by SCMFSA_2:71
.= s2 . b by A1, A7
.= (Exec (i,s2)) . b by A33, SCMFSA_2:71 ;
:: thesis: verum
end;
suppose InsCode i = 9 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then consider db, da being Int-Location , g being FinSeq-Location such that
A34: i = da := (g,db) by SCMFSA_2:38;
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:72;
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:72;
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:72
.= s2 . b by A1, A7
.= (Exec (i,s2)) . b by A34, A41, SCMFSA_2:72 ;
:: thesis: verum
end;
end;
end;
end;
suppose InsCode i = 10 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A42: ex db, da being Int-Location ex g being FinSeq-Location st i = (g,db) := da by SCMFSA_2:39;
hence (Exec (i,s1)) . b = s1 . b by SCMFSA_2:73
.= s2 . b by A1, A7
.= (Exec (i,s2)) . b by A42, SCMFSA_2:73 ;
:: thesis: verum
end;
suppose InsCode i = 11 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then consider da being Int-Location , g being FinSeq-Location such that
A43: i = da :=len g by SCMFSA_2:40;
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:74
.= len (s2 . g) by A1
.= (Exec (i,s2)) . b by A43, A44, SCMFSA_2:74 ;
:: 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:74
.= s2 . b by A1, A7
.= (Exec (i,s2)) . b by A43, A45, SCMFSA_2:74 ;
:: thesis: verum
end;
end;
end;
end;
suppose InsCode i = 12 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A46: ex da being Int-Location ex g being FinSeq-Location st i = g :=<0,...,0> da by SCMFSA_2:41;
hence (Exec (i,s1)) . b = s1 . b by SCMFSA_2:75
.= s2 . b by A1, A7
.= (Exec (i,s2)) . b by A46, SCMFSA_2:75 ;
:: 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)) . b1 = (Exec (i,s2)) . b1
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, NAT_1:36;
suppose InsCode i = 0 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A48: i = halt SCM+FSA by SCMFSA_2:95;
hence (Exec (i,s1)) . f = s1 . f by EXTPRO_1:def 3
.= s2 . f by A1
.= (Exec (i,s2)) . f by A48, EXTPRO_1:def 3 ;
:: thesis: verum
end;
suppose InsCode i = 1 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A49: ex da, db being Int-Location st i = da := db by SCMFSA_2:30;
hence (Exec (i,s1)) . f = s1 . f by SCMFSA_2:63
.= s2 . f by A1
.= (Exec (i,s2)) . f by A49, SCMFSA_2:63 ;
:: thesis: verum
end;
suppose InsCode i = 2 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A50: ex da, db being Int-Location st i = AddTo (da,db) by SCMFSA_2:31;
hence (Exec (i,s1)) . f = s1 . f by SCMFSA_2:64
.= s2 . f by A1
.= (Exec (i,s2)) . f by A50, SCMFSA_2:64 ;
:: thesis: verum
end;
suppose InsCode i = 3 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A51: ex da, db being Int-Location st i = SubFrom (da,db) by SCMFSA_2:32;
hence (Exec (i,s1)) . f = s1 . f by SCMFSA_2:65
.= s2 . f by A1
.= (Exec (i,s2)) . f by A51, SCMFSA_2:65 ;
:: thesis: verum
end;
suppose InsCode i = 4 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A52: ex da, db being Int-Location st i = MultBy (da,db) by SCMFSA_2:33;
hence (Exec (i,s1)) . f = s1 . f by SCMFSA_2:66
.= s2 . f by A1
.= (Exec (i,s2)) . f by A52, SCMFSA_2:66 ;
:: thesis: verum
end;
suppose InsCode i = 5 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A53: ex da, db being Int-Location st i = Divide (da,db) by SCMFSA_2:34;
hence (Exec (i,s1)) . f = s1 . f by SCMFSA_2:67
.= s2 . f by A1
.= (Exec (i,s2)) . f by A53, SCMFSA_2:67 ;
:: thesis: verum
end;
suppose InsCode i = 6 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A54: ex loc being Element of NAT st i = goto loc by SCMFSA_2:35;
hence (Exec (i,s1)) . f = s1 . f by SCMFSA_2:69
.= s2 . f by A1
.= (Exec (i,s2)) . f by A54, SCMFSA_2:69 ;
:: thesis: verum
end;
suppose InsCode i = 7 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A55: ex loc being Element of NAT ex da being Int-Location st i = da =0_goto loc by SCMFSA_2:36;
hence (Exec (i,s1)) . f = s1 . f by SCMFSA_2:70
.= s2 . f by A1
.= (Exec (i,s2)) . f by A55, SCMFSA_2:70 ;
:: thesis: verum
end;
suppose InsCode i = 8 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A56: ex loc being Element of NAT ex da being Int-Location st i = da >0_goto loc by SCMFSA_2:37;
hence (Exec (i,s1)) . f = s1 . f by SCMFSA_2:71
.= s2 . f by A1
.= (Exec (i,s2)) . f by A56, SCMFSA_2:71 ;
:: thesis: verum
end;
suppose InsCode i = 9 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A57: ex db, da being Int-Location ex g being FinSeq-Location st i = da := (g,db) by SCMFSA_2:38;
hence (Exec (i,s1)) . f = s1 . f by SCMFSA_2:72
.= s2 . f by A1
.= (Exec (i,s2)) . f by A57, SCMFSA_2:72 ;
:: thesis: verum
end;
suppose InsCode i = 10 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then consider db, da being Int-Location , g being FinSeq-Location such that
A58: i = (g,db) := da by SCMFSA_2:39;
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:73;
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:73;
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:73
.= s2 . f by A1
.= (Exec (i,s2)) . f by A58, A67, SCMFSA_2:73 ;
:: thesis: verum
end;
end;
end;
end;
suppose InsCode i = 11 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A68: ex da being Int-Location ex g being FinSeq-Location st i = da :=len g by SCMFSA_2:40;
hence (Exec (i,s1)) . f = s1 . f by SCMFSA_2:74
.= s2 . f by A1
.= (Exec (i,s2)) . f by A68, SCMFSA_2:74 ;
:: thesis: verum
end;
suppose InsCode i = 12 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then consider da being Int-Location , g being FinSeq-Location such that
A69: i = g :=<0,...,0> da by SCMFSA_2:41;
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:75;
ex m1 being Element of NAT st
( m1 = abs (s1 . da) & (Exec ((g :=<0,...,0> da),s1)) . g = m1 |-> 0 ) by SCMFSA_2:75;
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:75
.= s2 . f by A1
.= (Exec (i,s2)) . f by A69, A73, SCMFSA_2:75 ;
:: thesis: verum
end;
end;
end;
end;
end;
end;
hence S1[ 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, NAT_1:36;
suppose InsCode i = 0 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
then A74: i = halt SCM+FSA by SCMFSA_2:95;
hence (Exec (i,s1)) . (IC ) = IC s1 by EXTPRO_1:def 3
.= (Exec (i,s2)) . (IC ) by A47, A74, EXTPRO_1:def 3 ;
:: thesis: verum
end;
suppose InsCode i = 1 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
then A75: ex da, db being Int-Location st i = da := db by SCMFSA_2:30;
hence (Exec (i,s1)) . (IC ) = succ (IC s1) by SCMFSA_2:63
.= (Exec (i,s2)) . (IC ) by A47, A75, SCMFSA_2:63 ;
:: thesis: verum
end;
suppose InsCode i = 2 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
then A76: ex da, db being Int-Location st i = AddTo (da,db) by SCMFSA_2:31;
hence (Exec (i,s1)) . (IC ) = succ (IC s1) by SCMFSA_2:64
.= (Exec (i,s2)) . (IC ) by A47, A76, SCMFSA_2:64 ;
:: thesis: verum
end;
suppose InsCode i = 3 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
then A77: ex da, db being Int-Location st i = SubFrom (da,db) by SCMFSA_2:32;
hence (Exec (i,s1)) . (IC ) = succ (IC s1) by SCMFSA_2:65
.= (Exec (i,s2)) . (IC ) by A47, A77, SCMFSA_2:65 ;
:: thesis: verum
end;
suppose InsCode i = 4 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
then A78: ex da, db being Int-Location st i = MultBy (da,db) by SCMFSA_2:33;
hence (Exec (i,s1)) . (IC ) = succ (IC s1) by SCMFSA_2:66
.= (Exec (i,s2)) . (IC ) by A47, A78, SCMFSA_2:66 ;
:: thesis: verum
end;
suppose InsCode i = 5 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
then A79: ex da, db being Int-Location st i = Divide (da,db) by SCMFSA_2:34;
hence (Exec (i,s1)) . (IC ) = succ (IC s1) by SCMFSA_2:67
.= (Exec (i,s2)) . (IC ) by A47, A79, SCMFSA_2:67 ;
:: thesis: verum
end;
suppose InsCode i = 6 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
then consider loc being Element of NAT such that
A80: i = goto loc by SCMFSA_2:35;
thus (Exec (i,s1)) . (IC ) = loc by A80, SCMFSA_2:69
.= (Exec (i,s2)) . (IC ) by A80, SCMFSA_2:69 ; :: thesis: verum
end;
suppose InsCode i = 7 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
then consider loc being Element of NAT , da being Int-Location such that
A81: i = da =0_goto loc by SCMFSA_2:36;
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 ) = (Exec (i,s2)) . (IC )
hence (Exec (i,s1)) . (IC ) = loc by A81, SCMFSA_2:70
.= (Exec (i,s2)) . (IC ) by A81, A82, A83, SCMFSA_2:70 ;
:: thesis: verum
end;
suppose A84: s1 . da <> 0 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
hence (Exec (i,s1)) . (IC ) = succ (IC s1) by A81, SCMFSA_2:70
.= (Exec (i,s2)) . (IC ) by A47, A81, A82, A84, SCMFSA_2:70 ;
:: thesis: verum
end;
end;
end;
end;
suppose InsCode i = 8 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
then consider loc being Element of NAT , da being Int-Location such that
A85: i = da >0_goto loc by SCMFSA_2:37;
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 ) = (Exec (i,s2)) . (IC )
hence (Exec (i,s1)) . (IC ) = loc by A85, SCMFSA_2:71
.= (Exec (i,s2)) . (IC ) by A85, A86, A87, SCMFSA_2:71 ;
:: thesis: verum
end;
suppose A88: s1 . da <= 0 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
hence (Exec (i,s1)) . (IC ) = succ (IC s1) by A85, SCMFSA_2:71
.= (Exec (i,s2)) . (IC ) by A47, A85, A86, A88, SCMFSA_2:71 ;
:: thesis: verum
end;
end;
end;
end;
suppose InsCode i = 9 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
then A89: ex db, da being Int-Location ex g being FinSeq-Location st i = da := (g,db) by SCMFSA_2:38;
hence (Exec (i,s1)) . (IC ) = succ (IC s1) by SCMFSA_2:72
.= (Exec (i,s2)) . (IC ) by A47, A89, SCMFSA_2:72 ;
:: thesis: verum
end;
suppose InsCode i = 10 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
then A90: ex db, da being Int-Location ex g being FinSeq-Location st i = (g,db) := da by SCMFSA_2:39;
hence (Exec (i,s1)) . (IC ) = succ (IC s1) by SCMFSA_2:73
.= (Exec (i,s2)) . (IC ) by A47, A90, SCMFSA_2:73 ;
:: thesis: verum
end;
suppose InsCode i = 11 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
then A91: ex da being Int-Location ex g being FinSeq-Location st i = da :=len g by SCMFSA_2:40;
hence (Exec (i,s1)) . (IC ) = succ (IC s1) by SCMFSA_2:74
.= (Exec (i,s2)) . (IC ) by A47, A91, SCMFSA_2:74 ;
:: thesis: verum
end;
suppose InsCode i = 12 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
then A92: ex da being Int-Location ex g being FinSeq-Location st i = g :=<0,...,0> da by SCMFSA_2:41;
hence (Exec (i,s1)) . (IC ) = succ (IC s1) by SCMFSA_2:75
.= (Exec (i,s2)) . (IC ) by A47, A92, SCMFSA_2:75 ;
:: thesis: verum
end;
end;
end;
hence IC (Exec (i,s1)) = IC (Exec (i,s2)) ; :: thesis: verum