environ
vocabularies HIDDEN, FINSEQ_1, CARD_1, ORDINAL4, SUBSET_1, NUMBERS, ARYTM_3, TARSKI, RELAT_1, XBOOLE_0, FUNCT_1, QC_LANG1, XBOOLEAN, HILBERT1, MODELC_2, CQC_THE1, NAT_1, XXREAL_0, LTLAXIO1, ARYTM_1, ZF_LANG, PARTFUN1, MARGREL1, FUNCT_2, HILBERT2, ZFMISC_1, FUNCOP_1, ZF_MODEL, PBOOLE, GLIB_000;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, DOMAIN_1, SUBSET_1, RELAT_1, PARTFUN1, NUMBERS, XCMPLX_0, ORDINAL1, NAT_1, XXREAL_0, NAT_D, FUNCT_1, FUNCT_2, BINOP_1, FINSEQ_1, FUNCOP_1, HILBERT1, HILBERT2, PBOOLE, XBOOLEAN, MARGREL1, AOFA_I00;
definitions TARSKI;
theorems TARSKI, NAT_1, XBOOLE_0, XXREAL_0, FINSEQ_1, NAT_D, XBOOLEAN, FUNCT_2, PARTFUN1, XREAL_1, ZFMISC_1, ORDINAL1, FUNCOP_1, HILBERT2, BINOP_1, XREAL_0;
schemes NAT_1, XBOOLE_0, FUNCT_2, FINSEQ_1, BINOP_1, HILBERT2;
registrations SUBSET_1, ORDINAL1, FUNCT_1, XXREAL_0, NAT_1, XBOOLEAN, RELSET_1, MARGREL1, XBOOLE_0, XREAL_0, FUNCT_2, HILBERT1;
constructors HIDDEN, NAT_D, RELSET_1, AOFA_I00, HILBERT2, DOMAIN_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities XBOOLEAN, MARGREL1;
expansions TARSKI;
Lm1:
for X being set
for f being FinSequence of X
for i being Nat st 1 <= i & i <= len f holds
f . i = f /. i
definition
let M be
LTLModel;
func SAT M -> Function of
[:NAT,LTLB_WFF:],
BOOLEAN means :
Def11:
for
n being
Element of
NAT holds
(
it . [n,TFALSUM] = 0 & ( for
k being
Element of
NAT holds
(
it . [n,(prop k)] = 1 iff
prop k in M . n ) ) & ( for
p,
q being
Element of
LTLB_WFF holds
(
it . [n,(p => q)] = (it . [n,p]) => (it . [n,q]) & (
it . [n,(p 'U' q)] = 1 implies ex
i being
Element of
NAT st
(
0 < i &
it . [(n + i),q] = 1 & ( for
j being
Element of
NAT st 1
<= j &
j < i holds
it . [(n + j),p] = 1 ) ) ) & ( ex
i being
Element of
NAT st
(
0 < i &
it . [(n + i),q] = 1 & ( for
j being
Element of
NAT st 1
<= j &
j < i holds
it . [(n + j),p] = 1 ) ) implies
it . [n,(p 'U' q)] = 1 ) ) ) );
existence
ex b1 being Function of [:NAT,LTLB_WFF:],BOOLEAN st
for n being Element of NAT holds
( b1 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds
( b1 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds
( b1 . [n,(p => q)] = (b1 . [n,p]) => (b1 . [n,q]) & ( b1 . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st
( 0 < i & b1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b1 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st
( 0 < i & b1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b1 . [(n + j),p] = 1 ) ) implies b1 . [n,(p 'U' q)] = 1 ) ) ) )
uniqueness
for b1, b2 being Function of [:NAT,LTLB_WFF:],BOOLEAN st ( for n being Element of NAT holds
( b1 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds
( b1 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds
( b1 . [n,(p => q)] = (b1 . [n,p]) => (b1 . [n,q]) & ( b1 . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st
( 0 < i & b1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b1 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st
( 0 < i & b1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b1 . [(n + j),p] = 1 ) ) implies b1 . [n,(p 'U' q)] = 1 ) ) ) ) ) & ( for n being Element of NAT holds
( b2 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds
( b2 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds
( b2 . [n,(p => q)] = (b2 . [n,p]) => (b2 . [n,q]) & ( b2 . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st
( 0 < i & b2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b2 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st
( 0 < i & b2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b2 . [(n + j),p] = 1 ) ) implies b2 . [n,(p 'U' q)] = 1 ) ) ) ) ) holds
b1 = b2
end;
::
deftheorem Def11 defines
SAT LTLAXIO1:def 11 :
for M being LTLModel
for b2 being Function of [:NAT,LTLB_WFF:],BOOLEAN holds
( b2 = SAT M iff for n being Element of NAT holds
( b2 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds
( b2 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds
( b2 . [n,(p => q)] = (b2 . [n,p]) => (b2 . [n,q]) & ( b2 . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st
( 0 < i & b2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b2 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st
( 0 < i & b2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b2 . [(n + j),p] = 1 ) ) implies b2 . [n,(p 'U' q)] = 1 ) ) ) ) );