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 NPP s1 = NPP s2 or NPP (Exec (I,s1)) = NPP (Exec (I,s2)) )
assume A1: NPP s1 = NPP s2 ; :: thesis: NPP (Exec (I,s1)) = NPP (Exec (I,s2))
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 or InsCode I = 13 ) by SCMFSA_2:35, NAT_1:38;
suppose InsCode I = 0 ; :: thesis: NPP (Exec (I,s1)) = NPP (Exec (I,s2))
then A5: I = halt SCM+FSA by SCMFSA_2:122;
then Exec (I,s1) = s1 by EXTPRO_1:def 3;
hence NPP (Exec (I,s1)) = NPP (Exec (I,s2)) by A1, A5, EXTPRO_1:def 3; :: thesis: verum
end;
suppose InsCode I = 1 ; :: thesis: NPP (Exec (I,s1)) = NPP (Exec (I,s2))
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)) . b1 = (Exec (I,s2)) . b1
per cases ( c = da or c <> da ) ;
suppose A8: c = da ; :: thesis: (Exec (I,s1)) . b1 = (Exec (I,s2)) . b1
hence (Exec (I,s1)) . c = s1 . db by A6, SCMFSA_2:89
.= s2 . db by A1, Th92
.= (Exec (I,s2)) . c by A6, A8, SCMFSA_2:89 ;
:: thesis: verum
end;
suppose A9: c <> da ; :: thesis: (Exec (I,s1)) . b1 = (Exec (I,s2)) . b1
hence (Exec (I,s1)) . c = s1 . c by A6, SCMFSA_2:89
.= s2 . c by A1, Th92
.= (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, Th93
.= (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:230
.= IC (Exec (I,s2)) by A6, SCMFSA_2:89 ;
hence NPP (Exec (I,s1)) = NPP (Exec (I,s2)) by A7, A10, Th91; :: thesis: verum
end;
suppose InsCode I = 2 ; :: thesis: NPP (Exec (I,s1)) = NPP (Exec (I,s2))
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)) . b1 = (Exec (I,s2)) . b1
per cases ( c = da or c <> da ) ;
suppose A13: c = da ; :: thesis: (Exec (I,s1)) . b1 = (Exec (I,s2)) . b1
( s1 . da = s2 . da & s1 . db = s2 . db ) by A1, Th92;
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)) . b1 = (Exec (I,s2)) . b1
hence (Exec (I,s1)) . c = s1 . c by A11, SCMFSA_2:90
.= s2 . c by A1, Th92
.= (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, Th93
.= (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:230
.= IC (Exec (I,s2)) by A11, SCMFSA_2:90 ;
hence NPP (Exec (I,s1)) = NPP (Exec (I,s2)) by A12, A15, Th91; :: thesis: verum
end;
suppose InsCode I = 3 ; :: thesis: NPP (Exec (I,s1)) = NPP (Exec (I,s2))
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)) . b1 = (Exec (I,s2)) . b1
per cases ( c = da or c <> da ) ;
suppose A18: c = da ; :: thesis: (Exec (I,s1)) . b1 = (Exec (I,s2)) . b1
( s1 . da = s2 . da & s1 . db = s2 . db ) by A1, Th92;
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)) . b1 = (Exec (I,s2)) . b1
hence (Exec (I,s1)) . c = s1 . c by A16, SCMFSA_2:91
.= s2 . c by A1, Th92
.= (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, Th93
.= (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:230
.= IC (Exec (I,s2)) by A16, SCMFSA_2:91 ;
hence NPP (Exec (I,s1)) = NPP (Exec (I,s2)) by A17, A20, Th91; :: thesis: verum
end;
suppose InsCode I = 4 ; :: thesis: NPP (Exec (I,s1)) = NPP (Exec (I,s2))
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)) . b1 = (Exec (I,s2)) . b1
per cases ( c = da or c <> da ) ;
suppose A23: c = da ; :: thesis: (Exec (I,s1)) . b1 = (Exec (I,s2)) . b1
( s1 . da = s2 . da & s1 . db = s2 . db ) by A1, Th92;
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)) . b1 = (Exec (I,s2)) . b1
hence (Exec (I,s1)) . c = s1 . c by A21, SCMFSA_2:92
.= s2 . c by A1, Th92
.= (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, Th93
.= (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:230
.= IC (Exec (I,s2)) by A21, SCMFSA_2:92 ;
hence NPP (Exec (I,s1)) = NPP (Exec (I,s2)) by A22, A25, Th91; :: thesis: verum
end;
suppose InsCode I = 5 ; :: thesis: NPP (Exec (I,s1)) = NPP (Exec (I,s2))
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)) . b1 = (Exec (I,s2)) . b1
per cases ( c = db or ( c = da & c <> db ) or ( c <> da & c <> db ) ) ;
suppose A28: c = db ; :: thesis: (Exec (I,s1)) . b1 = (Exec (I,s2)) . b1
( s1 . da = s2 . da & s1 . db = s2 . db ) by A1, Th92;
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)) . b1 = (Exec (I,s2)) . b1
( s1 . da = s2 . da & s1 . db = s2 . db ) by A1, Th92;
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)) . b1 = (Exec (I,s2)) . b1
hence (Exec (I,s1)) . c = s1 . c by A26, SCMFSA_2:93
.= s2 . c by A1, Th92
.= (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, Th93
.= (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:230
.= IC (Exec (I,s2)) by A26, SCMFSA_2:93 ;
hence NPP (Exec (I,s1)) = NPP (Exec (I,s2)) by A27, A31, Th91; :: thesis: verum
end;
suppose InsCode I = 6 ; :: thesis: NPP (Exec (I,s1)) = NPP (Exec (I,s2))
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, Th93
.= (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, Th92
.= (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 NPP (Exec (I,s1)) = NPP (Exec (I,s2)) by A34, A33, Th91; :: thesis: verum
end;
suppose InsCode I = 7 ; :: thesis: NPP (Exec (I,s1)) = NPP (Exec (I,s2))
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, Th92;
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, Th92;
thus IC (Exec (I,s1)) = succ (IC s1) by A35, A39, SCMFSA_2:96
.= succ (IC s2) by A1, COMPOS_1:230
.= 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, Th93
.= (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, Th92
.= (Exec (I,s2)) . c by A35, SCMFSA_2:96 ; :: thesis: verum
end;
hence NPP (Exec (I,s1)) = NPP (Exec (I,s2)) by A41, A36, Th91; :: thesis: verum
end;
suppose InsCode I = 8 ; :: thesis: NPP (Exec (I,s1)) = NPP (Exec (I,s2))
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, Th92;
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, Th92;
thus IC (Exec (I,s1)) = succ (IC s1) by A42, A46, SCMFSA_2:97
.= succ (IC s2) by A1, COMPOS_1:230
.= 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, Th93
.= (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, Th92
.= (Exec (I,s2)) . c by A42, SCMFSA_2:97 ; :: thesis: verum
end;
hence NPP (Exec (I,s1)) = NPP (Exec (I,s2)) by A48, A43, Th91; :: thesis: verum
end;
suppose InsCode I = 9 ; :: thesis: NPP (Exec (I,s1)) = NPP (Exec (I,s2))
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)) . b1 = (Exec (I,s2)) . b1
per cases ( c = da or c <> da ) ;
suppose A51: c = da ; :: thesis: (Exec (I,s1)) . b1 = (Exec (I,s2)) . b1
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, Th92;
hence (Exec (I,s1)) . c = (Exec (I,s2)) . c by A1, A49, A55, A53, Th93; :: thesis: verum
end;
suppose A56: c <> da ; :: thesis: (Exec (I,s1)) . b1 = (Exec (I,s2)) . b1
hence (Exec (I,s1)) . c = s1 . c by A49, SCMFSA_2:98
.= s2 . c by A1, Th92
.= (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, Th93
.= (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:230
.= IC (Exec (I,s2)) by A49, SCMFSA_2:98 ;
hence NPP (Exec (I,s1)) = NPP (Exec (I,s2)) by A50, A57, Th91; :: thesis: verum
end;
suppose InsCode I = 10 ; :: thesis: NPP (Exec (I,s1)) = NPP (Exec (I,s2))
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)) . 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
A61: s1 . da = s2 . da by A1, Th92;
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, Th92;
hence (Exec (I,s1)) . g = (Exec (I,s2)) . g by A1, A58, A60, A65, A63, A61, Th93; :: thesis: verum
end;
suppose A66: g <> f ; :: thesis: (Exec (I,s1)) . b1 = (Exec (I,s2)) . b1
hence (Exec (I,s1)) . g = s1 . g by A58, SCMFSA_2:99
.= s2 . g by A1, Th93
.= (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, Th92
.= (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:230
.= IC (Exec (I,s2)) by A58, SCMFSA_2:99 ;
hence NPP (Exec (I,s1)) = NPP (Exec (I,s2)) by A67, A59, Th91; :: thesis: verum
end;
suppose InsCode I = 11 ; :: thesis: NPP (Exec (I,s1)) = NPP (Exec (I,s2))
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)) . b1 = (Exec (I,s2)) . b1
per cases ( c = da or c <> da ) ;
suppose A70: c = da ; :: thesis: (Exec (I,s1)) . b1 = (Exec (I,s2)) . b1
hence (Exec (I,s1)) . c = len (s1 . f) by A68, SCMFSA_2:100
.= len (s2 . f) by A1, Th93
.= (Exec (I,s2)) . c by A68, A70, SCMFSA_2:100 ;
:: thesis: verum
end;
suppose A71: c <> da ; :: thesis: (Exec (I,s1)) . b1 = (Exec (I,s2)) . b1
hence (Exec (I,s1)) . c = s1 . c by A68, SCMFSA_2:100
.= s2 . c by A1, Th92
.= (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, Th93
.= (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:230
.= IC (Exec (I,s2)) by A68, SCMFSA_2:100 ;
hence NPP (Exec (I,s1)) = NPP (Exec (I,s2)) by A69, A72, Th91; :: thesis: verum
end;
suppose InsCode I = 12 ; :: thesis: NPP (Exec (I,s1)) = NPP (Exec (I,s2))
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)) . b1 = (Exec (I,s2)) . b1
per cases ( g = f or g <> f ) ;
suppose A75: g = f ; :: thesis: (Exec (I,s1)) . b1 = (Exec (I,s2)) . b1
( 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, Th92; :: thesis: verum
end;
suppose A76: g <> f ; :: thesis: (Exec (I,s1)) . b1 = (Exec (I,s2)) . b1
hence (Exec (I,s1)) . g = s1 . g by A73, SCMFSA_2:101
.= s2 . g by A1, Th93
.= (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, Th92
.= (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:230
.= IC (Exec (I,s2)) by A73, SCMFSA_2:101 ;
hence NPP (Exec (I,s1)) = NPP (Exec (I,s2)) by A77, A74, Th91; :: thesis: verum
end;
suppose InsCode I = 13 ; :: thesis: NPP (Exec (I,s1)) = NPP (Exec (I,s2))
then consider da being Int-Location such that
A73: I = da :==1 by SCMFSA_2:134;
A74: now
let g be Int-Location ; :: thesis: (Exec (I,s1)) . b1 = (Exec (I,s2)) . b1
per cases ( g = da or g <> da ) ;
suppose A75: g = da ; :: thesis: (Exec (I,s1)) . b1 = (Exec (I,s2)) . b1
( (Exec ((da :==1),s1)) . da = 1 & (Exec ((da :==1),s2)) . da = 1 ) by SCMFSA_2:136;
hence (Exec (I,s1)) . g = (Exec (I,s2)) . g by A73, A75; :: thesis: verum
end;
suppose A76: g <> da ; :: thesis: (Exec (I,s1)) . b1 = (Exec (I,s2)) . b1
hence (Exec (I,s1)) . g = s1 . g by A73, SCMFSA_2:136
.= s2 . g by A1, Th92
.= (Exec (I,s2)) . g by A73, A76, SCMFSA_2:136 ;
:: thesis: verum
end;
end;
end;
A77: now
let c be FinSeq-Location ; :: thesis: (Exec (I,s1)) . c = (Exec (I,s2)) . c
thus (Exec (I,s1)) . c = s1 . c by A73, SCMFSA_2:136
.= s2 . c by A1, Th93
.= (Exec (I,s2)) . c by A73, SCMFSA_2:136 ; :: thesis: verum
end;
IC (Exec (I,s1)) = succ (IC s1) by A73, SCMFSA_2:136
.= succ (IC s2) by A1, COMPOS_1:230
.= IC (Exec (I,s2)) by A73, SCMFSA_2:136 ;
hence NPP (Exec (I,s1)) = NPP (Exec (I,s2)) by A77, A74, Th91; :: thesis: verum
end;
end;