let i be Instruction of SCM+FSA ; :: thesis: for s1, s2 being State of SCM+FSA st s1,s2 equal_outside NAT holds
Exec i,s1, Exec i,s2 equal_outside NAT
let s1, s2 be State of SCM+FSA ; :: thesis: ( s1,s2 equal_outside NAT implies Exec i,s1, Exec i,s2 equal_outside NAT )
assume A1: s1,s2 equal_outside NAT ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT
A2: InsCode i <= 11 + 1 by SCMFSA_2:35;
A3: ( not InsCode i <= 10 + 1 or InsCode i <= 10 or InsCode i = 11 ) by NAT_1:8;
A4: ( not InsCode i <= 9 + 1 or InsCode i <= 8 + 1 or InsCode i = 10 ) by NAT_1:8;
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 A2, A3, A4, NAT_1:8, NAT_1:33;
suppose InsCode i = 0 ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT
then i = halt SCM+FSA by SCMFSA_2:122;
then ( Exec i,s1 = s1 & Exec i,s2 = s2 ) by AMI_1:def 8;
hence Exec i,s1, Exec i,s2 equal_outside NAT by A1; :: thesis: verum
end;
suppose InsCode i = 1 ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT
then consider da, db being Int-Location such that
A5: i = da := db by SCMFSA_2:54;
A6: now
let c be Int-Location ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
per cases ( c = da or c <> da ) ;
suppose A7: c = da ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
hence (Exec i,s1) . c = s1 . db by A5, SCMFSA_2:89
.= s2 . db by A1, Th30
.= (Exec i,s2) . c by A5, A7, SCMFSA_2:89 ;
:: thesis: verum
end;
suppose A8: c <> da ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
hence (Exec i,s1) . c = s1 . c by A5, SCMFSA_2:89
.= s2 . c by A1, Th30
.= (Exec i,s2) . c by A5, A8, SCMFSA_2:89 ;
:: thesis: verum
end;
end;
end;
A9: now
let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec i,s2) . f
thus (Exec i,s1) . f = s1 . f by A5, SCMFSA_2:89
.= s2 . f by A1, Th31
.= (Exec i,s2) . f by A5, SCMFSA_2:89 ; :: thesis: verum
end;
IC (Exec i,s1) = Next (IC s1) by A5, SCMFSA_2:89
.= Next (IC s2) by A1, AMI_1:121
.= IC (Exec i,s2) by A5, SCMFSA_2:89 ;
hence Exec i,s1, Exec i,s2 equal_outside NAT by A6, A9, Th28; :: thesis: verum
end;
suppose InsCode i = 2 ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT
then consider da, db being Int-Location such that
A10: i = AddTo da,db by SCMFSA_2:55;
A11: now
let c be Int-Location ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
per cases ( c = da or c <> da ) ;
suppose A12: c = da ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
( s1 . da = s2 . da & s1 . db = s2 . db ) by A1, Th30;
hence (Exec i,s1) . c = (s2 . da) + (s2 . db) by A10, A12, SCMFSA_2:90
.= (Exec i,s2) . c by A10, A12, SCMFSA_2:90 ;
:: thesis: verum
end;
suppose A13: c <> da ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
hence (Exec i,s1) . c = s1 . c by A10, SCMFSA_2:90
.= s2 . c by A1, Th30
.= (Exec i,s2) . c by A10, A13, SCMFSA_2:90 ;
:: thesis: verum
end;
end;
end;
A14: now
let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec i,s2) . f
thus (Exec i,s1) . f = s1 . f by A10, SCMFSA_2:90
.= s2 . f by A1, Th31
.= (Exec i,s2) . f by A10, SCMFSA_2:90 ; :: thesis: verum
end;
IC (Exec i,s1) = Next (IC s1) by A10, SCMFSA_2:90
.= Next (IC s2) by A1, AMI_1:121
.= IC (Exec i,s2) by A10, SCMFSA_2:90 ;
hence Exec i,s1, Exec i,s2 equal_outside NAT by A11, A14, Th28; :: thesis: verum
end;
suppose InsCode i = 3 ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT
then consider da, db being Int-Location such that
A15: i = SubFrom da,db by SCMFSA_2:56;
A16: now
let c be Int-Location ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
per cases ( c = da or c <> da ) ;
suppose A17: c = da ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
( s1 . da = s2 . da & s1 . db = s2 . db ) by A1, Th30;
hence (Exec i,s1) . c = (s2 . da) - (s2 . db) by A15, A17, SCMFSA_2:91
.= (Exec i,s2) . c by A15, A17, SCMFSA_2:91 ;
:: thesis: verum
end;
suppose A18: c <> da ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
hence (Exec i,s1) . c = s1 . c by A15, SCMFSA_2:91
.= s2 . c by A1, Th30
.= (Exec i,s2) . c by A15, A18, SCMFSA_2:91 ;
:: thesis: verum
end;
end;
end;
A19: now
let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec i,s2) . f
thus (Exec i,s1) . f = s1 . f by A15, SCMFSA_2:91
.= s2 . f by A1, Th31
.= (Exec i,s2) . f by A15, SCMFSA_2:91 ; :: thesis: verum
end;
IC (Exec i,s1) = Next (IC s1) by A15, SCMFSA_2:91
.= Next (IC s2) by A1, AMI_1:121
.= IC (Exec i,s2) by A15, SCMFSA_2:91 ;
hence Exec i,s1, Exec i,s2 equal_outside NAT by A16, A19, Th28; :: thesis: verum
end;
suppose InsCode i = 4 ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT
then consider da, db being Int-Location such that
A20: i = MultBy da,db by SCMFSA_2:57;
A21: now
let c be Int-Location ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
per cases ( c = da or c <> da ) ;
suppose A22: c = da ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
( s1 . da = s2 . da & s1 . db = s2 . db ) by A1, Th30;
hence (Exec i,s1) . c = (s2 . da) * (s2 . db) by A20, A22, SCMFSA_2:92
.= (Exec i,s2) . c by A20, A22, SCMFSA_2:92 ;
:: thesis: verum
end;
suppose A23: c <> da ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
hence (Exec i,s1) . c = s1 . c by A20, SCMFSA_2:92
.= s2 . c by A1, Th30
.= (Exec i,s2) . c by A20, A23, SCMFSA_2:92 ;
:: thesis: verum
end;
end;
end;
A24: now
let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec i,s2) . f
thus (Exec i,s1) . f = s1 . f by A20, SCMFSA_2:92
.= s2 . f by A1, Th31
.= (Exec i,s2) . f by A20, SCMFSA_2:92 ; :: thesis: verum
end;
IC (Exec i,s1) = Next (IC s1) by A20, SCMFSA_2:92
.= Next (IC s2) by A1, AMI_1:121
.= IC (Exec i,s2) by A20, SCMFSA_2:92 ;
hence Exec i,s1, Exec i,s2 equal_outside NAT by A21, A24, Th28; :: thesis: verum
end;
suppose InsCode i = 5 ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT
then consider da, db being Int-Location such that
A25: i = Divide da,db by SCMFSA_2:58;
A26: now
let c be Int-Location ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
per cases ( c = db or ( c = da & c <> db ) or ( c <> da & c <> db ) ) ;
suppose A27: c = db ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
( s1 . da = s2 . da & s1 . db = s2 . db ) by A1, Th30;
hence (Exec i,s1) . c = (s2 . da) mod (s2 . db) by A25, A27, SCMFSA_2:93
.= (Exec i,s2) . c by A25, A27, SCMFSA_2:93 ;
:: thesis: verum
end;
suppose A28: ( c = da & c <> db ) ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
( s1 . da = s2 . da & s1 . db = s2 . db ) by A1, Th30;
hence (Exec i,s1) . c = (s2 . da) div (s2 . db) by A25, A28, SCMFSA_2:93
.= (Exec i,s2) . c by A25, A28, SCMFSA_2:93 ;
:: thesis: verum
end;
suppose A29: ( c <> da & c <> db ) ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
hence (Exec i,s1) . c = s1 . c by A25, SCMFSA_2:93
.= s2 . c by A1, Th30
.= (Exec i,s2) . c by A25, A29, SCMFSA_2:93 ;
:: thesis: verum
end;
end;
end;
A30: now
let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec i,s2) . f
thus (Exec i,s1) . f = s1 . f by A25, SCMFSA_2:93
.= s2 . f by A1, Th31
.= (Exec i,s2) . f by A25, SCMFSA_2:93 ; :: thesis: verum
end;
IC (Exec i,s1) = Next (IC s1) by A25, SCMFSA_2:93
.= Next (IC s2) by A1, AMI_1:121
.= IC (Exec i,s2) by A25, SCMFSA_2:93 ;
hence Exec i,s1, Exec i,s2 equal_outside NAT by A26, A30, Th28; :: thesis: verum
end;
suppose InsCode i = 6 ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT
then consider loc being Instruction-Location of SCM+FSA such that
A31: i = goto loc by SCMFSA_2:59;
A32: now
let c be Int-Location ; :: thesis: (Exec i,s1) . c = (Exec i,s2) . c
thus (Exec i,s1) . c = s1 . c by A31, SCMFSA_2:95
.= s2 . c by A1, Th30
.= (Exec i,s2) . c by A31, SCMFSA_2:95 ; :: thesis: verum
end;
A33: now
let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec i,s2) . f
thus (Exec i,s1) . f = s1 . f by A31, SCMFSA_2:95
.= s2 . f by A1, Th31
.= (Exec i,s2) . f by A31, SCMFSA_2:95 ; :: thesis: verum
end;
IC (Exec i,s1) = loc by A31, SCMFSA_2:95
.= IC (Exec i,s2) by A31, SCMFSA_2:95 ;
hence Exec i,s1, Exec i,s2 equal_outside NAT by A32, A33, Th28; :: thesis: verum
end;
suppose InsCode i = 7 ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT
then consider loc being Instruction-Location of SCM+FSA , da being Int-Location such that
A34: i = da =0_goto loc by SCMFSA_2:60;
A35: now
let c be Int-Location ; :: thesis: (Exec i,s1) . c = (Exec i,s2) . c
thus (Exec i,s1) . c = s1 . c by A34, SCMFSA_2:96
.= s2 . c by A1, Th30
.= (Exec i,s2) . c by A34, SCMFSA_2:96 ; :: thesis: verum
end;
A36: now
let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec i,s2) . f
thus (Exec i,s1) . f = s1 . f by A34, SCMFSA_2:96
.= s2 . f by A1, Th31
.= (Exec i,s2) . f by A34, SCMFSA_2:96 ; :: thesis: verum
end;
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 A34, A37, SCMFSA_2:96
.= IC (Exec i,s2) by A34, 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) = Next (IC s1) by A34, A39, SCMFSA_2:96
.= Next (IC s2) by A1, AMI_1:121
.= IC (Exec i,s2) by A34, A40, SCMFSA_2:96 ; :: thesis: verum
end;
end;
end;
hence Exec i,s1, Exec i,s2 equal_outside NAT by A35, A36, Th28; :: thesis: verum
end;
suppose InsCode i = 8 ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT
then consider loc being Instruction-Location of SCM+FSA , da being Int-Location such that
A41: i = da >0_goto loc by SCMFSA_2:61;
A42: now
let c be Int-Location ; :: thesis: (Exec i,s1) . c = (Exec i,s2) . c
thus (Exec i,s1) . c = s1 . c by A41, SCMFSA_2:97
.= s2 . c by A1, Th30
.= (Exec i,s2) . c by A41, SCMFSA_2:97 ; :: thesis: verum
end;
A43: now
let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec i,s2) . f
thus (Exec i,s1) . f = s1 . f by A41, SCMFSA_2:97
.= s2 . f by A1, Th31
.= (Exec i,s2) . f by A41, SCMFSA_2:97 ; :: thesis: verum
end;
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 A41, A44, SCMFSA_2:97
.= IC (Exec i,s2) by A41, 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) = Next (IC s1) by A41, A46, SCMFSA_2:97
.= Next (IC s2) by A1, AMI_1:121
.= IC (Exec i,s2) by A41, A47, SCMFSA_2:97 ; :: thesis: verum
end;
end;
end;
hence Exec i,s1, Exec i,s2 equal_outside NAT by A42, A43, Th28; :: thesis: verum
end;
suppose InsCode i = 9 ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT
then consider db, da being Int-Location , f being FinSeq-Location such that
A48: i = da := f,db by SCMFSA_2:62;
A49: now
let c be Int-Location ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
per cases ( c = da or c <> da ) ;
suppose A50: c = da ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
then consider m being Element of NAT such that
A51: m = abs (s1 . db) and
A52: (Exec (da := f,db),s1) . c = (s1 . f) /. m by SCMFSA_2:98;
consider n being Element of NAT such that
A53: n = abs (s2 . db) and
A54: (Exec (da := f,db),s2) . c = (s2 . f) /. n by A50, SCMFSA_2:98;
( m = n & s1 . f = s2 . f ) by A1, A51, A53, Th30, Th31;
hence (Exec i,s1) . c = (Exec i,s2) . c by A48, A52, A54; :: thesis: verum
end;
suppose A55: c <> da ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
hence (Exec i,s1) . c = s1 . c by A48, SCMFSA_2:98
.= s2 . c by A1, Th30
.= (Exec i,s2) . c by A48, A55, SCMFSA_2:98 ;
:: thesis: verum
end;
end;
end;
A56: now
let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec i,s2) . f
thus (Exec i,s1) . f = s1 . f by A48, SCMFSA_2:98
.= s2 . f by A1, Th31
.= (Exec i,s2) . f by A48, SCMFSA_2:98 ; :: thesis: verum
end;
IC (Exec i,s1) = Next (IC s1) by A48, SCMFSA_2:98
.= Next (IC s2) by A1, AMI_1:121
.= IC (Exec i,s2) by A48, SCMFSA_2:98 ;
hence Exec i,s1, Exec i,s2 equal_outside NAT by A49, A56, Th28; :: thesis: verum
end;
suppose InsCode i = 10 ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT
then consider db, da being Int-Location , f being FinSeq-Location such that
A57: i = f,db := da by SCMFSA_2:63;
A58: now
let c be Int-Location ; :: thesis: (Exec i,s1) . c = (Exec i,s2) . c
thus (Exec i,s1) . c = s1 . c by A57, SCMFSA_2:99
.= s2 . c by A1, Th30
.= (Exec i,s2) . c by A57, SCMFSA_2:99 ; :: thesis: verum
end;
A59: now
let g be FinSeq-Location ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
per cases ( g = f or g <> f ) ;
suppose A60: g = f ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
consider m being Element of NAT such that
A61: m = abs (s1 . db) and
A62: (Exec (f,db := da),s1) . f = (s1 . f) +* m,(s1 . da) by SCMFSA_2:99;
consider n being Element of NAT such that
A63: n = abs (s2 . db) and
A64: (Exec (f,db := da),s2) . f = (s2 . f) +* n,(s2 . da) by SCMFSA_2:99;
( m = n & s1 . da = s2 . da & s1 . f = s2 . f ) by A1, A61, A63, Th30, Th31;
hence (Exec i,s1) . g = (Exec i,s2) . g by A57, A60, A62, A64; :: thesis: verum
end;
suppose A65: g <> f ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
hence (Exec i,s1) . g = s1 . g by A57, SCMFSA_2:99
.= s2 . g by A1, Th31
.= (Exec i,s2) . g by A57, A65, SCMFSA_2:99 ;
:: thesis: verum
end;
end;
end;
IC (Exec i,s1) = Next (IC s1) by A57, SCMFSA_2:99
.= Next (IC s2) by A1, AMI_1:121
.= IC (Exec i,s2) by A57, SCMFSA_2:99 ;
hence Exec i,s1, Exec i,s2 equal_outside NAT by A58, A59, Th28; :: thesis: verum
end;
suppose InsCode i = 11 ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT
then consider da being Int-Location , f being FinSeq-Location such that
A66: i = da :=len f by SCMFSA_2:64;
A67: now
let c be Int-Location ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
per cases ( c = da or c <> da ) ;
suppose A68: c = da ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
hence (Exec i,s1) . c = len (s1 . f) by A66, SCMFSA_2:100
.= len (s2 . f) by A1, Th31
.= (Exec i,s2) . c by A66, A68, SCMFSA_2:100 ;
:: thesis: verum
end;
suppose A69: c <> da ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
hence (Exec i,s1) . c = s1 . c by A66, SCMFSA_2:100
.= s2 . c by A1, Th30
.= (Exec i,s2) . c by A66, A69, SCMFSA_2:100 ;
:: thesis: verum
end;
end;
end;
A70: now
let f be FinSeq-Location ; :: thesis: (Exec i,s1) . f = (Exec i,s2) . f
thus (Exec i,s1) . f = s1 . f by A66, SCMFSA_2:100
.= s2 . f by A1, Th31
.= (Exec i,s2) . f by A66, SCMFSA_2:100 ; :: thesis: verum
end;
IC (Exec i,s1) = Next (IC s1) by A66, SCMFSA_2:100
.= Next (IC s2) by A1, AMI_1:121
.= IC (Exec i,s2) by A66, SCMFSA_2:100 ;
hence Exec i,s1, Exec i,s2 equal_outside NAT by A67, A70, Th28; :: thesis: verum
end;
suppose InsCode i = 12 ; :: thesis: Exec i,s1, Exec i,s2 equal_outside NAT
then consider da being Int-Location , f being FinSeq-Location such that
A71: i = f :=<0,...,0> da by SCMFSA_2:65;
A72: now
let c be Int-Location ; :: thesis: (Exec i,s1) . c = (Exec i,s2) . c
thus (Exec i,s1) . c = s1 . c by A71, SCMFSA_2:101
.= s2 . c by A1, Th30
.= (Exec i,s2) . c by A71, SCMFSA_2:101 ; :: thesis: verum
end;
A73: now
let g be FinSeq-Location ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
per cases ( g = f or g <> f ) ;
suppose A74: g = f ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
consider m being Element of NAT such that
A75: m = abs (s1 . da) and
A76: (Exec (f :=<0,...,0> da),s1) . f = m |-> 0 by SCMFSA_2:101;
consider n being Element of NAT such that
A77: n = abs (s2 . da) and
A78: (Exec (f :=<0,...,0> da),s2) . f = n |-> 0 by SCMFSA_2:101;
thus (Exec i,s1) . g = (Exec i,s2) . g by A1, A71, A74, A75, A76, A77, A78, Th30; :: thesis: verum
end;
suppose A79: g <> f ; :: thesis: (Exec i,s1) . b1 = (Exec i,s2) . b1
hence (Exec i,s1) . g = s1 . g by A71, SCMFSA_2:101
.= s2 . g by A1, Th31
.= (Exec i,s2) . g by A71, A79, SCMFSA_2:101 ;
:: thesis: verum
end;
end;
end;
IC (Exec i,s1) = Next (IC s1) by A71, SCMFSA_2:101
.= Next (IC s2) by A1, AMI_1:121
.= IC (Exec i,s2) by A71, SCMFSA_2:101 ;
hence Exec i,s1, Exec i,s2 equal_outside NAT by A72, A73, Th28; :: thesis: verum
end;
end;