REAL is non empty non trivial non finite set
NAT is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty non trivial non finite set
omega is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal set
bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
K372() is set
CTL_WFF is non empty set
bool CTL_WFF is non empty set
LTL_WFF is non empty set
bool LTL_WFF is non empty set
AtomicFamily is non empty set
atomic_LTL is Element of bool LTL_WFF
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT : b1 is atomic } is set
bool atomic_LTL is non empty set
Inf_seq AtomicFamily is non empty set
K86(NAT,AtomicFamily) is functional non empty M4( NAT , AtomicFamily )
ModelSP (Inf_seq AtomicFamily) is set
bool (ModelSP (Inf_seq AtomicFamily)) is non empty set
AtomicBasicAsgn is non empty Element of bool (ModelSP (Inf_seq AtomicFamily))
{ b1 where b1 is Element of ModelSP (Inf_seq AtomicFamily) : ex b2 being set st b1 = AtomicAsgn b2 } is set
Inf_seqModel (AtomicFamily,AtomicBasicAsgn) is non empty strict with_basic LTLModelStr
And_ AtomicFamily is Relation-like [:(ModelSP (Inf_seq AtomicFamily)),(ModelSP (Inf_seq AtomicFamily)):] -defined ModelSP (Inf_seq AtomicFamily) -valued Function-like V25([:(ModelSP (Inf_seq AtomicFamily)),(ModelSP (Inf_seq AtomicFamily)):], ModelSP (Inf_seq AtomicFamily)) Element of bool [:[:(ModelSP (Inf_seq AtomicFamily)),(ModelSP (Inf_seq AtomicFamily)):],(ModelSP (Inf_seq AtomicFamily)):]
[:(ModelSP (Inf_seq AtomicFamily)),(ModelSP (Inf_seq AtomicFamily)):] is Relation-like set
[:[:(ModelSP (Inf_seq AtomicFamily)),(ModelSP (Inf_seq AtomicFamily)):],(ModelSP (Inf_seq AtomicFamily)):] is Relation-like set
bool [:[:(ModelSP (Inf_seq AtomicFamily)),(ModelSP (Inf_seq AtomicFamily)):],(ModelSP (Inf_seq AtomicFamily)):] is non empty set
Or_ AtomicFamily is Relation-like [:(ModelSP (Inf_seq AtomicFamily)),(ModelSP (Inf_seq AtomicFamily)):] -defined ModelSP (Inf_seq AtomicFamily) -valued Function-like V25([:(ModelSP (Inf_seq AtomicFamily)),(ModelSP (Inf_seq AtomicFamily)):], ModelSP (Inf_seq AtomicFamily)) Element of bool [:[:(ModelSP (Inf_seq AtomicFamily)),(ModelSP (Inf_seq AtomicFamily)):],(ModelSP (Inf_seq AtomicFamily)):]
Not_ AtomicFamily is Relation-like ModelSP (Inf_seq AtomicFamily) -defined ModelSP (Inf_seq AtomicFamily) -valued Function-like V21( ModelSP (Inf_seq AtomicFamily)) V25( ModelSP (Inf_seq AtomicFamily), ModelSP (Inf_seq AtomicFamily)) Element of bool [:(ModelSP (Inf_seq AtomicFamily)),(ModelSP (Inf_seq AtomicFamily)):]
bool [:(ModelSP (Inf_seq AtomicFamily)),(ModelSP (Inf_seq AtomicFamily)):] is non empty set
Next_ AtomicFamily is Relation-like ModelSP (Inf_seq AtomicFamily) -defined ModelSP (Inf_seq AtomicFamily) -valued Function-like V21( ModelSP (Inf_seq AtomicFamily)) V25( ModelSP (Inf_seq AtomicFamily), ModelSP (Inf_seq AtomicFamily)) Element of bool [:(ModelSP (Inf_seq AtomicFamily)),(ModelSP (Inf_seq AtomicFamily)):]
Until_ AtomicFamily is Relation-like [:(ModelSP (Inf_seq AtomicFamily)),(ModelSP (Inf_seq AtomicFamily)):] -defined ModelSP (Inf_seq AtomicFamily) -valued Function-like V25([:(ModelSP (Inf_seq AtomicFamily)),(ModelSP (Inf_seq AtomicFamily)):], ModelSP (Inf_seq AtomicFamily)) Element of bool [:[:(ModelSP (Inf_seq AtomicFamily)),(ModelSP (Inf_seq AtomicFamily)):],(ModelSP (Inf_seq AtomicFamily)):]
Release_ AtomicFamily is Relation-like [:(ModelSP (Inf_seq AtomicFamily)),(ModelSP (Inf_seq AtomicFamily)):] -defined ModelSP (Inf_seq AtomicFamily) -valued Function-like V25([:(ModelSP (Inf_seq AtomicFamily)),(ModelSP (Inf_seq AtomicFamily)):], ModelSP (Inf_seq AtomicFamily)) Element of bool [:[:(ModelSP (Inf_seq AtomicFamily)),(ModelSP (Inf_seq AtomicFamily)):],(ModelSP (Inf_seq AtomicFamily)):]
LTLModelStr(# (ModelSP (Inf_seq AtomicFamily)),AtomicBasicAsgn,(And_ AtomicFamily),(Or_ AtomicFamily),(Not_ AtomicFamily),(Next_ AtomicFamily),(Until_ AtomicFamily),(Release_ AtomicFamily) #) is strict LTLModelStr
the BasicAssign of (Inf_seqModel (AtomicFamily,AtomicBasicAsgn)) is non empty Element of bool the carrier of (Inf_seqModel (AtomicFamily,AtomicBasicAsgn))
the carrier of (Inf_seqModel (AtomicFamily,AtomicBasicAsgn)) is set
bool the carrier of (Inf_seqModel (AtomicFamily,AtomicBasicAsgn)) is non empty set
[:atomic_LTL, the BasicAssign of (Inf_seqModel (AtomicFamily,AtomicBasicAsgn)):] is Relation-like set
bool [:atomic_LTL, the BasicAssign of (Inf_seqModel (AtomicFamily,AtomicBasicAsgn)):] is non empty set
COMPLEX is non empty non trivial non finite set
RAT is non empty non trivial non finite set
INT is non empty non trivial non finite set
[:NAT,REAL:] is Relation-like non empty non trivial non finite set
bool [:NAT,REAL:] is non empty non trivial non finite set
ExtREAL is non empty set
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty real integer finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V257() V258() V259() V260() V261() set
1 is epsilon-transitive epsilon-connected ordinal natural non empty real integer finite cardinal ext-real positive non negative V257() Element of NAT
2 is epsilon-transitive epsilon-connected ordinal natural non empty real integer finite cardinal ext-real positive non negative V257() Element of NAT
3 is epsilon-transitive epsilon-connected ordinal natural non empty real integer finite cardinal ext-real positive non negative V257() Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty real integer finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V257() V258() V259() V260() V261() Element of NAT
Seg 1 is non empty trivial finite 1 -element Element of bool NAT
{1} is non empty trivial finite V42() 1 -element set
Seg 2 is non empty finite 2 -element Element of bool NAT
{1,2} is non empty finite V42() set
{{}} is functional non empty trivial finite V42() 1 -element set
atom. 0 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
6 is epsilon-transitive epsilon-connected ordinal natural non empty real integer finite cardinal ext-real positive non negative V257() Element of NAT
6 + 0 is epsilon-transitive epsilon-connected ordinal natural non empty real integer finite cardinal ext-real positive non negative V257() Element of NAT
<*(6 + 0)*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V258() V259() V260() V261() V262() V263() V264() V265() FinSequence of NAT
card {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty real integer finite finite-yielding V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V257() V258() V259() V260() V261() set
w is set
v is set
LS is set
v \/ LS is set
LT is set
(v \/ LS) \/ LT is set
w is set
v is set
LS is set
v \ LS is Element of bool v
bool v is non empty set
LT is set
IS is set
LT \ IS is Element of bool LT
bool LT is non empty set
(v \ LS) \/ (LT \ IS) is set
[:NAT,NAT:] is Relation-like non empty non trivial non finite set
bool [:NAT,NAT:] is non empty non trivial non finite set
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
<*w*> is Relation-like NAT -defined bool [:NAT,NAT:] -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of bool [:NAT,NAT:]
<*w*> . 1 is set
rng <*w*> is non empty trivial finite 1 -element Element of bool (bool [:NAT,NAT:])
bool (bool [:NAT,NAT:]) is non empty non trivial non finite set
{w} is functional non empty trivial finite V42() 1 -element set
dom <*w*> is non empty trivial finite 1 -element Element of bool NAT
w is real ext-real V257() set
v is real ext-real V257() set
[\w/] is real integer ext-real V257() set
[\v/] is real integer ext-real V257() set
[\v/] + 1 is real integer ext-real V257() Element of REAL
w is real ext-real V257() set
v is real ext-real V257() set
v - 1 is real ext-real V257() Element of REAL
[\w/] is real integer ext-real V257() set
[\v/] is real integer ext-real V257() set
[\v/] - 1 is real integer ext-real V257() Element of REAL
w + 1 is real ext-real V257() Element of REAL
(v - 1) + 1 is real ext-real V257() Element of REAL
[\(w + 1)/] is real integer ext-real V257() set
[\w/] + 1 is real integer ext-real V257() Element of REAL
([\w/] + 1) - 1 is real integer ext-real V257() Element of REAL
w is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative V257() set
0 + w is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative V257() Element of NAT
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
the_argument_of w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
the_left_argument_of w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
the_right_argument_of w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
{w} is functional non empty trivial finite V42() 1 -element set
v is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
Subformulae v is non empty set
bool (Subformulae v) is non empty set
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
v is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
Subformulae v is non empty set
bool (Subformulae v) is non empty set
LS is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
{w,LS} is functional non empty finite V42() set
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
the_left_argument_of w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
the_right_argument_of w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
{(the_left_argument_of w),(the_right_argument_of w)} is functional non empty finite V42() set
Subformulae w is non empty set
bool (Subformulae w) is non empty set
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
the_left_argument_of w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
{(the_left_argument_of w)} is functional non empty trivial finite V42() 1 -element set
Subformulae w is non empty set
bool (Subformulae w) is non empty set
the_right_argument_of w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
{(the_right_argument_of w)} is functional non empty trivial finite V42() 1 -element set
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
{w} is functional non empty trivial finite V42() 1 -element set
Subformulae w is non empty set
bool (Subformulae w) is non empty set
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
the_argument_of w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
{(the_argument_of w)} is functional non empty trivial finite V42() 1 -element set
Subformulae w is non empty set
bool (Subformulae w) is non empty set
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
Subformulae w is non empty set
bool (Subformulae w) is non empty set
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
the_left_argument_of w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
the_right_argument_of w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
{(the_left_argument_of w),(the_right_argument_of w)} is functional non empty finite V42() set
(w) is non empty Element of bool LTL_WFF
bool (w) is non empty set
{(the_left_argument_of w)} is functional non empty trivial finite V42() 1 -element set
{(the_right_argument_of w)} is functional non empty trivial finite V42() 1 -element set
v is Element of bool (w)
LS is Element of bool (w)
LT is Element of bool (w)
IS is Element of bool (w)
FS is Element of bool (w)
chf is Element of bool (w)
run is Element of bool (w)
FSet is Element of bool (w)
FK is Element of bool (w)
x is Element of bool (w)
v is Element of bool (w)
LS is Element of bool (w)
LT is Element of bool (w)
IS is Element of bool (w)
FS is Element of bool (w)
chf is Element of bool (w)
run is Element of bool (w)
FSet is Element of bool (w)
FK is Element of bool (w)
x is Element of bool (w)
the_argument_of w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
{(the_argument_of w)} is functional non empty trivial finite V42() 1 -element set
{w} is functional non empty trivial finite V42() 1 -element set
v is Element of bool (w)
LS is Element of bool (w)
LT is Element of bool (w)
IS is Element of bool (w)
FS is Element of bool (w)
chf is Element of bool (w)
run is Element of bool (w)
FSet is Element of bool (w)
FK is Element of bool (w)
x is Element of bool (w)
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
LS is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
v is (w)
the of v is Element of bool (w)
(w) is non empty Element of bool LTL_WFF
bool (w) is non empty set
the of v is Element of bool (w)
{LS} is functional non empty trivial finite V42() 1 -element set
the of v \/ {LS} is non empty set
the of v \ {LS} is Element of bool (w)
(LS) is non empty Element of bool LTL_WFF
(LS) is Element of bool (LS)
bool (LS) is non empty set
(LS) \ the of v is Element of bool (LS)
( the of v \ {LS}) \/ ((LS) \ the of v) is set
the of v is Element of bool (w)
(LS) is Element of bool (LS)
the of v \/ (LS) is set
FK is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
FSet is Element of bool (w)
FK is Element of bool (w)
x is Element of bool (w)
(w,FSet,FK,x) is (w) (w)
the of (w,FSet,FK,x) is Element of bool (w)
the of (w,FSet,FK,x) is Element of bool (w)
the of (w,FSet,FK,x) is Element of bool (w)
LT is (w) (w)
the of LT is Element of bool (w)
the of LT is Element of bool (w)
the of LT is Element of bool (w)
IS is (w) (w)
the of IS is Element of bool (w)
the of IS is Element of bool (w)
the of IS is Element of bool (w)
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
LS is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
v is (w)
the of v is Element of bool (w)
(w) is non empty Element of bool LTL_WFF
bool (w) is non empty set
the of v is Element of bool (w)
{LS} is functional non empty trivial finite V42() 1 -element set
the of v \/ {LS} is non empty set
the of v \ {LS} is Element of bool (w)
(LS) is non empty Element of bool LTL_WFF
(LS) is Element of bool (LS)
bool (LS) is non empty set
(LS) \ the of v is Element of bool (LS)
( the of v \ {LS}) \/ ((LS) \ the of v) is set
the of v is Element of bool (w)
FK is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
FSet is Element of bool (w)
FK is Element of bool (w)
(w,FSet,FK, the of v) is (w) (w)
the of (w,FSet,FK, the of v) is Element of bool (w)
the of (w,FSet,FK, the of v) is Element of bool (w)
the of (w,FSet,FK, the of v) is Element of bool (w)
LT is (w) (w)
the of LT is Element of bool (w)
the of LT is Element of bool (w)
the of LT is Element of bool (w)
IS is (w) (w)
the of IS is Element of bool (w)
the of IS is Element of bool (w)
the of IS is Element of bool (w)
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
(w) is non empty Element of bool LTL_WFF
bool (w) is non empty set
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
{w} is functional non empty trivial finite V42() 1 -element set
(w) is non empty Element of bool LTL_WFF
bool (w) is non empty set
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
(w) is Element of bool (w)
(w) is non empty Element of bool LTL_WFF
bool (w) is non empty set
(w,(w),(w),(w)) is (w) (w)
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
(w) is Element of bool (w)
(w) is non empty Element of bool LTL_WFF
bool (w) is non empty set
(w,(w),(w),(w)) is (w) (w)
w is set
v is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
(v) is Element of bool (v)
(v) is non empty Element of bool LTL_WFF
bool (v) is non empty set
(v,(v),(v),(v)) is (v) (v)
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
(w) is Element of bool (w)
(w) is non empty Element of bool LTL_WFF
bool (w) is non empty set
(w) is Element of bool (w)
{w} is functional non empty trivial finite V42() 1 -element set
(w,(w),(w),(w)) is (w) (w)
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
(w) is Element of bool (w)
(w) is non empty Element of bool LTL_WFF
bool (w) is non empty set
v is (w)
the of v is Element of bool (w)
(w,(w), the of v,(w)) is (w) (w)
w is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative V257() set
w - 1 is real integer ext-real V257() Element of REAL
v is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len v is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative V257() Element of NAT
v . w is set
(len v) - (w - 1) is real integer ext-real V257() Element of REAL
v . (len v) is set
LS is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
(len v) - 0 is real integer ext-real non negative V257() Element of REAL
IS is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative V257() set
Seg IS is finite IS -element Element of bool NAT
v | (Seg IS) is Relation-like NAT -defined Seg IS -defined NAT -defined Function-like finite FinSubsequence-like set
chf is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
run is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
chf ^ run is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len chf is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative V257() Element of NAT
len run is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative V257() Element of NAT
(len chf) + (len run) is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative V257() Element of NAT
(len v) - (len chf) is real integer ext-real V257() Element of REAL
(len v) - IS is real integer ext-real V257() Element of REAL
w - w is real integer ext-real V257() set
(len v) - w is real integer ext-real V257() Element of REAL
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty real integer finite cardinal ext-real positive non negative V257() Element of NAT
((len v) - w) + 1 is real integer ext-real V257() Element of REAL
dom run is finite Element of bool NAT
run . 1 is set
(len chf) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty real integer finite cardinal ext-real positive non negative V257() Element of NAT
v . ((len chf) + 1) is set
IS + 1 is epsilon-transitive epsilon-connected ordinal natural non empty real integer finite cardinal ext-real positive non negative V257() Element of NAT
v . (IS + 1) is set
FSet is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative V257() set
run . FSet is set
FSet + 1 is epsilon-transitive epsilon-connected ordinal natural non empty real integer finite cardinal ext-real positive non negative V257() Element of NAT
run . (FSet + 1) is set
FSet + IS is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative V257() set
1 + 0 is epsilon-transitive epsilon-connected ordinal natural non empty real integer finite cardinal ext-real positive non negative V257() Element of NAT
((len v) - IS) + IS is real integer ext-real V257() Element of REAL
v . (FSet + IS) is set
(FSet + IS) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty real integer finite cardinal ext-real positive non negative V257() Element of NAT
v . ((FSet + IS) + 1) is set
F is (LS) (LS)
F2 is (LS) (LS)
IS + (FSet + 1) is epsilon-transitive epsilon-connected ordinal natural non empty real integer finite cardinal ext-real positive non negative V257() Element of NAT
v . (IS + (FSet + 1)) is set
run . (len run) is set
v . ((len chf) + (len run)) is set
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
(w) is non empty Element of bool LTL_WFF
bool (w) is non empty set
v is Element of bool (w)
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
(w) is non empty Element of bool LTL_WFF
v is (w) (w)
the of v is Element of bool (w)
bool (w) is non empty set
the of v is Element of bool (w)
the of v \/ the of v is Element of bool (w)
the of v is Element of bool (w)
(w, the of v) is Element of bool LTL_WFF
'X' (w, the of v) is Element of bool LTL_WFF
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT : ex b2 being Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT st
( b2 in (w, the of v) & b1 = 'X' b2 ) } is set
( the of v \/ the of v) \/ ('X' (w, the of v)) is set
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
v is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
LS is (v) (v)
the of LS is Element of bool (v)
(v) is non empty Element of bool LTL_WFF
bool (v) is non empty set
(v,LS) is Element of bool LTL_WFF
the of LS is Element of bool (v)
the of LS \/ the of LS is Element of bool (v)
the of LS is Element of bool (v)
(v, the of LS) is Element of bool LTL_WFF
'X' (v, the of LS) is Element of bool LTL_WFF
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT : ex b2 being Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT st
( b2 in (v, the of LS) & b1 = 'X' b2 ) } is set
( the of LS \/ the of LS) \/ ('X' (v, the of LS)) is set
(v,LS,w) is (v) (v)
(v,(v,LS,w)) is Element of bool LTL_WFF
the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) \/ the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) is Element of bool (v)
(v, the of (v,LS,w)) is Element of bool LTL_WFF
'X' (v, the of (v,LS,w)) is Element of bool LTL_WFF
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT : ex b2 being Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT st
( b2 in (v, the of (v,LS,w)) & b1 = 'X' b2 ) } is set
( the of (v,LS,w) \/ the of (v,LS,w)) \/ ('X' (v, the of (v,LS,w))) is set
(w) is Element of bool (w)
(w) is non empty Element of bool LTL_WFF
bool (w) is non empty set
the of LS \/ (w) is set
{w} is functional non empty trivial finite V42() 1 -element set
the of LS \/ {w} is non empty set
(w) is Element of bool (w)
the of LS \ {w} is Element of bool (v)
(w) \ the of LS is Element of bool (w)
( the of LS \ {w}) \/ ((w) \ the of LS) is set
x is set
x is set
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
v is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
LS is (v) (v)
the of LS is Element of bool (v)
(v) is non empty Element of bool LTL_WFF
bool (v) is non empty set
(v,LS) is Element of bool LTL_WFF
the of LS is Element of bool (v)
the of LS \/ the of LS is Element of bool (v)
the of LS is Element of bool (v)
(v, the of LS) is Element of bool LTL_WFF
'X' (v, the of LS) is Element of bool LTL_WFF
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT : ex b2 being Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT st
( b2 in (v, the of LS) & b1 = 'X' b2 ) } is set
( the of LS \/ the of LS) \/ ('X' (v, the of LS)) is set
(v,LS,w) is (v) (v)
(v,(v,LS,w)) is Element of bool LTL_WFF
the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) \/ the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) is Element of bool (v)
(v, the of (v,LS,w)) is Element of bool LTL_WFF
'X' (v, the of (v,LS,w)) is Element of bool LTL_WFF
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT : ex b2 being Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT st
( b2 in (v, the of (v,LS,w)) & b1 = 'X' b2 ) } is set
( the of (v,LS,w) \/ the of (v,LS,w)) \/ ('X' (v, the of (v,LS,w))) is set
LT is Element of Inf_seq AtomicFamily
F1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
{w} is functional non empty trivial finite V42() 1 -element set
the of LS \/ {w} is non empty set
{w} is functional non empty trivial finite V42() 1 -element set
the of LS \ {w} is Element of bool (v)
(w) is non empty Element of bool LTL_WFF
(w) is Element of bool (w)
bool (w) is non empty set
(w) \ the of LS is Element of bool (w)
( the of LS \ {w}) \/ ((w) \ the of LS) is set
the_left_argument_of w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
the_right_argument_of w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
{(the_left_argument_of w),(the_right_argument_of w)} is functional non empty finite V42() set
(the_left_argument_of w) '&' (the_right_argument_of w) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
<*1*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V258() V259() V260() V261() V262() V263() V264() V265() FinSequence of NAT
<*1*> ^ (the_left_argument_of w) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
(<*1*> ^ (the_left_argument_of w)) ^ (the_right_argument_of w) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
m is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
w1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
'X' w1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
<*3*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V258() V259() V260() V261() V262() V263() V264() V265() FinSequence of NAT
<*3*> ^ w1 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
w1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
'X' w1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
<*3*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V258() V259() V260() V261() V262() V263() V264() V265() FinSequence of NAT
<*3*> ^ w1 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
(w) is Element of bool (w)
(w) is non empty Element of bool LTL_WFF
bool (w) is non empty set
the of LS \/ (w) is set
the_argument_of w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
{(the_argument_of w)} is functional non empty trivial finite V42() 1 -element set
F1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
{w} is functional non empty trivial finite V42() 1 -element set
the of LS \/ {w} is non empty set
{w} is functional non empty trivial finite V42() 1 -element set
the of LS \/ {w} is non empty set
{w} is functional non empty trivial finite V42() 1 -element set
the of LS \ {w} is Element of bool (v)
(w) is non empty Element of bool LTL_WFF
(w) is Element of bool (w)
bool (w) is non empty set
(w) \ the of LS is Element of bool (w)
( the of LS \ {w}) \/ ((w) \ the of LS) is set
(w) is Element of bool (w)
(w) is non empty Element of bool LTL_WFF
bool (w) is non empty set
the of LS \/ (w) is set
m is Element of bool (v)
(v,m) is Element of bool LTL_WFF
h is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
m2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
'X' m2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
<*3*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V258() V259() V260() V261() V262() V263() V264() V265() FinSequence of NAT
<*3*> ^ m2 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
m2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
'X' m2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
<*3*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V258() V259() V260() V261() V262() V263() V264() V265() FinSequence of NAT
<*3*> ^ m2 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
'X' (v,m) is Element of bool LTL_WFF
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT : ex b2 being Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT st
( b2 in (v,m) & b1 = 'X' b2 ) } is set
v is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
LS is (v) (v)
the of LS is Element of bool (v)
(v) is non empty Element of bool LTL_WFF
bool (v) is non empty set
LT is Element of Inf_seq AtomicFamily
(v,LS) is Element of bool LTL_WFF
the of LS is Element of bool (v)
the of LS \/ the of LS is Element of bool (v)
the of LS is Element of bool (v)
(v, the of LS) is Element of bool LTL_WFF
'X' (v, the of LS) is Element of bool LTL_WFF
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT : ex b2 being Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT st
( b2 in (v, the of LS) & b1 = 'X' b2 ) } is set
( the of LS \/ the of LS) \/ ('X' (v, the of LS)) is set
(v,LS,w) is (v) (v)
(v,(v,LS,w)) is Element of bool LTL_WFF
the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) \/ the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) is Element of bool (v)
(v, the of (v,LS,w)) is Element of bool LTL_WFF
'X' (v, the of (v,LS,w)) is Element of bool LTL_WFF
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT : ex b2 being Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT st
( b2 in (v, the of (v,LS,w)) & b1 = 'X' b2 ) } is set
( the of (v,LS,w) \/ the of (v,LS,w)) \/ ('X' (v, the of (v,LS,w))) is set
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
v is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
LS is (v) (v)
the of LS is Element of bool (v)
(v) is non empty Element of bool LTL_WFF
bool (v) is non empty set
(v,LS) is Element of bool LTL_WFF
the of LS is Element of bool (v)
the of LS \/ the of LS is Element of bool (v)
the of LS is Element of bool (v)
(v, the of LS) is Element of bool LTL_WFF
'X' (v, the of LS) is Element of bool LTL_WFF
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT : ex b2 being Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT st
( b2 in (v, the of LS) & b1 = 'X' b2 ) } is set
( the of LS \/ the of LS) \/ ('X' (v, the of LS)) is set
(v,LS,w) is (v) (v)
(v,(v,LS,w)) is Element of bool LTL_WFF
the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) \/ the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) is Element of bool (v)
(v, the of (v,LS,w)) is Element of bool LTL_WFF
'X' (v, the of (v,LS,w)) is Element of bool LTL_WFF
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT : ex b2 being Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT st
( b2 in (v, the of (v,LS,w)) & b1 = 'X' b2 ) } is set
( the of (v,LS,w) \/ the of (v,LS,w)) \/ ('X' (v, the of (v,LS,w))) is set
(v,LS,w) is (v) (v)
(v,(v,LS,w)) is Element of bool LTL_WFF
the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) \/ the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) is Element of bool (v)
(v, the of (v,LS,w)) is Element of bool LTL_WFF
'X' (v, the of (v,LS,w)) is Element of bool LTL_WFF
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT : ex b2 being Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT st
( b2 in (v, the of (v,LS,w)) & b1 = 'X' b2 ) } is set
( the of (v,LS,w) \/ the of (v,LS,w)) \/ ('X' (v, the of (v,LS,w))) is set
LT is Element of Inf_seq AtomicFamily
(w) is Element of bool (w)
(w) is non empty Element of bool LTL_WFF
bool (w) is non empty set
the of LS \/ {} is set
the_left_argument_of w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
{w} is functional non empty trivial finite V42() 1 -element set
the of LS \/ {w} is non empty set
(w) is Element of bool (w)
{(the_left_argument_of w)} is functional non empty trivial finite V42() 1 -element set
the of LS \ {w} is Element of bool (v)
{(the_left_argument_of w)} \ the of LS is functional trivial finite V42() Element of bool {(the_left_argument_of w)}
bool {(the_left_argument_of w)} is non empty finite V42() set
( the of LS \ {w}) \/ ({(the_left_argument_of w)} \ the of LS) is set
L is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
the_right_argument_of w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
(w) is Element of bool (w)
{(the_right_argument_of w)} is functional non empty trivial finite V42() 1 -element set
{(the_right_argument_of w)} \ the of LS is functional trivial finite V42() Element of bool {(the_right_argument_of w)}
bool {(the_right_argument_of w)} is non empty finite V42() set
( the of LS \ {w}) \/ ({(the_right_argument_of w)} \ the of LS) is set
m3 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
(the_left_argument_of w) 'or' (the_right_argument_of w) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
<*2*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V258() V259() V260() V261() V262() V263() V264() V265() FinSequence of NAT
<*2*> ^ (the_left_argument_of w) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
(<*2*> ^ (the_left_argument_of w)) ^ (the_right_argument_of w) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
m3 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
m3 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
m3 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
m3 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
v is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
LS is (v) (v)
the of LS is Element of bool (v)
(v) is non empty Element of bool LTL_WFF
bool (v) is non empty set
(v,LS) is Element of bool LTL_WFF
the of LS is Element of bool (v)
the of LS \/ the of LS is Element of bool (v)
the of LS is Element of bool (v)
(v, the of LS) is Element of bool LTL_WFF
'X' (v, the of LS) is Element of bool LTL_WFF
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT : ex b2 being Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT st
( b2 in (v, the of LS) & b1 = 'X' b2 ) } is set
( the of LS \/ the of LS) \/ ('X' (v, the of LS)) is set
(v,LS,w) is (v) (v)
(v,(v,LS,w)) is Element of bool LTL_WFF
the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) \/ the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) is Element of bool (v)
(v, the of (v,LS,w)) is Element of bool LTL_WFF
'X' (v, the of (v,LS,w)) is Element of bool LTL_WFF
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT : ex b2 being Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT st
( b2 in (v, the of (v,LS,w)) & b1 = 'X' b2 ) } is set
( the of (v,LS,w) \/ the of (v,LS,w)) \/ ('X' (v, the of (v,LS,w))) is set
(v,LS,w) is (v) (v)
(v,(v,LS,w)) is Element of bool LTL_WFF
the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) \/ the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) is Element of bool (v)
(v, the of (v,LS,w)) is Element of bool LTL_WFF
'X' (v, the of (v,LS,w)) is Element of bool LTL_WFF
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT : ex b2 being Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT st
( b2 in (v, the of (v,LS,w)) & b1 = 'X' b2 ) } is set
( the of (v,LS,w) \/ the of (v,LS,w)) \/ ('X' (v, the of (v,LS,w))) is set
LT is Element of Inf_seq AtomicFamily
(w) is Element of bool (w)
(w) is non empty Element of bool LTL_WFF
bool (w) is non empty set
{w} is functional non empty trivial finite V42() 1 -element set
the of LS \/ {w} is non empty set
the_right_argument_of w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
(w) is Element of bool (w)
{(the_right_argument_of w)} is functional non empty trivial finite V42() 1 -element set
the of LS \ {w} is Element of bool (v)
{(the_right_argument_of w)} \ the of LS is functional trivial finite V42() Element of bool {(the_right_argument_of w)}
bool {(the_right_argument_of w)} is non empty finite V42() set
( the of LS \ {w}) \/ ({(the_right_argument_of w)} \ the of LS) is set
the_left_argument_of w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
the of LS \/ {w} is non empty set
(w) is Element of bool (w)
{(the_left_argument_of w)} is functional non empty trivial finite V42() 1 -element set
{(the_left_argument_of w)} \ the of LS is functional trivial finite V42() Element of bool {(the_left_argument_of w)}
bool {(the_left_argument_of w)} is non empty finite V42() set
( the of LS \ {w}) \/ ({(the_left_argument_of w)} \ the of LS) is set
'X' w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
<*3*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V258() V259() V260() V261() V262() V263() V264() V265() FinSequence of NAT
<*3*> ^ w is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
m1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
h is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
m2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
'X' m2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
<*3*> ^ m2 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
m2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
'X' m2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
<*3*> ^ m2 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
m3 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
(the_left_argument_of w) 'U' (the_right_argument_of w) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
4 is epsilon-transitive epsilon-connected ordinal natural non empty real integer finite cardinal ext-real positive non negative V257() Element of NAT
<*4*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V258() V259() V260() V261() V262() V263() V264() V265() FinSequence of NAT
<*4*> ^ (the_left_argument_of w) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
(<*4*> ^ (the_left_argument_of w)) ^ (the_right_argument_of w) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
(the_left_argument_of w) '&' ('X' w) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
<*1*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V258() V259() V260() V261() V262() V263() V264() V265() FinSequence of NAT
<*1*> ^ (the_left_argument_of w) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
(<*1*> ^ (the_left_argument_of w)) ^ ('X' w) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
(the_right_argument_of w) 'or' ((the_left_argument_of w) '&' ('X' w)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
<*2*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V258() V259() V260() V261() V262() V263() V264() V265() FinSequence of NAT
<*2*> ^ (the_right_argument_of w) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
(<*2*> ^ (the_right_argument_of w)) ^ ((the_left_argument_of w) '&' ('X' w)) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
m3 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
m3 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
m3 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
natMAX is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
'X' k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
<*3*> ^ k is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
'X' k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
<*3*> ^ k is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
m3 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
v is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
LS is (v) (v)
the of LS is Element of bool (v)
(v) is non empty Element of bool LTL_WFF
bool (v) is non empty set
(v,LS) is Element of bool LTL_WFF
the of LS is Element of bool (v)
the of LS \/ the of LS is Element of bool (v)
the of LS is Element of bool (v)
(v, the of LS) is Element of bool LTL_WFF
'X' (v, the of LS) is Element of bool LTL_WFF
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT : ex b2 being Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT st
( b2 in (v, the of LS) & b1 = 'X' b2 ) } is set
( the of LS \/ the of LS) \/ ('X' (v, the of LS)) is set
(v,LS,w) is (v) (v)
(v,(v,LS,w)) is Element of bool LTL_WFF
the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) \/ the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) is Element of bool (v)
(v, the of (v,LS,w)) is Element of bool LTL_WFF
'X' (v, the of (v,LS,w)) is Element of bool LTL_WFF
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT : ex b2 being Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT st
( b2 in (v, the of (v,LS,w)) & b1 = 'X' b2 ) } is set
( the of (v,LS,w) \/ the of (v,LS,w)) \/ ('X' (v, the of (v,LS,w))) is set
(v,LS,w) is (v) (v)
(v,(v,LS,w)) is Element of bool LTL_WFF
the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) \/ the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) is Element of bool (v)
(v, the of (v,LS,w)) is Element of bool LTL_WFF
'X' (v, the of (v,LS,w)) is Element of bool LTL_WFF
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT : ex b2 being Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT st
( b2 in (v, the of (v,LS,w)) & b1 = 'X' b2 ) } is set
( the of (v,LS,w) \/ the of (v,LS,w)) \/ ('X' (v, the of (v,LS,w))) is set
LT is Element of Inf_seq AtomicFamily
(w) is Element of bool (w)
(w) is non empty Element of bool LTL_WFF
bool (w) is non empty set
{w} is functional non empty trivial finite V42() 1 -element set
the of LS \/ {w} is non empty set
the_right_argument_of w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
the_left_argument_of w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
(w) is Element of bool (w)
{(the_left_argument_of w),(the_right_argument_of w)} is functional non empty finite V42() set
the of LS \ {w} is Element of bool (v)
{(the_left_argument_of w),(the_right_argument_of w)} \ the of LS is functional finite V42() Element of bool {(the_left_argument_of w),(the_right_argument_of w)}
bool {(the_left_argument_of w),(the_right_argument_of w)} is non empty finite V42() set
( the of LS \ {w}) \/ ({(the_left_argument_of w),(the_right_argument_of w)} \ the of LS) is set
the of LS \/ {w} is non empty set
(w) is Element of bool (w)
{(the_right_argument_of w)} is functional non empty trivial finite V42() 1 -element set
{(the_right_argument_of w)} \ the of LS is functional trivial finite V42() Element of bool {(the_right_argument_of w)}
bool {(the_right_argument_of w)} is non empty finite V42() set
( the of LS \ {w}) \/ ({(the_right_argument_of w)} \ the of LS) is set
'X' w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
<*3*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V258() V259() V260() V261() V262() V263() V264() V265() FinSequence of NAT
<*3*> ^ w is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
m1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
h is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
m2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
'X' m2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
<*3*> ^ m2 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
m2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
'X' m2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
<*3*> ^ m2 is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
m3 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
(the_left_argument_of w) 'R' (the_right_argument_of w) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
5 is epsilon-transitive epsilon-connected ordinal natural non empty real integer finite cardinal ext-real positive non negative V257() Element of NAT
<*5*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V258() V259() V260() V261() V262() V263() V264() V265() FinSequence of NAT
<*5*> ^ (the_left_argument_of w) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
(<*5*> ^ (the_left_argument_of w)) ^ (the_right_argument_of w) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
(the_left_argument_of w) '&' (the_right_argument_of w) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
<*1*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V258() V259() V260() V261() V262() V263() V264() V265() FinSequence of NAT
<*1*> ^ (the_left_argument_of w) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
(<*1*> ^ (the_left_argument_of w)) ^ (the_right_argument_of w) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
(the_right_argument_of w) '&' ('X' w) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
<*1*> ^ (the_right_argument_of w) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
(<*1*> ^ (the_right_argument_of w)) ^ ('X' w) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
((the_left_argument_of w) '&' (the_right_argument_of w)) 'or' ((the_right_argument_of w) '&' ('X' w)) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
<*2*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V258() V259() V260() V261() V262() V263() V264() V265() FinSequence of NAT
<*2*> ^ ((the_left_argument_of w) '&' (the_right_argument_of w)) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
(<*2*> ^ ((the_left_argument_of w) '&' (the_right_argument_of w))) ^ ((the_right_argument_of w) '&' ('X' w)) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
m3 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
m3 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
m3 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
natMAX is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
'X' k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
<*3*> ^ k is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
'X' k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
<*3*> ^ k is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like V258() V259() V260() V261() FinSequence of NAT
m3 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
v is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
LS is (v) (v)
the of LS is Element of bool (v)
(v) is non empty Element of bool LTL_WFF
bool (v) is non empty set
LT is Element of Inf_seq AtomicFamily
(v,LS) is Element of bool LTL_WFF
the of LS is Element of bool (v)
the of LS \/ the of LS is Element of bool (v)
the of LS is Element of bool (v)
(v, the of LS) is Element of bool LTL_WFF
'X' (v, the of LS) is Element of bool LTL_WFF
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT : ex b2 being Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT st
( b2 in (v, the of LS) & b1 = 'X' b2 ) } is set
( the of LS \/ the of LS) \/ ('X' (v, the of LS)) is set
(v,LS,w) is (v) (v)
(v,(v,LS,w)) is Element of bool LTL_WFF
the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) \/ the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) is Element of bool (v)
(v, the of (v,LS,w)) is Element of bool LTL_WFF
'X' (v, the of (v,LS,w)) is Element of bool LTL_WFF
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT : ex b2 being Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT st
( b2 in (v, the of (v,LS,w)) & b1 = 'X' b2 ) } is set
( the of (v,LS,w) \/ the of (v,LS,w)) \/ ('X' (v, the of (v,LS,w))) is set
(v,LS,w) is (v) (v)
(v,(v,LS,w)) is Element of bool LTL_WFF
the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) \/ the of (v,LS,w) is Element of bool (v)
the of (v,LS,w) is Element of bool (v)
(v, the of (v,LS,w)) is Element of bool LTL_WFF
'X' (v, the of (v,LS,w)) is Element of bool LTL_WFF
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT : ex b2 being Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT st
( b2 in (v, the of (v,LS,w)) & b1 = 'X' b2 ) } is set
( the of (v,LS,w) \/ the of (v,LS,w)) \/ ('X' (v, the of (v,LS,w))) is set
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
(w) is non empty Element of bool LTL_WFF
the_argument_of w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
((the_argument_of w)) is non empty Element of bool LTL_WFF
{w} is functional non empty trivial finite V42() 1 -element set
((the_argument_of w)) \/ {w} is non empty set
LS is set
LT is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
(w) is non empty Element of bool LTL_WFF
the_left_argument_of w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
((the_left_argument_of w)) is non empty Element of bool LTL_WFF
the_right_argument_of w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
((the_right_argument_of w)) is non empty Element of bool LTL_WFF
((the_left_argument_of w)) \/ ((the_right_argument_of w)) is non empty Element of bool LTL_WFF
{w} is functional non empty trivial finite V42() 1 -element set
(((the_left_argument_of w)) \/ ((the_right_argument_of w))) \/ {w} is non empty set
IS is set
FS is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
(w) is non empty Element of bool LTL_WFF
{w} is functional non empty trivial finite V42() 1 -element set
len w is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative V257() Element of NAT
v is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative V257() set
atom. v is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
6 + v is epsilon-transitive epsilon-connected ordinal natural non empty real integer finite cardinal ext-real positive non negative V257() Element of NAT
<*(6 + v)*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V258() V259() V260() V261() V262() V263() V264() V265() FinSequence of NAT
v is set
LS is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
len LS is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal ext-real non negative V257() Element of NAT
v is set
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like LTL-formula-like V258() V259() V260() V261() FinSequence of NAT
Subformulae w is non empty