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
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 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() V40() Element of NAT
len (m ^ w) is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V35() V40() Element of NAT
(len (m ^ w)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
M is set
the non empty set is non empty set
[: the non empty set ,M:] is set
[:[: the non empty set ,M:], the non empty set :] is set
bool [:[: the non empty set ,M:], the non empty set :] is non empty set
the V16() V19([: the non empty set ,M:]) V20( the non empty set ) Function-like V30([: the non empty set ,M:], the non empty set ) Element of bool [:[: the non empty set ,M:], the non empty set :] is V16() V19([: the non empty set ,M:]) V20( the non empty set ) Function-like V30([: the non empty set ,M:], the non empty set ) Element of bool [:[: the non empty set ,M:], the non empty set :]
the Element of the non empty set is Element of the non empty set
bool the non empty set is non empty set
the Element of bool the non empty set is Element of bool the non empty set
(M, the non empty set , the V16() V19([: the non empty set ,M:]) V20( the non empty set ) Function-like V30([: the non empty set ,M:], the non empty set ) Element of bool [:[: the non empty set ,M:], the non empty set :], the Element of the non empty set , the Element of bool the non empty set ) is (M) (M)
01 is (M) (M)
the carrier of 01 is set
M is non empty set
M is non empty set
M is set
x is non empty set
the non empty set is non empty set
[: the non empty set ,M:] is set
[:[: the non empty set ,M:], the non empty set :] is set
bool [:[: the non empty set ,M:], the non empty set :] is non empty set
the V16() V19([: the non empty set ,M:]) V20( the non empty set ) Function-like V30([: the non empty set ,M:], the non empty set ) Element of bool [:[: the non empty set ,M:], the non empty set :] is V16() V19([: the non empty set ,M:]) V20( the non empty set ) Function-like V30([: the non empty set ,M:], the non empty set ) Element of bool [:[: the non empty set ,M:], the non empty set :]
[: the non empty set ,x:] is non empty set
bool [: the non empty set ,x:] is non empty set
the V16() V19( the non empty set ) V20(x) Function-like V30( the non empty set ,x) Element of bool [: the non empty set ,x:] is V16() V19( the non empty set ) V20(x) Function-like V30( the non empty set ,x) Element of bool [: the non empty set ,x:]
the Element of the non empty set is Element of the non empty set
bool the non empty set is non empty set
the Element of bool the non empty set is Element of bool the non empty set
(M,x, the non empty set , the V16() V19([: the non empty set ,M:]) V20( the non empty set ) Function-like V30([: the non empty set ,M:], the non empty set ) Element of bool [:[: the non empty set ,M:], the non empty set :], the V16() V19( the non empty set ) V20(x) Function-like V30( the non empty set ,x) Element of bool [: the non empty set ,x:], the Element of the non empty set , the Element of bool the non empty set ) is (M,x) (M,x)
m is (M,x) (M,x)
the carrier of m is set
y is set
f is set
{y,f} is non empty set
x is non empty set
[:{y,f},x:] is non empty set
bool [:{y,f},x:] is non empty set
M is non empty set
[:{y,f},M:] is non empty set
{f} is non empty trivial V42(1) set
[:{y,f},M:] --> f is V16() V19([:{y,f},M:]) V20({f}) Function-like V30([:{y,f},M:],{f}) Element of bool [:[:{y,f},M:],{f}:]
[:[:{y,f},M:],{f}:] is non empty set
bool [:[:{y,f},M:],{f}:] is non empty set
M is V16() V19({y,f}) V20(x) Function-like V30({y,f},x) Element of bool [:{y,f},x:]
01 is non empty (M,x) (M,x)
the carrier of 01 is non empty set
[: the carrier of 01,M:] is non empty set
the Tran of 01 is V16() V19([: the carrier of 01,M:]) V20( the carrier of 01) Function-like V30([: the carrier of 01,M:], the carrier of 01) Element of bool [:[: the carrier of 01,M:], the carrier of 01:]
[:[: the carrier of 01,M:], the carrier of 01:] is non empty set
bool [:[: the carrier of 01,M:], the carrier of 01:] is non empty set
the OFun of 01 is V16() V19( the carrier of 01) V20(x) Function-like V30( the carrier of 01,x) Element of bool [: the carrier of 01,x:]
[: the carrier of 01,x:] is non empty set
bool [: the carrier of 01,x:] is non empty set
the InitS of 01 is Element of the carrier of 01
the of 01 is Element of bool the carrier of 01
bool the carrier of 01 is non empty set
m is non empty (M,x) (M,x)
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
the OFun of m is V16() V19( the carrier of m) V20(x) Function-like V30( the carrier of m,x) Element of bool [: the carrier of m,x:]
[: the carrier of m,x:] is non empty set
bool [: the carrier of m,x:] is non empty set
the InitS of m is Element of the carrier of m
the of m is Element of bool the carrier of m
bool the carrier of m is non empty set
m is Element of {y,f}
[:{y,f},M:] --> m is V16() V19([:{y,f},M:]) V20({y,f}) Function-like V30([:{y,f},M:],{y,f}) Element of bool [:[:{y,f},M:],{y,f}:]
[:[:{y,f},M:],{y,f}:] is non empty set
bool [:[:{y,f},M:],{y,f}:] is non empty set
w is V16() V19({y,f}) V20(x) Function-like V30({y,f},x) Element of bool [:{y,f},x:]
m is Element of {y,f}
{m} is non empty trivial V42(1) Element of bool {y,f}
bool {y,f} is non empty set
(M,x,{y,f},([:{y,f},M:] --> m),w,m,{m}) is (M,x) (M,x)
M is non empty set
x is non empty set
y is V16() V19( NAT ) V20(x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of x
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
f is set
M is set
{f,M} is non empty set
[:{f,M},M:] is non empty set
bool [:{f,M},M:] is non empty set
01 is V16() V19({f,M}) V20(M) Function-like V30({f,M},M) Element of bool [:{f,M},M:]
(x,M,f,M,01) is non empty (x,M) (x,M)
the InitS of (x,M,f,M,01) is Element of the carrier of (x,M,f,M,01)
the carrier of (x,M,f,M,01) is non empty set
( the InitS of (x,M,f,M,01),y) -admissible is non empty V16() V19( NAT ) V20( the carrier of (x,M,f,M,01)) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of (x,M,f,M,01)
m 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,f,M,01),y) -admissible) . m is set
[: the carrier of (x,M,f,M,01),x:] is non empty set
[:{f,M},x:] is non empty set
{M} is non empty trivial V42(1) set
the Tran of (x,M,f,M,01) is V16() V19([: the carrier of (x,M,f,M,01),x:]) V20( the carrier of (x,M,f,M,01)) Function-like V30([: the carrier of (x,M,f,M,01),x:], the carrier of (x,M,f,M,01)) Element of bool [:[: the carrier of (x,M,f,M,01),x:], the carrier of (x,M,f,M,01):]
[:[: the carrier of (x,M,f,M,01),x:], the carrier of (x,M,f,M,01):] is non empty set
bool [:[: the carrier of (x,M,f,M,01),x:], the carrier of (x,M,f,M,01):] is non empty set
[:{f,M},x:] --> M is V16() V19([:{f,M},x:]) V20({M}) Function-like V30([:{f,M},x:],{M}) Element of bool [:[:{f,M},x:],{M}:]
[:[:{f,M},x:],{M}:] is non empty set
bool [:[:{f,M},x:],{M}:] is non empty set
(( the InitS of (x,M,f,M,01),y) -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
y . 1 is set
(( the InitS of (x,M,f,M,01),y) -admissible) . 1 is set
(( the InitS of (x,M,f,M,01),y) -admissible) . (1 + 1) is set
w is Element of x
w is Element of the carrier of (x,M,f,M,01)
W is Element of the carrier of (x,M,f,M,01)
w -succ_of w is Element of the carrier of (x,M,f,M,01)
[w,w] is non empty Element of [: the carrier of (x,M,f,M,01),x:]
the Tran of (x,M,f,M,01) . [w,w] is Element of the carrier of (x,M,f,M,01)
w is non empty non trivial epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() set
(( the InitS of (x,M,f,M,01),y) -admissible) . w is set
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,f,M,01),y) -admissible) . (w + 1) is set
y . w is set
w is Element of x
W is Element of the carrier of (x,M,f,M,01)
h is Element of the carrier of (x,M,f,M,01)
w -succ_of W is Element of the carrier of (x,M,f,M,01)
[W,w] is non empty Element of [: the carrier of (x,M,f,M,01),x:]
the Tran of (x,M,f,M,01) . [W,w] is Element of the carrier of (x,M,f,M,01)
y is set
f is set
{y,f} is non empty set
x is non empty set
[:{y,f},x:] is non empty set
bool [:{y,f},x:] is non empty set
M is non empty set
M is V16() V19({y,f}) V20(x) Function-like V30({y,f},x) Element of bool [:{y,f},x:]
(M,x,y,f,M) is non empty (M,x) (M,x)
the InitS of (M,x,y,f,M) is Element of the carrier of (M,x,y,f,M)
the carrier of (M,x,y,f,M) is non empty 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
( the InitS of (M,x,y,f,M),m) -admissible is non empty V16() V19( NAT ) V20( the carrier of (M,x,y,f,M)) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of (M,x,y,f,M)
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
( the InitS of (M,x,y,f,M),m) -admissible is non empty V16() V19( NAT ) V20( the carrier of (M,x,y,f,M)) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of (M,x,y,f,M)
w is V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set
w . 1 is set
w is V16() V19( NAT ) Function-like V35() FinSequence-like FinSubsequence-like set
w . 1 is set
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 is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V35() V40() Element of NAT
W is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V35() V40() set
w . W is set
w . W is set
y is set
f is set
{y,f} is non empty set
x is non empty set
[:{y,f},x:] is non empty set
bool [:{y,f},x:] is non empty set
M is non empty set
M is V16() V19({y,f}) V20(x) Function-like V30({y,f},x) Element of bool [:{y,f},x:]
(M,x,y,f,M) is non empty (M) (M,x) (M,x)
01 is Element of M
the carrier of (M,x,y,f,M) is non empty set
m is Element of the carrier of (M,x,y,f,M)
the of (M,x,y,f,M) is Element of bool the carrier of (M,x,y,f,M)
bool the carrier of (M,x,y,f,M) is non empty set
[:NAT,M:] is non empty V35() 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
<*01*> is non empty trivial V16() V19( NAT ) V20(M) Function-like V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of M
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
<*01*> ^ m is non empty V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M
the InitS of (M,x,y,f,M) is Element of the carrier of (M,x,y,f,M)
len (<*01*> ^ m) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
( the InitS of (M,x,y,f,M),(<*01*> ^ m)) -admissible is non empty V16() V19( NAT ) V20( the carrier of (M,x,y,f,M)) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of (M,x,y,f,M)
(len (<*01*> ^ 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 (M,x,y,f,M),(<*01*> ^ m)) -admissible) . ((len (<*01*> ^ m)) + 1) is set
{f} is non empty trivial V42(1) set
M is non empty set
x is non empty set
y is Element of x
f is non empty (x,M)
the InitS of f is Element of the carrier of f
the carrier of f is non empty set
the of f is Element of bool the carrier of f
bool the carrier of f is non empty set
M is Element of the carrier of f
<*y*> is non empty trivial V16() V19( NAT ) V20(x) Function-like V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of x
01 is V16() V19( NAT ) V20(x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of x
<*y*> ^ 01 is non empty V16() V19( NAT ) V20(x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of x
( the InitS of f,(<*y*> ^ 01)) -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
len (<*y*> ^ 01) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(len (<*y*> ^ 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 f,(<*y*> ^ 01)) -admissible) . ((len (<*y*> ^ 01)) + 1) is set
m is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V35() V40() set
(( the InitS of f,(<*y*> ^ 01)) -admissible) . m is set
m is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
w is V16() V19( NAT ) V20(x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of x
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
w . 1 is set
(<*y*> ^ 01) . 1 is set
( the InitS of f,w) -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
dom (( the InitS of f,(<*y*> ^ 01)) -admissible) is Element of bool NAT
len (( the InitS of f,(<*y*> ^ 01)) -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 f,(<*y*> ^ 01)) -admissible)) is non empty V35() V42( len (( the InitS of f,(<*y*> ^ 01)) -admissible)) Element of bool NAT
Seg ((len (<*y*> ^ 01)) + 1) is non empty V35() V42((len (<*y*> ^ 01)) + 1) Element of bool NAT
dom (( the InitS of f,w) -admissible) is Element of bool NAT
len (( the InitS of f,w) -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 f,w) -admissible)) is non empty V35() V42( len (( the InitS of f,w) -admissible)) Element of bool NAT
Seg ((len w) + 1) is non empty V35() V42((len w) + 1) Element of bool NAT
(( the InitS of f,w) -admissible) . m is set
w is V16() V19( NAT ) V20(x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of x
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
w . 1 is set
( the InitS of f,w) -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
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 f,w) -admissible) . w is set
dom (( the InitS of f,w) -admissible) is Element of bool NAT
len (( the InitS of f,w) -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 f,w) -admissible)) is non empty V35() V42( len (( the InitS of f,w) -admissible)) Element of bool NAT
Seg ((len w) + 1) is non empty V35() V42((len w) + 1) Element of bool NAT
(( the InitS of f,(<*y*> ^ 01)) -admissible) . w is set
M is non empty set
x is non empty set
M is non empty set
x is non empty set
y is Element of M
f is non empty (M,x)
the InitS of f is Element of the carrier of f
the carrier of f is non empty set
the of f is Element of bool the carrier of f
bool the carrier of f is non empty set
the OFun of f is V16() V19( the carrier of f) V20(x) Function-like V30( the carrier of f,x) Element of bool [: the carrier of f,x:]
[: the carrier of f,x:] is non empty set
bool [: the carrier of f,x:] is non empty set
the OFun of f . the InitS of f is Element of x
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 f,M) -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
(( the InitS of f,M) -admissible) . 1 is set
the OFun of f . ((( the InitS of f,M) -admissible) . 1) is set
01 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(( the InitS of f,M) -admissible) . 01 is set
M is non empty set
x is non empty set
y is Element of M
f is non empty (M,x)
the carrier of f is non empty set
the of f is Element of bool the carrier of f
bool the carrier of f is non empty set
M is Element of the carrier of f
<*y*> is non empty trivial V16() V19( NAT ) V20(M) Function-like V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of M
the InitS of f is Element of the carrier of f
01 is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M
<*y*> ^ 01 is non empty V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M
( the InitS of f,(<*y*> ^ 01)) -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
len (<*y*> ^ 01) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(len (<*y*> ^ 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 f,(<*y*> ^ 01)) -admissible) . ((len (<*y*> ^ 01)) + 1) is set
m is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(<*y*> ^ 01) . 1 is set
(( the InitS of f,(<*y*> ^ 01)) -admissible) . m is set
the OFun of f is V16() V19( the carrier of f) V20(x) Function-like V30( the carrier of f,x) Element of bool [: the carrier of f,x:]
[: the carrier of f,x:] is non empty set
bool [: the carrier of f,x:] is non empty set
the OFun of f . ((( the InitS of f,(<*y*> ^ 01)) -admissible) . m) is set
m is Element of x
w is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M
w . 1 is 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
( the InitS of f,w) -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
(( the InitS of f,w) -admissible) . m is set
the OFun of f . ((( the InitS of f,w) -admissible) . m) is set
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 f,w) -admissible) . w is set
M is non empty set
x is non empty set
y is Element of M
f is non empty (M,x)
M is Element of x
01 is Element of x
the OFun of f is V16() V19( the carrier of f) V20(x) Function-like V30( the carrier of f,x) Element of bool [: the carrier of f,x:]
the carrier of f is non empty set
[: the carrier of f,x:] is non empty set
bool [: the carrier of f,x:] is non empty set
the InitS of f is Element of the carrier of f
the of f is Element of bool the carrier of f
bool the carrier of f is non empty 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 non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
w is Element of the carrier of f
<*y*> is non empty trivial V16() V19( NAT ) V20(M) Function-like V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of M
w is V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M
<*y*> ^ w is non empty V16() V19( NAT ) V20(M) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of M
( the InitS of f,(<*y*> ^ w)) -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
len (<*y*> ^ w) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
(len (<*y*> ^ 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 f,(<*y*> ^ w)) -admissible) . ((len (<*y*> ^ w)) + 1) is set
(<*y*> ^ w) . 1 is set
(( the InitS of f,(<*y*> ^ w)) -admissible) . m is set
the OFun of f . ((( the InitS of f,(<*y*> ^ w)) -admissible) . m) is set
(( the InitS of f,(<*y*> ^ w)) -admissible) . m is set
M is non empty set
[:M,M:] is non empty set
[:[:M,M:],M:] is non empty set
bool [:[:M,M:],M:] is non empty set
succ M is non empty set
{M} is non empty trivial V42(1) set
M \/ {M} is non empty set
x is V16() V19([:M,M:]) V20(M) Function-like V30([:M,M:],M) Element of bool [:[:M,M:],M:]
y is non empty ([:M,M:], succ M)
the carrier of y is non empty set
the of y is Element of bool the carrier of y
bool the carrier of y is non empty set
the InitS of y is Element of the carrier of y
the OFun of y is V16() V19( the carrier of y) V20( succ M) Function-like V30( the carrier of y, succ M) Element of bool [: the carrier of y,(succ M):]
[: the carrier of y,(succ M):] is non empty set
bool [: the carrier of y,(succ M):] is non empty set
id the carrier of y is non empty V16() V19( the carrier of y) V20( the carrier of y) total Element of bool [: the carrier of y, the carrier of y:]
[: the carrier of y, the carrier of y:] is non empty set
bool [: the carrier of y, the carrier of y:] is non empty set
[: the carrier of y,[:M,M:]:] is non empty set
the Tran of y is V16() V19([: the carrier of y,[:M,M:]:]) V20( the carrier of y) Function-like V30([: the carrier of y,[:M,M:]:], the carrier of y) Element of bool [:[: the carrier of y,[:M,M:]:], the carrier of y:]
[:[: the carrier of y,[:M,M:]:], the carrier of y:] is non empty set
bool [:[: the carrier of y,[:M,M:]:], the carrier of y:] is non empty set
f is Element of [:M,M:]
M is set
01 is set
[M,01] is non empty set
m is Element of M
m is Element of M
x . (m,m) is Element of M
w is Element of the carrier of y
[:NAT,[:M,M:]:] is non empty V35() set
<*> [:M,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,M:]) Function-like functional V35() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of [:M,M:]
<*f*> is non empty trivial V16() V19( NAT ) V20([:M,M:]) Function-like V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of [:M,M:]
w 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,M:]) Function-like functional V35() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of [:M,M:]
<*f*> ^ w is non empty V16() V19( NAT ) V20([:M,M:]) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:M,M:]
W is V16() V19( NAT ) V20([:M,M:]) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:M,M:]
[m,m] is non empty Element of [:M,M:]
<*[m,m]*> is non empty trivial V16() V19( NAT ) V20([:M,M:]) Function-like V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of [:M,M:]
len W is epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real non negative V35() V40() Element of NAT
W . 1 is set
( the InitS of y,W) -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,W) -admissible) . 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
(( the InitS of y,W) -admissible) . (1 + 1) 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
(( the InitS of y,W) -admissible) . ((len W) + 1) is set
[ the InitS of y,(W . 1)] is non empty set
the Tran of y . [ the InitS of y,(W . 1)] is set
[ the InitS of y,[m,m]] is non empty Element of [: the carrier of y,[:M,M:]:]
the Tran of y . [ the InitS of y,[m,m]] is Element of the carrier of y
h is Element of [:M,M:]
WI2 is Element of the carrier of y
QI2 is Element of the carrier of y
h -succ_of WI2 is Element of the carrier of y
[WI2,h] is non empty Element of [: the carrier of y,[:M,M:]:]
the Tran of y . [WI2,h] is Element of the carrier of y
f is Element of M
M is Element of M
[f,M] is non empty Element of [:M,M:]
x . (f,M) is Element of M
01 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
w is V16() V19( NAT ) V20([:M,M:]) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of [:M,M:]
w . 1 is 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
( the InitS of y,w) -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,w) -admissible) . 01 is set
the OFun of y . ((( the InitS of y,w) -admissible) . 01) is set
(( the InitS of y,w) -admissible) . 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
(( the InitS of y,w) -admissible) . (1 + 1) is set
(( the InitS of y,w) -admissible) . 2 is set
[ the InitS of y,(w . 1)] is non empty set
the Tran of y . [ the InitS of y,(w . 1)] is set
w is Element of [:M,M:]
W is Element of the carrier of y
h is Element of the carrier of y
w -succ_of W is Element of the carrier of y
[W,w] is non empty Element of [: the carrier of y,[:M,M:]:]
the Tran of y . [W,w] is Element of the carrier of y
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,w) -admissible) . w is set
[:REAL,REAL:] is non empty V35() set
succ REAL is non empty set
{REAL} is non empty trivial V42(1) set
REAL \/ {REAL} is non empty set
[:[:REAL,REAL:],REAL:] is non empty V35() set
bool [:[:REAL,REAL:],REAL:] is non empty V35() set
M is V16() V19([:REAL,REAL:]) V20( REAL ) Function-like V30([:REAL,REAL:], REAL ) Element of bool [:[:REAL,REAL:],REAL:]
x is non empty ([:REAL,REAL:], succ REAL)
the carrier of x is non empty set
the of x is Element of bool the carrier of x
bool the carrier of x is non empty set
the InitS of x is Element of the carrier of x
the OFun of x is V16() V19( the carrier of x) V20( succ REAL) Function-like V30( the carrier of x, succ REAL) Element of bool [: the carrier of x,(succ REAL):]
[: the carrier of x,(succ REAL):] is non empty set
bool [: the carrier of x,(succ REAL):] is non empty set
id the carrier of x is non empty V16() V19( the carrier of x) V20( the carrier of x) total Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
[: the carrier of x,[:REAL,REAL:]:] is non empty V35() set
the Tran of x is V16() V19([: the carrier of x,[:REAL,REAL:]:]) V20( the carrier of x) Function-like V30([: the carrier of x,[:REAL,REAL:]:], the carrier of x) Element of bool [:[: the carrier of x,[:REAL,REAL:]:], the carrier of x:]
[:[: the carrier of x,[:REAL,REAL:]:], the carrier of x:] is non empty V35() set
bool [:[: the carrier of x,[:REAL,REAL:]:], the carrier of x:] is non empty V35() set
y is V11() V12() ext-real Element of REAL
f is V11() V12() ext-real Element of REAL
[y,f] is non empty Element of [:REAL,REAL:]
max (y,f) is V11() V12() ext-real Element of REAL
01 is V11() V12() ext-real Element of REAL
M is V11() V12() ext-real Element of REAL
[M,01] is non empty Element of [:REAL,REAL:]
[ the InitS of x,[M,01]] is non empty Element of [: the carrier of x,[:REAL,REAL:]:]
the Tran of x . [ the InitS of x,[M,01]] is Element of the carrier of x
max (M,01) is V11() V12() ext-real Element of REAL
M . (M,01) is V11() V12() ext-real Element of REAL
M . (y,f) is V11() V12() ext-real Element of REAL
[:[:REAL,REAL:],REAL:] is non empty V35() set
bool [:[:REAL,REAL:],REAL:] is non empty V35() set
M is V16() V19([:REAL,REAL:]) V20( REAL ) Function-like V30([:REAL,REAL:], REAL ) Element of bool [:[:REAL,REAL:],REAL:]
x is non empty ([:REAL,REAL:], succ REAL)
the carrier of x is non empty set
the of x is Element of bool the carrier of x
bool the carrier of x is non empty set
the InitS of x is Element of the carrier of x
the OFun of x is V16() V19( the carrier of x) V20( succ REAL) Function-like V30( the carrier of x, succ REAL) Element of bool [: the carrier of x,(succ REAL):]
[: the carrier of x,(succ REAL):] is non empty set
bool [: the carrier of x,(succ REAL):] is non empty set
id the carrier of x is non empty V16() V19( the carrier of x) V20( the carrier of x) total Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
[: the carrier of x,[:REAL,REAL:]:] is non empty V35() set
the Tran of x is V16() V19([: the carrier of x,[:REAL,REAL:]:]) V20( the carrier of x) Function-like V30([: the carrier of x,[:REAL,REAL:]:], the carrier of x) Element of bool [:[: the carrier of x,[:REAL,REAL:]:], the carrier of x:]
[:[: the carrier of x,[:REAL,REAL:]:], the carrier of x:] is non empty V35() set
bool [:[: the carrier of x,[:REAL,REAL:]:], the carrier of x:] is non empty V35() set
y is V11() V12() ext-real Element of REAL
f is V11() V12() ext-real Element of REAL
[y,f] is non empty Element of [:REAL,REAL:]
min (y,f) is V11() V12() ext-real Element of REAL
01 is V11() V12() ext-real Element of REAL
M is V11() V12() ext-real Element of REAL
[M,01] is non empty Element of [:REAL,REAL:]
[ the InitS of x,[M,01]] is non empty Element of [: the carrier of x,[:REAL,REAL:]:]
the Tran of x . [ the InitS of x,[M,01]] is Element of the carrier of x
min (M,01) is V11() V12() ext-real Element of REAL
M . (M,01) is V11() V12() ext-real Element of REAL
M . (y,f) is V11() V12() ext-real Element of REAL
[:[:REAL,REAL:],REAL:] is non empty V35() set
bool [:[:REAL,REAL:],REAL:] is non empty V35() set
M is V16() V19([:REAL,REAL:]) V20( REAL ) Function-like V30([:REAL,REAL:], REAL ) Element of bool [:[:REAL,REAL:],REAL:]
x is non empty ([:REAL,REAL:], succ REAL)
the carrier of x is non empty set
the of x is Element of bool the carrier of x
bool the carrier of x is non empty set
the InitS of x is Element of the carrier of x
the OFun of x is V16() V19( the carrier of x) V20( succ REAL) Function-like V30( the carrier of x, succ REAL) Element of bool [: the carrier of x,(succ REAL):]
[: the carrier of x,(succ REAL):] is non empty set
bool [: the carrier of x,(succ REAL):] is non empty set
id the carrier of x is non empty V16() V19( the carrier of x) V20( the carrier of x) total Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
[: the carrier of x,[:REAL,REAL:]:] is non empty V35() set
the Tran of x is V16() V19([: the carrier of x,[:REAL,REAL:]:]) V20( the carrier of x) Function-like V30([: the carrier of x,[:REAL,REAL:]:], the carrier of x) Element of bool [:[: the carrier of x,[:REAL,REAL:]:], the carrier of x:]
[:[: the carrier of x,[:REAL,REAL:]:], the carrier of x:] is non empty V35() set
bool [:[: the carrier of x,[:REAL,REAL:]:], the carrier of x:] is non empty V35() set
y is V11() V12() ext-real Element of REAL
f is V11() V12() ext-real Element of REAL
[y,f] is non empty Element of [:REAL,REAL:]
y + f is V11() V12() ext-real Element of REAL
M is V11() V12() ext-real Element of REAL
01 is V11() V12() ext-real Element of REAL
[M,01] is non empty Element of [:REAL,REAL:]
[ the InitS of x,[M,01]] is non empty Element of [: the carrier of x,[:REAL,REAL:]:]
the Tran of x . [ the InitS of x,[M,01]] is Element of the carrier of x
M + 01 is V11() V12() ext-real Element of REAL
M . (M,01) is V11() V12() ext-real Element of REAL
M . (y,f) is V11() V12() ext-real Element of REAL
[:[:REAL,REAL:],REAL:] is non empty V35() set
bool [:[:REAL,REAL:],REAL:] is non empty V35() set
M is V16() V19([:REAL,REAL:]) V20( REAL ) Function-like V30([:REAL,REAL:], REAL ) Element of bool [:[:REAL,REAL:],REAL:]
x is non empty ([:REAL,REAL:], succ REAL)
the carrier of x is non empty set
the of x is Element of bool the carrier of x
bool the carrier of x is non empty set
the InitS of x is Element of the carrier of x
the OFun of x is V16() V19( the carrier of x) V20( succ REAL) Function-like V30( the carrier of x, succ REAL) Element of bool [: the carrier of x,(succ REAL):]
[: the carrier of x,(succ REAL):] is non empty set
bool [: the carrier of x,(succ REAL):] is non empty set
id the carrier of x is non empty V16() V19( the carrier of x) V20( the carrier of x) total Element of bool [: the carrier of x, the carrier of x:]
[: the carrier of x, the carrier of x:] is non empty set
bool [: the carrier of x, the carrier of x:] is non empty set
[: the carrier of x,[:REAL,REAL:]:] is non empty V35() set
the Tran of x is V16() V19([: the carrier of x,[:REAL,REAL:]:]) V20( the carrier of x) Function-like V30([: the carrier of x,[:REAL,REAL:]:], the carrier of x) Element of bool [:[: the carrier of x,[:REAL,REAL:]:], the carrier of x:]
[:[: the carrier of x,[:REAL,REAL:]:], the carrier of x:] is non empty V35() set
bool [:[: the carrier of x,[:REAL,REAL:]:], the carrier of x:] is non empty V35() set
y is V11() V12() ext-real Element of REAL
sgn y is V11() V12() ext-real Element of REAL
f is V11() V12() ext-real Element of REAL
[y,f] is non empty Element of [:REAL,REAL:]
sgn f is V11() V12() ext-real Element of REAL
max ((sgn y),(sgn f)) is V11() V12() ext-real Element of REAL
M is V11() V12() ext-real Element of REAL
01 is V11() V12() ext-real Element of REAL
[M,01] is non empty Element of [:REAL,REAL:]
[ the InitS of x,[M,01]] is non empty Element of [: the carrier of x,[:REAL,REAL:]:]
the Tran of x . [ the InitS of x,[M,01]] is Element of the carrier of x
sgn M is V11() V12() ext-real Element of REAL
sgn 01 is V11() V12() ext-real Element of REAL
max ((sgn M),(sgn 01)) is V11() V12() ext-real Element of REAL
M . (M,01) is V11() V12() ext-real Element of REAL
M . (y,f) is V11() V12() ext-real Element of REAL
M is non empty set
x is non empty set
{0,1} is non empty Element of bool NAT
[:{0,1},x:] is non empty set
bool [:{0,1},x:] is non empty set
the V16() V19({0,1}) V20(x) Function-like V30({0,1},x) Element of bool [:{0,1},x:] is V16() V19({0,1}) V20(x) Function-like V30({0,1},x) Element of bool [:{0,1},x:]
(M,x,0,1, the V16() V19({0,1}) V20(x) Function-like V30({0,1},x) Element of bool [:{0,1},x:]) is non empty (M) (M) (M,x) (M,x)
M is non empty set
the non empty set is non empty set
the non empty (M) (M) (M, the non empty set ) is non empty (M) (M) (M, the non empty set )
M is non empty set
x is non empty set
f is Element of M
y is non empty (M) (M) (M,x)
M is Element of x
01 is Element of x
{0,1} is non empty Element of bool NAT
M is non empty set
[:{0,1},M:] is non empty set
bool [:{0,1},M:] is non empty set
x is non empty set
y is Element of x
f is V16() V19({0,1}) V20(M) Function-like V30({0,1},M) Element of bool [:{0,1},M:]
(x,M,0,1,f) is non empty (x) (x) (x,M) (x,M)
(x,M,(x,M,0,1,f),y) is Element of M
f . 1 is set
the of (x,M,0,1,f) is Element of bool the carrier of (x,M,0,1,f)
the carrier of (x,M,0,1,f) is non empty set
bool the carrier of (x,M,0,1,f) is non empty set
{1} is non empty trivial V42(1) Element of bool NAT
the OFun of (x,M,0,1,f) is V16() V19( the carrier of (x,M,0,1,f)) V20(M) Function-like V30( the carrier of (x,M,0,1,f),M) Element of bool [: the carrier of (x,M,0,1,f),M:]
[: the carrier of (x,M,0,1,f),M:] is non empty set
bool [: the carrier of (x,M,0,1,f),M:] is non empty set
the InitS of (x,M,0,1,f) is Element of the carrier of (x,M,0,1,f)
m is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive non negative V35() V40() Element of NAT
w is V16() V19( NAT ) V20(x) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of x
w . 1 is set
m is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() ext-real positive 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 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,0,1,f),w) -admissible is non empty V16() V19( NAT ) V20( the carrier of (x,M,0,1,f)) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of (x,M,0,1,f)
(( the InitS of (x,M,0,1,f),w) -admissible) . m is set
the OFun of (x,M,0,1,f) . ((( the InitS of (x,M,0,1,f),w) -admissible) . m) is set
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 (x,M,0,1,f),w) -admissible) . w is set
01 is Element of {0,1}
f . 01 is Element of M
m 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 ([:REAL,REAL:]) ([:REAL,REAL:]) ([:REAL,REAL:], succ REAL)
the carrier of M is non empty set
the of M is Element of bool the carrier of M
bool the carrier of M is non empty set
the InitS of M is Element of the carrier of M
the OFun of M is V16() V19( the carrier of M) V20( succ REAL) Function-like V30( the carrier of M, succ REAL) Element of bool [: the carrier of M,(succ REAL):]
[: the carrier of M,(succ REAL):] is non empty set
bool [: the carrier of M,(succ REAL):] is non empty set
id the carrier of M is non empty V16() V19( the carrier of M) V20( the carrier of M) total Element of bool [: the carrier of M, the carrier of M:]
[: the carrier of M, the carrier of M:] is non empty set
bool [: the carrier of M, the carrier of M:] is non empty set
[: the carrier of M,[:REAL,REAL:]:] is non empty V35() set
the Tran of M is V16() V19([: the carrier of M,[:REAL,REAL:]:]) V20( the carrier of M) Function-like V30([: the carrier of M,[:REAL,REAL:]:], the carrier of M) Element of bool [:[: the carrier of M,[:REAL,REAL:]:], the carrier of M:]
[:[: the carrier of M,[:REAL,REAL:]:], the carrier of M:] is non empty V35() set
bool [:[: the carrier of M,[:REAL,REAL:]:], the carrier of M:] is non empty V35() set
x is V11() V12() ext-real Element of REAL
y is V11() V12() ext-real Element of REAL
[x,y] is non empty Element of [:REAL,REAL:]
([:REAL,REAL:],(succ REAL),M,[x,y]) is Element of succ REAL
max (x,y) is V11() V12() ext-real Element of REAL
M is non empty ([:REAL,REAL:]) ([:REAL,REAL:]) ([:REAL,REAL:], succ REAL)
the carrier of M is non empty set
the of M is Element of bool the carrier of M
bool the carrier of M is non empty set
the InitS of M is Element of the carrier of M
the OFun of M is V16() V19( the carrier of M) V20( succ REAL) Function-like V30( the carrier of M, succ REAL) Element of bool [: the carrier of M,(succ REAL):]
[: the carrier of M,(succ REAL):] is non empty set
bool [: the carrier of M,(succ REAL):] is non empty set
id the carrier of M is non empty V16() V19( the carrier of M) V20( the carrier of M) total Element of bool [: the carrier of M, the carrier of M:]
[: the carrier of M, the carrier of M:] is non empty set
bool [: the carrier of M, the carrier of M:] is non empty set
[: the carrier of M,[:REAL,REAL:]:] is non empty V35() set
the Tran of M is V16() V19([: the carrier of M,[:REAL,REAL:]:]) V20( the carrier of M) Function-like V30([: the carrier of M,[:REAL,REAL:]:], the carrier of M) Element of bool [:[: the carrier of M,[:REAL,REAL:]:], the carrier of M:]
[:[: the carrier of M,[:REAL,REAL:]:], the carrier of M:] is non empty V35() set
bool [:[: the carrier of M,[:REAL,REAL:]:], the carrier of M:] is non empty V35() set
x is V11() V12() ext-real Element of REAL
y is V11() V12() ext-real Element of REAL
[x,y] is non empty Element of [:REAL,REAL:]
([:REAL,REAL:],(succ REAL),M,[x,y]) is Element of succ REAL
min (x,y) is V11() V12() ext-real Element of REAL
M is non empty ([:REAL,REAL:]) ([:REAL,REAL:]) ([:REAL,REAL:], succ REAL)
the carrier of M is non empty set
the of M is Element of bool the carrier of M
bool the carrier of M is non empty set
the InitS of M is Element of the carrier of M
the OFun of M is V16() V19( the carrier of M) V20( succ REAL) Function-like V30( the carrier of M, succ REAL) Element of bool [: the carrier of M,(succ REAL):]
[: the carrier of M,(succ REAL):] is non empty set
bool [: the carrier of M,(succ REAL):] is non empty set
id the carrier of M is non empty V16() V19( the carrier of M) V20( the carrier of M) total Element of bool [: the carrier of M, the carrier of M:]
[: the carrier of M, the carrier of M:] is non empty set
bool [: the carrier of M, the carrier of M:] is non empty set
[: the carrier of M,[:REAL,REAL:]:] is non empty V35() set
the Tran of M is V16() V19([: the carrier of M,[:REAL,REAL:]:]) V20( the carrier of M) Function-like V30([: the carrier of M,[:REAL,REAL:]:], the carrier of M) Element of bool [:[: the carrier of M,[:REAL,REAL:]:], the carrier of M:]
[:[: the carrier of M,[:REAL,REAL:]:], the carrier of M:] is non empty V35() set
bool [:[: the carrier of M,[:REAL,REAL:]:], the carrier of M:] is non empty V35() set
x is V11() V12() ext-real Element of REAL
y is V11() V12() ext-real Element of REAL
[x,y] is non empty Element of [:REAL,REAL:]
([:REAL,REAL:],(succ REAL),M,[x,y]) is Element of succ REAL
x + y is V11() V12() ext-real Element of REAL
M is non empty ([:REAL,REAL:]) ([:REAL,REAL:]) ([:REAL,REAL:], succ REAL)
the carrier of M is non empty set
the of M is Element of bool the carrier of M
bool the carrier of M is non empty set
the InitS of M is Element of the carrier of M
the OFun of M is V16() V19( the carrier of M) V20( succ REAL) Function-like V30( the carrier of M, succ REAL) Element of bool [: the carrier of M,(succ REAL):]
[: the carrier of M,(succ REAL):] is non empty set
bool [: the carrier of M,(succ REAL):] is non empty set
id the carrier of M is non empty V16() V19( the carrier of M) V20( the carrier of M) total Element of bool [: the carrier of M, the carrier of M:]
[: the carrier of M, the carrier of M:] is non empty set
bool [: the carrier of M, the carrier of M:] is non empty set
[: the carrier of M,[:REAL,REAL:]:] is non empty V35() set
the Tran of M is V16() V19([: the carrier of M,[:REAL,REAL:]:]) V20( the carrier of M) Function-like V30([: the carrier of M,[:REAL,REAL:]:], the carrier of M) Element of bool [:[: the carrier of M,[:REAL,REAL:]:], the carrier of M:]
[:[: the carrier of M,[:REAL,REAL:]:], the carrier of M:] is non empty V35() set
bool [:[: the carrier of M,[:REAL,REAL:]:], the carrier of M:] is non empty V35() set
x is V11() V12() ext-real Element of REAL
sgn x is V11() V12() ext-real Element of REAL
y is V11() V12() ext-real Element of REAL
[x,y] is non empty Element of [:REAL,REAL:]
([:REAL,REAL:],(succ REAL),M,[x,y]) is Element of succ REAL
sgn y is V11() V12() ext-real Element of REAL
max ((sgn x),(sgn y)) is V11() V12() ext-real Element of REAL