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 A2: 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)) ) )
A3: InsCode i <= 12 by SCMFSA_2:16;
A4: now :: thesis: for b being Int-Location st a <> b holds
(Exec (i,s1)) . b = (Exec (i,s2)) . b
let b be Int-Location; :: thesis: ( a <> b implies (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1 )
assume A5: a <> b ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
not not InsCode i = 0 & ... & not InsCode i = 12 by A3;
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 ) ;
suppose InsCode i = 0 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A6: i = halt SCM+FSA by SCMFSA_2:95;
hence (Exec (i,s1)) . b = s1 . b by EXTPRO_1:def 3
.= s2 . b by A1, A5
.= (Exec (i,s2)) . b by A6, 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
A7: i = da := db by SCMFSA_2:30;
A8: a <> db by A2, A7, SCMFSA7B:def 1;
hereby :: thesis: verum
per cases ( b = da or b <> da ) ;
suppose A9: b = da ; :: thesis: (Exec (i,s1)) . b = (Exec (i,s2)) . b
hence (Exec (i,s1)) . b = s1 . db by A7, SCMFSA_2:63
.= s2 . db by A1, A8
.= (Exec (i,s2)) . b by A7, A9, SCMFSA_2:63 ;
:: thesis: verum
end;
suppose A10: b <> da ; :: thesis: (Exec (i,s1)) . b = (Exec (i,s2)) . b
hence (Exec (i,s1)) . b = s1 . b by A7, SCMFSA_2:63
.= s2 . b by A1, A5
.= (Exec (i,s2)) . b by A7, A10, 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
A11: i = AddTo (da,db) by SCMFSA_2:31;
A12: a <> db by A2, A11, SCMFSA7B:def 1;
hereby :: thesis: verum
per cases ( b = da or b <> da ) ;
suppose A13: b = da ; :: thesis: (Exec (i,s1)) . b = (Exec (i,s2)) . b
hence (Exec (i,s1)) . b = (s1 . b) + (s1 . db) by A11, SCMFSA_2:64
.= (s2 . b) + (s1 . db) by A1, A5
.= (s2 . b) + (s2 . db) by A1, A12
.= (Exec (i,s2)) . b by A11, A13, SCMFSA_2:64 ;
:: thesis: verum
end;
suppose A14: b <> da ; :: thesis: (Exec (i,s1)) . b = (Exec (i,s2)) . b
hence (Exec (i,s1)) . b = s1 . b by A11, SCMFSA_2:64
.= s2 . b by A1, A5
.= (Exec (i,s2)) . b by A11, A14, 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
A15: i = SubFrom (da,db) by SCMFSA_2:32;
A16: a <> db by A2, A15, SCMFSA7B:def 1;
hereby :: thesis: verum
per cases ( b = da or b <> da ) ;
suppose A17: b = da ; :: thesis: (Exec (i,s1)) . b = (Exec (i,s2)) . b
hence (Exec (i,s1)) . b = (s1 . b) - (s1 . db) by A15, SCMFSA_2:65
.= (s2 . b) - (s1 . db) by A1, A5
.= (s2 . b) - (s2 . db) by A1, A16
.= (Exec (i,s2)) . b by A15, A17, SCMFSA_2:65 ;
:: thesis: verum
end;
suppose A18: b <> da ; :: thesis: (Exec (i,s1)) . b = (Exec (i,s2)) . b
hence (Exec (i,s1)) . b = s1 . b by A15, SCMFSA_2:65
.= s2 . b by A1, A5
.= (Exec (i,s2)) . b by A15, A18, 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
A19: i = MultBy (da,db) by SCMFSA_2:33;
A20: a <> db by A2, A19, SCMFSA7B:def 1;
hereby :: thesis: verum
per cases ( b = da or b <> da ) ;
suppose A21: b = da ; :: thesis: (Exec (i,s1)) . b = (Exec (i,s2)) . b
hence (Exec (i,s1)) . b = (s1 . b) * (s1 . db) by A19, SCMFSA_2:66
.= (s2 . b) * (s1 . db) by A1, A5
.= (s2 . b) * (s2 . db) by A1, A20
.= (Exec (i,s2)) . b by A19, A21, SCMFSA_2:66 ;
:: thesis: verum
end;
suppose A22: b <> da ; :: thesis: (Exec (i,s1)) . b = (Exec (i,s2)) . b
hence (Exec (i,s1)) . b = s1 . b by A19, SCMFSA_2:66
.= s2 . b by A1, A5
.= (Exec (i,s2)) . b by A19, A22, 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
A23: i = Divide (da,db) by SCMFSA_2:34;
A24: a <> db by A2, A23, SCMFSA7B:def 1;
A25: a <> da by A2, A23, SCMFSA7B:def 1;
hereby :: thesis: verum
per cases ( b = db or ( b = da & b <> db ) or ( b <> da & b <> db ) ) ;
suppose A26: b = db ; :: thesis: (Exec (i,s1)) . b = (Exec (i,s2)) . b
hence (Exec (i,s1)) . b = (s1 . da) mod (s1 . db) by A23, SCMFSA_2:67
.= (s2 . da) mod (s1 . db) by A1, A25
.= (s2 . da) mod (s2 . db) by A1, A24
.= (Exec (i,s2)) . b by A23, A26, SCMFSA_2:67 ;
:: thesis: verum
end;
suppose A27: ( b = da & b <> db ) ; :: thesis: (Exec (i,s1)) . b = (Exec (i,s2)) . b
hence (Exec (i,s1)) . b = (s1 . da) div (s1 . db) by A23, SCMFSA_2:67
.= (s1 . da) div (s2 . db) by A1, A24
.= (s2 . da) div (s2 . db) by A1, A25
.= (Exec (i,s2)) . b by A23, A27, SCMFSA_2:67 ;
:: thesis: verum
end;
suppose A28: ( b <> da & b <> db ) ; :: thesis: (Exec (i,s1)) . b = (Exec (i,s2)) . b
hence (Exec (i,s1)) . b = s1 . b by A23, SCMFSA_2:67
.= s2 . b by A1, A5
.= (Exec (i,s2)) . b by A23, A28, SCMFSA_2:67 ;
:: thesis: verum
end;
end;
end;
end;
suppose InsCode i = 6 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A29: ex loc being Nat st i = goto loc by SCMFSA_2:35;
hence (Exec (i,s1)) . b = s1 . b by SCMFSA_2:69
.= s2 . b by A1, A5
.= (Exec (i,s2)) . b by A29, SCMFSA_2:69 ;
:: thesis: verum
end;
suppose InsCode i = 7 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A30: ex loc being 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, A5
.= (Exec (i,s2)) . b by A30, SCMFSA_2:70 ;
:: thesis: verum
end;
suppose InsCode i = 8 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A31: ex loc being 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, A5
.= (Exec (i,s2)) . b by A31, 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
A32: i = da := (g,db) by SCMFSA_2:38;
A33: a <> db by A2, A32, SCMFSA7B:def 1;
hereby :: thesis: verum
per cases ( b = da or b <> da ) ;
suppose A34: b = da ; :: thesis: (Exec (i,s1)) . b = (Exec (i,s2)) . b
then consider m2 being Nat such that
A35: m2 = |.(s2 . db).| and
A36: (Exec ((da := (g,db)),s2)) . b = (s2 . g) /. m2 by SCMFSA_2:72;
consider m1 being Nat such that
A37: m1 = |.(s1 . db).| and
A38: (Exec ((da := (g,db)),s1)) . b = (s1 . g) /. m1 by A34, SCMFSA_2:72;
m1 = m2 by A1, A33, A37, A35;
hence (Exec (i,s1)) . b = (Exec (i,s2)) . b by A1, A32, A38, A36; :: thesis: verum
end;
suppose A39: b <> da ; :: thesis: (Exec (i,s1)) . b = (Exec (i,s2)) . b
hence (Exec (i,s1)) . b = s1 . b by A32, SCMFSA_2:72
.= s2 . b by A1, A5
.= (Exec (i,s2)) . b by A32, A39, SCMFSA_2:72 ;
:: thesis: verum
end;
end;
end;
end;
suppose InsCode i = 10 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A40: 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, A5
.= (Exec (i,s2)) . b by A40, 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
A41: i = da :=len g by SCMFSA_2:40;
hereby :: thesis: verum
per cases ( b = da or b <> da ) ;
suppose A42: b = da ; :: thesis: (Exec (i,s1)) . b = (Exec (i,s2)) . b
hence (Exec (i,s1)) . b = len (s1 . g) by A41, SCMFSA_2:74
.= len (s2 . g) by A1
.= (Exec (i,s2)) . b by A41, A42, SCMFSA_2:74 ;
:: thesis: verum
end;
suppose A43: b <> da ; :: thesis: (Exec (i,s1)) . b = (Exec (i,s2)) . b
hence (Exec (i,s1)) . b = s1 . b by A41, SCMFSA_2:74
.= s2 . b by A1, A5
.= (Exec (i,s2)) . b by A41, A43, SCMFSA_2:74 ;
:: thesis: verum
end;
end;
end;
end;
suppose InsCode i = 12 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A44: 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, A5
.= (Exec (i,s2)) . b by A44, SCMFSA_2:75 ;
:: thesis: verum
end;
end;
end;
assume A45: 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 :: thesis: for f being FinSeq-Location holds (Exec (i,s1)) . f = (Exec (i,s2)) . f
let f be FinSeq-Location ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
not not InsCode i = 0 & ... & not InsCode i = 12 by A3;
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 ) ;
suppose InsCode i = 0 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A46: 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 A46, EXTPRO_1:def 3 ;
:: thesis: verum
end;
suppose InsCode i = 1 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A47: 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 A47, SCMFSA_2:63 ;
:: thesis: verum
end;
suppose InsCode i = 2 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A48: 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 A48, SCMFSA_2:64 ;
:: thesis: verum
end;
suppose InsCode i = 3 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A49: 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 A49, SCMFSA_2:65 ;
:: thesis: verum
end;
suppose InsCode i = 4 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A50: 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 A50, SCMFSA_2:66 ;
:: thesis: verum
end;
suppose InsCode i = 5 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A51: 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 A51, SCMFSA_2:67 ;
:: thesis: verum
end;
suppose InsCode i = 6 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A52: ex loc being 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 A52, SCMFSA_2:69 ;
:: thesis: verum
end;
suppose InsCode i = 7 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A53: ex loc being 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 A53, SCMFSA_2:70 ;
:: thesis: verum
end;
suppose InsCode i = 8 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A54: ex loc being 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 A54, SCMFSA_2:71 ;
:: thesis: verum
end;
suppose InsCode i = 9 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A55: 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 A55, 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
A56: i = (g,db) := da by SCMFSA_2:39;
A57: a <> db by A2, A56, SCMFSA7B:def 1;
A58: a <> da by A2, A56, SCMFSA7B:def 1;
hereby :: thesis: verum
per cases ( f = g or f <> g ) ;
suppose A59: f = g ; :: thesis: (Exec (i,s1)) . f = (Exec (i,s2)) . f
A60: s1 . da = s2 . da by A1, A58;
consider m2 being Nat such that
A61: m2 = |.(s2 . db).| and
A62: (Exec (((g,db) := da),s2)) . g = (s2 . g) +* (m2,(s2 . da)) by SCMFSA_2:73;
consider m1 being Nat such that
A63: m1 = |.(s1 . db).| and
A64: (Exec (((g,db) := da),s1)) . g = (s1 . g) +* (m1,(s1 . da)) by SCMFSA_2:73;
m1 = m2 by A1, A57, A63, A61;
hence (Exec (i,s1)) . f = (Exec (i,s2)) . f by A1, A56, A59, A64, A62, A60; :: thesis: verum
end;
suppose A65: f <> g ; :: thesis: (Exec (i,s1)) . f = (Exec (i,s2)) . f
hence (Exec (i,s1)) . f = s1 . f by A56, SCMFSA_2:73
.= s2 . f by A1
.= (Exec (i,s2)) . f by A56, A65, SCMFSA_2:73 ;
:: thesis: verum
end;
end;
end;
end;
suppose InsCode i = 11 ; :: thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A66: 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 A66, 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
A67: i = g :=<0,...,0> da by SCMFSA_2:41;
A68: a <> da by A2, A67, SCMFSA7B:def 1;
hereby :: thesis: verum
per cases ( f = g or f <> g ) ;
suppose A69: f = g ; :: thesis: (Exec (i,s1)) . f = (Exec (i,s2)) . f
A70: ex m2 being Nat st
( m2 = |.(s2 . da).| & (Exec ((g :=<0,...,0> da),s2)) . g = m2 |-> 0 ) by SCMFSA_2:75;
ex m1 being Nat st
( m1 = |.(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, A67, A68, A69, A70; :: thesis: verum
end;
suppose A71: f <> g ; :: thesis: (Exec (i,s1)) . f = (Exec (i,s2)) . f
hence (Exec (i,s1)) . f = s1 . f by A67, SCMFSA_2:75
.= s2 . f by A1
.= (Exec (i,s2)) . f by A67, A71, SCMFSA_2:75 ;
:: thesis: verum
end;
end;
end;
end;
end;
end;
hence S1[ Exec (i,s1), Exec (i,s2)] by A4; :: thesis: IC (Exec (i,s1)) = IC (Exec (i,s2))
now :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
not not InsCode i = 0 & ... & not InsCode i = 12 by A3;
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 ) ;
suppose InsCode i = 0 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
then A72: 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 A45, A72, EXTPRO_1:def 3 ;
:: thesis: verum
end;
suppose InsCode i = 1 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
then A73: ex da, db being Int-Location st i = da := db by SCMFSA_2:30;
hence (Exec (i,s1)) . (IC ) = (IC s1) + 1 by SCMFSA_2:63
.= (Exec (i,s2)) . (IC ) by A45, A73, SCMFSA_2:63 ;
:: thesis: verum
end;
suppose InsCode i = 2 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
then A74: ex da, db being Int-Location st i = AddTo (da,db) by SCMFSA_2:31;
hence (Exec (i,s1)) . (IC ) = (IC s1) + 1 by SCMFSA_2:64
.= (Exec (i,s2)) . (IC ) by A45, A74, SCMFSA_2:64 ;
:: thesis: verum
end;
suppose InsCode i = 3 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
then A75: ex da, db being Int-Location st i = SubFrom (da,db) by SCMFSA_2:32;
hence (Exec (i,s1)) . (IC ) = (IC s1) + 1 by SCMFSA_2:65
.= (Exec (i,s2)) . (IC ) by A45, A75, SCMFSA_2:65 ;
:: thesis: verum
end;
suppose InsCode i = 4 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
then A76: ex da, db being Int-Location st i = MultBy (da,db) by SCMFSA_2:33;
hence (Exec (i,s1)) . (IC ) = (IC s1) + 1 by SCMFSA_2:66
.= (Exec (i,s2)) . (IC ) by A45, A76, SCMFSA_2:66 ;
:: thesis: verum
end;
suppose InsCode i = 5 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
then A77: ex da, db being Int-Location st i = Divide (da,db) by SCMFSA_2:34;
hence (Exec (i,s1)) . (IC ) = (IC s1) + 1 by SCMFSA_2:67
.= (Exec (i,s2)) . (IC ) by A45, A77, SCMFSA_2:67 ;
:: thesis: verum
end;
suppose InsCode i = 6 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
then consider loc being Nat such that
A78: i = goto loc by SCMFSA_2:35;
thus (Exec (i,s1)) . (IC ) = loc by A78, SCMFSA_2:69
.= (Exec (i,s2)) . (IC ) by A78, SCMFSA_2:69 ; :: thesis: verum
end;
suppose InsCode i = 7 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
then consider loc being Nat, da being Int-Location such that
A79: i = da =0_goto loc by SCMFSA_2:36;
a <> da by A2, A79, SCMFSA7B:def 1;
then A80: s1 . da = s2 . da by A1;
hereby :: thesis: verum
per cases ( s1 . da = 0 or s1 . da <> 0 ) ;
suppose A81: s1 . da = 0 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
hence (Exec (i,s1)) . (IC ) = loc by A79, SCMFSA_2:70
.= (Exec (i,s2)) . (IC ) by A79, A80, A81, SCMFSA_2:70 ;
:: thesis: verum
end;
suppose A82: s1 . da <> 0 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
hence (Exec (i,s1)) . (IC ) = (IC s1) + 1 by A79, SCMFSA_2:70
.= (Exec (i,s2)) . (IC ) by A45, A79, A80, A82, 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 Nat, da being Int-Location such that
A83: i = da >0_goto loc by SCMFSA_2:37;
a <> da by A2, A83, SCMFSA7B:def 1;
then A84: s1 . da = s2 . da by A1;
hereby :: thesis: verum
per cases ( s1 . da > 0 or s1 . da <= 0 ) ;
suppose A85: s1 . da > 0 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
hence (Exec (i,s1)) . (IC ) = loc by A83, SCMFSA_2:71
.= (Exec (i,s2)) . (IC ) by A83, A84, A85, SCMFSA_2:71 ;
:: thesis: verum
end;
suppose A86: s1 . da <= 0 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
hence (Exec (i,s1)) . (IC ) = (IC s1) + 1 by A83, SCMFSA_2:71
.= (Exec (i,s2)) . (IC ) by A45, A83, A84, A86, SCMFSA_2:71 ;
:: thesis: verum
end;
end;
end;
end;
suppose InsCode i = 9 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
then A87: 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 ) = (IC s1) + 1 by SCMFSA_2:72
.= (Exec (i,s2)) . (IC ) by A45, A87, SCMFSA_2:72 ;
:: thesis: verum
end;
suppose InsCode i = 10 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
then A88: 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 ) = (IC s1) + 1 by SCMFSA_2:73
.= (Exec (i,s2)) . (IC ) by A45, A88, SCMFSA_2:73 ;
:: thesis: verum
end;
suppose InsCode i = 11 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
then A89: ex da being Int-Location ex g being FinSeq-Location st i = da :=len g by SCMFSA_2:40;
hence (Exec (i,s1)) . (IC ) = (IC s1) + 1 by SCMFSA_2:74
.= (Exec (i,s2)) . (IC ) by A45, A89, SCMFSA_2:74 ;
:: thesis: verum
end;
suppose InsCode i = 12 ; :: thesis: (Exec (i,s1)) . (IC ) = (Exec (i,s2)) . (IC )
then A90: 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 ) = (IC s1) + 1 by SCMFSA_2:75
.= (Exec (i,s2)) . (IC ) by A45, A90, SCMFSA_2:75 ;
:: thesis: verum
end;
end;
end;
hence IC (Exec (i,s1)) = IC (Exec (i,s2)) ; :: thesis: verum