:: FSM_3 semantic presentation

REAL is V32() V33() V34() V38() set
NAT is non trivial V6() V32() V33() V34() V35() V36() V37() V38() non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty set
NAT is non trivial V6() V32() V33() V34() V35() V36() V37() V38() 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
0 is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of NAT
0 is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() set
1 is non empty V6() V10() V11() ext-real positive non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
{0,1} is non empty V32() V33() V34() V35() V36() V37() finite V43() Element of bool NAT
{0,1} ^omega is non empty functional set
bool ({0,1} ^omega) is non empty set
[:NAT,REAL:] is V15() set
bool [:NAT,REAL:] is non empty set
2 is non empty V6() V10() V11() ext-real positive non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
3 is non empty V6() V10() V11() ext-real positive non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 0 is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() set
proj2 0 is empty trivial V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V63() V67() V69() set
E is V6() V10() V11() ext-real non negative finite cardinal V69() set
FA is V6() V10() V11() ext-real non negative finite cardinal V69() set
bNFA is V6() V10() V11() ext-real non negative finite cardinal V69() set
FA + bNFA is V6() V10() V11() ext-real non negative finite cardinal V69() set
(FA + bNFA) + 0 is V6() V10() V11() ext-real non negative finite cardinal V69() set
E + bNFA is V6() V10() V11() ext-real non negative finite cardinal V69() set
E is V15() V18( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
FA is V15() V18( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
E ^ FA is V15() V18( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
FA ^ E is V15() V18( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len (E ^ FA) is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
len E is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
len FA is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
(len E) + (len FA) is V6() V10() V11() ext-real non negative finite cardinal V69() set
len (FA ^ E) is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
len FA is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
len E is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
(len FA) + (len E) is V6() V10() V11() ext-real non negative finite cardinal V69() set
E is V6() V10() V11() ext-real non negative finite cardinal V69() set
E + 1 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
FA is V15() V18( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
dom FA is V32() V33() V34() V35() V36() V37() finite Element of bool NAT
len FA is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
(len FA) + 1 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
bNFA is V15() V18( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len bNFA is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
dom bNFA is V32() V33() V34() V35() V36() V37() finite Element of bool NAT
1 + 0 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
E is non empty set
E ^omega is non empty functional set
FA is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
len FA is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 FA is V6() V10() V11() ext-real non negative finite cardinal V69() set
FA . 0 is set
0 + 1 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
bNFA is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
len bNFA is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 bNFA is V6() V10() V11() ext-real non negative finite cardinal V69() set
c₄ is Element of E
<%c₄%> is non empty trivial V8() V15() V18( NAT ) V19(E) Function-like constant finite 1 -element V67() Element of K232(E)
K232(E) is non empty functional M11(E)
bNFA ^ <%c₄%> is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(E)
<%> E is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(E) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(E)
0 ^ <%c₄%> is V8() V15() V18( NAT ) Function-like finite V67() set
E is non empty set
E ^omega is non empty functional set
FA is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
len FA is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 FA is V6() V10() V11() ext-real non negative finite cardinal V69() set
bNFA is V6() V10() V11() ext-real non negative finite cardinal V69() set
bNFA + 1 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
c₄ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
len c₄ is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 c₄ is V6() V10() V11() ext-real non negative finite cardinal V69() set
x is Element of E
<%x%> is non empty trivial V8() V15() V18( NAT ) V19(E) Function-like constant finite 1 -element V67() Element of K232(E)
K232(E) is non empty functional M11(E)
c₄ ^ <%x%> is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(E)
Es is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
len Es is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 Es is V6() V10() V11() ext-real non negative finite cardinal V69() set
c₄ ^ Es is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(E)
0 + 1 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
<%> E is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(E) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(E)
K232(E) is non empty functional M11(E)
c₄ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
len c₄ is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 c₄ is V6() V10() V11() ext-real non negative finite cardinal V69() set
FA ^ c₄ is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(E)
FA ^ 0 is V8() V15() V18( NAT ) Function-like finite V67() set
E is set
<%E%> is non empty trivial V8() V15() V18( NAT ) Function-like constant finite 1 -element V67() set
FA is set
<%FA%> is non empty trivial V8() V15() V18( NAT ) Function-like constant finite 1 -element V67() set
bNFA is V8() V15() V18( NAT ) Function-like finite V67() set
<%E%> ^ bNFA is V8() V15() V18( NAT ) Function-like finite V67() set
c₄ is V8() V15() V18( NAT ) Function-like finite V67() set
<%FA%> ^ c₄ is V8() V15() V18( NAT ) Function-like finite V67() set
(<%E%> ^ bNFA) . 0 is set
E is non empty set
E ^omega is non empty functional set
FA is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
len FA is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 FA is V6() V10() V11() ext-real non negative finite cardinal V69() set
bNFA is V6() V10() V11() ext-real non negative finite cardinal V69() set
bNFA + 1 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
c₄ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
len c₄ is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 c₄ is V6() V10() V11() ext-real non negative finite cardinal V69() set
x is Element of E
<%x%> is non empty trivial V8() V15() V18( NAT ) V19(E) Function-like constant finite 1 -element V67() Element of K232(E)
K232(E) is non empty functional M11(E)
<%x%> ^ c₄ is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(E)
E is non empty set
Lex E is functional Element of bool K232(E)
K232(E) is non empty functional M11(E)
bool K232(E) is non empty set
FA is Element of E
<%FA%> is non empty trivial V8() V15() V18( NAT ) V19(E) Function-like constant finite 1 -element V67() Element of K232(E)
E is non empty set
<%> E is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(E) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(E)
K232(E) is non empty functional M11(E)
Lex E is non empty functional Element of bool K232(E)
bool K232(E) is non empty set
FA is Element of E
<%FA%> is non empty trivial V8() V15() V18( NAT ) V19(E) Function-like constant finite 1 -element V67() Element of K232(E)
E is non empty set
E ^omega is non empty functional set
Lex E is non empty functional Element of bool K232(E)
K232(E) is non empty functional M11(E)
bool K232(E) is non empty set
FA is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
len FA is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 FA is V6() V10() V11() ext-real non negative finite cardinal V69() set
bNFA is Element of E
<%bNFA%> is non empty trivial V8() V15() V18( NAT ) V19(E) Function-like constant finite 1 -element V67() Element of K232(E)
FA . 0 is set
bNFA is Element of E
<%bNFA%> is non empty trivial V8() V15() V18( NAT ) V19(E) Function-like constant finite 1 -element V67() Element of K232(E)
E is non empty set
E ^omega is non empty functional set
Lex E is non empty functional Element of bool K232(E)
K232(E) is non empty functional M11(E)
bool K232(E) is non empty set
FA is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
bNFA is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
len FA is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 FA is V6() V10() V11() ext-real non negative finite cardinal V69() set
c₄ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
FA ^ c₄ is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(E)
c₄ ^ FA is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(E)
len bNFA is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 bNFA is V6() V10() V11() ext-real non negative finite cardinal V69() set
FA ^ 0 is V8() V15() V18( NAT ) Function-like finite V67() set
0 ^ FA is V8() V15() V18( NAT ) Function-like finite V67() set
len (FA ^ c₄) is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 (FA ^ c₄) is V6() V10() V11() ext-real non negative finite cardinal V69() set
len c₄ is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 c₄ is V6() V10() V11() ext-real non negative finite cardinal V69() set
1 + (len c₄) is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
<%> E is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(E) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(E)
len (c₄ ^ FA) is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 (c₄ ^ FA) is V6() V10() V11() ext-real non negative finite cardinal V69() set
len c₄ is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 c₄ is V6() V10() V11() ext-real non negative finite cardinal V69() set
1 + (len c₄) is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
<%> E is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(E) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(E)
E is non empty set
Lex E is non empty functional Element of bool K232(E)
K232(E) is non empty functional M11(E)
bool K232(E) is non empty set
FA is transition-system over Lex E
the Tran of FA is V15() V18([: the carrier of FA,(Lex E):]) V19( the carrier of FA) Element of bool [:[: the carrier of FA,(Lex E):], the carrier of FA:]
the carrier of FA is set
[: the carrier of FA,(Lex E):] is V15() set
[:[: the carrier of FA,(Lex E):], the carrier of FA:] is V15() set
bool [:[: the carrier of FA,(Lex E):], the carrier of FA:] is non empty set
E ^omega is non empty functional set
c₄ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
x is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
bNFA is Element of the carrier of FA
[bNFA,c₄] is V26() set
dom the Tran of FA is V15() V18( the carrier of FA) V19( Lex E) Element of bool [: the carrier of FA,(Lex E):]
bool [: the carrier of FA,(Lex E):] is non empty set
[bNFA,x] is V26() set
Es is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
c₄ ^ Es is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(E)
u is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
x ^ u is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(E)
<%> E is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(E) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(E)
rng (dom the Tran of FA) is functional Element of bool (Lex E)
bool (Lex E) is non empty set
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
FA is functional Element of bool (E ^omega)
Lex E is non empty functional Element of bool K232(E)
K232(E) is non empty functional M11(E)
bool K232(E) is non empty set
bNFA is non empty transition-system over FA
the carrier of bNFA is non empty set
bool the carrier of bNFA is non empty set
[:(bool the carrier of bNFA),(E ^omega):] is non empty V15() set
[:(bool the carrier of bNFA),(Lex E):] is non empty V15() set
[:[:(bool the carrier of bNFA),(Lex E):],(bool the carrier of bNFA):] is non empty V15() set
bool [:[:(bool the carrier of bNFA),(Lex E):],(bool the carrier of bNFA):] is non empty set
x is V15() V18([:(bool the carrier of bNFA),(Lex E):]) V19( bool the carrier of bNFA) Element of bool [:[:(bool the carrier of bNFA),(Lex E):],(bool the carrier of bNFA):]
transition-system(# (bool the carrier of bNFA),x #) is strict transition-system over Lex E
u is strict transition-system over Lex E
the carrier of u is set
the Tran of u is V15() V18([: the carrier of u,(Lex E):]) V19( the carrier of u) Element of bool [:[: the carrier of u,(Lex E):], the carrier of u:]
[: the carrier of u,(Lex E):] is V15() set
[:[: the carrier of u,(Lex E):], the carrier of u:] is V15() set
bool [:[: the carrier of u,(Lex E):], the carrier of u:] is non empty set
v is Element of bool the carrier of bNFA
bTS is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
[v,bTS] is V26() Element of [:(bool the carrier of bNFA),(E ^omega):]
len bTS is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 bTS is V6() V10() V11() ext-real non negative finite cardinal V69() set
bTS -succ_of (v,bNFA) is Element of bool the carrier of bNFA
v1 is Element of bool the carrier of bNFA
[[v,bTS],v1] is V26() Element of [:[:(bool the carrier of bNFA),(E ^omega):],(bool the carrier of bNFA):]
[:[:(bool the carrier of bNFA),(E ^omega):],(bool the carrier of bNFA):] is non empty V15() set
v2 is Element of [:(bool the carrier of bNFA),(Lex E):]
[v2,v1] is V26() Element of [:[:(bool the carrier of bNFA),(Lex E):],(bool the carrier of bNFA):]
v2 is Element of bool the carrier of bNFA
u1 is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
[v2,u1] is V26() Element of [:(bool the carrier of bNFA),(E ^omega):]
len u1 is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 u1 is V6() V10() V11() ext-real non negative finite cardinal V69() set
u1 -succ_of (v2,bNFA) is Element of bool the carrier of bNFA
v2 is Element of [:(bool the carrier of bNFA),(Lex E):]
[v2,v1] is V26() Element of [:[:(bool the carrier of bNFA),(Lex E):],(bool the carrier of bNFA):]
x is strict transition-system over Lex E
the carrier of x is set
the Tran of x is V15() V18([: the carrier of x,(Lex E):]) V19( the carrier of x) Element of bool [:[: the carrier of x,(Lex E):], the carrier of x:]
[: the carrier of x,(Lex E):] is V15() set
[:[: the carrier of x,(Lex E):], the carrier of x:] is V15() set
bool [:[: the carrier of x,(Lex E):], the carrier of x:] is non empty set
Es is strict transition-system over Lex E
the carrier of Es is set
the Tran of Es is V15() V18([: the carrier of Es,(Lex E):]) V19( the carrier of Es) Element of bool [:[: the carrier of Es,(Lex E):], the carrier of Es:]
[: the carrier of Es,(Lex E):] is V15() set
[:[: the carrier of Es,(Lex E):], the carrier of Es:] is V15() set
bool [:[: the carrier of Es,(Lex E):], the carrier of Es:] is non empty set
u is set
[:(bool the carrier of bNFA),(Lex E):] is non empty V15() set
v is set
bTS is set
[v,bTS] is V26() set
v2 is set
v2 is set
[v2,v2] is V26() set
xi is V15() Function-like Element of Lex E
xc is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
len xc is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 xc is V6() V10() V11() ext-real non negative finite cardinal V69() set
v1 is Element of bool the carrier of bNFA
u1 is Element of bool the carrier of bNFA
xi -succ_of (u1,bNFA) is Element of bool the carrier of bNFA
u is set
[:(bool the carrier of bNFA),(Lex E):] is non empty V15() set
v is set
bTS is set
[v,bTS] is V26() set
v2 is set
v2 is set
[v2,v2] is V26() set
xi is V15() Function-like Element of Lex E
xc is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
len xc is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 xc is V6() V10() V11() ext-real non negative finite cardinal V69() set
v1 is Element of bool the carrier of bNFA
u1 is Element of bool the carrier of bNFA
xi -succ_of (u1,bNFA) is Element of bool the carrier of bNFA
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
FA is functional Element of bool (E ^omega)
bNFA is non empty transition-system over FA
(E,FA,bNFA) is strict transition-system over Lex E
Lex E is non empty functional Element of bool K232(E)
K232(E) is non empty functional M11(E)
bool K232(E) is non empty set
the carrier of (E,FA,bNFA) is set
the Tran of (E,FA,bNFA) is V15() V18([: the carrier of (E,FA,bNFA),(Lex E):]) V19( the carrier of (E,FA,bNFA)) Element of bool [:[: the carrier of (E,FA,bNFA),(Lex E):], the carrier of (E,FA,bNFA):]
[: the carrier of (E,FA,bNFA),(Lex E):] is V15() set
[:[: the carrier of (E,FA,bNFA),(Lex E):], the carrier of (E,FA,bNFA):] is V15() set
bool [:[: the carrier of (E,FA,bNFA),(Lex E):], the carrier of (E,FA,bNFA):] is non empty set
u is set
v is set
[u,v] is V26() set
bTS is set
[u,bTS] is V26() set
the carrier of bNFA is non empty set
bool the carrier of bNFA is non empty set
v1 is Element of [: the carrier of (E,FA,bNFA),(Lex E):]
u1 is set
xi is set
[u1,xi] is V26() set
xi is V15() Function-like Element of Lex E
xc is Element of the carrier of (E,FA,bNFA)
v2 is Element of the carrier of (E,FA,bNFA)
v2 is Element of the carrier of (E,FA,bNFA)
y1 is Element of bool the carrier of bNFA
xi is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
xc is Element of bool the carrier of bNFA
xi -succ_of (xc,bNFA) is Element of bool the carrier of bNFA
y2 is Element of bool the carrier of bNFA
the carrier of bNFA is non empty set
bool the carrier of bNFA is non empty set
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
FA is functional Element of bool (E ^omega)
bNFA is non empty finite transition-system over FA
(E,FA,bNFA) is non empty strict deterministic transition-system over Lex E
Lex E is non empty functional Element of bool K232(E)
K232(E) is non empty functional M11(E)
bool K232(E) is non empty set
the carrier of bNFA is non empty finite set
bool the carrier of bNFA is non empty finite V43() set
E is set
FA is set
bNFA is non empty set
bNFA ^omega is non empty functional set
bool (bNFA ^omega) is non empty set
Lex bNFA is non empty functional Element of bool K232(bNFA)
K232(bNFA) is non empty functional M11(bNFA)
bool K232(bNFA) is non empty set
<%> bNFA is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(bNFA) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(bNFA)
c₄ is Element of bNFA
<%c₄%> is non empty trivial V8() V15() V18( NAT ) V19(bNFA) Function-like constant finite 1 -element V67() Element of K232(bNFA)
x is functional Element of bool (bNFA ^omega)
Es is non empty transition-system over x
(bNFA,x,Es) is non empty strict deterministic transition-system over Lex bNFA
the carrier of (bNFA,x,Es) is non empty set
[: the carrier of (bNFA,x,Es),(Lex bNFA):] is non empty V15() set
the Tran of (bNFA,x,Es) is V15() V18([: the carrier of (bNFA,x,Es),(Lex bNFA):]) V19( the carrier of (bNFA,x,Es)) Element of bool [:[: the carrier of (bNFA,x,Es),(Lex bNFA):], the carrier of (bNFA,x,Es):]
[:[: the carrier of (bNFA,x,Es),(Lex bNFA):], the carrier of (bNFA,x,Es):] is non empty V15() set
bool [:[: the carrier of (bNFA,x,Es),(Lex bNFA):], the carrier of (bNFA,x,Es):] is non empty set
dom the Tran of (bNFA,x,Es) is V15() V18( the carrier of (bNFA,x,Es)) V19( Lex bNFA) Element of bool [: the carrier of (bNFA,x,Es),(Lex bNFA):]
bool [: the carrier of (bNFA,x,Es),(Lex bNFA):] is non empty set
rng (dom the Tran of (bNFA,x,Es)) is functional Element of bool (Lex bNFA)
bool (Lex bNFA) is non empty set
E is set
FA is non empty set
FA ^omega is non empty functional set
bool (FA ^omega) is non empty set
Lex FA is non empty functional Element of bool K232(FA)
K232(FA) is non empty functional M11(FA)
bool K232(FA) is non empty set
bNFA is V8() V15() V18( NAT ) Function-like finite V67() Element of FA ^omega
len bNFA is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 bNFA is V6() V10() V11() ext-real non negative finite cardinal V69() set
c₄ is functional Element of bool (FA ^omega)
x is non empty transition-system over c₄
the carrier of x is non empty set
bool the carrier of x is non empty set
(FA,c₄,x) is non empty strict deterministic transition-system over Lex FA
Es is Element of bool the carrier of x
bNFA -succ_of (Es,x) is Element of bool the carrier of x
[Es,bNFA] is V26() Element of [:(bool the carrier of x),(FA ^omega):]
[:(bool the carrier of x),(FA ^omega):] is non empty V15() set
[[Es,bNFA],E] is V26() set
the Tran of (FA,c₄,x) is V15() V18([: the carrier of (FA,c₄,x),(Lex FA):]) V19( the carrier of (FA,c₄,x)) Element of bool [:[: the carrier of (FA,c₄,x),(Lex FA):], the carrier of (FA,c₄,x):]
the carrier of (FA,c₄,x) is non empty set
[: the carrier of (FA,c₄,x),(Lex FA):] is non empty V15() set
[:[: the carrier of (FA,c₄,x),(Lex FA):], the carrier of (FA,c₄,x):] is non empty V15() set
bool [:[: the carrier of (FA,c₄,x),(Lex FA):], the carrier of (FA,c₄,x):] is non empty set
<%> FA is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(FA) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(FA)
<%> FA is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(FA) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(FA)
bNFA . 0 is set
bNFA ^ 0 is V8() V15() V18( NAT ) Function-like finite V67() set
u is Element of FA
<%u%> is non empty trivial V8() V15() V18( NAT ) V19(FA) Function-like constant finite 1 -element V67() Element of K232(FA)
the carrier of (FA,c₄,x) is non empty set
[:(bool the carrier of x),(FA ^omega):] is non empty V15() set
[Es,bNFA] is V26() Element of [:(bool the carrier of x),(FA ^omega):]
u is Element of bool the carrier of x
[[Es,bNFA],u] is V26() Element of [:[:(bool the carrier of x),(FA ^omega):],(bool the carrier of x):]
[:[:(bool the carrier of x),(FA ^omega):],(bool the carrier of x):] is non empty V15() set
the Tran of (FA,c₄,x) is V15() V18([: the carrier of (FA,c₄,x),(Lex FA):]) V19( the carrier of (FA,c₄,x)) Element of bool [:[: the carrier of (FA,c₄,x),(Lex FA):], the carrier of (FA,c₄,x):]
[: the carrier of (FA,c₄,x),(Lex FA):] is non empty V15() set
[:[: the carrier of (FA,c₄,x),(Lex FA):], the carrier of (FA,c₄,x):] is non empty V15() set
bool [:[: the carrier of (FA,c₄,x),(Lex FA):], the carrier of (FA,c₄,x):] is non empty set
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
FA is functional Element of bool (E ^omega)
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
FA is functional Element of bool (E ^omega)
the non empty finite set is non empty finite set
[: the non empty finite set ,FA:] is V15() set
[:[: the non empty finite set ,FA:], the non empty finite set :] is V15() set
bool [:[: the non empty finite set ,FA:], the non empty finite set :] is non empty set
the Element of the non empty finite set is Element of the non empty finite set
bool the non empty finite set is non empty finite V43() set
{ the Element of the non empty finite set } is non empty trivial finite 1 -element Element of bool the non empty finite set
c₄ is V15() V18([: the non empty finite set ,FA:]) V19( the non empty finite set ) Element of bool [:[: the non empty finite set ,FA:], the non empty finite set :]
Es is finite Element of bool the non empty finite set
(E,FA, the non empty finite set ,c₄,Es) is (E,FA) (E,FA)
u is (E,FA) (E,FA)
the carrier of u is set
the Tran of u is V15() V18([: the carrier of u,FA:]) V19( the carrier of u) Element of bool [:[: the carrier of u,FA:], the carrier of u:]
[: the carrier of u,FA:] is V15() set
[:[: the carrier of u,FA:], the carrier of u:] is V15() set
bool [:[: the carrier of u,FA:], the carrier of u:] is non empty set
transition-system(# the carrier of u, the Tran of u #) is strict transition-system over FA
the of u is Element of bool the carrier of u
bool the carrier of u is non empty set
card the of u is V6() cardinal set
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
FA is functional Element of bool (E ^omega)
bNFA is non empty (E,FA)
the carrier of bNFA is non empty set
the Tran of bNFA is V15() V18([: the carrier of bNFA,FA:]) V19( the carrier of bNFA) Element of bool [:[: the carrier of bNFA,FA:], the carrier of bNFA:]
[: the carrier of bNFA,FA:] is V15() set
[:[: the carrier of bNFA,FA:], the carrier of bNFA:] is V15() set
bool [:[: the carrier of bNFA,FA:], the carrier of bNFA:] is non empty set
transition-system(# the carrier of bNFA, the Tran of bNFA #) is strict transition-system over FA
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
FA is functional Element of bool (E ^omega)
Lex E is non empty functional Element of bool K232(E)
K232(E) is non empty functional M11(E)
bool K232(E) is non empty set
bNFA is non empty (E,FA)
the carrier of bNFA is non empty set
the Tran of bNFA is V15() V18([: the carrier of bNFA,FA:]) V19( the carrier of bNFA) Element of bool [:[: the carrier of bNFA,FA:], the carrier of bNFA:]
[: the carrier of bNFA,FA:] is V15() set
[:[: the carrier of bNFA,FA:], the carrier of bNFA:] is V15() set
bool [:[: the carrier of bNFA,FA:], the carrier of bNFA:] is non empty set
transition-system(# the carrier of bNFA, the Tran of bNFA #) is non empty strict transition-system over FA
(E,FA,transition-system(# the carrier of bNFA, the Tran of bNFA #)) is non empty strict deterministic transition-system over Lex E
bool the carrier of bNFA is non empty set
<%> E is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(E) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(E)
the of bNFA is Element of bool the carrier of bNFA
(<%> E) -succ_of ( the of bNFA,bNFA) is Element of bool the carrier of bNFA
{((<%> E) -succ_of ( the of bNFA,bNFA))} is non empty trivial finite 1 -element Element of bool (bool the carrier of bNFA)
bool (bool the carrier of bNFA) is non empty set
c₄ is non empty transition-system over FA
(E,FA,c₄) is non empty strict deterministic transition-system over Lex E
the carrier of (E,FA,c₄) is non empty set
bool the carrier of (E,FA,c₄) is non empty set
[: the carrier of (E,FA,c₄),(Lex E):] is non empty V15() set
[:[: the carrier of (E,FA,c₄),(Lex E):], the carrier of (E,FA,c₄):] is non empty V15() set
bool [:[: the carrier of (E,FA,c₄),(Lex E):], the carrier of (E,FA,c₄):] is non empty set
the Tran of (E,FA,c₄) is V15() V18([: the carrier of (E,FA,c₄),(Lex E):]) V19( the carrier of (E,FA,c₄)) Element of bool [:[: the carrier of (E,FA,c₄),(Lex E):], the carrier of (E,FA,c₄):]
u is V15() V18([: the carrier of (E,FA,c₄),(Lex E):]) V19( the carrier of (E,FA,c₄)) Element of bool [:[: the carrier of (E,FA,c₄),(Lex E):], the carrier of (E,FA,c₄):]
Es is Element of bool the carrier of (E,FA,c₄)
(E,(Lex E), the carrier of (E,FA,c₄),u,Es) is (E, Lex E) (E, Lex E)
card Es is V6() cardinal set
bTS is non empty (E, Lex E) (E, Lex E) (E, Lex E)
the carrier of bTS is non empty set
the Tran of bTS is V15() V18([: the carrier of bTS,(Lex E):]) V19( the carrier of bTS) Element of bool [:[: the carrier of bTS,(Lex E):], the carrier of bTS:]
[: the carrier of bTS,(Lex E):] is non empty V15() set
[:[: the carrier of bTS,(Lex E):], the carrier of bTS:] is non empty V15() set
bool [:[: the carrier of bTS,(Lex E):], the carrier of bTS:] is non empty set
transition-system(# the carrier of bTS, the Tran of bTS #) is non empty strict transition-system over Lex E
the of bTS is Element of bool the carrier of bTS
bool the carrier of bTS is non empty set
c₄ is (E, Lex E) (E, Lex E)
the carrier of c₄ is set
the Tran of c₄ is V15() V18([: the carrier of c₄,(Lex E):]) V19( the carrier of c₄) Element of bool [:[: the carrier of c₄,(Lex E):], the carrier of c₄:]
[: the carrier of c₄,(Lex E):] is V15() set
[:[: the carrier of c₄,(Lex E):], the carrier of c₄:] is V15() set
bool [:[: the carrier of c₄,(Lex E):], the carrier of c₄:] is non empty set
transition-system(# the carrier of c₄, the Tran of c₄ #) is strict transition-system over Lex E
the of c₄ is Element of bool the carrier of c₄
bool the carrier of c₄ is non empty set
x is (E, Lex E) (E, Lex E)
the carrier of x is set
the Tran of x is V15() V18([: the carrier of x,(Lex E):]) V19( the carrier of x) Element of bool [:[: the carrier of x,(Lex E):], the carrier of x:]
[: the carrier of x,(Lex E):] is V15() set
[:[: the carrier of x,(Lex E):], the carrier of x:] is V15() set
bool [:[: the carrier of x,(Lex E):], the carrier of x:] is non empty set
transition-system(# the carrier of x, the Tran of x #) is strict transition-system over Lex E
the of x is Element of bool the carrier of x
bool the carrier of x is non empty set
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
FA is functional Element of bool (E ^omega)
bNFA is non empty (E,FA)
(E,FA,bNFA) is (E, Lex E) (E, Lex E)
Lex E is non empty functional Element of bool K232(E)
K232(E) is non empty functional M11(E)
bool K232(E) is non empty set
the of (E,FA,bNFA) is Element of bool the carrier of (E,FA,bNFA)
the carrier of (E,FA,bNFA) is set
bool the carrier of (E,FA,bNFA) is non empty set
the carrier of bNFA is non empty set
bool the carrier of bNFA is non empty set
<%> E is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(E) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(E)
the of bNFA is Element of bool the carrier of bNFA
(<%> E) -succ_of ( the of bNFA,bNFA) is Element of bool the carrier of bNFA
{((<%> E) -succ_of ( the of bNFA,bNFA))} is non empty trivial finite 1 -element Element of bool (bool the carrier of bNFA)
bool (bool the carrier of bNFA) is non empty set
card the of (E,FA,bNFA) is V6() cardinal set
the Tran of (E,FA,bNFA) is V15() V18([: the carrier of (E,FA,bNFA),(Lex E):]) V19( the carrier of (E,FA,bNFA)) Element of bool [:[: the carrier of (E,FA,bNFA),(Lex E):], the carrier of (E,FA,bNFA):]
[: the carrier of (E,FA,bNFA),(Lex E):] is V15() set
[:[: the carrier of (E,FA,bNFA),(Lex E):], the carrier of (E,FA,bNFA):] is V15() set
bool [:[: the carrier of (E,FA,bNFA),(Lex E):], the carrier of (E,FA,bNFA):] is non empty set
transition-system(# the carrier of (E,FA,bNFA), the Tran of (E,FA,bNFA) #) is strict transition-system over Lex E
the Tran of bNFA is V15() V18([: the carrier of bNFA,FA:]) V19( the carrier of bNFA) Element of bool [:[: the carrier of bNFA,FA:], the carrier of bNFA:]
[: the carrier of bNFA,FA:] is V15() set
[:[: the carrier of bNFA,FA:], the carrier of bNFA:] is V15() set
bool [:[: the carrier of bNFA,FA:], the carrier of bNFA:] is non empty set
transition-system(# the carrier of bNFA, the Tran of bNFA #) is non empty strict transition-system over FA
(E,FA,transition-system(# the carrier of bNFA, the Tran of bNFA #)) is non empty strict deterministic transition-system over Lex E
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
FA is functional Element of bool (E ^omega)
bNFA is non empty (E,FA)
(E,FA,bNFA) is non empty (E, Lex E) (E, Lex E) (E, Lex E)
Lex E is non empty functional Element of bool K232(E)
K232(E) is non empty functional M11(E)
bool K232(E) is non empty set
the carrier of (E,FA,bNFA) is non empty set
the carrier of bNFA is non empty set
bool the carrier of bNFA is non empty set
the Tran of (E,FA,bNFA) is V15() V18([: the carrier of (E,FA,bNFA),(Lex E):]) V19( the carrier of (E,FA,bNFA)) Element of bool [:[: the carrier of (E,FA,bNFA),(Lex E):], the carrier of (E,FA,bNFA):]
[: the carrier of (E,FA,bNFA),(Lex E):] is non empty V15() set
[:[: the carrier of (E,FA,bNFA),(Lex E):], the carrier of (E,FA,bNFA):] is non empty V15() set
bool [:[: the carrier of (E,FA,bNFA),(Lex E):], the carrier of (E,FA,bNFA):] is non empty set
transition-system(# the carrier of (E,FA,bNFA), the Tran of (E,FA,bNFA) #) is non empty strict transition-system over Lex E
the Tran of bNFA is V15() V18([: the carrier of bNFA,FA:]) V19( the carrier of bNFA) Element of bool [:[: the carrier of bNFA,FA:], the carrier of bNFA:]
[: the carrier of bNFA,FA:] is V15() set
[:[: the carrier of bNFA,FA:], the carrier of bNFA:] is V15() set
bool [:[: the carrier of bNFA,FA:], the carrier of bNFA:] is non empty set
transition-system(# the carrier of bNFA, the Tran of bNFA #) is non empty strict transition-system over FA
(E,FA,transition-system(# the carrier of bNFA, the Tran of bNFA #)) is non empty strict deterministic transition-system over Lex E
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
FA is functional Element of bool (E ^omega)
bNFA is non empty finite (E,FA)
(E,FA,bNFA) is non empty (E, Lex E) (E, Lex E) (E, Lex E)
Lex E is non empty functional Element of bool K232(E)
K232(E) is non empty functional M11(E)
bool K232(E) is non empty set
the carrier of bNFA is non empty finite set
bool the carrier of bNFA is non empty finite V43() set
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
FA is functional Element of bool (E ^omega)
bNFA is non empty (E,FA)
the carrier of bNFA is non empty set
bool the carrier of bNFA is non empty set
c₄ is Element of bool the carrier of bNFA
the of bNFA is Element of bool the carrier of bNFA
{ b₁ where b₁ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : not c₄ misses b₁ -succ_of ( the of bNFA,bNFA) } is set
{ b₁ where b₁ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : S₁[b₁] } is set
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
FA is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
bNFA is functional Element of bool (E ^omega)
c₄ is non empty (E,bNFA)
the carrier of c₄ is non empty set
bool the carrier of c₄ is non empty set
the of c₄ is Element of bool the carrier of c₄
FA -succ_of ( the of c₄,c₄) is Element of bool the carrier of c₄
x is Element of bool the carrier of c₄
(E,bNFA,c₄,x) is functional Element of bool (E ^omega)
{ b₁ where b₁ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : not x misses b₁ -succ_of ( the of c₄,c₄) } is set
Es is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
Es -succ_of ( the of c₄,c₄) is Element of bool the carrier of c₄
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
FA is functional Element of bool (E ^omega)
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
FA is functional Element of bool (E ^omega)
the non empty finite set is non empty finite set
[: the non empty finite set ,FA:] is V15() set
[:[: the non empty finite set ,FA:], the non empty finite set :] is V15() set
bool [:[: the non empty finite set ,FA:], the non empty finite set :] is non empty set
the Element of the non empty finite set is Element of the non empty finite set
bool the non empty finite set is non empty finite V43() set
{ the Element of the non empty finite set } is non empty trivial finite 1 -element Element of bool the non empty finite set
c₄ is V15() V18([: the non empty finite set ,FA:]) V19( the non empty finite set ) Element of bool [:[: the non empty finite set ,FA:], the non empty finite set :]
Es is finite Element of bool the non empty finite set
(E,FA, the non empty finite set ,c₄,Es,Es) is (E,FA) (E,FA)
u is (E,FA) (E,FA)
the carrier of u is set
the Tran of u is V15() V18([: the carrier of u,FA:]) V19( the carrier of u) Element of bool [:[: the carrier of u,FA:], the carrier of u:]
[: the carrier of u,FA:] is V15() set
[:[: the carrier of u,FA:], the carrier of u:] is V15() set
bool [:[: the carrier of u,FA:], the carrier of u:] is non empty set
transition-system(# the carrier of u, the Tran of u #) is strict transition-system over FA
the of u is Element of bool the carrier of u
bool the carrier of u is non empty set
card the of u is V6() cardinal set
(E,FA, the carrier of u, the Tran of u, the of u) is (E,FA) (E,FA)
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
FA is functional Element of bool (E ^omega)
bNFA is non empty (E,FA)
the carrier of bNFA is non empty set
the Tran of bNFA is V15() V18([: the carrier of bNFA,FA:]) V19( the carrier of bNFA) Element of bool [:[: the carrier of bNFA,FA:], the carrier of bNFA:]
[: the carrier of bNFA,FA:] is V15() set
[:[: the carrier of bNFA,FA:], the carrier of bNFA:] is V15() set
bool [:[: the carrier of bNFA,FA:], the carrier of bNFA:] is non empty set
transition-system(# the carrier of bNFA, the Tran of bNFA #) is non empty strict transition-system over FA
the of bNFA is Element of bool the carrier of bNFA
bool the carrier of bNFA is non empty set
(E,FA, the carrier of bNFA, the Tran of bNFA, the of bNFA) is (E,FA) (E,FA)
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
FA is functional Element of bool (E ^omega)
Lex E is non empty functional Element of bool K232(E)
K232(E) is non empty functional M11(E)
bool K232(E) is non empty set
bNFA is non empty (E,FA)
the carrier of bNFA is non empty set
the Tran of bNFA is V15() V18([: the carrier of bNFA,FA:]) V19( the carrier of bNFA) Element of bool [:[: the carrier of bNFA,FA:], the carrier of bNFA:]
[: the carrier of bNFA,FA:] is V15() set
[:[: the carrier of bNFA,FA:], the carrier of bNFA:] is V15() set
bool [:[: the carrier of bNFA,FA:], the carrier of bNFA:] is non empty set
the of bNFA is Element of bool the carrier of bNFA
bool the carrier of bNFA is non empty set
(E,FA, the carrier of bNFA, the Tran of bNFA, the of bNFA) is non empty (E,FA) (E,FA)
(E,FA,(E,FA, the carrier of bNFA, the Tran of bNFA, the of bNFA)) is non empty (E, Lex E) (E, Lex E) (E, Lex E)
the of bNFA is Element of bool the carrier of bNFA
c₄ is non empty (E,FA)
(E,FA,c₄) is non empty (E, Lex E) (E, Lex E) (E, Lex E)
the carrier of (E,FA,c₄) is non empty set
[: the carrier of (E,FA,c₄),(Lex E):] is non empty V15() set
[:[: the carrier of (E,FA,c₄),(Lex E):], the carrier of (E,FA,c₄):] is non empty V15() set
bool [:[: the carrier of (E,FA,c₄),(Lex E):], the carrier of (E,FA,c₄):] is non empty set
the Tran of (E,FA,c₄) is V15() V18([: the carrier of (E,FA,c₄),(Lex E):]) V19( the carrier of (E,FA,c₄)) Element of bool [:[: the carrier of (E,FA,c₄),(Lex E):], the carrier of (E,FA,c₄):]
the of (E,FA,c₄) is Element of bool the carrier of (E,FA,c₄)
bool the carrier of (E,FA,c₄) is non empty set
{ b₁ where b₁ is Element of the carrier of (E,FA,c₄) : not b₁ misses the of bNFA } is set
{ b₁ where b₁ is Element of the carrier of (E,FA,c₄) : S₁[b₁] } is set
Es is V15() V18([: the carrier of (E,FA,c₄),(Lex E):]) V19( the carrier of (E,FA,c₄)) Element of bool [:[: the carrier of (E,FA,c₄),(Lex E):], the carrier of (E,FA,c₄):]
v is Element of bool the carrier of (E,FA,c₄)
(E,(Lex E), the carrier of (E,FA,c₄),Es, the of (E,FA,c₄),v) is (E, Lex E) (E, Lex E)
v1 is non empty (E, Lex E) (E, Lex E) (E, Lex E)
the carrier of v1 is non empty set
the Tran of v1 is V15() V18([: the carrier of v1,(Lex E):]) V19( the carrier of v1) Element of bool [:[: the carrier of v1,(Lex E):], the carrier of v1:]
[: the carrier of v1,(Lex E):] is non empty V15() set
[:[: the carrier of v1,(Lex E):], the carrier of v1:] is non empty V15() set
bool [:[: the carrier of v1,(Lex E):], the carrier of v1:] is non empty set
the of v1 is Element of bool the carrier of v1
bool the carrier of v1 is non empty set
(E,(Lex E), the carrier of v1, the Tran of v1, the of v1) is non empty (E, Lex E) (E, Lex E)
the of v1 is Element of bool the carrier of v1
{ b₁ where b₁ is Element of the carrier of v1 : not b₁ misses the of bNFA } is set
c₄ is (E, Lex E) (E, Lex E)
the carrier of c₄ is set
the Tran of c₄ is V15() V18([: the carrier of c₄,(Lex E):]) V19( the carrier of c₄) Element of bool [:[: the carrier of c₄,(Lex E):], the carrier of c₄:]
[: the carrier of c₄,(Lex E):] is V15() set
[:[: the carrier of c₄,(Lex E):], the carrier of c₄:] is V15() set
bool [:[: the carrier of c₄,(Lex E):], the carrier of c₄:] is non empty set
the of c₄ is Element of bool the carrier of c₄
bool the carrier of c₄ is non empty set
(E,(Lex E), the carrier of c₄, the Tran of c₄, the of c₄) is (E, Lex E) (E, Lex E)
the of c₄ is Element of bool the carrier of c₄
{ b₁ where b₁ is Element of the carrier of c₄ : not b₁ misses the of bNFA } is set
x is (E, Lex E) (E, Lex E)
the carrier of x is set
the Tran of x is V15() V18([: the carrier of x,(Lex E):]) V19( the carrier of x) Element of bool [:[: the carrier of x,(Lex E):], the carrier of x:]
[: the carrier of x,(Lex E):] is V15() set
[:[: the carrier of x,(Lex E):], the carrier of x:] is V15() set
bool [:[: the carrier of x,(Lex E):], 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
(E,(Lex E), the carrier of x, the Tran of x, the of x) is (E, Lex E) (E, Lex E)
the of x is Element of bool the carrier of x
{ b₁ where b₁ is Element of the carrier of x : not b₁ misses the of bNFA } is set
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
FA is functional Element of bool (E ^omega)
bNFA is non empty (E,FA)
(E,FA,bNFA) is (E, Lex E) (E, Lex E)
Lex E is non empty functional Element of bool K232(E)
K232(E) is non empty functional M11(E)
bool K232(E) is non empty set
the carrier of (E,FA,bNFA) is set
the Tran of (E,FA,bNFA) is V15() V18([: the carrier of (E,FA,bNFA),(Lex E):]) V19( the carrier of (E,FA,bNFA)) Element of bool [:[: the carrier of (E,FA,bNFA),(Lex E):], the carrier of (E,FA,bNFA):]
[: the carrier of (E,FA,bNFA),(Lex E):] is V15() set
[:[: the carrier of (E,FA,bNFA),(Lex E):], the carrier of (E,FA,bNFA):] is V15() set
bool [:[: the carrier of (E,FA,bNFA),(Lex E):], the carrier of (E,FA,bNFA):] is non empty set
the of (E,FA,bNFA) is Element of bool the carrier of (E,FA,bNFA)
bool the carrier of (E,FA,bNFA) is non empty set
(E,(Lex E), the carrier of (E,FA,bNFA), the Tran of (E,FA,bNFA), the of (E,FA,bNFA)) is (E, Lex E) (E, Lex E)
the carrier of bNFA is non empty set
the Tran of bNFA is V15() V18([: the carrier of bNFA,FA:]) V19( the carrier of bNFA) Element of bool [:[: the carrier of bNFA,FA:], the carrier of bNFA:]
[: the carrier of bNFA,FA:] is V15() set
[:[: the carrier of bNFA,FA:], the carrier of bNFA:] is V15() set
bool [:[: the carrier of bNFA,FA:], the carrier of bNFA:] is non empty set
the of bNFA is Element of bool the carrier of bNFA
bool the carrier of bNFA is non empty set
(E,FA, the carrier of bNFA, the Tran of bNFA, the of bNFA) is non empty (E,FA) (E,FA)
(E,FA,(E,FA, the carrier of bNFA, the Tran of bNFA, the of bNFA)) is non empty (E, Lex E) (E, Lex E) (E, Lex E)
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
FA is functional Element of bool (E ^omega)
bNFA is non empty (E,FA)
(E,FA,bNFA) is non empty (E, Lex E) (E, Lex E) (E, Lex E)
Lex E is non empty functional Element of bool K232(E)
K232(E) is non empty functional M11(E)
bool K232(E) is non empty set
the carrier of (E,FA,bNFA) is non empty set
the carrier of bNFA is non empty set
bool the carrier of bNFA is non empty set
the Tran of (E,FA,bNFA) is V15() V18([: the carrier of (E,FA,bNFA),(Lex E):]) V19( the carrier of (E,FA,bNFA)) Element of bool [:[: the carrier of (E,FA,bNFA),(Lex E):], the carrier of (E,FA,bNFA):]
[: the carrier of (E,FA,bNFA),(Lex E):] is non empty V15() set
[:[: the carrier of (E,FA,bNFA),(Lex E):], the carrier of (E,FA,bNFA):] is non empty V15() set
bool [:[: the carrier of (E,FA,bNFA),(Lex E):], the carrier of (E,FA,bNFA):] is non empty set
the of (E,FA,bNFA) is Element of bool the carrier of (E,FA,bNFA)
bool the carrier of (E,FA,bNFA) is non empty set
(E,(Lex E), the carrier of (E,FA,bNFA), the Tran of (E,FA,bNFA), the of (E,FA,bNFA)) is non empty (E, Lex E) (E, Lex E)
the Tran of bNFA is V15() V18([: the carrier of bNFA,FA:]) V19( the carrier of bNFA) Element of bool [:[: the carrier of bNFA,FA:], the carrier of bNFA:]
[: the carrier of bNFA,FA:] is V15() set
[:[: the carrier of bNFA,FA:], the carrier of bNFA:] is V15() set
bool [:[: the carrier of bNFA,FA:], the carrier of bNFA:] is non empty set
the of bNFA is Element of bool the carrier of bNFA
(E,FA, the carrier of bNFA, the Tran of bNFA, the of bNFA) is non empty (E,FA) (E,FA)
(E,FA,(E,FA, the carrier of bNFA, the Tran of bNFA, the of bNFA)) is non empty (E, Lex E) (E, Lex E) (E, Lex E)
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
FA is functional Element of bool (E ^omega)
bNFA is non empty finite (E,FA)
(E,FA,bNFA) is non empty (E, Lex E) (E, Lex E) (E, Lex E)
Lex E is non empty functional Element of bool K232(E)
K232(E) is non empty functional M11(E)
bool K232(E) is non empty set
the carrier of bNFA is non empty finite set
bool the carrier of bNFA is non empty finite V43() set
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
FA is functional Element of bool (E ^omega)
bNFA is non empty (E,FA)
the carrier of bNFA is non empty set
bool the carrier of bNFA is non empty set
c₄ is Element of bool the carrier of bNFA
the of bNFA is Element of bool the carrier of bNFA
{ b₁ where b₁ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : not b₁ -succ_of (c₄,bNFA) misses the of bNFA } is set
{ b₁ where b₁ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : S₁[b₁] } is set
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
FA is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
bNFA is functional Element of bool (E ^omega)
c₄ is non empty (E,bNFA)
the carrier of c₄ is non empty set
bool the carrier of c₄ is non empty set
the of c₄ is Element of bool the carrier of c₄
x is Element of bool the carrier of c₄
(E,bNFA,c₄,x) is functional Element of bool (E ^omega)
{ b₁ where b₁ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : not b₁ -succ_of (x,c₄) misses the of c₄ } is set
FA -succ_of (x,c₄) is Element of bool the carrier of c₄
Es is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
Es -succ_of (x,c₄) is Element of bool the carrier of c₄
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
FA is functional Element of bool (E ^omega)
bNFA is non empty (E,FA)
the carrier of bNFA is non empty set
the of bNFA is Element of bool the carrier of bNFA
bool the carrier of bNFA is non empty set
the of bNFA is Element of bool the carrier of bNFA
{ b₁ where b₁ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : ex b₂, b₃ being Element of the carrier of bNFA st
( b₂ in the of bNFA & b₃ in the of bNFA & b₂,b₁ ==>* b₃,bNFA ) } is set
{ b₁ where b₁ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : S₁[b₁] } is set
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
FA is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
bNFA is functional Element of bool (E ^omega)
c₄ is non empty (E,bNFA)
(E,bNFA,c₄) is functional Element of bool (E ^omega)
the carrier of c₄ is non empty set
the of c₄ is Element of bool the carrier of c₄
bool the carrier of c₄ is non empty set
the of c₄ is Element of bool the carrier of c₄
{ b₁ where b₁ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : ex b₂, b₃ being Element of the carrier of c₄ st
( b₂ in the of c₄ & b₃ in the of c₄ & b₂,b₁ ==>* b₃,c₄ ) } is set
x is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
Es is Element of the carrier of c₄
u is Element of the carrier of c₄
x is Element of the carrier of c₄
Es is Element of the carrier of c₄
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
FA is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
bNFA is functional Element of bool (E ^omega)
c₄ is non empty (E,bNFA)
(E,bNFA,c₄) is functional Element of bool (E ^omega)
the carrier of c₄ is non empty set
the of c₄ is Element of bool the carrier of c₄
bool the carrier of c₄ is non empty set
the of c₄ is Element of bool the carrier of c₄
{ b₁ where b₁ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : ex b₂, b₃ being Element of the carrier of c₄ st
( b₂ in the of c₄ & b₃ in the of c₄ & b₂,b₁ ==>* b₃,c₄ ) } is set
FA -succ_of ( the of c₄,c₄) is Element of bool the carrier of c₄
x is Element of the carrier of c₄
Es is Element of the carrier of c₄
x is set
Es is Element of the carrier of c₄
u is Element of the carrier of c₄
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
FA is functional Element of bool (E ^omega)
bNFA is non empty (E,FA)
(E,FA,bNFA) is functional Element of bool (E ^omega)
the carrier of bNFA is non empty set
the of bNFA is Element of bool the carrier of bNFA
bool the carrier of bNFA is non empty set
the of bNFA is Element of bool the carrier of bNFA
{ b₁ where b₁ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : ex b₂, b₃ being Element of the carrier of bNFA st
( b₂ in the of bNFA & b₃ in the of bNFA & b₂,b₁ ==>* b₃,bNFA ) } is set
(E,FA,bNFA, the of bNFA) is functional Element of bool (E ^omega)
{ b₁ where b₁ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : not the of bNFA misses b₁ -succ_of ( the of bNFA,bNFA) } is set
c₄ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
c₄ -succ_of ( the of bNFA,bNFA) is Element of bool the carrier of bNFA
c₄ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
c₄ -succ_of ( the of bNFA,bNFA) is Element of bool the carrier of bNFA
E is non empty set
E ^omega is non empty functional set
bool (E ^omega) is non empty set
FA is functional Element of bool (E ^omega)
bNFA is non empty (E,FA)
(E,FA,bNFA) is functional Element of bool (E ^omega)
the carrier of bNFA is non empty set
the of bNFA is Element of bool the carrier of bNFA
bool the carrier of bNFA is non empty set
the of bNFA is Element of bool the carrier of bNFA
{ b₁ where b₁ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : ex b₂, b₃ being Element of the carrier of bNFA st
( b₂ in the of bNFA & b₃ in the of bNFA & b₂,b₁ ==>* b₃,bNFA ) } is set
(E,FA,bNFA, the of bNFA) is functional Element of bool (E ^omega)
{ b₁ where b₁ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : not b₁ -succ_of ( the of bNFA,bNFA) misses the of bNFA } is set
c₄ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
c₄ -succ_of ( the of bNFA,bNFA) is Element of bool the carrier of bNFA
c₄ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
c₄ -succ_of ( the of bNFA,bNFA) is Element of bool the carrier of bNFA
E is non empty set
E ^omega is non empty functional set
K232(E) is non empty functional M11(E)
Lex E is non empty functional Element of bool K232(E)
bool K232(E) is non empty set
<%> E is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(E) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(E)
{(<%> E)} is non empty trivial functional V32() V33() V34() V35() V36() V37() finite V43() 1 -element Element of bool K232(E)
(Lex E) \/ {(<%> E)} is non empty functional Element of bool K232(E)
FA is Element of E
<%FA%> is non empty trivial V8() V15() V18( NAT ) V19(E) Function-like constant finite 1 -element V67() Element of K232(E)
bNFA is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
<%FA%> ^ bNFA is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(E)
c₄ is non empty transition-system over (Lex E) \/ {(<%> E)}
==>.-relation c₄ is V15() V18([: the carrier of c₄,(E ^omega):]) V19([: the carrier of c₄,(E ^omega):]) Element of bool [:[: the carrier of c₄,(E ^omega):],[: the carrier of c₄,(E ^omega):]:]
the carrier of c₄ is non empty set
[: the carrier of c₄,(E ^omega):] is non empty V15() set
[:[: the carrier of c₄,(E ^omega):],[: the carrier of c₄,(E ^omega):]:] is non empty V15() set
bool [:[: the carrier of c₄,(E ^omega):],[: the carrier of c₄,(E ^omega):]:] is non empty set
x is non empty V15() V18( NAT ) Function-like finite FinSequence-like FinSubsequence-like RedSequence of ==>.-relation c₄
x . 1 is set
(x . 1) `2 is set
len x is non empty V6() V10() V11() ext-real positive non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
x . (len x) is set
(x . (len x)) `2 is set
x . 2 is set
(x . 2) `2 is set
1 + 1 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
proj2 x is non empty finite set
dom x is non empty V32() V33() V34() V35() V36() V37() finite Element of bool NAT
[(x . 1),(x . 2)] is V26() set
Es is Element of the carrier of c<sub>4</sub>
u is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
[Es,u] is V26() Element of [: the carrier of c<sub>4</sub>,(E ^omega):]
v is Element of the carrier of c<sub>4</sub>
bTS is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
[v,bTS] is V26() Element of [: the carrier of c<sub>4</sub>,(E ^omega):]
v1 is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
v1 ^ bTS is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(E)
len v1 is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 v1 is V6() V10() V11() ext-real non negative finite cardinal V69() set
v1 . 0 is set
v2 is Element of E
<%v2%> is non empty trivial V8() V15() V18( NAT ) V19(E) Function-like constant finite 1 -element V67() Element of K232(E)
<%v2%> ^ bTS is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(E)
0 ^ bTS is V8() V15() V18( NAT ) Function-like finite V67() set
E is non empty set
E ^omega is non empty functional set
K232(E) is non empty functional M11(E)
Lex E is non empty functional Element of bool K232(E)
bool K232(E) is non empty set
<%> E is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(E) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(E)
{(<%> E)} is non empty trivial functional V32() V33() V34() V35() V36() V37() finite V43() 1 -element Element of bool K232(E)
(Lex E) \/ {(<%> E)} is non empty functional Element of bool K232(E)
FA is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
len FA is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 FA is V6() V10() V11() ext-real non negative finite cardinal V69() set
bNFA is non empty transition-system over (Lex E) \/ {(<%> E)}
==>.-relation bNFA is V15() V18([: the carrier of bNFA,(E ^omega):]) V19([: the carrier of bNFA,(E ^omega):]) Element of bool [:[: the carrier of bNFA,(E ^omega):],[: the carrier of bNFA,(E ^omega):]:]
the carrier of bNFA is non empty set
[: the carrier of bNFA,(E ^omega):] is non empty V15() set
[:[: the carrier of bNFA,(E ^omega):],[: the carrier of bNFA,(E ^omega):]:] is non empty V15() set
bool [:[: the carrier of bNFA,(E ^omega):],[: the carrier of bNFA,(E ^omega):]:] is non empty set
c<sub>4</sub> is V6() V10() V11() ext-real non negative finite cardinal V69() set
x is non empty V15() V18( NAT ) Function-like finite FinSequence-like FinSubsequence-like RedSequence of ==>.-relation bNFA
len x is non empty V6() V10() V11() ext-real positive non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
c<sub>4</sub> + 1 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
x . 1 is set
(x . 1) `2 is set
Es is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
x . (len x) is set
(x . (len x)) `2 is set
len Es is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 Es is V6() V10() V11() ext-real non negative finite cardinal V69() set
len Es is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 Es is V6() V10() V11() ext-real non negative finite cardinal V69() set
u is Element of E
<%u%> is non empty trivial V8() V15() V18( NAT ) V19(E) Function-like constant finite 1 -element V67() Element of K232(E)
v is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
<%u%> ^ v is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(E)
<*(x . 1)*> is non empty trivial V15() V18( NAT ) Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
bTS is non empty V15() V18( NAT ) Function-like finite FinSequence-like FinSubsequence-like RedSequence of ==>.-relation bNFA
<*(x . 1)*> ^ bTS is non empty V15() V18( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len bTS is non empty V6() V10() V11() ext-real positive non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
(len bTS) + 1 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
(len bTS) + 0 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
0 + 1 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
dom bTS is non empty V32() V33() V34() V35() V36() V37() finite Element of bool NAT
bTS . (len bTS) is set
(bTS . (len bTS)) `2 is set
1 + 1 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
(<*(x . 1)*> ^ bTS) . (1 + 1) is set
bTS . 1 is set
x . 2 is set
(x . 2) `2 is set
x . 2 is set
(x . 2) `2 is set
len v is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 v is V6() V10() V11() ext-real non negative finite cardinal V69() set
1 + (len v) is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
len <%u%> is non empty V6() V10() V11() ext-real positive non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 <%u%> is non empty trivial V6() V10() V11() ext-real positive non negative finite cardinal 1 -element V69() set
(len <%u%>) + (len v) is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
x . 2 is set
(x . 2) `2 is set
len Es is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 Es is V6() V10() V11() ext-real non negative finite cardinal V69() set
x is non empty V15() V18( NAT ) Function-like finite FinSequence-like FinSubsequence-like RedSequence of ==>.-relation bNFA
len x is non empty V6() V10() V11() ext-real positive non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
x . 1 is set
(x . 1) `2 is set
Es is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
x . (len x) is set
(x . (len x)) `2 is set
len Es is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 Es is V6() V10() V11() ext-real non negative finite cardinal V69() set
c<sub>4</sub> is non empty V15() V18( NAT ) Function-like finite FinSequence-like FinSubsequence-like RedSequence of ==>.-relation bNFA
len c<sub>4</sub> is non empty V6() V10() V11() ext-real positive non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
c<sub>4</sub> . 1 is set
(c<sub>4</sub> . 1) `2 is set
x is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
c₄ . (len c₄) is set
(c₄ . (len c₄)) `2 is set
len x is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 x is V6() V10() V11() ext-real non negative finite cardinal V69() set
c<sub>4</sub> is non empty V15() V18( NAT ) Function-like finite FinSequence-like FinSubsequence-like RedSequence of ==>.-relation bNFA
c<sub>4</sub> . 1 is set
(c<sub>4</sub> . 1) `2 is set
len c₄ is non empty V6() V10() V11() ext-real positive non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
c₄ . (len c₄) is set
(c₄ . (len c₄)) `2 is set
E is non empty set
E ^omega is non empty functional set
K232(E) is non empty functional M11(E)
Lex E is non empty functional Element of bool K232(E)
bool K232(E) is non empty set
<%> E is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(E) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(E)
{(<%> E)} is non empty trivial functional V32() V33() V34() V35() V36() V37() finite V43() 1 -element Element of bool K232(E)
(Lex E) \/ {(<%> E)} is non empty functional Element of bool K232(E)
FA is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
bNFA is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
FA ^ bNFA is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(E)
c<sub>4</sub> is non empty transition-system over (Lex E) \/ {(<%> E)}
==>.-relation c<sub>4</sub> is V15() V18([: the carrier of c<sub>4</sub>,(E ^omega):]) V19([: the carrier of c<sub>4</sub>,(E ^omega):]) Element of bool [:[: the carrier of c<sub>4</sub>,(E ^omega):],[: the carrier of c<sub>4</sub>,(E ^omega):]:]
the carrier of c<sub>4</sub> is non empty set
[: the carrier of c<sub>4</sub>,(E ^omega):] is non empty V15() set
[:[: the carrier of c<sub>4</sub>,(E ^omega):],[: the carrier of c<sub>4</sub>,(E ^omega):]:] is non empty V15() set
bool [:[: the carrier of c<sub>4</sub>,(E ^omega):],[: the carrier of c<sub>4</sub>,(E ^omega):]:] is non empty set
x is V6() V10() V11() ext-real non negative finite cardinal V69() set
x + 1 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
Es is non empty V15() V18( NAT ) Function-like finite FinSequence-like FinSubsequence-like RedSequence of ==>.-relation c<sub>4</sub>
len Es is non empty V6() V10() V11() ext-real positive non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
Es . 1 is set
(Es . 1) `2 is set
Es . (len Es) is set
(Es . (len Es)) `2 is set
dom Es is non empty V32() V33() V34() V35() V36() V37() finite Element of bool NAT
u is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
u ^ bNFA is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(E)
len u is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 u is V6() V10() V11() ext-real non negative finite cardinal V69() set
proj2 Es is non empty finite set
0 ^ bNFA is V8() V15() V18( NAT ) Function-like finite V67() set
len u is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 u is V6() V10() V11() ext-real non negative finite cardinal V69() set
v is Element of E
<%v%> is non empty trivial V8() V15() V18( NAT ) V19(E) Function-like constant finite 1 -element V67() Element of K232(E)
bTS is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
<%v%> ^ bTS is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(E)
0 + 1 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
len bNFA is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 bNFA is V6() V10() V11() ext-real non negative finite cardinal V69() set
1 + (len bNFA) is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
(len u) + (len bNFA) is V6() V10() V11() ext-real non negative finite cardinal V69() set
len (u ^ bNFA) is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 (u ^ bNFA) is V6() V10() V11() ext-real non negative finite cardinal V69() set
(len Es) + (len (u ^ bNFA)) is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
(len (u ^ bNFA)) + 1 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
v1 is non empty V15() V18( NAT ) Function-like finite FinSequence-like FinSubsequence-like RedSequence of ==>.-relation c<sub>4</sub>
len v1 is non empty V6() V10() V11() ext-real positive non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
(len v1) + 1 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
dom v1 is non empty V32() V33() V34() V35() V36() V37() finite Element of bool NAT
proj2 v1 is non empty finite set
v1 . 1 is set
(v1 . 1) `2 is set
1 + 1 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
Es . (1 + 1) is set
(Es . (1 + 1)) `2 is set
v1 . (len v1) is set
(v1 . (len v1)) `2 is set
bTS ^ bNFA is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(E)
<%v%> ^ (bTS ^ bNFA) is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(E)
Es . 2 is set
(Es . 2) `2 is set
v2 is V6() V10() V11() ext-real non negative finite cardinal V69() set
v1 . v2 is set
(v1 . v2) `2 is set
v2 + 1 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
Es . (v2 + 1) is set
(Es . (v2 + 1)) `2 is set
Es . 2 is set
(Es . 2) `2 is set
v2 is V6() V10() V11() ext-real non negative finite cardinal V69() set
v1 . v2 is set
(v1 . v2) `2 is set
v2 + 1 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
Es . (v2 + 1) is set
(Es . (v2 + 1)) `2 is set
Es . 2 is set
(Es . 2) `2 is set
len u is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 u is V6() V10() V11() ext-real non negative finite cardinal V69() set
x is non empty V15() V18( NAT ) Function-like finite FinSequence-like FinSubsequence-like RedSequence of ==>.-relation c<sub>4</sub>
len x is non empty V6() V10() V11() ext-real positive non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
x . 1 is set
(x . 1) `2 is set
Es is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
Es ^ bNFA is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(E)
x . (len x) is set
(x . (len x)) `2 is set
dom x is non empty V32() V33() V34() V35() V36() V37() finite Element of bool NAT
x is non empty V15() V18( NAT ) Function-like finite FinSequence-like FinSubsequence-like RedSequence of ==>.-relation c<sub>4</sub>
x . 1 is set
(x . 1) `2 is set
len x is non empty V6() V10() V11() ext-real positive non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
x . (len x) is set
(x . (len x)) `2 is set
dom x is non empty V32() V33() V34() V35() V36() V37() finite Element of bool NAT
E is non empty set
E ^omega is non empty functional set
bNFA is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
FA is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
c<sub>4</sub> is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
c<sub>4</sub> ^ bNFA is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(E)
K232(E) is non empty functional M11(E)
x is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
x ^ bNFA is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(E)
c<sub>4</sub> is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
x is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
Es is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
Es ^ bNFA is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(E)
K232(E) is non empty functional M11(E)
E is set
FA is set
bNFA is non empty set
bNFA ^omega is non empty functional set
K232(bNFA) is non empty functional M11(bNFA)
Lex bNFA is non empty functional Element of bool K232(bNFA)
bool K232(bNFA) is non empty set
<%> bNFA is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(bNFA) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(bNFA)
{(<%> bNFA)} is non empty trivial functional V32() V33() V34() V35() V36() V37() finite V43() 1 -element Element of bool K232(bNFA)
(Lex bNFA) \/ {(<%> bNFA)} is non empty functional Element of bool K232(bNFA)
c<sub>4</sub> is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
[E,c<sub>4</sub>] is V26() set
x is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
c<sub>4</sub> ^ x is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(bNFA)
[E,(c<sub>4</sub> ^ x)] is V26() set
Es is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
Es ^ x is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(bNFA)
[FA,(Es ^ x)] is V26() set
[FA,Es] is V26() set
u is non empty transition-system over (Lex bNFA) \/ {(<%> bNFA)}
==>.-relation u is V15() V18([: the carrier of u,(bNFA ^omega):]) V19([: the carrier of u,(bNFA ^omega):]) Element of bool [:[: the carrier of u,(bNFA ^omega):],[: the carrier of u,(bNFA ^omega):]:]
the carrier of u is non empty set
[: the carrier of u,(bNFA ^omega):] is non empty V15() set
[:[: the carrier of u,(bNFA ^omega):],[: the carrier of u,(bNFA ^omega):]:] is non empty V15() set
bool [:[: the carrier of u,(bNFA ^omega):],[: the carrier of u,(bNFA ^omega):]:] is non empty set
v is non empty V15() V18( NAT ) Function-like finite FinSequence-like FinSubsequence-like RedSequence of ==>.-relation u
v . 1 is set
len v is non empty V6() V10() V11() ext-real positive non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
v . (len v) is set
0 + 1 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
dom v is non empty V32() V33() V34() V35() V36() V37() finite Element of bool NAT
dim2 ((v . 1),bNFA) is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
(v . 1) `2 is set
bTS is V15() V18( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len bTS is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
dom bTS is V32() V33() V34() V35() V36() V37() finite Element of bool NAT
v1 is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
v1 + 1 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
bTS . v1 is set
bTS . (v1 + 1) is set
[(bTS . v1),(bTS . (v1 + 1))] is V26() set
v . v1 is set
(v . v1) `2 is set
v2 is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
v2 ^ (Es ^ x) is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(bNFA)
v . (v1 + 1) is set
(v . (v1 + 1)) `2 is set
v2 is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
v2 ^ (Es ^ x) is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(bNFA)
[(v . v1),(v . (v1 + 1))] is V26() set
(v . (v1 + 1)) `1 is set
[((v . (v1 + 1)) `1),(v2 ^ (Es ^ x))] is V26() set
[(v . v1),[((v . (v1 + 1)) `1),(v2 ^ (Es ^ x))]] is V26() set
(v . v1) `1 is set
[((v . v1) `1),(v2 ^ (Es ^ x))] is V26() set
[[((v . v1) `1),(v2 ^ (Es ^ x))],[((v . (v1 + 1)) `1),(v2 ^ (Es ^ x))]] is V26() set
u1 is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
u1 ^ (v2 ^ (Es ^ x)) is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(bNFA)
dim2 ((v . (v1 + 1)),bNFA) is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
xi is Element of the carrier of u
xc is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
[xi,xc] is V26() Element of [: the carrier of u,(bNFA ^omega):]
xi is Element of the carrier of u
xi is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
[xi,xi] is V26() Element of [: the carrier of u,(bNFA ^omega):]
(bNFA,(v2 ^ (Es ^ x)),x) is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
[((v . (v1 + 1)) `1),(bNFA,(v2 ^ (Es ^ x)),x)] is V26() set
v2 ^ Es is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(bNFA)
(v2 ^ Es) ^ x is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(bNFA)
(bNFA,((v2 ^ Es) ^ x),x) is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
[((v . (v1 + 1)) `1),(bNFA,((v2 ^ Es) ^ x),x)] is V26() set
[((v . (v1 + 1)) `1),(v2 ^ Es)] is V26() set
v2 ^ Es is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(bNFA)
(v2 ^ Es) ^ x is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(bNFA)
u1 ^ v2 is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(bNFA)
(u1 ^ v2) ^ (Es ^ x) is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(bNFA)
(u1 ^ v2) ^ Es is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(bNFA)
((u1 ^ v2) ^ Es) ^ x is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(bNFA)
u1 ^ (v2 ^ Es) is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(bNFA)
dim2 ((v . v1),bNFA) is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
xi is Element of the carrier of u
xc is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
[xi,xc] is V26() Element of [: the carrier of u,(bNFA ^omega):]
xi is Element of the carrier of u
xi is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
[xi,xi] is V26() Element of [: the carrier of u,(bNFA ^omega):]
(bNFA,(v2 ^ (Es ^ x)),x) is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
[((v . v1) `1),(bNFA,(v2 ^ (Es ^ x)),x)] is V26() set
(bNFA,((v2 ^ Es) ^ x),x) is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
[((v . v1) `1),(bNFA,((v2 ^ Es) ^ x),x)] is V26() set
[((v . v1) `1),(v2 ^ Es)] is V26() set
dim2 ((v . (len v)),bNFA) is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
(v . (len v)) `2 is set
v1 is non empty V15() V18( NAT ) Function-like finite FinSequence-like FinSubsequence-like RedSequence of ==>.-relation u
dom v1 is non empty V32() V33() V34() V35() V36() V37() finite Element of bool NAT
v1 . 1 is set
(v . 1) `1 is set
(bNFA,(dim2 ((v . 1),bNFA)),x) is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
[((v . 1) `1),(bNFA,(dim2 ((v . 1),bNFA)),x)] is V26() set
(bNFA,(c₄ ^ x),x) is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
[E,(bNFA,(c₄ ^ x),x)] is V26() set
len v1 is non empty V6() V10() V11() ext-real positive non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
v1 . (len v1) is set
(v . (len v)) `1 is set
(bNFA,(dim2 ((v . (len v)),bNFA)),x) is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
[((v . (len v)) `1),(bNFA,(dim2 ((v . (len v)),bNFA)),x)] is V26() set
(bNFA,(Es ^ x),x) is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
[FA,(bNFA,(Es ^ x),x)] is V26() set
E is set
FA is set
bNFA is non empty set
bNFA ^omega is non empty functional set
K232(bNFA) is non empty functional M11(bNFA)
Lex bNFA is non empty functional Element of bool K232(bNFA)
bool K232(bNFA) is non empty set
<%> bNFA is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(bNFA) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(bNFA)
{(<%> bNFA)} is non empty trivial functional V32() V33() V34() V35() V36() V37() finite V43() 1 -element Element of bool K232(bNFA)
(Lex bNFA) \/ {(<%> bNFA)} is non empty functional Element of bool K232(bNFA)
c₄ is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
[E,c₄] is V26() set
x is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
c₄ ^ x is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(bNFA)
[E,(c₄ ^ x)] is V26() set
Es is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
Es ^ x is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(bNFA)
[FA,(Es ^ x)] is V26() set
[FA,Es] is V26() set
u is non empty transition-system over (Lex bNFA) \/ {(<%> bNFA)}
==>.-relation u is V15() V18([: the carrier of u,(bNFA ^omega):]) V19([: the carrier of u,(bNFA ^omega):]) Element of bool [:[: the carrier of u,(bNFA ^omega):],[: the carrier of u,(bNFA ^omega):]:]
the carrier of u is non empty set
[: the carrier of u,(bNFA ^omega):] is non empty V15() set
[:[: the carrier of u,(bNFA ^omega):],[: the carrier of u,(bNFA ^omega):]:] is non empty V15() set
bool [:[: the carrier of u,(bNFA ^omega):],[: the carrier of u,(bNFA ^omega):]:] is non empty set
v is non empty V15() V18( NAT ) Function-like finite FinSequence-like FinSubsequence-like RedSequence of ==>.-relation u
v . 1 is set
len v is non empty V6() V10() V11() ext-real positive non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
v . (len v) is set
v is non empty V15() V18( NAT ) Function-like finite FinSequence-like FinSubsequence-like RedSequence of ==>.-relation u
v . 1 is set
len v is non empty V6() V10() V11() ext-real positive non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
v . (len v) is set
E is set
FA is set
bNFA is non empty set
bNFA ^omega is non empty functional set
K232(bNFA) is non empty functional M11(bNFA)
Lex bNFA is non empty functional Element of bool K232(bNFA)
bool K232(bNFA) is non empty set
<%> bNFA is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(bNFA) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(bNFA)
{(<%> bNFA)} is non empty trivial functional V32() V33() V34() V35() V36() V37() finite V43() 1 -element Element of bool K232(bNFA)
(Lex bNFA) \/ {(<%> bNFA)} is non empty functional Element of bool K232(bNFA)
c₄ is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
x is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
c₄ ^ x is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(bNFA)
Es is V8() V15() V18( NAT ) Function-like finite V67() Element of bNFA ^omega
Es ^ x is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(bNFA)
u is non empty transition-system over (Lex bNFA) \/ {(<%> bNFA)}
==>.-relation u is V15() V18([: the carrier of u,(bNFA ^omega):]) V19([: the carrier of u,(bNFA ^omega):]) Element of bool [:[: the carrier of u,(bNFA ^omega):],[: the carrier of u,(bNFA ^omega):]:]
the carrier of u is non empty set
[: the carrier of u,(bNFA ^omega):] is non empty V15() set
[:[: the carrier of u,(bNFA ^omega):],[: the carrier of u,(bNFA ^omega):]:] is non empty V15() set
bool [:[: the carrier of u,(bNFA ^omega):],[: the carrier of u,(bNFA ^omega):]:] is non empty set
[E,(c₄ ^ x)] is V26() set
[FA,(Es ^ x)] is V26() set
[E,c₄] is V26() set
[FA,Es] is V26() set
E is non empty set
E ^omega is non empty functional set
K232(E) is non empty functional M11(E)
Lex E is non empty functional Element of bool K232(E)
bool K232(E) is non empty set
<%> E is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(E) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(E)
{(<%> E)} is non empty trivial functional V32() V33() V34() V35() V36() V37() finite V43() 1 -element Element of bool K232(E)
(Lex E) \/ {(<%> E)} is non empty functional Element of bool K232(E)
FA is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
bNFA is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
FA ^ bNFA is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(E)
c₄ is non empty transition-system over (Lex E) \/ {(<%> E)}
the carrier of c₄ is non empty set
x is Element of the carrier of c₄
Es is Element of the carrier of c₄
==>.-relation c₄ is V15() V18([: the carrier of c₄,(E ^omega):]) V19([: the carrier of c₄,(E ^omega):]) Element of bool [:[: the carrier of c₄,(E ^omega):],[: the carrier of c₄,(E ^omega):]:]
[: the carrier of c₄,(E ^omega):] is non empty V15() set
[:[: the carrier of c₄,(E ^omega):],[: the carrier of c₄,(E ^omega):]:] is non empty V15() set
bool [:[: the carrier of c₄,(E ^omega):],[: the carrier of c₄,(E ^omega):]:] is non empty set
[x,(FA ^ bNFA)] is V26() Element of [: the carrier of c₄,K232(E):]
[: the carrier of c₄,K232(E):] is non empty V15() set
[Es,(<%> E)] is V26() Element of [: the carrier of c₄,K232(E):]
u is non empty V15() V18( NAT ) Function-like finite FinSequence-like FinSubsequence-like RedSequence of ==>.-relation c₄
u . 1 is set
len u is non empty V6() V10() V11() ext-real positive non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
u . (len u) is set
(u . (len u)) `2 is set
(u . 1) `2 is set
dom u is non empty V32() V33() V34() V35() V36() V37() finite Element of bool NAT
v is V6() V10() V11() ext-real non negative finite cardinal V69() set
u . v is set
(u . v) `2 is set
v + 1 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
(u . v) `1 is set
bTS is Element of the carrier of c₄
[bTS,bNFA] is V26() Element of [: the carrier of c₄,(E ^omega):]
v1 is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
u . v1 is set
0 ^ bNFA is V8() V15() V18( NAT ) Function-like finite V67() set
0 + 1 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
v + 1 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
FA ^ 0 is V8() V15() V18( NAT ) Function-like finite V67() set
v + 1 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
E is set
FA is non empty set
FA ^omega is non empty functional set
K232(FA) is non empty functional M11(FA)
Lex FA is non empty functional Element of bool K232(FA)
bool K232(FA) is non empty set
<%> FA is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(FA) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(FA)
{(<%> FA)} is non empty trivial functional V32() V33() V34() V35() V36() V37() finite V43() 1 -element Element of bool K232(FA)
(Lex FA) \/ {(<%> FA)} is non empty functional Element of bool K232(FA)
bNFA is V8() V15() V18( NAT ) Function-like finite V67() Element of FA ^omega
c₄ is V8() V15() V18( NAT ) Function-like finite V67() Element of FA ^omega
bNFA ^ c₄ is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(FA)
x is non empty transition-system over (Lex FA) \/ {(<%> FA)}
(bNFA ^ c₄) -succ_of (E,x) is Element of bool the carrier of x
the carrier of x is non empty set
bool the carrier of x is non empty set
bNFA -succ_of (E,x) is Element of bool the carrier of x
c₄ -succ_of ((bNFA -succ_of (E,x)),x) is Element of bool the carrier of x
Es is set
u is Element of the carrier of x
v is Element of the carrier of x
bTS is Element of the carrier of x
Es is set
u is Element of the carrier of x
v is Element of the carrier of x
bTS is Element of the carrier of x
E is non empty set
K232(E) is non empty functional M11(E)
Lex E is non empty functional Element of bool K232(E)
bool K232(E) is non empty set
<%> E is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(E) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(E)
{(<%> E)} is non empty trivial functional V32() V33() V34() V35() V36() V37() finite V43() 1 -element Element of bool K232(E)
(Lex E) \/ {(<%> E)} is non empty functional Element of bool K232(E)
FA is non empty transition-system over (Lex E) \/ {(<%> E)}
(E,((Lex E) \/ {(<%> E)}),FA) is non empty strict deterministic transition-system over Lex E
the carrier of (E,((Lex E) \/ {(<%> E)}),FA) is non empty set
[: the carrier of (E,((Lex E) \/ {(<%> E)}),FA),(Lex E):] is non empty V15() set
the Tran of (E,((Lex E) \/ {(<%> E)}),FA) is V15() V18([: the carrier of (E,((Lex E) \/ {(<%> E)}),FA),(Lex E):]) V19( the carrier of (E,((Lex E) \/ {(<%> E)}),FA)) Element of bool [:[: the carrier of (E,((Lex E) \/ {(<%> E)}),FA),(Lex E):], the carrier of (E,((Lex E) \/ {(<%> E)}),FA):]
[:[: the carrier of (E,((Lex E) \/ {(<%> E)}),FA),(Lex E):], the carrier of (E,((Lex E) \/ {(<%> E)}),FA):] is non empty V15() set
bool [:[: the carrier of (E,((Lex E) \/ {(<%> E)}),FA),(Lex E):], the carrier of (E,((Lex E) \/ {(<%> E)}),FA):] is non empty set
dom the Tran of (E,((Lex E) \/ {(<%> E)}),FA) is V15() V18( the carrier of (E,((Lex E) \/ {(<%> E)}),FA)) V19( Lex E) Element of bool [: the carrier of (E,((Lex E) \/ {(<%> E)}),FA),(Lex E):]
bool [: the carrier of (E,((Lex E) \/ {(<%> E)}),FA),(Lex E):] is non empty set
[: the carrier of (E,((Lex E) \/ {(<%> E)}),FA),((Lex E) \/ {(<%> E)}):] is non empty V15() set
E is set
FA is non empty set
FA ^omega is non empty functional set
K232(FA) is non empty functional M11(FA)
Lex FA is non empty functional Element of bool K232(FA)
bool K232(FA) is non empty set
<%> FA is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(FA) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(FA)
{(<%> FA)} is non empty trivial functional V32() V33() V34() V35() V36() V37() finite V43() 1 -element Element of bool K232(FA)
(Lex FA) \/ {(<%> FA)} is non empty functional Element of bool K232(FA)
bNFA is V8() V15() V18( NAT ) Function-like finite V67() Element of FA ^omega
c₄ is V8() V15() V18( NAT ) Function-like finite V67() Element of FA ^omega
c₄ ^ bNFA is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(FA)
x is non empty transition-system over (Lex FA) \/ {(<%> FA)}
(FA,((Lex FA) \/ {(<%> FA)}),x) is non empty strict deterministic transition-system over Lex FA
the carrier of x is non empty set
bool the carrier of x is non empty set
c₄ -succ_of (E,x) is Element of bool the carrier of x
{(c₄ -succ_of (E,x))} is non empty trivial finite 1 -element Element of bool (bool the carrier of x)
bool (bool the carrier of x) is non empty set
bNFA -succ_of ({(c₄ -succ_of (E,x))},(FA,((Lex FA) \/ {(<%> FA)}),x)) is Element of bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x)
the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x) is non empty set
bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x) is non empty set
(c₄ ^ bNFA) -succ_of (E,x) is Element of bool the carrier of x
{((c₄ ^ bNFA) -succ_of (E,x))} is non empty trivial finite 1 -element Element of bool (bool the carrier of x)
[: the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x),(Lex FA):] is non empty V15() set
the Tran of (FA,((Lex FA) \/ {(<%> FA)}),x) is V15() V18([: the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x),(Lex FA):]) V19( the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x)) Element of bool [:[: the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x),(Lex FA):], the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x):]
[:[: the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x),(Lex FA):], the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x):] is non empty V15() set
bool [:[: the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x),(Lex FA):], the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x):] is non empty set
dom the Tran of (FA,((Lex FA) \/ {(<%> FA)}),x) is V15() V18( the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x)) V19( Lex FA) Element of bool [: the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x),(Lex FA):]
bool [: the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x),(Lex FA):] is non empty set
rng (dom the Tran of (FA,((Lex FA) \/ {(<%> FA)}),x)) is functional Element of bool (Lex FA)
bool (Lex FA) is non empty set
Es is V8() V15() V18( NAT ) Function-like finite V67() Element of FA ^omega
len Es is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 Es is V6() V10() V11() ext-real non negative finite cardinal V69() set
u is V8() V15() V18( NAT ) Function-like finite V67() Element of FA ^omega
u -succ_of (E,x) is Element of bool the carrier of x
{(u -succ_of (E,x))} is non empty trivial finite 1 -element Element of bool (bool the carrier of x)
Es -succ_of ({(u -succ_of (E,x))},(FA,((Lex FA) \/ {(<%> FA)}),x)) is Element of bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x)
u ^ Es is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(FA)
(u ^ Es) -succ_of (E,x) is Element of bool the carrier of x
{((u ^ Es) -succ_of (E,x))} is non empty trivial finite 1 -element Element of bool (bool the carrier of x)
v is Element of bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x)
Es -succ_of (v,(FA,((Lex FA) \/ {(<%> FA)}),x)) is Element of bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x)
u ^ 0 is V8() V15() V18( NAT ) Function-like finite V67() set
(u ^ 0) -succ_of (E,x) is Element of bool the carrier of x
{((u ^ 0) -succ_of (E,x))} is non empty trivial finite 1 -element Element of bool (bool the carrier of x)
Es is V6() V10() V11() ext-real non negative finite cardinal V69() set
u is V8() V15() V18( NAT ) Function-like finite V67() Element of FA ^omega
len u is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 u is V6() V10() V11() ext-real non negative finite cardinal V69() set
Es + 1 is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set
v is V8() V15() V18( NAT ) Function-like finite V67() Element of FA ^omega
v -succ_of (E,x) is Element of bool the carrier of x
{(v -succ_of (E,x))} is non empty trivial finite 1 -element Element of bool (bool the carrier of x)
u -succ_of ({(v -succ_of (E,x))},(FA,((Lex FA) \/ {(<%> FA)}),x)) is Element of bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x)
v ^ u is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(FA)
(v ^ u) -succ_of (E,x) is Element of bool the carrier of x
{((v ^ u) -succ_of (E,x))} is non empty trivial finite 1 -element Element of bool (bool the carrier of x)
bTS is set
v is V8() V15() V18( NAT ) Function-like finite V67() Element of FA ^omega
v ^ u is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(FA)
(v ^ u) -succ_of (E,x) is Element of bool the carrier of x
{((v ^ u) -succ_of (E,x))} is non empty trivial finite 1 -element Element of bool (bool the carrier of x)
v -succ_of (E,x) is Element of bool the carrier of x
u -succ_of ((v -succ_of (E,x)),x) is Element of bool the carrier of x
{(v -succ_of (E,x))} is non empty trivial finite 1 -element Element of bool (bool the carrier of x)
v1 is Element of the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x)
u -succ_of ({(v -succ_of (E,x))},(FA,((Lex FA) \/ {(<%> FA)}),x)) is Element of bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x)
bTS is set
v1 is Element of the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x)
v2 is Element of the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x)
u -succ_of (v2,x) is Element of bool the carrier of x
v1 is V8() V15() V18( NAT ) Function-like finite V67() Element of FA ^omega
len v1 is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 v1 is V6() V10() V11() ext-real non negative finite cardinal V69() set
v2 is V8() V15() V18( NAT ) Function-like finite V67() Element of FA ^omega
len v2 is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 v2 is V6() V10() V11() ext-real non negative finite cardinal V69() set
v1 ^ v2 is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(FA)
v is V8() V15() V18( NAT ) Function-like finite V67() Element of FA ^omega
v -succ_of (E,x) is Element of bool the carrier of x
{(v -succ_of (E,x))} is non empty trivial finite 1 -element Element of bool (bool the carrier of x)
v1 -succ_of ({(v -succ_of (E,x))},(FA,((Lex FA) \/ {(<%> FA)}),x)) is Element of bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x)
v ^ v1 is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(FA)
(v ^ v1) -succ_of (E,x) is Element of bool the carrier of x
{((v ^ v1) -succ_of (E,x))} is non empty trivial finite 1 -element Element of bool (bool the carrier of x)
bTS is non empty transition-system over (Lex FA) \/ {(<%> FA)}
the Tran of bTS is V15() V18([: the carrier of bTS,((Lex FA) \/ {(<%> FA)}):]) V19( the carrier of bTS) Element of bool [:[: the carrier of bTS,((Lex FA) \/ {(<%> FA)}):], the carrier of bTS:]
the carrier of bTS is non empty set
[: the carrier of bTS,((Lex FA) \/ {(<%> FA)}):] is non empty V15() set
[:[: the carrier of bTS,((Lex FA) \/ {(<%> FA)}):], the carrier of bTS:] is non empty V15() set
bool [:[: the carrier of bTS,((Lex FA) \/ {(<%> FA)}):], the carrier of bTS:] is non empty set
(v1 ^ v2) -succ_of ({(v -succ_of (E,x))},(FA,((Lex FA) \/ {(<%> FA)}),x)) is Element of bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x)
(v1 ^ v2) -succ_of ({(v -succ_of (E,x))},bTS) is Element of bool the carrier of bTS
bool the carrier of bTS is non empty set
v1 -succ_of ({(v -succ_of (E,x))},bTS) is Element of bool the carrier of bTS
v2 -succ_of ((v1 -succ_of ({(v -succ_of (E,x))},bTS)),bTS) is Element of bool the carrier of bTS
v2 -succ_of ((v1 -succ_of ({(v -succ_of (E,x))},(FA,((Lex FA) \/ {(<%> FA)}),x))),bTS) is Element of bool the carrier of bTS
v2 -succ_of ((v1 -succ_of ({(v -succ_of (E,x))},(FA,((Lex FA) \/ {(<%> FA)}),x))),(FA,((Lex FA) \/ {(<%> FA)}),x)) is Element of bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x)
(v ^ v1) ^ v2 is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(FA)
((v ^ v1) ^ v2) -succ_of (E,x) is Element of bool the carrier of x
{(((v ^ v1) ^ v2) -succ_of (E,x))} is non empty trivial finite 1 -element Element of bool (bool the carrier of x)
v ^ (v1 ^ v2) is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(FA)
(v ^ (v1 ^ v2)) -succ_of (E,x) is Element of bool the carrier of x
{((v ^ (v1 ^ v2)) -succ_of (E,x))} is non empty trivial finite 1 -element Element of bool (bool the carrier of x)
u -succ_of ({(v -succ_of (E,x))},(FA,((Lex FA) \/ {(<%> FA)}),x)) is Element of bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x)
v ^ u is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(FA)
(v ^ u) -succ_of (E,x) is Element of bool the carrier of x
{((v ^ u) -succ_of (E,x))} is non empty trivial finite 1 -element Element of bool (bool the carrier of x)
u is V8() V15() V18( NAT ) Function-like finite V67() Element of FA ^omega
len u is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 u is V6() V10() V11() ext-real non negative finite cardinal V69() set
v is V8() V15() V18( NAT ) Function-like finite V67() Element of FA ^omega
v -succ_of (E,x) is Element of bool the carrier of x
{(v -succ_of (E,x))} is non empty trivial finite 1 -element Element of bool (bool the carrier of x)
u -succ_of ({(v -succ_of (E,x))},(FA,((Lex FA) \/ {(<%> FA)}),x)) is Element of bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),x)
v ^ u is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(FA)
(v ^ u) -succ_of (E,x) is Element of bool the carrier of x
{((v ^ u) -succ_of (E,x))} is non empty trivial finite 1 -element Element of bool (bool the carrier of x)
len bNFA is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 bNFA is V6() V10() V11() ext-real non negative finite cardinal V69() set
E is set
FA is non empty set
FA ^omega is non empty functional set
K232(FA) is non empty functional M11(FA)
Lex FA is non empty functional Element of bool K232(FA)
bool K232(FA) is non empty set
<%> FA is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(FA) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(FA)
{(<%> FA)} is non empty trivial functional V32() V33() V34() V35() V36() V37() finite V43() 1 -element Element of bool K232(FA)
(Lex FA) \/ {(<%> FA)} is non empty functional Element of bool K232(FA)
bNFA is V8() V15() V18( NAT ) Function-like finite V67() Element of FA ^omega
c₄ is non empty (FA,(Lex FA) \/ {(<%> FA)})
(FA,((Lex FA) \/ {(<%> FA)}),c₄) is non empty (FA, Lex FA) (FA, Lex FA) (FA, Lex FA)
the carrier of c₄ is non empty set
bool the carrier of c₄ is non empty set
(<%> FA) -succ_of (E,c₄) is Element of bool the carrier of c₄
{((<%> FA) -succ_of (E,c₄))} is non empty trivial finite 1 -element Element of bool (bool the carrier of c₄)
bool (bool the carrier of c₄) is non empty set
bNFA -succ_of ({((<%> FA) -succ_of (E,c₄))},(FA,((Lex FA) \/ {(<%> FA)}),c₄)) is Element of bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄)
the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄) is non empty set
bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄) is non empty set
bNFA -succ_of (E,c₄) is Element of bool the carrier of c₄
{(bNFA -succ_of (E,c₄))} is non empty trivial finite 1 -element Element of bool (bool the carrier of c₄)
the Tran of c₄ is V15() V18([: the carrier of c₄,((Lex FA) \/ {(<%> FA)}):]) V19( the carrier of c₄) Element of bool [:[: the carrier of c₄,((Lex FA) \/ {(<%> FA)}):], the carrier of c₄:]
[: the carrier of c₄,((Lex FA) \/ {(<%> FA)}):] is non empty V15() set
[:[: the carrier of c₄,((Lex FA) \/ {(<%> FA)}):], the carrier of c₄:] is non empty V15() set
bool [:[: the carrier of c₄,((Lex FA) \/ {(<%> FA)}):], the carrier of c₄:] is non empty set
transition-system(# the carrier of c₄, the Tran of c₄ #) is non empty strict transition-system over (Lex FA) \/ {(<%> FA)}
the Tran of (FA,((Lex FA) \/ {(<%> FA)}),c₄) is V15() V18([: the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄),(Lex FA):]) V19( the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄)) Element of bool [:[: the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄),(Lex FA):], the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄):]
[: the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄),(Lex FA):] is non empty V15() set
[:[: the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄),(Lex FA):], the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄):] is non empty V15() set
bool [:[: the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄),(Lex FA):], the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄):] is non empty set
transition-system(# the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄), the Tran of (FA,((Lex FA) \/ {(<%> FA)}),c₄) #) is non empty strict transition-system over Lex FA
(FA,((Lex FA) \/ {(<%> FA)}),transition-system(# the carrier of c₄, the Tran of c₄ #)) is non empty strict deterministic transition-system over Lex FA
bNFA -succ_of ({((<%> FA) -succ_of (E,c₄))},(FA,((Lex FA) \/ {(<%> FA)}),transition-system(# the carrier of c₄, the Tran of c₄ #))) is Element of bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),transition-system(# the carrier of c₄, the Tran of c₄ #))
the carrier of (FA,((Lex FA) \/ {(<%> FA)}),transition-system(# the carrier of c₄, the Tran of c₄ #)) is non empty set
bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),transition-system(# the carrier of c₄, the Tran of c₄ #)) is non empty set
the carrier of transition-system(# the carrier of c₄, the Tran of c₄ #) is non empty set
bool the carrier of transition-system(# the carrier of c₄, the Tran of c₄ #) is non empty set
(<%> FA) -succ_of (E,transition-system(# the carrier of c₄, the Tran of c₄ #)) is Element of bool the carrier of transition-system(# the carrier of c₄, the Tran of c₄ #)
{((<%> FA) -succ_of (E,transition-system(# the carrier of c₄, the Tran of c₄ #)))} is non empty trivial finite 1 -element Element of bool (bool the carrier of transition-system(# the carrier of c₄, the Tran of c₄ #))
bool (bool the carrier of transition-system(# the carrier of c₄, the Tran of c₄ #)) is non empty set
bNFA -succ_of ({((<%> FA) -succ_of (E,transition-system(# the carrier of c₄, the Tran of c₄ #)))},(FA,((Lex FA) \/ {(<%> FA)}),transition-system(# the carrier of c₄, the Tran of c₄ #))) is Element of bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),transition-system(# the carrier of c₄, the Tran of c₄ #))
0 ^ bNFA is V8() V15() V18( NAT ) Function-like finite V67() set
(0 ^ bNFA) -succ_of (E,transition-system(# the carrier of c₄, the Tran of c₄ #)) is Element of bool the carrier of transition-system(# the carrier of c₄, the Tran of c₄ #)
{((0 ^ bNFA) -succ_of (E,transition-system(# the carrier of c₄, the Tran of c₄ #)))} is non empty trivial finite 1 -element Element of bool (bool the carrier of transition-system(# the carrier of c₄, the Tran of c₄ #))
bNFA -succ_of (E,transition-system(# the carrier of c₄, the Tran of c₄ #)) is Element of bool the carrier of transition-system(# the carrier of c₄, the Tran of c₄ #)
{(bNFA -succ_of (E,transition-system(# the carrier of c₄, the Tran of c₄ #)))} is non empty trivial finite 1 -element Element of bool (bool the carrier of transition-system(# the carrier of c₄, the Tran of c₄ #))
E is set
FA is non empty set
K232(FA) is non empty functional M11(FA)
Lex FA is non empty functional Element of bool K232(FA)
bool K232(FA) is non empty set
<%> FA is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(FA) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(FA)
{(<%> FA)} is non empty trivial functional V32() V33() V34() V35() V36() V37() finite V43() 1 -element Element of bool K232(FA)
(Lex FA) \/ {(<%> FA)} is non empty functional Element of bool K232(FA)
bNFA is non empty (FA,(Lex FA) \/ {(<%> FA)})
the carrier of bNFA is non empty set
bool the carrier of bNFA is non empty set
the of bNFA is Element of bool the carrier of bNFA
(FA,((Lex FA) \/ {(<%> FA)}),bNFA) is non empty (FA, Lex FA) (FA, Lex FA) (FA, Lex FA)
the of (FA,((Lex FA) \/ {(<%> FA)}),bNFA) is Element of bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),bNFA)
the carrier of (FA,((Lex FA) \/ {(<%> FA)}),bNFA) is non empty set
bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),bNFA) is non empty set
c₄ is Element of bool the carrier of bNFA
{ b₁ where b₁ is Element of the carrier of (FA,((Lex FA) \/ {(<%> FA)}),bNFA) : not b₁ misses the of bNFA } is set
E is set
FA is non empty set
K232(FA) is non empty functional M11(FA)
Lex FA is non empty functional Element of bool K232(FA)
bool K232(FA) is non empty set
<%> FA is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(FA) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(FA)
{(<%> FA)} is non empty trivial functional V32() V33() V34() V35() V36() V37() finite V43() 1 -element Element of bool K232(FA)
(Lex FA) \/ {(<%> FA)} is non empty functional Element of bool K232(FA)
bNFA is non empty (FA,(Lex FA) \/ {(<%> FA)})
(FA,((Lex FA) \/ {(<%> FA)}),bNFA) is non empty (FA, Lex FA) (FA, Lex FA) (FA, Lex FA)
the of (FA,((Lex FA) \/ {(<%> FA)}),bNFA) is Element of bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),bNFA)
the carrier of (FA,((Lex FA) \/ {(<%> FA)}),bNFA) is non empty set
bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),bNFA) is non empty set
the of bNFA is Element of bool the carrier of bNFA
the carrier of bNFA is non empty set
bool the carrier of bNFA is non empty set
{ b₁ where b₁ is Element of the carrier of (FA,((Lex FA) \/ {(<%> FA)}),bNFA) : not b₁ misses the of bNFA } is set
c₄ is Element of the carrier of (FA,((Lex FA) \/ {(<%> FA)}),bNFA)
E is non empty set
K232(E) is non empty functional M11(E)
Lex E is non empty functional Element of bool K232(E)
bool K232(E) is non empty set
<%> E is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(E) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(E)
{(<%> E)} is non empty trivial functional V32() V33() V34() V35() V36() V37() finite V43() 1 -element Element of bool K232(E)
(Lex E) \/ {(<%> E)} is non empty functional Element of bool K232(E)
FA is non empty (E,(Lex E) \/ {(<%> E)})
(E,((Lex E) \/ {(<%> E)}),FA) is non empty (E, Lex E) (E, Lex E) (E, Lex E)
the of (E,((Lex E) \/ {(<%> E)}),FA) is Element of bool the carrier of (E,((Lex E) \/ {(<%> E)}),FA)
the carrier of (E,((Lex E) \/ {(<%> E)}),FA) is non empty set
bool the carrier of (E,((Lex E) \/ {(<%> E)}),FA) is non empty set
the carrier of FA is non empty set
bool the carrier of FA is non empty set
the of FA is Element of bool the carrier of FA
(<%> E) -succ_of ( the of FA,FA) is Element of bool the carrier of FA
{((<%> E) -succ_of ( the of FA,FA))} is non empty trivial finite 1 -element Element of bool (bool the carrier of FA)
bool (bool the carrier of FA) is non empty set
the Tran of (E,((Lex E) \/ {(<%> E)}),FA) is V15() V18([: the carrier of (E,((Lex E) \/ {(<%> E)}),FA),(Lex E):]) V19( the carrier of (E,((Lex E) \/ {(<%> E)}),FA)) Element of bool [:[: the carrier of (E,((Lex E) \/ {(<%> E)}),FA),(Lex E):], the carrier of (E,((Lex E) \/ {(<%> E)}),FA):]
[: the carrier of (E,((Lex E) \/ {(<%> E)}),FA),(Lex E):] is non empty V15() set
[:[: the carrier of (E,((Lex E) \/ {(<%> E)}),FA),(Lex E):], the carrier of (E,((Lex E) \/ {(<%> E)}),FA):] is non empty V15() set
bool [:[: the carrier of (E,((Lex E) \/ {(<%> E)}),FA),(Lex E):], the carrier of (E,((Lex E) \/ {(<%> E)}),FA):] is non empty set
(E,(Lex E), the carrier of (E,((Lex E) \/ {(<%> E)}),FA), the Tran of (E,((Lex E) \/ {(<%> E)}),FA), the of (E,((Lex E) \/ {(<%> E)}),FA)) is non empty (E, Lex E) (E, Lex E)
the of (E,(Lex E), the carrier of (E,((Lex E) \/ {(<%> E)}),FA), the Tran of (E,((Lex E) \/ {(<%> E)}),FA), the of (E,((Lex E) \/ {(<%> E)}),FA)) is Element of bool the carrier of (E,(Lex E), the carrier of (E,((Lex E) \/ {(<%> E)}),FA), the Tran of (E,((Lex E) \/ {(<%> E)}),FA), the of (E,((Lex E) \/ {(<%> E)}),FA))
the carrier of (E,(Lex E), the carrier of (E,((Lex E) \/ {(<%> E)}),FA), the Tran of (E,((Lex E) \/ {(<%> E)}),FA), the of (E,((Lex E) \/ {(<%> E)}),FA)) is non empty set
bool the carrier of (E,(Lex E), the carrier of (E,((Lex E) \/ {(<%> E)}),FA), the Tran of (E,((Lex E) \/ {(<%> E)}),FA), the of (E,((Lex E) \/ {(<%> E)}),FA)) is non empty set
the Tran of FA is V15() V18([: the carrier of FA,((Lex E) \/ {(<%> E)}):]) V19( the carrier of FA) Element of bool [:[: the carrier of FA,((Lex E) \/ {(<%> E)}):], the carrier of FA:]
[: the carrier of FA,((Lex E) \/ {(<%> E)}):] is non empty V15() set
[:[: the carrier of FA,((Lex E) \/ {(<%> E)}):], the carrier of FA:] is non empty V15() set
bool [:[: the carrier of FA,((Lex E) \/ {(<%> E)}):], the carrier of FA:] is non empty set
(E,((Lex E) \/ {(<%> E)}), the carrier of FA, the Tran of FA, the of FA) is non empty (E,(Lex E) \/ {(<%> E)}) (E,(Lex E) \/ {(<%> E)})
(E,((Lex E) \/ {(<%> E)}),(E,((Lex E) \/ {(<%> E)}), the carrier of FA, the Tran of FA, the of FA)) is non empty (E, Lex E) (E, Lex E) (E, Lex E)
the of (E,((Lex E) \/ {(<%> E)}),(E,((Lex E) \/ {(<%> E)}), the carrier of FA, the Tran of FA, the of FA)) is Element of bool the carrier of (E,((Lex E) \/ {(<%> E)}),(E,((Lex E) \/ {(<%> E)}), the carrier of FA, the Tran of FA, the of FA))
the carrier of (E,((Lex E) \/ {(<%> E)}),(E,((Lex E) \/ {(<%> E)}), the carrier of FA, the Tran of FA, the of FA)) is non empty set
bool the carrier of (E,((Lex E) \/ {(<%> E)}),(E,((Lex E) \/ {(<%> E)}), the carrier of FA, the Tran of FA, the of FA)) is non empty set
the carrier of (E,((Lex E) \/ {(<%> E)}), the carrier of FA, the Tran of FA, the of FA) is non empty set
bool the carrier of (E,((Lex E) \/ {(<%> E)}), the carrier of FA, the Tran of FA, the of FA) is non empty set
the of (E,((Lex E) \/ {(<%> E)}), the carrier of FA, the Tran of FA, the of FA) is Element of bool the carrier of (E,((Lex E) \/ {(<%> E)}), the carrier of FA, the Tran of FA, the of FA)
(<%> E) -succ_of ( the of (E,((Lex E) \/ {(<%> E)}), the carrier of FA, the Tran of FA, the of FA),(E,((Lex E) \/ {(<%> E)}), the carrier of FA, the Tran of FA, the of FA)) is Element of bool the carrier of (E,((Lex E) \/ {(<%> E)}), the carrier of FA, the Tran of FA, the of FA)
{((<%> E) -succ_of ( the of (E,((Lex E) \/ {(<%> E)}), the carrier of FA, the Tran of FA, the of FA),(E,((Lex E) \/ {(<%> E)}), the carrier of FA, the Tran of FA, the of FA)))} is non empty trivial finite 1 -element Element of bool (bool the carrier of (E,((Lex E) \/ {(<%> E)}), the carrier of FA, the Tran of FA, the of FA))
bool (bool the carrier of (E,((Lex E) \/ {(<%> E)}), the carrier of FA, the Tran of FA, the of FA)) is non empty set
E is set
FA is non empty set
FA ^omega is non empty functional set
K232(FA) is non empty functional M11(FA)
Lex FA is non empty functional Element of bool K232(FA)
bool K232(FA) is non empty set
<%> FA is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(FA) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(FA)
{(<%> FA)} is non empty trivial functional V32() V33() V34() V35() V36() V37() finite V43() 1 -element Element of bool K232(FA)
(Lex FA) \/ {(<%> FA)} is non empty functional Element of bool K232(FA)
bNFA is V8() V15() V18( NAT ) Function-like finite V67() Element of FA ^omega
c₄ is non empty (FA,(Lex FA) \/ {(<%> FA)})
(FA,((Lex FA) \/ {(<%> FA)}),c₄) is non empty (FA, Lex FA) (FA, Lex FA) (FA, Lex FA)
the carrier of c₄ is non empty set
bool the carrier of c₄ is non empty set
(<%> FA) -succ_of (E,c₄) is Element of bool the carrier of c₄
{((<%> FA) -succ_of (E,c₄))} is non empty trivial finite 1 -element Element of bool (bool the carrier of c₄)
bool (bool the carrier of c₄) is non empty set
bNFA -succ_of ({((<%> FA) -succ_of (E,c₄))},(FA,((Lex FA) \/ {(<%> FA)}),c₄)) is Element of bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄)
the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄) is non empty set
bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄) is non empty set
bNFA -succ_of (E,c₄) is Element of bool the carrier of c₄
{(bNFA -succ_of (E,c₄))} is non empty trivial finite 1 -element Element of bool (bool the carrier of c₄)
the Tran of c₄ is V15() V18([: the carrier of c₄,((Lex FA) \/ {(<%> FA)}):]) V19( the carrier of c₄) Element of bool [:[: the carrier of c₄,((Lex FA) \/ {(<%> FA)}):], the carrier of c₄:]
[: the carrier of c₄,((Lex FA) \/ {(<%> FA)}):] is non empty V15() set
[:[: the carrier of c₄,((Lex FA) \/ {(<%> FA)}):], the carrier of c₄:] is non empty V15() set
bool [:[: the carrier of c₄,((Lex FA) \/ {(<%> FA)}):], the carrier of c₄:] is non empty set
the of c₄ is Element of bool the carrier of c₄
(FA,((Lex FA) \/ {(<%> FA)}), the carrier of c₄, the Tran of c₄, the of c₄) is non empty (FA,(Lex FA) \/ {(<%> FA)}) (FA,(Lex FA) \/ {(<%> FA)})
the Tran of (FA,((Lex FA) \/ {(<%> FA)}),c₄) is V15() V18([: the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄),(Lex FA):]) V19( the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄)) Element of bool [:[: the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄),(Lex FA):], the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄):]
[: the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄),(Lex FA):] is non empty V15() set
[:[: the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄),(Lex FA):], the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄):] is non empty V15() set
bool [:[: the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄),(Lex FA):], the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄):] is non empty set
the of (FA,((Lex FA) \/ {(<%> FA)}),c₄) is Element of bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄)
(FA,(Lex FA), the carrier of (FA,((Lex FA) \/ {(<%> FA)}),c₄), the Tran of (FA,((Lex FA) \/ {(<%> FA)}),c₄), the of (FA,((Lex FA) \/ {(<%> FA)}),c₄)) is non empty (FA, Lex FA) (FA, Lex FA)
(FA,((Lex FA) \/ {(<%> FA)}),(FA,((Lex FA) \/ {(<%> FA)}), the carrier of c₄, the Tran of c₄, the of c₄)) is non empty (FA, Lex FA) (FA, Lex FA) (FA, Lex FA)
bNFA -succ_of ({((<%> FA) -succ_of (E,c₄))},(FA,((Lex FA) \/ {(<%> FA)}),(FA,((Lex FA) \/ {(<%> FA)}), the carrier of c₄, the Tran of c₄, the of c₄))) is Element of bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),(FA,((Lex FA) \/ {(<%> FA)}), the carrier of c₄, the Tran of c₄, the of c₄))
the carrier of (FA,((Lex FA) \/ {(<%> FA)}),(FA,((Lex FA) \/ {(<%> FA)}), the carrier of c₄, the Tran of c₄, the of c₄)) is non empty set
bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),(FA,((Lex FA) \/ {(<%> FA)}), the carrier of c₄, the Tran of c₄, the of c₄)) is non empty set
the carrier of (FA,((Lex FA) \/ {(<%> FA)}), the carrier of c₄, the Tran of c₄, the of c₄) is non empty set
bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}), the carrier of c₄, the Tran of c₄, the of c₄) is non empty set
(<%> FA) -succ_of (E,(FA,((Lex FA) \/ {(<%> FA)}), the carrier of c₄, the Tran of c₄, the of c₄)) is Element of bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}), the carrier of c₄, the Tran of c₄, the of c₄)
{((<%> FA) -succ_of (E,(FA,((Lex FA) \/ {(<%> FA)}), the carrier of c₄, the Tran of c₄, the of c₄)))} is non empty trivial finite 1 -element Element of bool (bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}), the carrier of c₄, the Tran of c₄, the of c₄))
bool (bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}), the carrier of c₄, the Tran of c₄, the of c₄)) is non empty set
bNFA -succ_of ({((<%> FA) -succ_of (E,(FA,((Lex FA) \/ {(<%> FA)}), the carrier of c₄, the Tran of c₄, the of c₄)))},(FA,((Lex FA) \/ {(<%> FA)}),(FA,((Lex FA) \/ {(<%> FA)}), the carrier of c₄, the Tran of c₄, the of c₄))) is Element of bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}),(FA,((Lex FA) \/ {(<%> FA)}), the carrier of c₄, the Tran of c₄, the of c₄))
bNFA -succ_of (E,(FA,((Lex FA) \/ {(<%> FA)}), the carrier of c₄, the Tran of c₄, the of c₄)) is Element of bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}), the carrier of c₄, the Tran of c₄, the of c₄)
{(bNFA -succ_of (E,(FA,((Lex FA) \/ {(<%> FA)}), the carrier of c₄, the Tran of c₄, the of c₄)))} is non empty trivial finite 1 -element Element of bool (bool the carrier of (FA,((Lex FA) \/ {(<%> FA)}), the carrier of c₄, the Tran of c₄, the of c₄))
E is non empty set
E ^omega is non empty functional set
K232(E) is non empty functional M11(E)
Lex E is non empty functional Element of bool K232(E)
bool K232(E) is non empty set
<%> E is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(E) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(E)
{(<%> E)} is non empty trivial functional V32() V33() V34() V35() V36() V37() finite V43() 1 -element Element of bool K232(E)
(Lex E) \/ {(<%> E)} is non empty functional Element of bool K232(E)
FA is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
bNFA is non empty (E,(Lex E) \/ {(<%> E)})
(E,((Lex E) \/ {(<%> E)}),bNFA) is non empty (E, Lex E) (E, Lex E) (E, Lex E)
the of (E,((Lex E) \/ {(<%> E)}),bNFA) is Element of bool the carrier of (E,((Lex E) \/ {(<%> E)}),bNFA)
the carrier of (E,((Lex E) \/ {(<%> E)}),bNFA) is non empty set
bool the carrier of (E,((Lex E) \/ {(<%> E)}),bNFA) is non empty set
FA -succ_of ( the of (E,((Lex E) \/ {(<%> E)}),bNFA),(E,((Lex E) \/ {(<%> E)}),bNFA)) is Element of bool the carrier of (E,((Lex E) \/ {(<%> E)}),bNFA)
the carrier of bNFA is non empty set
bool the carrier of bNFA is non empty set
the of bNFA is Element of bool the carrier of bNFA
FA -succ_of ( the of bNFA,bNFA) is Element of bool the carrier of bNFA
{(FA -succ_of ( the of bNFA,bNFA))} is non empty trivial finite 1 -element Element of bool (bool the carrier of bNFA)
bool (bool the carrier of bNFA) is non empty set
(<%> E) -succ_of ( the of bNFA,bNFA) is Element of bool the carrier of bNFA
{((<%> E) -succ_of ( the of bNFA,bNFA))} is non empty trivial finite 1 -element Element of bool (bool the carrier of bNFA)
E is non empty set
K232(E) is non empty functional M11(E)
Lex E is non empty functional Element of bool K232(E)
bool K232(E) is non empty set
<%> E is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(E) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(E)
{(<%> E)} is non empty trivial functional V32() V33() V34() V35() V36() V37() finite V43() 1 -element Element of bool K232(E)
(Lex E) \/ {(<%> E)} is non empty functional Element of bool K232(E)
FA is non empty (E,(Lex E) \/ {(<%> E)})
(E,((Lex E) \/ {(<%> E)}),FA) is functional Element of bool (E ^omega)
E ^omega is non empty functional set
bool (E ^omega) is non empty set
the carrier of FA is non empty set
the of FA is Element of bool the carrier of FA
bool the carrier of FA is non empty set
the of FA is Element of bool the carrier of FA
{ b₁ where b₁ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : ex b₂, b₃ being Element of the carrier of FA st
( b₂ in the of FA & b₃ in the of FA & b₂,b₁ ==>* b₃,FA ) } is set
(E,((Lex E) \/ {(<%> E)}),FA) is non empty (E, Lex E) (E, Lex E) (E, Lex E)
(E,(Lex E),(E,((Lex E) \/ {(<%> E)}),FA)) is functional Element of bool (E ^omega)
the carrier of (E,((Lex E) \/ {(<%> E)}),FA) is non empty set
the of (E,((Lex E) \/ {(<%> E)}),FA) is Element of bool the carrier of (E,((Lex E) \/ {(<%> E)}),FA)
bool the carrier of (E,((Lex E) \/ {(<%> E)}),FA) is non empty set
the of (E,((Lex E) \/ {(<%> E)}),FA) is Element of bool the carrier of (E,((Lex E) \/ {(<%> E)}),FA)
{ b₁ where b₁ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : ex b₂, b₃ being Element of the carrier of (E,((Lex E) \/ {(<%> E)}),FA) st
( b₂ in the of (E,((Lex E) \/ {(<%> E)}),FA) & b₃ in the of (E,((Lex E) \/ {(<%> E)}),FA) & b₂,b₁ ==>* b₃,(E,((Lex E) \/ {(<%> E)}),FA) ) } is set
c₄ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
c₄ -succ_of ( the of FA,FA) is Element of bool the carrier of FA
x is set
c₄ -succ_of ( the of (E,((Lex E) \/ {(<%> E)}),FA),(E,((Lex E) \/ {(<%> E)}),FA)) is Element of bool the carrier of (E,((Lex E) \/ {(<%> E)}),FA)
{(c₄ -succ_of ( the of FA,FA))} is non empty trivial finite 1 -element Element of bool (bool the carrier of FA)
bool (bool the carrier of FA) is non empty set
c₄ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
c₄ -succ_of ( the of (E,((Lex E) \/ {(<%> E)}),FA),(E,((Lex E) \/ {(<%> E)}),FA)) is Element of bool the carrier of (E,((Lex E) \/ {(<%> E)}),FA)
x is set
c₄ -succ_of ( the of FA,FA) is Element of bool the carrier of FA
{(c₄ -succ_of ( the of FA,FA))} is non empty trivial finite 1 -element Element of bool (bool the carrier of FA)
bool (bool the carrier of FA) is non empty set
E is non empty set
K232(E) is non empty functional M11(E)
Lex E is non empty functional Element of bool K232(E)
bool K232(E) is non empty set
<%> E is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(E) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(E)
{(<%> E)} is non empty trivial functional V32() V33() V34() V35() V36() V37() finite V43() 1 -element Element of bool K232(E)
(Lex E) \/ {(<%> E)} is non empty functional Element of bool K232(E)
FA is non empty (E,(Lex E) \/ {(<%> E)})
(E,((Lex E) \/ {(<%> E)}),FA) is functional Element of bool (E ^omega)
E ^omega is non empty functional set
bool (E ^omega) is non empty set
the carrier of FA is non empty set
the of FA is Element of bool the carrier of FA
bool the carrier of FA is non empty set
the of FA is Element of bool the carrier of FA
{ b₁ where b₁ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : ex b₂, b₃ being Element of the carrier of FA st
( b₂ in the of FA & b₃ in the of FA & b₂,b₁ ==>* b₃,FA ) } is set
(E,((Lex E) \/ {(<%> E)}),FA) is non empty (E, Lex E) (E, Lex E) (E, Lex E)
(E,(Lex E),(E,((Lex E) \/ {(<%> E)}),FA)) is functional Element of bool (E ^omega)
the carrier of (E,((Lex E) \/ {(<%> E)}),FA) is non empty set
the of (E,((Lex E) \/ {(<%> E)}),FA) is Element of bool the carrier of (E,((Lex E) \/ {(<%> E)}),FA)
bool the carrier of (E,((Lex E) \/ {(<%> E)}),FA) is non empty set
the of (E,((Lex E) \/ {(<%> E)}),FA) is Element of bool the carrier of (E,((Lex E) \/ {(<%> E)}),FA)
{ b₁ where b₁ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : ex b₂, b₃ being Element of the carrier of (E,((Lex E) \/ {(<%> E)}),FA) st
( b₂ in the of (E,((Lex E) \/ {(<%> E)}),FA) & b₃ in the of (E,((Lex E) \/ {(<%> E)}),FA) & b₂,b₁ ==>* b₃,(E,((Lex E) \/ {(<%> E)}),FA) ) } is set
E is non empty set
K232(E) is non empty functional M11(E)
Lex E is non empty functional Element of bool K232(E)
bool K232(E) is non empty set
<%> E is empty V6() V8() V10() V11() ext-real non positive non negative V15() non-empty empty-yielding V18( NAT ) V19(E) Function-like one-to-one constant functional V32() V33() V34() V35() V36() V37() V38() finite finite-yielding V43() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V67() V69() Element of K232(E)
{(<%> E)} is non empty trivial functional V32() V33() V34() V35() V36() V37() finite V43() 1 -element Element of bool K232(E)
(Lex E) \/ {(<%> E)} is non empty functional Element of bool K232(E)
FA is non empty finite (E,(Lex E) \/ {(<%> E)})
(E,((Lex E) \/ {(<%> E)}),FA) is functional Element of bool (E ^omega)
E ^omega is non empty functional set
bool (E ^omega) is non empty set
the carrier of FA is non empty finite set
the of FA is finite Element of bool the carrier of FA
bool the carrier of FA is non empty finite V43() set
the of FA is finite Element of bool the carrier of FA
{ b₁ where b₁ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : ex b₂, b₃ being Element of the carrier of FA st
( b₂ in the of FA & b₃ in the of FA & b₂,b₁ ==>* b₃,FA ) } is set
(E,((Lex E) \/ {(<%> E)}),FA) is non empty finite (E, Lex E) (E, Lex E) (E, Lex E)
(E,(Lex E),(E,((Lex E) \/ {(<%> E)}),FA)) is functional Element of bool (E ^omega)
the carrier of (E,((Lex E) \/ {(<%> E)}),FA) is non empty finite set
the of (E,((Lex E) \/ {(<%> E)}),FA) is finite Element of bool the carrier of (E,((Lex E) \/ {(<%> E)}),FA)
bool the carrier of (E,((Lex E) \/ {(<%> E)}),FA) is non empty finite V43() set
the of (E,((Lex E) \/ {(<%> E)}),FA) is finite Element of bool the carrier of (E,((Lex E) \/ {(<%> E)}),FA)
{ b₁ where b₁ is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : ex b₂, b₃ being Element of the carrier of (E,((Lex E) \/ {(<%> E)}),FA) st
( b₂ in the of (E,((Lex E) \/ {(<%> E)}),FA) & b₃ in the of (E,((Lex E) \/ {(<%> E)}),FA) & b₂,b₁ ==>* b₃,(E,((Lex E) \/ {(<%> E)}),FA) ) } is set