:: FSM_2 semantic presentation

REAL is non empty V35() set

bool REAL is non empty V35() set
COMPLEX is non empty V35() set

bool omega is non empty V35() set
bool NAT is non empty V35() set
K272() is L6()
the carrier of K272() is set
RAT is non empty V35() set
INT is non empty V35() set

Seg 1 is non empty trivial V35() V42(1) Element of bool NAT
- 1 is V11() V12() ext-real non positive Element of REAL
M is non empty set
x is non empty FSM over M
the carrier of x is non empty set
M is non empty set
x is non empty FSM over M
the carrier of x is non empty set
y is Element of the carrier of x

(y,f) -admissible is V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x

(len f) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
M is non empty set
x is Element of M
<*x*> is non empty trivial V16() V19( NAT ) V20(M) Function-like V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of M
y is non empty FSM over M
the carrier of y is non empty set
[: the carrier of y,M:] is non empty set
the Tran of y is V16() V19([: the carrier of y,M:]) V20( the carrier of y) Function-like V30([: the carrier of y,M:], the carrier of y) Element of bool [:[: the carrier of y,M:], the carrier of y:]
[:[: the carrier of y,M:], the carrier of y:] is non empty set
bool [:[: the carrier of y,M:], the carrier of y:] is non empty set
f is Element of the carrier of y
(f,<*x*>) -admissible is non empty V16() V19( NAT ) V20( the carrier of y) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of y
[f,x] is non empty Element of [: the carrier of y,M:]
the Tran of y . [f,x] is Element of the carrier of y
<*f,( the Tran of y . [f,x])*> is non empty V16() V19( NAT ) V20( the carrier of y) Function-like V35() V42(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of y

() + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
((f,<*x*>) -admissible) . 1 is set
<*x*> . 1 is set

((f,<*x*>) -admissible) . (1 + 1) is set
M is Element of M
01 is Element of the carrier of y
m is Element of the carrier of y
M -succ_of 01 is Element of the carrier of y
[01,M] is non empty Element of [: the carrier of y,M:]
the Tran of y . [01,M] is Element of the carrier of y
M is non empty set
x is Element of M
y is Element of M
<*x,y*> is non empty V16() V19( NAT ) V20(M) Function-like V35() V42(2) FinSequence-like FinSubsequence-like FinSequence of M
f is non empty FSM over M
the carrier of f is non empty set
[: the carrier of f,M:] is non empty set
the Tran of f is V16() V19([: the carrier of f,M:]) V20( the carrier of f) Function-like V30([: the carrier of f,M:], the carrier of f) Element of bool [:[: the carrier of f,M:], the carrier of f:]
[:[: the carrier of f,M:], the carrier of f:] is non empty set
bool [:[: the carrier of f,M:], the carrier of f:] is non empty set
M is Element of the carrier of f
(M,<*x,y*>) -admissible is non empty V16() V19( NAT ) V20( the carrier of f) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of f
[M,x] is non empty Element of [: the carrier of f,M:]
the Tran of f . [M,x] is Element of the carrier of f
[( the Tran of f . [M,x]),y] is non empty Element of [: the carrier of f,M:]
the Tran of f . [( the Tran of f . [M,x]),y] is Element of the carrier of f
<*M,( the Tran of f . [M,x]),( the Tran of f . [( the Tran of f . [M,x]),y])*> is non empty V16() V19( NAT ) V20( the carrier of f) Function-like V35() V42(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of f
((M,<*x,y*>) -admissible) . 1 is set
<*x*> is non empty trivial V16() V19( NAT ) V20(M) Function-like V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of M
<*y*> is non empty trivial V16() V19( NAT ) V20(M) Function-like V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of M
<*x*> ^ <*y*> is non empty V16() V19( NAT ) V20(M) Function-like V35() V42(1 + 1) FinSequence-like FinSubsequence-like FinSequence of M

(M,<*x*>) -admissible is non empty V16() V19( NAT ) V20( the carrier of f) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of f
<*M,( the Tran of f . [M,x])*> is non empty V16() V19( NAT ) V20( the carrier of f) Function-like V35() V42(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of f

((M,<*x*>) -admissible) . (1 + 1) is set
((M,<*x,y*>) -admissible) . (1 + 1) is set

<*x,y*> . 2 is set
((M,<*x,y*>) -admissible) . 2 is set

((M,<*x,y*>) -admissible) . (2 + 1) is set
m is Element of M
m is Element of the carrier of f
w is Element of the carrier of f
m -succ_of m is Element of the carrier of f
[m,m] is non empty Element of [: the carrier of f,M:]
the Tran of f . [m,m] is Element of the carrier of f
len ((M,<*x,y*>) -admissible) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(len <*x,y*>) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
M is non empty set
x is Element of M
y is Element of M
f is Element of M
<*x,y,f*> is non empty V16() V19( NAT ) V20(M) Function-like V35() V42(3) FinSequence-like FinSubsequence-like FinSequence of M
M is non empty FSM over M
the carrier of M is non empty set
[: the carrier of M,M:] is non empty set
the Tran of M is V16() V19([: the carrier of M,M:]) V20( the carrier of M) Function-like V30([: the carrier of M,M:], the carrier of M) Element of bool [:[: the carrier of M,M:], the carrier of M:]
[:[: the carrier of M,M:], the carrier of M:] is non empty set
bool [:[: the carrier of M,M:], the carrier of M:] is non empty set
01 is Element of the carrier of M
(01,<*x,y,f*>) -admissible is non empty V16() V19( NAT ) V20( the carrier of M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of M
[01,x] is non empty Element of [: the carrier of M,M:]
the Tran of M . [01,x] is Element of the carrier of M
[( the Tran of M . [01,x]),y] is non empty Element of [: the carrier of M,M:]
the Tran of M . [( the Tran of M . [01,x]),y] is Element of the carrier of M
[( the Tran of M . [( the Tran of M . [01,x]),y]),f] is non empty Element of [: the carrier of M,M:]
the Tran of M . [( the Tran of M . [( the Tran of M . [01,x]),y]),f] is Element of the carrier of M
<*01,( the Tran of M . [01,x]),( the Tran of M . [( the Tran of M . [01,x]),y]),( the Tran of M . [( the Tran of M . [( the Tran of M . [01,x]),y]),f])*> is V16() V19( NAT ) V20( the carrier of M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of M
<*x,y*> is non empty V16() V19( NAT ) V20(M) Function-like V35() V42(2) FinSequence-like FinSubsequence-like FinSequence of M
<*f*> is non empty trivial V16() V19( NAT ) V20(M) Function-like V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of M

(01,m) -admissible is non empty V16() V19( NAT ) V20( the carrier of M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of M
<*01,( the Tran of M . [01,x]),( the Tran of M . [( the Tran of M . [01,x]),y])*> is non empty V16() V19( NAT ) V20( the carrier of M) Function-like V35() V42(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of M
(len m) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
((01,m) -admissible) . ((len m) + 1) is set
Del (((01,m) -admissible),((len m) + 1)) is V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set
(( the Tran of M . [( the Tran of M . [01,x]),y]),w) -admissible is non empty V16() V19( NAT ) V20( the carrier of M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of M
(Del (((01,m) -admissible),((len m) + 1))) ^ ((( the Tran of M . [( the Tran of M . [01,x]),y]),w) -admissible) is non empty V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set
Del (<*01,( the Tran of M . [01,x]),( the Tran of M . [( the Tran of M . [01,x]),y])*>,3) is V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set
<*01,( the Tran of M . [01,x])*> is non empty V16() V19( NAT ) V20( the carrier of M) Function-like V35() V42(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of M
<*( the Tran of M . [( the Tran of M . [01,x]),y]),( the Tran of M . [( the Tran of M . [( the Tran of M . [01,x]),y]),f])*> is non empty V16() V19( NAT ) V20( the carrier of M) Function-like V35() V42(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of M
<*01,( the Tran of M . [01,x])*> ^ <*( the Tran of M . [( the Tran of M . [01,x]),y]),( the Tran of M . [( the Tran of M . [( the Tran of M . [01,x]),y]),f])*> is non empty V16() V19( NAT ) V20( the carrier of M) Function-like V35() V42(2 + 2) FinSequence-like FinSubsequence-like FinSequence of the carrier of M

M is non empty set
M is non empty set
x is non empty FSM over M
the InitS of x is Element of the carrier of x
the carrier of x is non empty set

y . 1 is set
( the InitS of x,y) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x

f . 1 is set
( the InitS of x,f) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x

1 + (len y) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
Seg (1 + (len y)) is non empty V35() V42(1 + (len y)) Element of bool NAT

1 + (len f) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
Seg (1 + (len f)) is non empty V35() V42(1 + (len f)) Element of bool NAT
(Seg (1 + (len y))) /\ (Seg (1 + (len f))) is Element of bool NAT
len (( the InitS of x,y) -admissible) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
len (( the InitS of x,f) -admissible) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
dom (( the InitS of x,y) -admissible) is Element of bool NAT
dom (( the InitS of x,f) -admissible) is Element of bool NAT
01 is set

(( the InitS of x,y) -admissible) . 01 is set
(( the InitS of x,f) -admissible) . 01 is set
M is non empty set
x is non empty FSM over M
the InitS of x is Element of the carrier of x
the carrier of x is non empty set

f . 1 is set

(len f) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
( the InitS of x,f) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(( the InitS of x,f) -admissible) . y is set

M . 1 is set

(len M) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
( the InitS of x,M) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(( the InitS of x,M) -admissible) . y is set
dom (( the InitS of x,f) -admissible) is Element of bool NAT
len (( the InitS of x,f) -admissible) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
Seg (len (( the InitS of x,f) -admissible)) is non empty V35() V42( len (( the InitS of x,f) -admissible)) Element of bool NAT
Seg ((len f) + 1) is non empty V35() V42((len f) + 1) Element of bool NAT
dom (( the InitS of x,M) -admissible) is Element of bool NAT
len (( the InitS of x,M) -admissible) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
Seg (len (( the InitS of x,M) -admissible)) is non empty V35() V42( len (( the InitS of x,M) -admissible)) Element of bool NAT
Seg ((len M) + 1) is non empty V35() V42((len M) + 1) Element of bool NAT
(dom (( the InitS of x,f) -admissible)) /\ (dom (( the InitS of x,M) -admissible)) is Element of bool NAT
M is non empty set
x is non empty FSM over M
the InitS of x is Element of the carrier of x
the carrier of x is non empty set

y . 1 is set

( the InitS of x,y) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x

f . 1 is set

( the InitS of x,f) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
len (( the InitS of x,y) -admissible) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
1 + (len y) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
len (( the InitS of x,f) -admissible) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
1 + (len f) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
M is non empty set
x is non empty FSM over M
the carrier of x is non empty set
f is Element of the carrier of x

(f,y) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
dom ((f,y) -admissible) is Element of bool NAT
len ((f,y) -admissible) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
Seg (len ((f,y) -admissible)) is non empty V35() V42( len ((f,y) -admissible)) Element of bool NAT

(len y) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
Seg ((len y) + 1) is non empty V35() V42((len y) + 1) Element of bool NAT
((f,y) -admissible) . 1 is set
[1,f] is non empty Element of [:NAT, the carrier of x:]
[:NAT, the carrier of x:] is non empty V35() set
{[1,f]} is non empty trivial V16() V19( NAT ) V20( the carrier of x) V42(1) Element of bool [:NAT, the carrier of x:]
bool [:NAT, the carrier of x:] is non empty V35() set
<*f*> is non empty trivial V16() V19( NAT ) V20( the carrier of x) Function-like V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of x

[:NAT,M:] is non empty V35() set
(f,(<*> M)) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x

M . (len M) is set
x . 1 is set

f is set

M is set

(len 01) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT

(len y) + () is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(len y) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT

(Del (M,(len M))) ^ x is V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set
y ^ (<*M*> ^ 01) is non empty V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set

M ^ (Del (x,1)) is V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set
M is non empty set
x is non empty FSM over M
the InitS of x is Element of the carrier of x
the carrier of x is non empty set

y . 1 is set

f . 1 is set
( the InitS of x,y) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
( the InitS of x,f) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x

[:NAT,M:] is non empty V35() set

Seg (len y) is V35() V42( len y) Element of bool NAT
f | (Seg (len y)) is V16() V19( NAT ) V20(M) Function-like FinSubsequence-like Element of bool [:NAT,M:]
[:NAT,M:] is non empty V35() set
bool [:NAT,M:] is non empty V35() set

Seg (len f) is V35() V42( len f) Element of bool NAT
y | (Seg (len f)) is V16() V19( NAT ) V20(M) Function-like FinSubsequence-like Element of bool [:NAT,M:]

M . 1 is set
01 . 1 is set
( the InitS of x,M) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
( the InitS of x,01) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x

dom M is Element of bool NAT
dom f is Element of bool NAT
(dom f) /\ (Seg (len y)) is Element of bool NAT
(Seg (len f)) /\ (Seg (len y)) is Element of bool NAT
M . (len M) is set
(( the InitS of x,M) -admissible) . (len M) is set
(len M) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(( the InitS of x,M) -admissible) . ((len M) + 1) is set
dom 01 is Element of bool NAT
dom y is Element of bool NAT
(dom y) /\ (Seg (len f)) is Element of bool NAT
(Seg (len y)) /\ (Seg (len f)) is Element of bool NAT
01 . (len 01) is set
(( the InitS of x,01) -admissible) . (len 01) is set
(len 01) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(( the InitS of x,01) -admissible) . ((len 01) + 1) is set
WI2 is Element of M
QI2 is Element of the carrier of x
QI12 is Element of the carrier of x
WI2 -succ_of QI2 is Element of the carrier of x
[: the carrier of x,M:] is non empty set
the Tran of x is V16() V19([: the carrier of x,M:]) V20( the carrier of x) Function-like V30([: the carrier of x,M:], the carrier of x) Element of bool [:[: the carrier of x,M:], the carrier of x:]
[:[: the carrier of x,M:], the carrier of x:] is non empty set
bool [:[: the carrier of x,M:], the carrier of x:] is non empty set
[QI2,WI2] is non empty Element of [: the carrier of x,M:]
the Tran of x . [QI2,WI2] is Element of the carrier of x
c16 is Element of M
c17 is Element of the carrier of x
c18 is Element of the carrier of x
c16 -succ_of c17 is Element of the carrier of x
[c17,c16] is non empty Element of [: the carrier of x,M:]
the Tran of x . [c17,c16] is Element of the carrier of x
W is Element of the carrier of x

(W,w) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
((W,w) -admissible) . 1 is set
h is Element of the carrier of x

(h,w) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
((h,w) -admissible) . 1 is set
len (( the InitS of x,M) -admissible) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
len (( the InitS of x,01) -admissible) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
Del ((( the InitS of x,M) -admissible),((len M) + 1)) is V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set
(Del ((( the InitS of x,M) -admissible),((len M) + 1))) ^ ((W,w) -admissible) is non empty V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set
Del (((W,w) -admissible),1) is V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set
(( the InitS of x,M) -admissible) ^ (Del (((W,w) -admissible),1)) is non empty V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set
Del ((( the InitS of x,01) -admissible),((len 01) + 1)) is V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set
(Del ((( the InitS of x,01) -admissible),((len 01) + 1))) ^ ((h,w) -admissible) is non empty V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set
Del (((h,w) -admissible),1) is V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set
(( the InitS of x,01) -admissible) ^ (Del (((h,w) -admissible),1)) is non empty V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set

[:NAT,M:] is non empty V35() set
M is non empty set
x is non empty FSM over M
the carrier of x is non empty set
M is non empty set
x is non empty FSM over M
the carrier of x is non empty set
M is non empty set
x is Element of M
y is non empty FSM over M
the carrier of y is non empty set
f is Element of the carrier of y
<*x*> is non empty trivial V16() V19( NAT ) V20(M) Function-like V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of M
the InitS of y is Element of the carrier of y

<*x*> ^ M is non empty V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M
M is non empty set
x is non empty FSM over M
the carrier of x is non empty set
the InitS of x is Element of the carrier of x
y is Element of the carrier of x

( the InitS of x,f) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(len f) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(( the InitS of x,f) -admissible) . ((len f) + 1) is set
f . 1 is set
M is Element of M
<*M*> is non empty trivial V16() V19( NAT ) V20(M) Function-like V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of M

<*M*> ^ 01 is non empty V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M
M is non empty set
x is non empty FSM over M
the InitS of x is Element of the carrier of x
the carrier of x is non empty set

[:NAT,M:] is non empty V35() set
( the InitS of x,(<*> M)) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x

(len (<*> M)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(( the InitS of x,(<*> M)) -admissible) . ((len (<*> M)) + 1) is set
M is non empty set
x is Element of M
y is non empty FSM over M
the carrier of y is non empty set
the InitS of y is Element of the carrier of y
f is Element of the carrier of y
<*x*> is non empty trivial V16() V19( NAT ) V20(M) Function-like V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of M

<*x*> ^ M is non empty V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M
( the InitS of y,(<*x*> ^ M)) -admissible is non empty V16() V19( NAT ) V20( the carrier of y) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of y
len (<*x*> ^ M) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(len (<*x*> ^ M)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(( the InitS of y,(<*x*> ^ M)) -admissible) . ((len (<*x*> ^ M)) + 1) is set

(( the InitS of y,(<*x*> ^ M)) -admissible) . 01 is set

(len m) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
m . 1 is set
( the InitS of y,m) -admissible is non empty V16() V19( NAT ) V20( the carrier of y) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of y
(( the InitS of y,m) -admissible) . m is set
(<*x*> ^ M) . 1 is set
dom (( the InitS of y,(<*x*> ^ M)) -admissible) is Element of bool NAT
len (( the InitS of y,(<*x*> ^ M)) -admissible) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
Seg (len (( the InitS of y,(<*x*> ^ M)) -admissible)) is non empty V35() V42( len (( the InitS of y,(<*x*> ^ M)) -admissible)) Element of bool NAT
Seg ((len (<*x*> ^ M)) + 1) is non empty V35() V42((len (<*x*> ^ M)) + 1) Element of bool NAT
dom (( the InitS of y,m) -admissible) is Element of bool NAT
len (( the InitS of y,m) -admissible) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
Seg (len (( the InitS of y,m) -admissible)) is non empty V35() V42( len (( the InitS of y,m) -admissible)) Element of bool NAT
Seg ((len m) + 1) is non empty V35() V42((len m) + 1) Element of bool NAT

(( the InitS of y,m) -admissible) . w is set
(( the InitS of y,(<*x*> ^ M)) -admissible) . w is set
M is non empty set
M is non empty set
x is non empty FSM over M
the carrier of x is non empty set
[: the carrier of x,M:] is non empty set
the Tran of x is V16() V19([: the carrier of x,M:]) V20( the carrier of x) Function-like V30([: the carrier of x,M:], the carrier of x) Element of bool [:[: the carrier of x,M:], the carrier of x:]
[:[: the carrier of x,M:], the carrier of x:] is non empty set
bool [:[: the carrier of x,M:], the carrier of x:] is non empty set
the InitS of x is Element of the carrier of x

f . 1 is set

(len f) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
( the InitS of x,f) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(( the InitS of x,f) -admissible) . y is set

M . 1 is set

(len M) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
( the InitS of x,M) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(( the InitS of x,M) -admissible) . y is set

01 . 1 is set

(len 01) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
( the InitS of x,01) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(( the InitS of x,01) -admissible) . 1 is set

m . 1 is set

(len m) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
( the InitS of x,m) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(( the InitS of x,m) -admissible) . 1 is set

m . 1 is set

(len m) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
( the InitS of x,m) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(( the InitS of x,m) -admissible) . (01 + 1) is set

m . 1 is set

(len m) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
( the InitS of x,m) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(( the InitS of x,m) -admissible) . (01 + 1) is set
m . 01 is set
(( the InitS of x,m) -admissible) . 01 is set
w is Element of M
w is Element of the carrier of x
W is Element of the carrier of x
w -succ_of w is Element of the carrier of x
[w,w] is non empty Element of [: the carrier of x,M:]
the Tran of x . [w,w] is Element of the carrier of x
m . 01 is set
(( the InitS of x,m) -admissible) . 01 is set
h is Element of M
WI2 is Element of the carrier of x
QI2 is Element of the carrier of x
h -succ_of WI2 is Element of the carrier of x
[WI2,h] is non empty Element of [: the carrier of x,M:]
the Tran of x . [WI2,h] is Element of the carrier of x
M is non empty set
x is non empty FSM over M
the carrier of x is non empty set
the InitS of x is Element of the carrier of x
[: the carrier of x,M:] is non empty set
the Tran of x is V16() V19([: the carrier of x,M:]) V20( the carrier of x) Function-like V30([: the carrier of x,M:], the carrier of x) Element of bool [:[: the carrier of x,M:], the carrier of x:]
[:[: the carrier of x,M:], the carrier of x:] is non empty set
bool [:[: the carrier of x,M:], the carrier of x:] is non empty set

(len f) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
( the InitS of x,f) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(( the InitS of x,f) -admissible) . 2 is set

f . 1 is set
(( the InitS of x,f) -admissible) . 1 is set
(( the InitS of x,f) -admissible) . (1 + 1) is set
M is Element of M
01 is Element of the carrier of x
m is Element of the carrier of x
M -succ_of 01 is Element of the carrier of x
[01,M] is non empty Element of [: the carrier of x,M:]
the Tran of x . [01,M] is Element of the carrier of x

(len M) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
( the InitS of x,M) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(( the InitS of x,M) -admissible) . (f + 1) is set
M . f is set
(( the InitS of x,M) -admissible) . f is set
01 is Element of M
m is Element of the carrier of x
m is Element of the carrier of x
01 -succ_of m is Element of the carrier of x
[m,01] is non empty Element of [: the carrier of x,M:]
the Tran of x . [m,01] is Element of the carrier of x

(len f) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
( the InitS of x,f) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(( the InitS of x,f) -admissible) . y is set

f . 1 is set

(len f) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
( the InitS of x,f) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(( the InitS of x,f) -admissible) . y is set

M . 1 is set

(len M) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
( the InitS of x,M) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(( the InitS of x,M) -admissible) . y is set

01 . 1 is set

(len 01) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
( the InitS of x,01) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(( the InitS of x,01) -admissible) . 1 is set

m . 1 is set

(len m) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
( the InitS of x,m) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(( the InitS of x,m) -admissible) . 1 is set

m . 1 is set

(len m) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
( the InitS of x,m) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(( the InitS of x,m) -admissible) . (01 + 1) is set

m . 1 is set

(len m) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
( the InitS of x,m) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(( the InitS of x,m) -admissible) . (01 + 1) is set
m . 01 is set
(( the InitS of x,m) -admissible) . 01 is set
w is Element of M
w is Element of the carrier of x
W is Element of the carrier of x
w -succ_of w is Element of the carrier of x
[w,w] is non empty Element of [: the carrier of x,M:]
the Tran of x . [w,w] is Element of the carrier of x
m . 01 is set
(( the InitS of x,m) -admissible) . 01 is set
h is Element of M
WI2 is Element of the carrier of x
QI2 is Element of the carrier of x
h -succ_of WI2 is Element of the carrier of x
[WI2,h] is non empty Element of [: the carrier of x,M:]
the Tran of x . [WI2,h] is Element of the carrier of x

M is non empty set
x is non empty FSM over M
the carrier of x is non empty set
the InitS of x is Element of the carrier of x
y is Element of M
<*y*> is non empty trivial V16() V19( NAT ) V20(M) Function-like V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of M
f is Element of M
<*f*> is non empty trivial V16() V19( NAT ) V20(M) Function-like V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of M
M is Element of the carrier of x
(M,<*y*>) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
((M,<*y*>) -admissible) . 2 is set
(M,<*f*>) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
((M,<*f*>) -admissible) . 2 is set

( the InitS of x,01) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(len 01) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(( the InitS of x,01) -admissible) . ((len 01) + 1) is set
01 . 1 is set
m is Element of M
<*m*> is non empty trivial V16() V19( NAT ) V20(M) Function-like V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of M

<*m*> ^ m is non empty V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M
01 ^ <*y*> is non empty V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M
01 ^ <*f*> is non empty V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

() + (len m) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT

dom 01 is Element of bool NAT
(01 ^ <*y*>) . 1 is set
(01 ^ <*f*>) . 1 is set

len (01 ^ <*y*>) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(len 01) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT

len (01 ^ <*f*>) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
( the InitS of x,01) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
Del ((( the InitS of x,01) -admissible),((len 01) + 1)) is V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set
( the InitS of x,(01 ^ <*y*>)) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(Del ((( the InitS of x,01) -admissible),((len 01) + 1))) ^ ((M,<*y*>) -admissible) is non empty V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set
len (( the InitS of x,01) -admissible) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
len (Del ((( the InitS of x,01) -admissible),((len 01) + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V35() V40() Element of NAT

() + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT

len (( the InitS of x,(01 ^ <*y*>)) -admissible) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
len ((Del ((( the InitS of x,01) -admissible),((len 01) + 1))) ^ ((M,<*y*>) -admissible)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(len (Del ((( the InitS of x,01) -admissible),((len 01) + 1)))) + (len ((M,<*y*>) -admissible)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(len 01) + (1 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
((len 01) + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(len (01 ^ <*y*>)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(len (Del ((( the InitS of x,01) -admissible),((len 01) + 1)))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(( the InitS of x,(01 ^ <*y*>)) -admissible) . ((len (01 ^ <*y*>)) + 1) is set
((len (01 ^ <*y*>)) + 1) - (len (Del ((( the InitS of x,01) -admissible),((len 01) + 1)))) is V11() V12() ext-real Element of REAL
((M,<*y*>) -admissible) . (((len (01 ^ <*y*>)) + 1) - (len (Del ((( the InitS of x,01) -admissible),((len 01) + 1))))) is set
((len (01 ^ <*y*>)) + 1) - (len 01) is V11() V12() ext-real Element of REAL
((M,<*y*>) -admissible) . (((len (01 ^ <*y*>)) + 1) - (len 01)) is set
(((len 01) + 1) + 1) - (len 01) is V11() V12() ext-real Element of REAL
((M,<*y*>) -admissible) . ((((len 01) + 1) + 1) - (len 01)) is set
( the InitS of x,(01 ^ <*f*>)) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(Del ((( the InitS of x,01) -admissible),((len 01) + 1))) ^ ((M,<*f*>) -admissible) is non empty V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set

() + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
len (( the InitS of x,(01 ^ <*f*>)) -admissible) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
len ((Del ((( the InitS of x,01) -admissible),((len 01) + 1))) ^ ((M,<*f*>) -admissible)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(len (Del ((( the InitS of x,01) -admissible),((len 01) + 1)))) + (len ((M,<*f*>) -admissible)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(len (01 ^ <*f*>)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(( the InitS of x,(01 ^ <*f*>)) -admissible) . ((len (01 ^ <*f*>)) + 1) is set
((len (01 ^ <*f*>)) + 1) - (len (Del ((( the InitS of x,01) -admissible),((len 01) + 1)))) is V11() V12() ext-real Element of REAL
((M,<*f*>) -admissible) . (((len (01 ^ <*f*>)) + 1) - (len (Del ((( the InitS of x,01) -admissible),((len 01) + 1))))) is set
((len (01 ^ <*f*>)) + 1) - (len 01) is V11() V12() ext-real Element of REAL
((M,<*f*>) -admissible) . (((len (01 ^ <*f*>)) + 1) - (len 01)) is set
((M,<*f*>) -admissible) . ((((len 01) + 1) + 1) - (len 01)) is set
M is non empty set
x is non empty FSM over M
the carrier of x is non empty set
the InitS of x is Element of the carrier of x
[: the carrier of x,M:] is non empty set
the Tran of x is V16() V19([: the carrier of x,M:]) V20( the carrier of x) Function-like V30([: the carrier of x,M:], the carrier of x) Element of bool [:[: the carrier of x,M:], the carrier of x:]
[:[: the carrier of x,M:], the carrier of x:] is non empty set
bool [:[: the carrier of x,M:], the carrier of x:] is non empty set
y is Element of M
f is Element of M
M is Element of the carrier of x
[M,y] is non empty Element of [: the carrier of x,M:]
the Tran of x . [M,y] is Element of the carrier of x
[M,f] is non empty Element of [: the carrier of x,M:]
the Tran of x . [M,f] is Element of the carrier of x
<*y*> is non empty trivial V16() V19( NAT ) V20(M) Function-like V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of M
<*f*> is non empty trivial V16() V19( NAT ) V20(M) Function-like V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of M

<*y*> . m is set
(M,<*y*>) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
((M,<*y*>) -admissible) . m is set

((M,<*y*>) -admissible) . (m + 1) is set
w is Element of M
w is Element of the carrier of x
W is Element of the carrier of x
w -succ_of w is Element of the carrier of x
[w,w] is non empty Element of [: the carrier of x,M:]
the Tran of x . [w,w] is Element of the carrier of x
y -succ_of M is Element of the carrier of x

<*f*> . h is set
(M,<*f*>) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
((M,<*f*>) -admissible) . h is set

((M,<*f*>) -admissible) . (h + 1) is set
WI2 is Element of M
QI2 is Element of the carrier of x
QI12 is Element of the carrier of x
WI2 -succ_of QI2 is Element of the carrier of x
[QI2,WI2] is non empty Element of [: the carrier of x,M:]
the Tran of x . [QI2,WI2] is Element of the carrier of x
M is non empty set
x is non empty FSM over M
the carrier of x is non empty set
[: the carrier of x,M:] is non empty set
the Tran of x is V16() V19([: the carrier of x,M:]) V20( the carrier of x) Function-like V30([: the carrier of x,M:], the carrier of x) Element of bool [:[: the carrier of x,M:], the carrier of x:]
[:[: the carrier of x,M:], the carrier of x:] is non empty set
bool [:[: the carrier of x,M:], the carrier of x:] is non empty set
the InitS of x is Element of the carrier of x
y is Element of M
f is Element of M
[ the InitS of x,f] is non empty Element of [: the carrier of x,M:]
the Tran of x . [ the InitS of x,f] is Element of the carrier of x
M is Element of M
[ the InitS of x,M] is non empty Element of [: the carrier of x,M:]
the Tran of x . [ the InitS of x,M] is Element of the carrier of x
01 is Element of the carrier of x
[01,y] is non empty Element of [: the carrier of x,M:]
the Tran of x . [01,y] is Element of the carrier of x

( the InitS of x,m) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x

(len m) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(( the InitS of x,m) -admissible) . ((len m) + 1) is set
<*y,f*> is non empty V16() V19( NAT ) V20(M) Function-like V35() V42(2) FinSequence-like FinSubsequence-like FinSequence of M
<*y,M*> is non empty V16() V19( NAT ) V20(M) Function-like V35() V42(2) FinSequence-like FinSubsequence-like FinSequence of M

(01,m) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
<*01, the InitS of x,( the Tran of x . [ the InitS of x,f])*> is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() V42(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of x

(01,w) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
<*01, the InitS of x,( the Tran of x . [ the InitS of x,M])*> is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() V42(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of x
((01,m) -admissible) . 3 is set
((01,w) -admissible) . 3 is set

(len m) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(len w) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT

( the InitS of x,(m ^ m)) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(len m) + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(( the InitS of x,(m ^ m)) -admissible) . ((len m) + 3) is set

( the InitS of x,(m ^ w)) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
(( the InitS of x,(m ^ w)) -admissible) . ((len m) + 3) is set
( the InitS of x,m) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
[ the InitS of x,y] is non empty Element of [: the carrier of x,M:]
the Tran of x . [ the InitS of x,y] is Element of the carrier of x
[( the Tran of x . [ the InitS of x,y]),f] is non empty Element of [: the carrier of x,M:]
the Tran of x . [( the Tran of x . [ the InitS of x,y]),f] is Element of the carrier of x
<* the InitS of x,( the Tran of x . [ the InitS of x,y]),( the Tran of x . [( the Tran of x . [ the InitS of x,y]),f])*> is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() V42(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of x
( the InitS of x,w) -admissible is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of x
[( the Tran of x . [ the InitS of x,y]),M] is non empty Element of [: the carrier of x,M:]
the Tran of x . [( the Tran of x . [ the InitS of x,y]),M] is Element of the carrier of x
<* the InitS of x,( the Tran of x . [ the InitS of x,y]),( the Tran of x . [( the Tran of x . [ the InitS of x,y]),M])*> is non empty V16() V19( NAT ) V20( the carrier of x) Function-like V35() V42(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of x
m . 1 is set
w . 1 is set
(( the InitS of x,m) -admissible) . 3 is set
(( the InitS of x,w) -admissible) . 3 is set
w is set

(len W) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
dom <*w*> is non empty trivial V42(1) Element of bool NAT
m . 1 is set
<*w*> . 1 is set
dom m is Element of bool NAT
(m ^ m) . 1 is set
(m ^ w) . 1 is set

(len (m ^ m)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(len m) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
((len m) + 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35()