REAL is V35() V36() V37() V41() set
NAT is non trivial V23() V35() V36() V37() V38() V39() V40() V41() non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty set
COMPLEX is V35() V41() set
NAT is non trivial V23() V35() V36() V37() V38() V39() V40() V41() non finite cardinal limit_cardinal set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
K304() is L6()
the carrier of K304() is set
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V23() V27() V28() V29() ext-real non positive non negative integer V35() V36() V37() V38() V39() V40() V41() finite finite-yielding V48() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V23() V27() V28() V29() ext-real non positive non negative integer V35() V36() V37() V38() V39() V40() V41() finite finite-yielding V48() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V23() V27() V28() V29() ext-real non positive non negative integer V35() V36() V37() V38() V39() V40() V41() finite finite-yielding V48() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
2 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
3 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V23() V27() V28() V29() ext-real non positive non negative integer V35() V36() V37() V38() V39() V40() V41() finite finite-yielding V48() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
Seg 1 is non empty trivial V35() V36() V37() V38() V39() V40() finite 1 -element Element of bool NAT
{1} is non empty trivial V35() V36() V37() V38() V39() V40() finite V48() 1 -element set
Seg 2 is non empty V35() V36() V37() V38() V39() V40() finite 2 -element Element of bool NAT
{1,2} is non empty V35() V36() V37() V38() V39() V40() finite V48() set
IAlph is set
IAlph is set
the non empty finite set is non empty finite set
[: the non empty finite set ,IAlph:] is Relation-like set
[:[: the non empty finite set ,IAlph:], the non empty finite set :] is Relation-like set
bool [:[: the non empty finite set ,IAlph:], the non empty finite set :] is non empty set
the Relation-like [: the non empty finite set ,IAlph:] -defined the non empty finite set -valued Function-like V14([: the non empty finite set ,IAlph:]) quasi_total Element of bool [:[: the non empty finite set ,IAlph:], the non empty finite set :] is Relation-like [: the non empty finite set ,IAlph:] -defined the non empty finite set -valued Function-like V14([: the non empty finite set ,IAlph:]) quasi_total Element of bool [:[: the non empty finite set ,IAlph:], the non empty finite set :]
the Element of the non empty finite set is Element of the non empty finite set
(IAlph, the non empty finite set , the Relation-like [: the non empty finite set ,IAlph:] -defined the non empty finite set -valued Function-like V14([: the non empty finite set ,IAlph:]) quasi_total Element of bool [:[: the non empty finite set ,IAlph:], the non empty finite set :], the Element of the non empty finite set ) is (IAlph) (IAlph)
rtfsm2 is (IAlph) (IAlph)
IAlph is non empty set
OAlph is non empty (IAlph)
the carrier of OAlph is non empty set
[: the carrier of OAlph,IAlph:] is Relation-like non empty set
the of OAlph is Relation-like [: the carrier of OAlph,IAlph:] -defined the carrier of OAlph -valued Function-like non empty V14([: the carrier of OAlph,IAlph:]) quasi_total Element of bool [:[: the carrier of OAlph,IAlph:], the carrier of OAlph:]
[:[: the carrier of OAlph,IAlph:], the carrier of OAlph:] is Relation-like non empty set
bool [:[: the carrier of OAlph,IAlph:], the carrier of OAlph:] is non empty set
M2 is Element of the carrier of OAlph
M1 is Element of IAlph
[M2,M1] is V15() Element of [: the carrier of OAlph,IAlph:]
{M2,M1} is non empty finite set
{M2} is non empty trivial finite 1 -element set
{{M2,M1},{M2}} is non empty finite V48() set
the of OAlph . [M2,M1] is Element of the carrier of OAlph
IAlph is non empty set
OAlph is non empty (IAlph)
the carrier of OAlph is non empty set
M1 is Element of the carrier of OAlph
M2 is Relation-like NAT -defined IAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of IAlph
len M2 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len M2) + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
fsm1 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
M2 . fsm1 is set
dom M2 is V35() V36() V37() V38() V39() V40() finite Element of bool NAT
Srtfsm1 is Element of the carrier of OAlph
fsm2 is Element of IAlph
(IAlph,OAlph,fsm2,Srtfsm1) is Element of the carrier of OAlph
[: the carrier of OAlph,IAlph:] is Relation-like non empty set
the of OAlph is Relation-like [: the carrier of OAlph,IAlph:] -defined the carrier of OAlph -valued Function-like non empty V14([: the carrier of OAlph,IAlph:]) quasi_total Element of bool [:[: the carrier of OAlph,IAlph:], the carrier of OAlph:]
[:[: the carrier of OAlph,IAlph:], the carrier of OAlph:] is Relation-like non empty set
bool [:[: the carrier of OAlph,IAlph:], the carrier of OAlph:] is non empty set
[Srtfsm1,fsm2] is V15() Element of [: the carrier of OAlph,IAlph:]
{Srtfsm1,fsm2} is non empty finite set
{Srtfsm1} is non empty trivial finite 1 -element set
{{Srtfsm1,fsm2},{Srtfsm1}} is non empty finite V48() set
the of OAlph . [Srtfsm1,fsm2] is Element of the carrier of OAlph
fsm1 is Relation-like NAT -defined the carrier of OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of OAlph
len fsm1 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
fsm1 . 1 is set
fsm2 is V23() V27() V28() V29() ext-real non negative integer finite cardinal set
M2 . fsm2 is set
fsm1 . fsm2 is set
fsm2 + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
fsm1 . (fsm2 + 1) is set
rtfsm2 is Relation-like NAT -defined the carrier of OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of OAlph
rtfsm2 . 1 is set
len rtfsm2 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
rtfsm1 is Relation-like NAT -defined the carrier of OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of OAlph
rtfsm1 . 1 is set
len rtfsm1 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
fsm1 is V23() V27() V28() V29() ext-real non negative integer finite cardinal set
rtfsm2 . fsm1 is set
rtfsm1 . fsm1 is set
fsm1 + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
rtfsm2 . (fsm1 + 1) is set
rtfsm1 . (fsm1 + 1) is set
0 + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
M2 . fsm1 is set
fsm2 is Element of IAlph
Srtfsm1 is Element of the carrier of OAlph
Srtfsm2 is Element of the carrier of OAlph
(IAlph,OAlph,fsm2,Srtfsm1) is Element of the carrier of OAlph
[: the carrier of OAlph,IAlph:] is Relation-like non empty set
the of OAlph is Relation-like [: the carrier of OAlph,IAlph:] -defined the carrier of OAlph -valued Function-like non empty V14([: the carrier of OAlph,IAlph:]) quasi_total Element of bool [:[: the carrier of OAlph,IAlph:], the carrier of OAlph:]
[:[: the carrier of OAlph,IAlph:], the carrier of OAlph:] is Relation-like non empty set
bool [:[: the carrier of OAlph,IAlph:], the carrier of OAlph:] is non empty set
[Srtfsm1,fsm2] is V15() Element of [: the carrier of OAlph,IAlph:]
{Srtfsm1,fsm2} is non empty finite set
{Srtfsm1} is non empty trivial finite 1 -element set
{{Srtfsm1,fsm2},{Srtfsm1}} is non empty finite V48() set
the of OAlph . [Srtfsm1,fsm2] is Element of the carrier of OAlph
ISrtfsm1 is Element of IAlph
ISrtfsm2 is Element of the carrier of OAlph
Sfsm1 is Element of the carrier of OAlph
(IAlph,OAlph,ISrtfsm1,ISrtfsm2) is Element of the carrier of OAlph
[ISrtfsm2,ISrtfsm1] is V15() Element of [: the carrier of OAlph,IAlph:]
{ISrtfsm2,ISrtfsm1} is non empty finite set
{ISrtfsm2} is non empty trivial finite 1 -element set
{{ISrtfsm2,ISrtfsm1},{ISrtfsm2}} is non empty finite V48() set
the of OAlph . [ISrtfsm2,ISrtfsm1] is Element of the carrier of OAlph
rtfsm2 . 0 is set
rtfsm1 . 0 is set
IAlph is non empty set
<*> IAlph is Relation-like non-empty empty-yielding NAT -defined IAlph -valued Function-like one-to-one constant functional empty V23() V27() V28() V29() ext-real non positive non negative integer V35() V36() V37() V38() V39() V40() V41() finite finite-yielding V48() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of IAlph
OAlph is non empty (IAlph)
the carrier of OAlph is non empty set
M1 is Element of the carrier of OAlph
(IAlph,OAlph,M1,(<*> IAlph)) is Relation-like NAT -defined the carrier of OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of OAlph
<*M1*> is Relation-like NAT -defined the carrier of OAlph -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of OAlph
len (<*> IAlph) is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V23() V27() V28() V29() ext-real non positive non negative integer V35() V36() V37() V38() V39() V40() V41() finite finite-yielding V48() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
rtfsm2 is V23() V27() V28() V29() ext-real non negative integer finite cardinal set
(<*> IAlph) . rtfsm2 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V23() V27() V28() V29() ext-real non positive non negative integer V35() V36() V37() V38() V39() V40() V41() finite finite-yielding V48() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
<*M1*> . rtfsm2 is set
rtfsm2 + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
<*M1*> . (rtfsm2 + 1) is set
len <*M1*> is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len (<*> IAlph)) + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
<*M1*> . 1 is set
IAlph is non empty set
OAlph is non empty (IAlph)
the carrier of OAlph is non empty set
IAlph is non empty set
<*> IAlph is Relation-like non-empty empty-yielding NAT -defined IAlph -valued Function-like one-to-one constant functional empty V23() V27() V28() V29() ext-real non positive non negative integer V35() V36() V37() V38() V39() V40() V41() finite finite-yielding V48() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of IAlph
OAlph is non empty (IAlph)
the carrier of OAlph is non empty set
M1 is Element of the carrier of OAlph
<*M1*> is Relation-like NAT -defined the carrier of OAlph -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of OAlph
len (<*> IAlph) is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V23() V27() V28() V29() ext-real non positive non negative integer V35() V36() V37() V38() V39() V40() V41() finite finite-yielding V48() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
(len (<*> IAlph)) + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
<*M1*> . ((len (<*> IAlph)) + 1) is set
0 + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
<*M1*> . (0 + 1) is set
(IAlph,OAlph,M1,(<*> IAlph)) is Relation-like NAT -defined the carrier of OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of OAlph
IAlph is non empty set
OAlph is non empty (IAlph)
the carrier of OAlph is non empty set
IAlph is non empty set
<*> IAlph is Relation-like non-empty empty-yielding NAT -defined IAlph -valued Function-like one-to-one constant functional empty V23() V27() V28() V29() ext-real non positive non negative integer V35() V36() V37() V38() V39() V40() V41() finite finite-yielding V48() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of IAlph
OAlph is non empty (IAlph)
the carrier of OAlph is non empty set
M1 is Element of the carrier of OAlph
<*M1*> is Relation-like NAT -defined the carrier of OAlph -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of OAlph
(IAlph,OAlph,M1,(<*> IAlph)) is Relation-like NAT -defined the carrier of OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of OAlph
<*M1*> . 1 is set
IAlph is non empty set
OAlph is non empty (IAlph)
the carrier of OAlph is non empty set
M2 is Relation-like NAT -defined IAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of IAlph
M1 is Element of the carrier of OAlph
(IAlph,OAlph,M1,M2) is Relation-like NAT -defined the carrier of OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of OAlph
len (IAlph,OAlph,M1,M2) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
len M2 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len M2) + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
Seg ((len M2) + 1) is non empty V35() V36() V37() V38() V39() V40() finite (len M2) + 1 -element Element of bool NAT
dom (IAlph,OAlph,M1,M2) is V35() V36() V37() V38() V39() V40() finite Element of bool NAT
(IAlph,OAlph,M1,M2) . ((len M2) + 1) is set
rtfsm2 is Element of the carrier of OAlph
rtfsm2 is Element of the carrier of OAlph
rtfsm1 is Element of the carrier of OAlph
(IAlph,OAlph,M1,M2) is Relation-like NAT -defined the carrier of OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of OAlph
len M2 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len M2) + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(IAlph,OAlph,M1,M2) . ((len M2) + 1) is set
IAlph is non empty set
OAlph is non empty (IAlph)
the carrier of OAlph is non empty set
M1 is Relation-like NAT -defined IAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of IAlph
M2 is Element of the carrier of OAlph
(IAlph,OAlph,M2,M1) is Relation-like NAT -defined the carrier of OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of OAlph
len (IAlph,OAlph,M2,M1) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(IAlph,OAlph,M2,M1) . (len (IAlph,OAlph,M2,M1)) is set
rtfsm2 is Element of the carrier of OAlph
len M1 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len M1) + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(IAlph,OAlph,M2,M1) . ((len M1) + 1) is set
IAlph is non empty set
OAlph is non empty (IAlph)
the carrier of OAlph is non empty set
M1 is Relation-like NAT -defined IAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of IAlph
len M1 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
M2 is Relation-like NAT -defined IAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of IAlph
M1 ^ M2 is Relation-like NAT -defined IAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of IAlph
rtfsm2 is Element of the carrier of OAlph
(IAlph,OAlph,rtfsm2,(M1 ^ M2)) is Relation-like NAT -defined the carrier of OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of OAlph
(IAlph,OAlph,rtfsm2,M1) is Relation-like NAT -defined the carrier of OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of OAlph
fsm2 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(IAlph,OAlph,rtfsm2,(M1 ^ M2)) . fsm2 is set
(IAlph,OAlph,rtfsm2,M1) . fsm2 is set
fsm2 + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(IAlph,OAlph,rtfsm2,(M1 ^ M2)) . (fsm2 + 1) is set
(IAlph,OAlph,rtfsm2,M1) . (fsm2 + 1) is set
0 + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
len M2 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len M1) + (len M2) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
len (M1 ^ M2) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(M1 ^ M2) . fsm2 is set
M1 . fsm2 is set
dom M1 is V35() V36() V37() V38() V39() V40() finite Element of bool NAT
Srtfsm1 is Element of IAlph
Srtfsm2 is Element of the carrier of OAlph
ISrtfsm1 is Element of the carrier of OAlph
(IAlph,OAlph,Srtfsm1,Srtfsm2) is Element of the carrier of OAlph
[: the carrier of OAlph,IAlph:] is Relation-like non empty set
the of OAlph is Relation-like [: the carrier of OAlph,IAlph:] -defined the carrier of OAlph -valued Function-like non empty V14([: the carrier of OAlph,IAlph:]) quasi_total Element of bool [:[: the carrier of OAlph,IAlph:], the carrier of OAlph:]
[:[: the carrier of OAlph,IAlph:], the carrier of OAlph:] is Relation-like non empty set
bool [:[: the carrier of OAlph,IAlph:], the carrier of OAlph:] is non empty set
[Srtfsm2,Srtfsm1] is V15() Element of [: the carrier of OAlph,IAlph:]
{Srtfsm2,Srtfsm1} is non empty finite set
{Srtfsm2} is non empty trivial finite 1 -element set
{{Srtfsm2,Srtfsm1},{Srtfsm2}} is non empty finite V48() set
the of OAlph . [Srtfsm2,Srtfsm1] is Element of the carrier of OAlph
ISrtfsm2 is Element of IAlph
Sfsm1 is Element of the carrier of OAlph
Sfsm2 is Element of the carrier of OAlph
(IAlph,OAlph,ISrtfsm2,Sfsm1) is Element of the carrier of OAlph
[Sfsm1,ISrtfsm2] is V15() Element of [: the carrier of OAlph,IAlph:]
{Sfsm1,ISrtfsm2} is non empty finite set
{Sfsm1} is non empty trivial finite 1 -element set
{{Sfsm1,ISrtfsm2},{Sfsm1}} is non empty finite V48() set
the of OAlph . [Sfsm1,ISrtfsm2] is Element of the carrier of OAlph
(IAlph,OAlph,rtfsm2,(M1 ^ M2)) . 0 is set
(IAlph,OAlph,rtfsm2,M1) . 0 is set
IAlph is non empty set
OAlph is non empty (IAlph)
the carrier of OAlph is non empty set
M1 is Relation-like NAT -defined IAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of IAlph
len M1 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len M1) + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
M2 is Relation-like NAT -defined IAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of IAlph
M1 ^ M2 is Relation-like NAT -defined IAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of IAlph
rtfsm2 is Element of the carrier of OAlph
(IAlph,OAlph,rtfsm2,(M1 ^ M2)) is Relation-like NAT -defined the carrier of OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of OAlph
(IAlph,OAlph,rtfsm2,(M1 ^ M2)) . ((len M1) + 1) is set
rtfsm1 is Element of the carrier of OAlph
(IAlph,OAlph,rtfsm2,M1) is Relation-like NAT -defined the carrier of OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of OAlph
(IAlph,OAlph,rtfsm2,M1) . 1 is set
(IAlph,OAlph,rtfsm2,M1) . ((len M1) + 1) is set
len (IAlph,OAlph,rtfsm2,M1) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
0 + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
M1 . (len M1) is set
(IAlph,OAlph,rtfsm2,M1) . (len M1) is set
(IAlph,OAlph,rtfsm2,M1) . ((len M1) + 1) is set
Srtfsm1 is Element of IAlph
Srtfsm2 is Element of the carrier of OAlph
ISrtfsm1 is Element of the carrier of OAlph
(IAlph,OAlph,Srtfsm1,Srtfsm2) is Element of the carrier of OAlph
[: the carrier of OAlph,IAlph:] is Relation-like non empty set
the of OAlph is Relation-like [: the carrier of OAlph,IAlph:] -defined the carrier of OAlph -valued Function-like non empty V14([: the carrier of OAlph,IAlph:]) quasi_total Element of bool [:[: the carrier of OAlph,IAlph:], the carrier of OAlph:]
[:[: the carrier of OAlph,IAlph:], the carrier of OAlph:] is Relation-like non empty set
bool [:[: the carrier of OAlph,IAlph:], the carrier of OAlph:] is non empty set
[Srtfsm2,Srtfsm1] is V15() Element of [: the carrier of OAlph,IAlph:]
{Srtfsm2,Srtfsm1} is non empty finite set
{Srtfsm2} is non empty trivial finite 1 -element set
{{Srtfsm2,Srtfsm1},{Srtfsm2}} is non empty finite V48() set
the of OAlph . [Srtfsm2,Srtfsm1] is Element of the carrier of OAlph
len (M1 ^ M2) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
len M2 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len M1) + (len M2) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(M1 ^ M2) . (len M1) is set
(IAlph,OAlph,rtfsm2,(M1 ^ M2)) . (len M1) is set
ISrtfsm2 is Element of IAlph
Sfsm1 is Element of the carrier of OAlph
Sfsm2 is Element of the carrier of OAlph
(IAlph,OAlph,ISrtfsm2,Sfsm1) is Element of the carrier of OAlph
[Sfsm1,ISrtfsm2] is V15() Element of [: the carrier of OAlph,IAlph:]
{Sfsm1,ISrtfsm2} is non empty finite set
{Sfsm1} is non empty trivial finite 1 -element set
{{Sfsm1,ISrtfsm2},{Sfsm1}} is non empty finite V48() set
the of OAlph . [Sfsm1,ISrtfsm2] is Element of the carrier of OAlph
Seg (len M1) is V35() V36() V37() V38() V39() V40() finite len M1 -element Element of bool NAT
dom M1 is V35() V36() V37() V38() V39() V40() finite Element of bool NAT
IAlph is non empty set
OAlph is non empty (IAlph)
the carrier of OAlph is non empty set
M1 is Relation-like NAT -defined IAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of IAlph
len M1 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
M2 is Relation-like NAT -defined IAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of IAlph
len M2 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len M2) + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
M1 ^ M2 is Relation-like NAT -defined IAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of IAlph
rtfsm2 is Element of the carrier of OAlph
(IAlph,OAlph,rtfsm2,(M1 ^ M2)) is Relation-like NAT -defined the carrier of OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of OAlph
rtfsm1 is Element of the carrier of OAlph
(IAlph,OAlph,rtfsm1,M2) is Relation-like NAT -defined the carrier of OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of OAlph
Srtfsm1 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len M1) + Srtfsm1 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(IAlph,OAlph,rtfsm2,(M1 ^ M2)) . ((len M1) + Srtfsm1) is set
(IAlph,OAlph,rtfsm1,M2) . Srtfsm1 is set
Srtfsm1 + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len M1) + (Srtfsm1 + 1) is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(IAlph,OAlph,rtfsm2,(M1 ^ M2)) . ((len M1) + (Srtfsm1 + 1)) is set
(IAlph,OAlph,rtfsm1,M2) . (Srtfsm1 + 1) is set
0 + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
M2 . Srtfsm1 is set
dom M2 is V35() V36() V37() V38() V39() V40() finite Element of bool NAT
len (M1 ^ M2) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len M1) + (len M2) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(M1 ^ M2) . ((len M1) + Srtfsm1) is set
((len M1) + Srtfsm1) + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(IAlph,OAlph,rtfsm2,(M1 ^ M2)) . (((len M1) + Srtfsm1) + 1) is set
Srtfsm2 is Element of IAlph
ISrtfsm1 is Element of the carrier of OAlph
ISrtfsm2 is Element of the carrier of OAlph
(IAlph,OAlph,Srtfsm2,ISrtfsm1) is Element of the carrier of OAlph
[: the carrier of OAlph,IAlph:] is Relation-like non empty set
the of OAlph is Relation-like [: the carrier of OAlph,IAlph:] -defined the carrier of OAlph -valued Function-like non empty V14([: the carrier of OAlph,IAlph:]) quasi_total Element of bool [:[: the carrier of OAlph,IAlph:], the carrier of OAlph:]
[:[: the carrier of OAlph,IAlph:], the carrier of OAlph:] is Relation-like non empty set
bool [:[: the carrier of OAlph,IAlph:], the carrier of OAlph:] is non empty set
[ISrtfsm1,Srtfsm2] is V15() Element of [: the carrier of OAlph,IAlph:]
{ISrtfsm1,Srtfsm2} is non empty finite set
{ISrtfsm1} is non empty trivial finite 1 -element set
{{ISrtfsm1,Srtfsm2},{ISrtfsm1}} is non empty finite V48() set
the of OAlph . [ISrtfsm1,Srtfsm2] is Element of the carrier of OAlph
Sfsm1 is Element of IAlph
Sfsm2 is Element of the carrier of OAlph
ISfsm1 is Element of the carrier of OAlph
(IAlph,OAlph,Sfsm1,Sfsm2) is Element of the carrier of OAlph
[Sfsm2,Sfsm1] is V15() Element of [: the carrier of OAlph,IAlph:]
{Sfsm2,Sfsm1} is non empty finite set
{Sfsm2} is non empty trivial finite 1 -element set
{{Sfsm2,Sfsm1},{Sfsm2}} is non empty finite V48() set
the of OAlph . [Sfsm2,Sfsm1] is Element of the carrier of OAlph
(len M1) + 0 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(IAlph,OAlph,rtfsm2,(M1 ^ M2)) . ((len M1) + 0) is set
(IAlph,OAlph,rtfsm1,M2) . 0 is set
IAlph is non empty set
OAlph is non empty (IAlph)
the carrier of OAlph is non empty set
M1 is Relation-like NAT -defined IAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of IAlph
len M1 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len M1) + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
M2 is Relation-like NAT -defined IAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of IAlph
M1 ^ M2 is Relation-like NAT -defined IAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of IAlph
rtfsm2 is Element of the carrier of OAlph
(IAlph,OAlph,rtfsm2,(M1 ^ M2)) is Relation-like NAT -defined the carrier of OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of OAlph
(IAlph,OAlph,rtfsm2,M1) is Relation-like NAT -defined the carrier of OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of OAlph
Del ((IAlph,OAlph,rtfsm2,M1),((len M1) + 1)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rtfsm1 is Element of the carrier of OAlph
(IAlph,OAlph,rtfsm1,M2) is Relation-like NAT -defined the carrier of OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of OAlph
(Del ((IAlph,OAlph,rtfsm2,M1),((len M1) + 1))) ^ (IAlph,OAlph,rtfsm1,M2) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (IAlph,OAlph,rtfsm2,M1) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
dom (IAlph,OAlph,rtfsm2,M1) is V35() V36() V37() V38() V39() V40() finite Element of bool NAT
Seg (len (IAlph,OAlph,rtfsm2,M1)) is V35() V36() V37() V38() V39() V40() finite len (IAlph,OAlph,rtfsm2,M1) -element Element of bool NAT
len (Del ((IAlph,OAlph,rtfsm2,M1),((len M1) + 1))) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
len (IAlph,OAlph,rtfsm2,(M1 ^ M2)) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
len (M1 ^ M2) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len (M1 ^ M2)) + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
len M2 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len M1) + (len M2) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
((len M1) + (len M2)) + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len M2) + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len (Del ((IAlph,OAlph,rtfsm2,M1),((len M1) + 1)))) + ((len M2) + 1) is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
len (IAlph,OAlph,rtfsm1,M2) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len (Del ((IAlph,OAlph,rtfsm2,M1),((len M1) + 1)))) + (len (IAlph,OAlph,rtfsm1,M2)) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
len ((Del ((IAlph,OAlph,rtfsm2,M1),((len M1) + 1))) ^ (IAlph,OAlph,rtfsm1,M2)) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
ISrtfsm1 is V23() V27() V28() V29() ext-real non negative integer finite cardinal set
ISrtfsm1 + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
ISrtfsm1 is V23() V27() V28() V29() ext-real non negative integer finite cardinal set
dom (Del ((IAlph,OAlph,rtfsm2,M1),((len M1) + 1))) is V35() V36() V37() V38() V39() V40() finite Element of bool NAT
ISrtfsm2 is V23() V27() V28() V29() ext-real non negative integer finite cardinal set
ISrtfsm2 + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(IAlph,OAlph,rtfsm2,(M1 ^ M2)) . ISrtfsm1 is set
(IAlph,OAlph,rtfsm2,M1) . ISrtfsm1 is set
(Del ((IAlph,OAlph,rtfsm2,M1),((len M1) + 1))) . ISrtfsm1 is set
((Del ((IAlph,OAlph,rtfsm2,M1),((len M1) + 1))) ^ (IAlph,OAlph,rtfsm1,M2)) . ISrtfsm1 is set
((Del ((IAlph,OAlph,rtfsm2,M1),((len M1) + 1))) ^ (IAlph,OAlph,rtfsm1,M2)) . ISrtfsm1 is set
ISrtfsm1 - (len M1) is V28() V29() ext-real integer set
(IAlph,OAlph,rtfsm1,M2) . (ISrtfsm1 - (len M1)) is set
ISrtfsm2 is V23() V27() V28() V29() ext-real non negative integer finite cardinal set
ISrtfsm2 + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
((len M1) + 1) - (len M1) is V28() V29() ext-real integer set
ISrtfsm2 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len M1) + ISrtfsm2 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len M1) + ((len M2) + 1) is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(IAlph,OAlph,rtfsm2,(M1 ^ M2)) . ISrtfsm1 is set
OAlph is non empty finite set
IAlph is set
[:OAlph,IAlph:] is Relation-like set
[:[:OAlph,IAlph:],OAlph:] is Relation-like set
bool [:[:OAlph,IAlph:],OAlph:] is non empty set
M1 is Relation-like [:OAlph,IAlph:] -defined OAlph -valued Function-like V14([:OAlph,IAlph:]) quasi_total Element of bool [:[:OAlph,IAlph:],OAlph:]
M2 is Element of OAlph
(IAlph,OAlph,M1,M2) is (IAlph) (IAlph)
M1 is non empty finite set
IAlph is set
[:M1,IAlph:] is Relation-like set
[:[:M1,IAlph:],M1:] is Relation-like set
bool [:[:M1,IAlph:],M1:] is non empty set
OAlph is non empty set
[:[:M1,IAlph:],OAlph:] is Relation-like set
bool [:[:M1,IAlph:],OAlph:] is non empty set
M2 is Relation-like [:M1,IAlph:] -defined M1 -valued Function-like V14([:M1,IAlph:]) quasi_total Element of bool [:[:M1,IAlph:],M1:]
rtfsm2 is Relation-like [:M1,IAlph:] -defined OAlph -valued Function-like V14([:M1,IAlph:]) quasi_total Element of bool [:[:M1,IAlph:],OAlph:]
rtfsm1 is Element of M1
(IAlph,OAlph,M1,M2,rtfsm2,rtfsm1) is (IAlph,OAlph) (IAlph,OAlph)
M1 is non empty finite set
IAlph is set
[:M1,IAlph:] is Relation-like set
[:[:M1,IAlph:],M1:] is Relation-like set
bool [:[:M1,IAlph:],M1:] is non empty set
OAlph is non empty set
[:M1,OAlph:] is Relation-like non empty set
bool [:M1,OAlph:] is non empty set
M2 is Relation-like [:M1,IAlph:] -defined M1 -valued Function-like V14([:M1,IAlph:]) quasi_total Element of bool [:[:M1,IAlph:],M1:]
rtfsm2 is Relation-like M1 -defined OAlph -valued Function-like non empty V14(M1) quasi_total finite Element of bool [:M1,OAlph:]
rtfsm1 is Element of M1
(IAlph,OAlph,M1,M2,rtfsm2,rtfsm1) is (IAlph,OAlph) (IAlph,OAlph)
IAlph is set
OAlph is non empty set
the non empty finite set is non empty finite set
[: the non empty finite set ,IAlph:] is Relation-like set
[:[: the non empty finite set ,IAlph:], the non empty finite set :] is Relation-like set
bool [:[: the non empty finite set ,IAlph:], the non empty finite set :] is non empty set
the Relation-like [: the non empty finite set ,IAlph:] -defined the non empty finite set -valued Function-like V14([: the non empty finite set ,IAlph:]) quasi_total Element of bool [:[: the non empty finite set ,IAlph:], the non empty finite set :] is Relation-like [: the non empty finite set ,IAlph:] -defined the non empty finite set -valued Function-like V14([: the non empty finite set ,IAlph:]) quasi_total Element of bool [:[: the non empty finite set ,IAlph:], the non empty finite set :]
[:[: the non empty finite set ,IAlph:],OAlph:] is Relation-like set
bool [:[: the non empty finite set ,IAlph:],OAlph:] is non empty set
the Relation-like [: the non empty finite set ,IAlph:] -defined OAlph -valued Function-like V14([: the non empty finite set ,IAlph:]) quasi_total Element of bool [:[: the non empty finite set ,IAlph:],OAlph:] is Relation-like [: the non empty finite set ,IAlph:] -defined OAlph -valued Function-like V14([: the non empty finite set ,IAlph:]) quasi_total Element of bool [:[: the non empty finite set ,IAlph:],OAlph:]
the Element of the non empty finite set is Element of the non empty finite set
(IAlph,OAlph, the non empty finite set , the Relation-like [: the non empty finite set ,IAlph:] -defined the non empty finite set -valued Function-like V14([: the non empty finite set ,IAlph:]) quasi_total Element of bool [:[: the non empty finite set ,IAlph:], the non empty finite set :], the Relation-like [: the non empty finite set ,IAlph:] -defined OAlph -valued Function-like V14([: the non empty finite set ,IAlph:]) quasi_total Element of bool [:[: the non empty finite set ,IAlph:],OAlph:], the Element of the non empty finite set ) is non empty finite (IAlph,OAlph) (IAlph,OAlph)
the non empty finite set is non empty finite set
[: the non empty finite set ,IAlph:] is Relation-like set
[:[: the non empty finite set ,IAlph:], the non empty finite set :] is Relation-like set
bool [:[: the non empty finite set ,IAlph:], the non empty finite set :] is non empty set
the Relation-like [: the non empty finite set ,IAlph:] -defined the non empty finite set -valued Function-like V14([: the non empty finite set ,IAlph:]) quasi_total Element of bool [:[: the non empty finite set ,IAlph:], the non empty finite set :] is Relation-like [: the non empty finite set ,IAlph:] -defined the non empty finite set -valued Function-like V14([: the non empty finite set ,IAlph:]) quasi_total Element of bool [:[: the non empty finite set ,IAlph:], the non empty finite set :]
[: the non empty finite set ,OAlph:] is Relation-like non empty set
bool [: the non empty finite set ,OAlph:] is non empty set
the Relation-like the non empty finite set -defined OAlph -valued Function-like non empty V14( the non empty finite set ) quasi_total finite Element of bool [: the non empty finite set ,OAlph:] is Relation-like the non empty finite set -defined OAlph -valued Function-like non empty V14( the non empty finite set ) quasi_total finite Element of bool [: the non empty finite set ,OAlph:]
the Element of the non empty finite set is Element of the non empty finite set
(IAlph,OAlph, the non empty finite set , the Relation-like [: the non empty finite set ,IAlph:] -defined the non empty finite set -valued Function-like V14([: the non empty finite set ,IAlph:]) quasi_total Element of bool [:[: the non empty finite set ,IAlph:], the non empty finite set :], the Relation-like the non empty finite set -defined OAlph -valued Function-like non empty V14( the non empty finite set ) quasi_total finite Element of bool [: the non empty finite set ,OAlph:], the Element of the non empty finite set ) is non empty finite (IAlph,OAlph) (IAlph,OAlph)
IAlph is non empty set
OAlph is non empty set
M1 is non empty (IAlph,OAlph)
the carrier of M1 is non empty set
rtfsm2 is Relation-like NAT -defined IAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of IAlph
len rtfsm2 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
dom rtfsm2 is V35() V36() V37() V38() V39() V40() finite Element of bool NAT
the of M1 is Relation-like [: the carrier of M1,IAlph:] -defined OAlph -valued Function-like non empty V14([: the carrier of M1,IAlph:]) quasi_total Element of bool [:[: the carrier of M1,IAlph:],OAlph:]
[: the carrier of M1,IAlph:] is Relation-like non empty set
[:[: the carrier of M1,IAlph:],OAlph:] is Relation-like non empty set
bool [:[: the carrier of M1,IAlph:],OAlph:] is non empty set
M2 is Element of the carrier of M1
(IAlph,M1,M2,rtfsm2) is Relation-like NAT -defined the carrier of M1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of M1
fsm1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len fsm1 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
dom fsm1 is V35() V36() V37() V38() V39() V40() finite Element of bool NAT
Seg (len rtfsm2) is V35() V36() V37() V38() V39() V40() finite len rtfsm2 -element Element of bool NAT
proj2 fsm1 is finite set
fsm2 is set
Srtfsm1 is set
fsm1 . Srtfsm1 is set
Srtfsm2 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len fsm1) + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
len (IAlph,M1,M2,rtfsm2) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
Seg (len fsm1) is V35() V36() V37() V38() V39() V40() finite len fsm1 -element Element of bool NAT
rtfsm2 . Srtfsm2 is set
dom (IAlph,M1,M2,rtfsm2) is V35() V36() V37() V38() V39() V40() finite Element of bool NAT
(IAlph,M1,M2,rtfsm2) . Srtfsm2 is set
fsm1 . Srtfsm2 is set
ISrtfsm2 is Element of the carrier of M1
ISrtfsm1 is Element of IAlph
[ISrtfsm2,ISrtfsm1] is V15() Element of [: the carrier of M1,IAlph:]
{ISrtfsm2,ISrtfsm1} is non empty finite set
{ISrtfsm2} is non empty trivial finite 1 -element set
{{ISrtfsm2,ISrtfsm1},{ISrtfsm2}} is non empty finite V48() set
the of M1 . [ISrtfsm2,ISrtfsm1] is Element of OAlph
fsm2 is Relation-like NAT -defined OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of OAlph
Srtfsm1 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
fsm2 . Srtfsm1 is set
(IAlph,M1,M2,rtfsm2) . Srtfsm1 is set
rtfsm2 . Srtfsm1 is set
[((IAlph,M1,M2,rtfsm2) . Srtfsm1),(rtfsm2 . Srtfsm1)] is V15() set
{((IAlph,M1,M2,rtfsm2) . Srtfsm1),(rtfsm2 . Srtfsm1)} is non empty finite set
{((IAlph,M1,M2,rtfsm2) . Srtfsm1)} is non empty trivial finite 1 -element set
{{((IAlph,M1,M2,rtfsm2) . Srtfsm1),(rtfsm2 . Srtfsm1)},{((IAlph,M1,M2,rtfsm2) . Srtfsm1)}} is non empty finite V48() set
the of M1 . [((IAlph,M1,M2,rtfsm2) . Srtfsm1),(rtfsm2 . Srtfsm1)] is set
rtfsm1 is Relation-like NAT -defined OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of OAlph
len rtfsm1 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
fsm1 is Relation-like NAT -defined OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of OAlph
len fsm1 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
dom rtfsm1 is V35() V36() V37() V38() V39() V40() finite Element of bool NAT
Srtfsm1 is V23() V27() V28() V29() ext-real non negative integer finite cardinal set
rtfsm1 . Srtfsm1 is set
(IAlph,M1,M2,rtfsm2) . Srtfsm1 is set
rtfsm2 . Srtfsm1 is set
[((IAlph,M1,M2,rtfsm2) . Srtfsm1),(rtfsm2 . Srtfsm1)] is V15() set
{((IAlph,M1,M2,rtfsm2) . Srtfsm1),(rtfsm2 . Srtfsm1)} is non empty finite set
{((IAlph,M1,M2,rtfsm2) . Srtfsm1)} is non empty trivial finite 1 -element set
{{((IAlph,M1,M2,rtfsm2) . Srtfsm1),(rtfsm2 . Srtfsm1)},{((IAlph,M1,M2,rtfsm2) . Srtfsm1)}} is non empty finite V48() set
the of M1 . [((IAlph,M1,M2,rtfsm2) . Srtfsm1),(rtfsm2 . Srtfsm1)] is set
fsm1 . Srtfsm1 is set
IAlph is non empty set
<*> IAlph is Relation-like non-empty empty-yielding NAT -defined IAlph -valued Function-like one-to-one constant functional empty V23() V27() V28() V29() ext-real non positive non negative integer V35() V36() V37() V38() V39() V40() V41() finite finite-yielding V48() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of IAlph
OAlph is non empty set
<*> OAlph is Relation-like non-empty empty-yielding NAT -defined OAlph -valued Function-like one-to-one constant functional empty V23() V27() V28() V29() ext-real non positive non negative integer V35() V36() V37() V38() V39() V40() V41() finite finite-yielding V48() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of OAlph
M1 is non empty (IAlph,OAlph)
the carrier of M1 is non empty set
M2 is Element of the carrier of M1
(IAlph,OAlph,M1,M2,(<*> IAlph)) is Relation-like NAT -defined OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of OAlph
len (IAlph,OAlph,M1,M2,(<*> IAlph)) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
len (<*> IAlph) is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V23() V27() V28() V29() ext-real non positive non negative integer V35() V36() V37() V38() V39() V40() V41() finite finite-yielding V48() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
IAlph is non empty set
OAlph is non empty set
M1 is non empty (IAlph,OAlph)
the carrier of M1 is non empty set
rtfsm2 is Relation-like NAT -defined IAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of IAlph
len rtfsm2 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len rtfsm2) + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
Seg ((len rtfsm2) + 1) is non empty V35() V36() V37() V38() V39() V40() finite (len rtfsm2) + 1 -element Element of bool NAT
the of M1 is Relation-like the carrier of M1 -defined OAlph -valued Function-like non empty V14( the carrier of M1) quasi_total Element of bool [: the carrier of M1,OAlph:]
[: the carrier of M1,OAlph:] is Relation-like non empty set
bool [: the carrier of M1,OAlph:] is non empty set
M2 is Element of the carrier of M1
(IAlph,M1,M2,rtfsm2) is Relation-like NAT -defined the carrier of M1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of M1
len (IAlph,M1,M2,rtfsm2) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
fsm1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len fsm1 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
dom fsm1 is V35() V36() V37() V38() V39() V40() finite Element of bool NAT
Seg (len (IAlph,M1,M2,rtfsm2)) is V35() V36() V37() V38() V39() V40() finite len (IAlph,M1,M2,rtfsm2) -element Element of bool NAT
dom (IAlph,M1,M2,rtfsm2) is V35() V36() V37() V38() V39() V40() finite Element of bool NAT
proj2 fsm1 is finite set
fsm2 is set
Srtfsm1 is set
fsm1 . Srtfsm1 is set
Seg (len fsm1) is V35() V36() V37() V38() V39() V40() finite len fsm1 -element Element of bool NAT
Srtfsm2 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(IAlph,M1,M2,rtfsm2) . Srtfsm2 is set
fsm1 . Srtfsm2 is set
ISrtfsm1 is Element of the carrier of M1
the of M1 . ISrtfsm1 is Element of OAlph
fsm2 is Relation-like NAT -defined OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of OAlph
Srtfsm1 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
fsm2 . Srtfsm1 is set
(IAlph,M1,M2,rtfsm2) . Srtfsm1 is set
the of M1 . ((IAlph,M1,M2,rtfsm2) . Srtfsm1) is set
rtfsm1 is Relation-like NAT -defined OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of OAlph
len rtfsm1 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
fsm1 is Relation-like NAT -defined OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of OAlph
len fsm1 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
Srtfsm1 is V23() V27() V28() V29() ext-real non negative integer finite cardinal set
Seg (len rtfsm1) is V35() V36() V37() V38() V39() V40() finite len rtfsm1 -element Element of bool NAT
rtfsm1 . Srtfsm1 is set
(IAlph,M1,M2,rtfsm2) . Srtfsm1 is set
the of M1 . ((IAlph,M1,M2,rtfsm2) . Srtfsm1) is set
fsm1 . Srtfsm1 is set
IAlph is non empty set
OAlph is non empty set
M1 is Relation-like NAT -defined IAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of IAlph
M2 is non empty (IAlph,OAlph)
the carrier of M2 is non empty set
the of M2 is Relation-like the carrier of M2 -defined OAlph -valued Function-like non empty V14( the carrier of M2) quasi_total Element of bool [: the carrier of M2,OAlph:]
[: the carrier of M2,OAlph:] is Relation-like non empty set
bool [: the carrier of M2,OAlph:] is non empty set
rtfsm2 is Element of the carrier of M2
(IAlph,OAlph,M2,rtfsm2,M1) is Relation-like NAT -defined OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of OAlph
(IAlph,OAlph,M2,rtfsm2,M1) . 1 is set
the of M2 . rtfsm2 is Element of OAlph
len M1 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len M1) + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
Seg ((len M1) + 1) is non empty V35() V36() V37() V38() V39() V40() finite (len M1) + 1 -element Element of bool NAT
(IAlph,M2,rtfsm2,M1) is Relation-like NAT -defined the carrier of M2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of M2
(IAlph,M2,rtfsm2,M1) . 1 is set
the of M2 . ((IAlph,M2,rtfsm2,M1) . 1) is set
IAlph is non empty set
OAlph is non empty set
M1 is Relation-like NAT -defined IAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of IAlph
M2 is Relation-like NAT -defined IAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of IAlph
M1 ^ M2 is Relation-like NAT -defined IAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of IAlph
rtfsm2 is non empty (IAlph,OAlph)
the carrier of rtfsm2 is non empty set
rtfsm1 is Element of the carrier of rtfsm2
(IAlph,OAlph,rtfsm2,rtfsm1,(M1 ^ M2)) is Relation-like NAT -defined OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of OAlph
(IAlph,OAlph,rtfsm2,rtfsm1,M1) is Relation-like NAT -defined OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of OAlph
fsm1 is Element of the carrier of rtfsm2
(IAlph,OAlph,rtfsm2,fsm1,M2) is Relation-like NAT -defined OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of OAlph
(IAlph,OAlph,rtfsm2,rtfsm1,M1) ^ (IAlph,OAlph,rtfsm2,fsm1,M2) is Relation-like NAT -defined OAlph -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of OAlph
len M1 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len M1) + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(IAlph,rtfsm2,rtfsm1,M1) is Relation-like NAT -defined the carrier of rtfsm2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of rtfsm2
Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
the of rtfsm2 is Relation-like [: the carrier of rtfsm2,IAlph:] -defined OAlph -valued Function-like non empty V14([: the carrier of rtfsm2,IAlph:]) quasi_total Element of bool [:[: the carrier of rtfsm2,IAlph:],OAlph:]
[: the carrier of rtfsm2,IAlph:] is Relation-like non empty set
[:[: the carrier of rtfsm2,IAlph:],OAlph:] is Relation-like non empty set
bool [:[: the carrier of rtfsm2,IAlph:],OAlph:] is non empty set
dom (IAlph,rtfsm2,rtfsm1,M1) is V35() V36() V37() V38() V39() V40() finite Element of bool NAT
len (IAlph,rtfsm2,rtfsm1,M1) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
Seg (len (IAlph,rtfsm2,rtfsm1,M1)) is V35() V36() V37() V38() V39() V40() finite len (IAlph,rtfsm2,rtfsm1,M1) -element Element of bool NAT
Seg ((len M1) + 1) is non empty V35() V36() V37() V38() V39() V40() finite (len M1) + 1 -element Element of bool NAT
len (Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
Sfsm1 is V23() V27() V28() V29() ext-real non negative integer finite cardinal set
Sfsm1 + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
len (IAlph,OAlph,rtfsm2,rtfsm1,M1) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
Sfsm2 is V23() V27() V28() V29() ext-real non negative integer finite cardinal set
len (IAlph,OAlph,rtfsm2,rtfsm1,(M1 ^ M2)) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
dom M1 is V35() V36() V37() V38() V39() V40() finite Element of bool NAT
dom (Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) is V35() V36() V37() V38() V39() V40() finite Element of bool NAT
dom (IAlph,OAlph,rtfsm2,rtfsm1,M1) is V35() V36() V37() V38() V39() V40() finite Element of bool NAT
len (M1 ^ M2) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
dom (M1 ^ M2) is V35() V36() V37() V38() V39() V40() finite Element of bool NAT
(IAlph,OAlph,rtfsm2,rtfsm1,(M1 ^ M2)) . Sfsm2 is set
(IAlph,rtfsm2,rtfsm1,(M1 ^ M2)) is Relation-like NAT -defined the carrier of rtfsm2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of rtfsm2
(IAlph,rtfsm2,rtfsm1,(M1 ^ M2)) . Sfsm2 is set
(M1 ^ M2) . Sfsm2 is set
[((IAlph,rtfsm2,rtfsm1,(M1 ^ M2)) . Sfsm2),((M1 ^ M2) . Sfsm2)] is V15() set
{((IAlph,rtfsm2,rtfsm1,(M1 ^ M2)) . Sfsm2),((M1 ^ M2) . Sfsm2)} is non empty finite set
{((IAlph,rtfsm2,rtfsm1,(M1 ^ M2)) . Sfsm2)} is non empty trivial finite 1 -element set
{{((IAlph,rtfsm2,rtfsm1,(M1 ^ M2)) . Sfsm2),((M1 ^ M2) . Sfsm2)},{((IAlph,rtfsm2,rtfsm1,(M1 ^ M2)) . Sfsm2)}} is non empty finite V48() set
the of rtfsm2 . [((IAlph,rtfsm2,rtfsm1,(M1 ^ M2)) . Sfsm2),((M1 ^ M2) . Sfsm2)] is set
(IAlph,rtfsm2,fsm1,M2) is Relation-like NAT -defined the carrier of rtfsm2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of rtfsm2
(Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) ^ (IAlph,rtfsm2,fsm1,M2) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
((Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) ^ (IAlph,rtfsm2,fsm1,M2)) . Sfsm2 is set
[(((Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) ^ (IAlph,rtfsm2,fsm1,M2)) . Sfsm2),((M1 ^ M2) . Sfsm2)] is V15() set
{(((Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) ^ (IAlph,rtfsm2,fsm1,M2)) . Sfsm2),((M1 ^ M2) . Sfsm2)} is non empty finite set
{(((Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) ^ (IAlph,rtfsm2,fsm1,M2)) . Sfsm2)} is non empty trivial finite 1 -element set
{{(((Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) ^ (IAlph,rtfsm2,fsm1,M2)) . Sfsm2),((M1 ^ M2) . Sfsm2)},{(((Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) ^ (IAlph,rtfsm2,fsm1,M2)) . Sfsm2)}} is non empty finite V48() set
the of rtfsm2 . [(((Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) ^ (IAlph,rtfsm2,fsm1,M2)) . Sfsm2),((M1 ^ M2) . Sfsm2)] is set
(Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) . Sfsm2 is set
[((Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) . Sfsm2),((M1 ^ M2) . Sfsm2)] is V15() set
{((Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) . Sfsm2),((M1 ^ M2) . Sfsm2)} is non empty finite set
{((Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) . Sfsm2)} is non empty trivial finite 1 -element set
{{((Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) . Sfsm2),((M1 ^ M2) . Sfsm2)},{((Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) . Sfsm2)}} is non empty finite V48() set
the of rtfsm2 . [((Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) . Sfsm2),((M1 ^ M2) . Sfsm2)] is set
M1 . Sfsm2 is set
[((Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) . Sfsm2),(M1 . Sfsm2)] is V15() set
{((Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) . Sfsm2),(M1 . Sfsm2)} is non empty finite set
{{((Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) . Sfsm2),(M1 . Sfsm2)},{((Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) . Sfsm2)}} is non empty finite V48() set
the of rtfsm2 . [((Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) . Sfsm2),(M1 . Sfsm2)] is set
(IAlph,rtfsm2,rtfsm1,M1) . Sfsm2 is set
[((IAlph,rtfsm2,rtfsm1,M1) . Sfsm2),(M1 . Sfsm2)] is V15() set
{((IAlph,rtfsm2,rtfsm1,M1) . Sfsm2),(M1 . Sfsm2)} is non empty finite set
{((IAlph,rtfsm2,rtfsm1,M1) . Sfsm2)} is non empty trivial finite 1 -element set
{{((IAlph,rtfsm2,rtfsm1,M1) . Sfsm2),(M1 . Sfsm2)},{((IAlph,rtfsm2,rtfsm1,M1) . Sfsm2)}} is non empty finite V48() set
the of rtfsm2 . [((IAlph,rtfsm2,rtfsm1,M1) . Sfsm2),(M1 . Sfsm2)] is set
(IAlph,OAlph,rtfsm2,rtfsm1,M1) . Sfsm2 is set
((IAlph,OAlph,rtfsm2,rtfsm1,M1) ^ (IAlph,OAlph,rtfsm2,fsm1,M2)) . Sfsm2 is set
(len (IAlph,OAlph,rtfsm2,rtfsm1,M1)) + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
((len (IAlph,OAlph,rtfsm2,rtfsm1,M1)) + 1) - (len (IAlph,OAlph,rtfsm2,rtfsm1,M1)) is V28() V29() ext-real integer set
Sfsm2 - (len (IAlph,OAlph,rtfsm2,rtfsm1,M1)) is V28() V29() ext-real integer set
len (M1 ^ M2) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
len M2 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len M1) + (len M2) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len (IAlph,OAlph,rtfsm2,rtfsm1,M1)) + (len M2) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
((len (IAlph,OAlph,rtfsm2,rtfsm1,M1)) + (len M2)) - (len (IAlph,OAlph,rtfsm2,rtfsm1,M1)) is V28() V29() ext-real integer set
ISfsm1 is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
dom M2 is V35() V36() V37() V38() V39() V40() finite Element of bool NAT
(len (Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1)))) + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
len (IAlph,OAlph,rtfsm2,fsm1,M2) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len (IAlph,OAlph,rtfsm2,rtfsm1,M1)) + (len (IAlph,OAlph,rtfsm2,fsm1,M2)) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
((IAlph,OAlph,rtfsm2,rtfsm1,M1) ^ (IAlph,OAlph,rtfsm2,fsm1,M2)) . Sfsm2 is set
(IAlph,OAlph,rtfsm2,fsm1,M2) . ISfsm1 is set
(IAlph,rtfsm2,fsm1,M2) is Relation-like NAT -defined the carrier of rtfsm2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of rtfsm2
(IAlph,rtfsm2,fsm1,M2) . ISfsm1 is set
M2 . ISfsm1 is set
[((IAlph,rtfsm2,fsm1,M2) . ISfsm1),(M2 . ISfsm1)] is V15() set
{((IAlph,rtfsm2,fsm1,M2) . ISfsm1),(M2 . ISfsm1)} is non empty finite set
{((IAlph,rtfsm2,fsm1,M2) . ISfsm1)} is non empty trivial finite 1 -element set
{{((IAlph,rtfsm2,fsm1,M2) . ISfsm1),(M2 . ISfsm1)},{((IAlph,rtfsm2,fsm1,M2) . ISfsm1)}} is non empty finite V48() set
the of rtfsm2 . [((IAlph,rtfsm2,fsm1,M2) . ISfsm1),(M2 . ISfsm1)] is set
Sfsm2 - (len M1) is V28() V29() ext-real integer set
(IAlph,rtfsm2,fsm1,M2) . (Sfsm2 - (len M1)) is set
M2 . (Sfsm2 - (len (IAlph,OAlph,rtfsm2,rtfsm1,M1))) is set
[((IAlph,rtfsm2,fsm1,M2) . (Sfsm2 - (len M1))),(M2 . (Sfsm2 - (len (IAlph,OAlph,rtfsm2,rtfsm1,M1))))] is V15() set
{((IAlph,rtfsm2,fsm1,M2) . (Sfsm2 - (len M1))),(M2 . (Sfsm2 - (len (IAlph,OAlph,rtfsm2,rtfsm1,M1))))} is non empty finite set
{((IAlph,rtfsm2,fsm1,M2) . (Sfsm2 - (len M1)))} is non empty trivial finite 1 -element set
{{((IAlph,rtfsm2,fsm1,M2) . (Sfsm2 - (len M1))),(M2 . (Sfsm2 - (len (IAlph,OAlph,rtfsm2,rtfsm1,M1))))},{((IAlph,rtfsm2,fsm1,M2) . (Sfsm2 - (len M1)))}} is non empty finite V48() set
the of rtfsm2 . [((IAlph,rtfsm2,fsm1,M2) . (Sfsm2 - (len M1))),(M2 . (Sfsm2 - (len (IAlph,OAlph,rtfsm2,rtfsm1,M1))))] is set
M2 . (Sfsm2 - (len M1)) is set
[((IAlph,rtfsm2,fsm1,M2) . (Sfsm2 - (len M1))),(M2 . (Sfsm2 - (len M1)))] is V15() set
{((IAlph,rtfsm2,fsm1,M2) . (Sfsm2 - (len M1))),(M2 . (Sfsm2 - (len M1)))} is non empty finite set
{{((IAlph,rtfsm2,fsm1,M2) . (Sfsm2 - (len M1))),(M2 . (Sfsm2 - (len M1)))},{((IAlph,rtfsm2,fsm1,M2) . (Sfsm2 - (len M1)))}} is non empty finite V48() set
the of rtfsm2 . [((IAlph,rtfsm2,fsm1,M2) . (Sfsm2 - (len M1))),(M2 . (Sfsm2 - (len M1)))] is set
(len M2) + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len (Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1)))) + (len M2) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len (Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1)))) + ((len M2) + 1) is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
len (IAlph,rtfsm2,fsm1,M2) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
(len (Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1)))) + (len (IAlph,rtfsm2,fsm1,M2)) is V23() V27() V28() V29() ext-real non negative integer V35() V36() V37() V38() V39() V40() finite cardinal Element of NAT
dom (M1 ^ M2) is V35() V36() V37() V38() V39() V40() finite Element of bool NAT
(IAlph,OAlph,rtfsm2,rtfsm1,(M1 ^ M2)) . Sfsm2 is set
(IAlph,rtfsm2,rtfsm1,(M1 ^ M2)) is Relation-like NAT -defined the carrier of rtfsm2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of rtfsm2
(IAlph,rtfsm2,rtfsm1,(M1 ^ M2)) . Sfsm2 is set
(M1 ^ M2) . Sfsm2 is set
[((IAlph,rtfsm2,rtfsm1,(M1 ^ M2)) . Sfsm2),((M1 ^ M2) . Sfsm2)] is V15() set
{((IAlph,rtfsm2,rtfsm1,(M1 ^ M2)) . Sfsm2),((M1 ^ M2) . Sfsm2)} is non empty finite set
{((IAlph,rtfsm2,rtfsm1,(M1 ^ M2)) . Sfsm2)} is non empty trivial finite 1 -element set
{{((IAlph,rtfsm2,rtfsm1,(M1 ^ M2)) . Sfsm2),((M1 ^ M2) . Sfsm2)},{((IAlph,rtfsm2,rtfsm1,(M1 ^ M2)) . Sfsm2)}} is non empty finite V48() set
the of rtfsm2 . [((IAlph,rtfsm2,rtfsm1,(M1 ^ M2)) . Sfsm2),((M1 ^ M2) . Sfsm2)] is set
(Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) ^ (IAlph,rtfsm2,fsm1,M2) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
((Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) ^ (IAlph,rtfsm2,fsm1,M2)) . Sfsm2 is set
[(((Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) ^ (IAlph,rtfsm2,fsm1,M2)) . Sfsm2),((M1 ^ M2) . Sfsm2)] is V15() set
{(((Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) ^ (IAlph,rtfsm2,fsm1,M2)) . Sfsm2),((M1 ^ M2) . Sfsm2)} is non empty finite set
{(((Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) ^ (IAlph,rtfsm2,fsm1,M2)) . Sfsm2)} is non empty trivial finite 1 -element set
{{(((Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) ^ (IAlph,rtfsm2,fsm1,M2)) . Sfsm2),((M1 ^ M2) . Sfsm2)},{(((Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) ^ (IAlph,rtfsm2,fsm1,M2)) . Sfsm2)}} is non empty finite V48() set
the of rtfsm2 . [(((Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))) ^ (IAlph,rtfsm2,fsm1,M2)) . Sfsm2),((M1 ^ M2) . Sfsm2)] is set
Sfsm2 - (len (Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1)))) is V28() V29() ext-real integer set
(IAlph,rtfsm2,fsm1,M2) . (Sfsm2 - (len (Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))))) is set
[((IAlph,rtfsm2,fsm1,M2) . (Sfsm2 - (len (Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1)))))),((M1 ^ M2) . Sfsm2)] is V15() set
{((IAlph,rtfsm2,fsm1,M2) . (Sfsm2 - (len (Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1)))))),((M1 ^ M2) . Sfsm2)} is non empty finite set
{((IAlph,rtfsm2,fsm1,M2) . (Sfsm2 - (len (Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))))))} is non empty trivial finite 1 -element set
{{((IAlph,rtfsm2,fsm1,M2) . (Sfsm2 - (len (Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1)))))),((M1 ^ M2) . Sfsm2)},{((IAlph,rtfsm2,fsm1,M2) . (Sfsm2 - (len (Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1))))))}} is non empty finite V48() set
the of rtfsm2 . [((IAlph,rtfsm2,fsm1,M2) . (Sfsm2 - (len (Del ((IAlph,rtfsm2,rtfsm1,M1),((len M1) + 1)))))),((M1 ^ M2) . Sfsm2)] is set
(len (IAlph,OAlph,rtfsm2,rtfsm1,M1)) + 1 is non empty V23() V27() V28() V29() ext-real positive non negative integer V35() V36()