:: deftheorem Def12 defines CTL_WFF MODELC_1:def 12 :
for b₁ being non empty set holds
( b₁ = CTL_WFF iff ( ( for a being set st a in b₁ holds
a is FinSequence of NAT ) & ( for n being Element of NAT holds atom. n in b₁ ) & ( for p being FinSequence of NAT st p in b₁ holds
'not' p in b₁ ) & ( for p, q being FinSequence of NAT st p in b₁ & q in b₁ holds
p '&' q in b₁ ) & ( for p being FinSequence of NAT st p in b₁ holds
EX p in b₁ ) & ( for p being FinSequence of NAT st p in b₁ holds
EG p in b₁ ) & ( for p, q being FinSequence of NAT st p in b₁ & q in b₁ holds
p EU q in b₁ ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for n being Element of NAT holds atom. n in D ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for p being FinSequence of NAT st p in D holds
EX p in D ) & ( for p being FinSequence of NAT st p in D holds
EG p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p EU q in D ) holds
b₁ c= D ) ) );