:: FSM_2 semantic presentation

REAL is non empty V35() set

NAT is non empty epsilon-transitive epsilon-connected ordinal V35() V40() V41() Element of bool REAL

bool REAL is non empty V35() set

COMPLEX is non empty V35() set

omega is non empty epsilon-transitive epsilon-connected ordinal V35() V40() V41() 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

{} is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() ext-real non positive non negative functional V35() V40() V42( {} ) FinSequence-membered set

the empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() ext-real non positive non negative functional V35() V40() V42( {} ) FinSequence-membered set is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() ext-real non positive non negative functional V35() V40() V42( {} ) FinSequence-membered set

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

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

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

0 is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() ext-real non positive non negative functional V35() V40() V42( {} ) FinSequence-membered Element of NAT

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

f is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

(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 ((y,f) -admissible) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V35() V40() Element of NAT

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

(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

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

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

(len <*x*>) + 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

1 + 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 + 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

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

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

(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

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

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

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

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

<*x,y*> . 2 is set

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

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

((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

m is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

w is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

m ^ w is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

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

(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

2 + 2 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

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 is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

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 is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

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 y is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real 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

Seg (1 + (len y)) is non empty V35() V42(1 + (len y)) Element of bool NAT

len f is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real 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

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

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

(( 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

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

f is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

f . 1 is set

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

(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 is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

M . 1 is set

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

(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 is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

y . 1 is set

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

( 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 is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

f . 1 is set

len f is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real 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

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

y is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

(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 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real 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

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

<*> M is empty trivial proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() ext-real non positive non negative V16() V19( NAT ) V20(M) Function-like functional V35() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of M

[: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 is V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set

x is V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set

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

M . (len M) is set

x . 1 is set

y is V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set

f is set

<*f*> is non empty trivial V16() V19( NAT ) Function-like V35() V42(1) FinSequence-like FinSubsequence-like set

y ^ <*f*> is non empty V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set

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

M is set

<*M*> is non empty trivial V16() V19( NAT ) Function-like V35() V42(1) FinSequence-like FinSubsequence-like set

01 is V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set

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

len 01 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real 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 y is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V35() V40() Element of NAT

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

(len y) + (len <*f*>) 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)) is V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set

(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 ^ 01 is V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set

Del (x,1) is 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 is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

y . 1 is set

f is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

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

<*> M is empty trivial proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() ext-real non positive non negative V16() V19( NAT ) V20(M) Function-like functional V35() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of M

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

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

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

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

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 is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

01 is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

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

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

0 + 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

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

m is V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set

M ^ m is V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set

m is V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set

01 ^ m is V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set

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

c

c

c

c

[c

the Tran of x . [c

W is Element of the carrier of x

w is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

(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

w is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

(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

<*> M is empty trivial proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() ext-real non positive non negative V16() V19( NAT ) V20(M) Function-like functional V35() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of M

[: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

M is V16() V19( NAT ) V20(M) Function-like V35() 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

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

f is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

len f is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real 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

(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

01 is V16() V19( NAT ) V20(M) Function-like V35() 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

<*> M is empty trivial proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() ext-real non positive non negative V16() V19( NAT ) V20(M) Function-like functional V35() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of M

[: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) is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() ext-real non positive non negative functional V35() V40() V42( {} ) FinSequence-membered Element of NAT

(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

M is V16() V19( NAT ) V20(M) Function-like V35() 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

01 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V35() V40() set

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

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

m is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

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

(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

w 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,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

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

f is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

f . 1 is set

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

(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 is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

M . 1 is set

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

(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 is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

01 . 1 is set

len 01 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real 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

( 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 is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

m . 1 is set

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

(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

01 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() set

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

m is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

m . 1 is set

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

(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 is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

m . 1 is set

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

(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

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

f is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

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

(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

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

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

f is non empty non trivial epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() set

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 V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

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

(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

f is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

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

(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

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

f is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

f . 1 is set

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

(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 is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

M . 1 is set

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

(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 is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

01 . 1 is set

len 01 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real 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

( 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 is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

m . 1 is set

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

(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

01 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() set

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

m is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

m . 1 is set

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

(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 is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

m . 1 is set

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

(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

1 + 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 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

01 is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

len 01 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real 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

(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 is V16() V19( NAT ) V20(M) Function-like V35() 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

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

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

len 01 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real 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 <*y*> is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT

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 <*f*> 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

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 <*y*>) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT

1 + 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

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 <*f*>) + 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

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

0 + 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 epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT

<*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 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT

((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

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

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

<*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

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

((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

m is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

( 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 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V35() V40() Element of NAT

(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

m is V16() V19( NAT ) V20(M) Function-like V35() 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

w is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

(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 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V35() V40() Element of NAT

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

(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

m ^ m is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

( 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

m ^ w is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M

( 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

<*w*> is non empty trivial V16() V19( NAT ) Function-like V35() V42(1) FinSequence-like FinSubsequence-like set

W is V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set

<*w*> ^ W is non empty V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set

len W is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real 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

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) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V35() V40() Element of NAT

(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()