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

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 () is non empty set
is V15() set
bool 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

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

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

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

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
c4 is Element of E
<%c4%> 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 ^ <%c4%> is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(E)

0 ^ <%c4%> 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
c4 is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
len c4 is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 c4 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)
c4 ^ <%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
c4 ^ 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

K232(E) is non empty functional M11(E)
c4 is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
len c4 is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 c4 is V6() V10() V11() ext-real non negative finite cardinal V69() set
FA ^ c4 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
c4 is V8() V15() V18( NAT ) Function-like finite V67() set
<%FA%> ^ c4 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
c4 is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
len c4 is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 c4 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%> ^ c4 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

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
c4 is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
FA ^ c4 is V8() V15() V18( NAT ) Function-like finite V67() Element of K232(E)
c4 ^ 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 ^ c4) is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 (FA ^ c4) is V6() V10() V11() ext-real non negative finite cardinal V69() set
len c4 is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 c4 is V6() V10() V11() ext-real non negative finite cardinal V69() set
1 + (len c4) is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set

len (c4 ^ FA) is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 (c4 ^ FA) is V6() V10() V11() ext-real non negative finite cardinal V69() set
len c4 is V6() V10() V11() ext-real non negative V32() V33() V34() V35() V36() V37() finite cardinal V69() Element of NAT
proj1 c4 is V6() V10() V11() ext-real non negative finite cardinal V69() set
1 + (len c4) is non empty V6() V10() V11() ext-real positive non negative finite cardinal V69() set

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
c4 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,c4] 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
c4 ^ 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)

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 () is non empty set
FA is functional Element of bool ()
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),():] 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),():]
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),():],(bool the carrier of bNFA):]
[:[:(bool the carrier of bNFA),():],(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),():]
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 () is non empty set
FA is functional Element of bool ()
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 () is non empty set
FA is functional Element of bool ()
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

c4 is Element of bNFA
<%c4%> 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
c4 is functional Element of bool (FA ^omega)
x is non empty transition-system over c4
the carrier of x is non empty set
bool the carrier of x is non empty set
(FA,c4,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,c4,x) is V15() V18([: the carrier of (FA,c4,x),(Lex FA):]) V19( the carrier of (FA,c4,x)) Element of bool [:[: the carrier of (FA,c4,x),(Lex FA):], the carrier of (FA,c4,x):]
the carrier of (FA,c4,x) is non empty set
[: the carrier of (FA,c4,x),(Lex FA):] is non empty V15() set
[:[: the carrier of (FA,c4,x),(Lex FA):], the carrier of (FA,c4,x):] is non empty V15() set
bool [:[: the carrier of (FA,c4,x),(Lex FA):], the carrier of (FA,c4,x):] is non empty set

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,c4,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,c4,x) is V15() V18([: the carrier of (FA,c4,x),(Lex FA):]) V19( the carrier of (FA,c4,x)) Element of bool [:[: the carrier of (FA,c4,x),(Lex FA):], the carrier of (FA,c4,x):]
[: the carrier of (FA,c4,x),(Lex FA):] is non empty V15() set
[:[: the carrier of (FA,c4,x),(Lex FA):], the carrier of (FA,c4,x):] is non empty V15() set
bool [:[: the carrier of (FA,c4,x),(Lex FA):], the carrier of (FA,c4,x):] is non empty set
E is non empty set
E ^omega is non empty functional set
bool () is non empty set
E is non empty set
E ^omega is non empty functional set
bool () is non empty set
FA is functional Element of bool ()
E is non empty set
E ^omega is non empty functional set
bool () is non empty set
FA is functional Element of bool ()
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
c4 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 ,c4,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 () is non empty set
FA is functional Element of bool ()
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 () is non empty set
FA is functional Element of bool ()
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

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
c4 is non empty transition-system over FA
(E,FA,c4) is non empty strict deterministic transition-system over Lex E
the carrier of (E,FA,c4) is non empty set
bool the carrier of (E,FA,c4) is non empty set
[: the carrier of (E,FA,c4),(Lex E):] is non empty V15() set
[:[: the carrier of (E,FA,c4),(Lex E):], the carrier of (E,FA,c4):] is non empty V15() set
bool [:[: the carrier of (E,FA,c4),(Lex E):], the carrier of (E,FA,c4):] is non empty set
the Tran of (E,FA,c4) is V15() V18([: the carrier of (E,FA,c4),(Lex E):]) V19( the carrier of (E,FA,c4)) Element of bool [:[: the carrier of (E,FA,c4),(Lex E):], the carrier of (E,FA,c4):]
u is V15() V18([: the carrier of (E,FA,c4),(Lex E):]) V19( the carrier of (E,FA,c4)) Element of bool [:[: the carrier of (E,FA,c4),(Lex E):], the carrier of (E,FA,c4):]
Es is Element of bool the carrier of (E,FA,c4)
(E,(Lex E), the carrier of (E,FA,c4),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
c4 is (E, Lex E) (E, Lex E)
the carrier of c4 is set
the Tran of c4 is V15() V18([: the carrier of c4,(Lex E):]) V19( the carrier of c4) Element of bool [:[: the carrier of c4,(Lex E):], the carrier of c4:]
[: the carrier of c4,(Lex E):] is V15() set
[:[: the carrier of c4,(Lex E):], the carrier of c4:] is V15() set
bool [:[: the carrier of c4,(Lex E):], the carrier of c4:] is non empty set
transition-system(# the carrier of c4, the Tran of c4 #) is strict transition-system over Lex E
the of c4 is Element of bool the carrier of c4
bool the carrier of c4 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 () is non empty set
FA is functional Element of bool ()
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

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 () is non empty set
FA is functional Element of bool ()
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 () is non empty set
FA is functional Element of bool ()
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 () is non empty set
FA is functional Element of bool ()
bNFA is non empty (E,FA)
the carrier of bNFA is non empty set
bool the carrier of bNFA is non empty set
c4 is Element of bool the carrier of bNFA
the of bNFA is Element of bool the carrier of bNFA
{ b1 where b1 is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : not c4 misses b1 -succ_of ( the of bNFA,bNFA) } is set
{ b1 where b1 is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : S1[b1] } is set
E is non empty set
E ^omega is non empty functional set
bool () is non empty set
FA is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
bNFA is functional Element of bool ()
c4 is non empty (E,bNFA)
the carrier of c4 is non empty set
bool the carrier of c4 is non empty set
the of c4 is Element of bool the carrier of c4
FA -succ_of ( the of c4,c4) is Element of bool the carrier of c4
x is Element of bool the carrier of c4
(E,bNFA,c4,x) is functional Element of bool ()
{ b1 where b1 is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : not x misses b1 -succ_of ( the of c4,c4) } is set
Es is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
Es -succ_of ( the of c4,c4) is Element of bool the carrier of c4
E is non empty set
E ^omega is non empty functional set
bool () is non empty set
E is non empty set
E ^omega is non empty functional set
bool () is non empty set
FA is functional Element of bool ()
E is non empty set
E ^omega is non empty functional set
bool () is non empty set
FA is functional Element of bool ()
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
c4 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 ,c4,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 () is non empty set
FA is functional Element of bool ()
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 () is non empty set
FA is functional Element of bool ()
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
c4 is non empty (E,FA)
(E,FA,c4) is non empty (E, Lex E) (E, Lex E) (E, Lex E)
the carrier of (E,FA,c4) is non empty set
[: the carrier of (E,FA,c4),(Lex E):] is non empty V15() set
[:[: the carrier of (E,FA,c4),(Lex E):], the carrier of (E,FA,c4):] is non empty V15() set
bool [:[: the carrier of (E,FA,c4),(Lex E):], the carrier of (E,FA,c4):] is non empty set
the Tran of (E,FA,c4) is V15() V18([: the carrier of (E,FA,c4),(Lex E):]) V19( the carrier of (E,FA,c4)) Element of bool [:[: the carrier of (E,FA,c4),(Lex E):], the carrier of (E,FA,c4):]
the of (E,FA,c4) is Element of bool the carrier of (E,FA,c4)
bool the carrier of (E,FA,c4) is non empty set
{ b1 where b1 is Element of the carrier of (E,FA,c4) : not b1 misses the of bNFA } is set
{ b1 where b1 is Element of the carrier of (E,FA,c4) : S1[b1] } is set
Es is V15() V18([: the carrier of (E,FA,c4),(Lex E):]) V19( the carrier of (E,FA,c4)) Element of bool [:[: the carrier of (E,FA,c4),(Lex E):], the carrier of (E,FA,c4):]
v is Element of bool the carrier of (E,FA,c4)
(E,(Lex E), the carrier of (E,FA,c4),Es, the of (E,FA,c4),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
{ b1 where b1 is Element of the carrier of v1 : not b1 misses the of bNFA } is set
c4 is (E, Lex E) (E, Lex E)
the carrier of c4 is set
the Tran of c4 is V15() V18([: the carrier of c4,(Lex E):]) V19( the carrier of c4) Element of bool [:[: the carrier of c4,(Lex E):], the carrier of c4:]
[: the carrier of c4,(Lex E):] is V15() set
[:[: the carrier of c4,(Lex E):], the carrier of c4:] is V15() set
bool [:[: the carrier of c4,(Lex E):], the carrier of c4:] is non empty set
the of c4 is Element of bool the carrier of c4
bool the carrier of c4 is non empty set
(E,(Lex E), the carrier of c4, the Tran of c4, the of c4) is (E, Lex E) (E, Lex E)
the of c4 is Element of bool the carrier of c4
{ b1 where b1 is Element of the carrier of c4 : not b1 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
{ b1 where b1 is Element of the carrier of x : not b1 misses the of bNFA } is set
E is non empty set
E ^omega is non empty functional set
bool () is non empty set
FA is functional Element of bool ()
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 () is non empty set
FA is functional Element of bool ()
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 () is non empty set
FA is functional Element of bool ()
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 () is non empty set
FA is functional Element of bool ()
bNFA is non empty (E,FA)
the carrier of bNFA is non empty set
bool the carrier of bNFA is non empty set
c4 is Element of bool the carrier of bNFA
the of bNFA is Element of bool the carrier of bNFA
{ b1 where b1 is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : not b1 -succ_of (c4,bNFA) misses the of bNFA } is set
{ b1 where b1 is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : S1[b1] } is set
E is non empty set
E ^omega is non empty functional set
bool () is non empty set
FA is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
bNFA is functional Element of bool ()
c4 is non empty (E,bNFA)
the carrier of c4 is non empty set
bool the carrier of c4 is non empty set
the of c4 is Element of bool the carrier of c4
x is Element of bool the carrier of c4
(E,bNFA,c4,x) is functional Element of bool ()
{ b1 where b1 is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : not b1 -succ_of (x,c4) misses the of c4 } is set
FA -succ_of (x,c4) is Element of bool the carrier of c4
Es is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
Es -succ_of (x,c4) is Element of bool the carrier of c4
E is non empty set
E ^omega is non empty functional set
bool () is non empty set
FA is functional Element of bool ()
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
{ b1 where b1 is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : ex b2, b3 being Element of the carrier of bNFA st
( b2 in the of bNFA & b3 in the of bNFA & b2,b1 ==>* b3,bNFA )
}
is set

{ b1 where b1 is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : S1[b1] } is set
E is non empty set
E ^omega is non empty functional set
bool () is non empty set
FA is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
bNFA is functional Element of bool ()
c4 is non empty (E,bNFA)
(E,bNFA,c4) is functional Element of bool ()
the carrier of c4 is non empty set
the of c4 is Element of bool the carrier of c4
bool the carrier of c4 is non empty set
the of c4 is Element of bool the carrier of c4
{ b1 where b1 is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : ex b2, b3 being Element of the carrier of c4 st
( b2 in the of c4 & b3 in the of c4 & b2,b1 ==>* b3,c4 )
}
is set

x is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
Es is Element of the carrier of c4
u is Element of the carrier of c4
x is Element of the carrier of c4
Es is Element of the carrier of c4
E is non empty set
E ^omega is non empty functional set
bool () is non empty set
FA is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
bNFA is functional Element of bool ()
c4 is non empty (E,bNFA)
(E,bNFA,c4) is functional Element of bool ()
the carrier of c4 is non empty set
the of c4 is Element of bool the carrier of c4
bool the carrier of c4 is non empty set
the of c4 is Element of bool the carrier of c4
{ b1 where b1 is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : ex b2, b3 being Element of the carrier of c4 st
( b2 in the of c4 & b3 in the of c4 & b2,b1 ==>* b3,c4 )
}
is set

FA -succ_of ( the of c4,c4) is Element of bool the carrier of c4
x is Element of the carrier of c4
Es is Element of the carrier of c4
x is set
Es is Element of the carrier of c4
u is Element of the carrier of c4
E is non empty set
E ^omega is non empty functional set
bool () is non empty set
FA is functional Element of bool ()
bNFA is non empty (E,FA)
(E,FA,bNFA) is functional Element of bool ()
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
{ b1 where b1 is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : ex b2, b3 being Element of the carrier of bNFA st
( b2 in the of bNFA & b3 in the of bNFA & b2,b1 ==>* b3,bNFA )
}
is set

(E,FA,bNFA, the of bNFA) is functional Element of bool ()
{ b1 where b1 is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : not the of bNFA misses b1 -succ_of ( the of bNFA,bNFA) } is set
c4 is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
c4 -succ_of ( the of bNFA,bNFA) is Element of bool the carrier of bNFA
c4 is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
c4 -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 () is non empty set
FA is functional Element of bool ()
bNFA is non empty (E,FA)
(E,FA,bNFA) is functional Element of bool ()
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
{ b1 where b1 is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : ex b2, b3 being Element of the carrier of bNFA st
( b2 in the of bNFA & b3 in the of bNFA & b2,b1 ==>* b3,bNFA )
}
is set

(E,FA,bNFA, the of bNFA) is functional Element of bool ()
{ b1 where b1 is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega : not b1 -succ_of ( the of bNFA,bNFA) misses the of bNFA } is set
c4 is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
c4 -succ_of ( the of bNFA,bNFA) is Element of bool the carrier of bNFA
c4 is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
c4 -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 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)
c4 is non empty transition-system over (Lex E) \/ {(<%> E)}
==>.-relation c4 is V15() V18([: the carrier of c4,():]) V19([: the carrier of c4,():]) Element of bool [:[: the carrier of c4,():],[: the carrier of c4,():]:]
the carrier of c4 is non empty set
[: the carrier of c4,():] is non empty V15() set
[:[: the carrier of c4,():],[: the carrier of c4,():]:] is non empty V15() set
bool [:[: the carrier of c4,():],[: the carrier of c4,():]:] is non empty set

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 c4
u is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
[Es,u] is V26() Element of [: the carrier of c4,():]
v is Element of the carrier of c4
bTS is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega
[v,bTS] is V26() Element of [: the carrier of c4,():]
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 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,():]) V19([: the carrier of bNFA,():]) Element of bool [:[: the carrier of bNFA,():],[: the carrier of bNFA,():]:]
the carrier of bNFA is non empty set
[: the carrier of bNFA,():] is non empty V15() set
[:[: the carrier of bNFA,():],[: the carrier of bNFA,():]:] is non empty V15() set
bool [:[: the carrier of bNFA,():],[: the carrier of bNFA,():]:] is non empty set
c4 is V6() V10() V11() ext-real non negative finite cardinal V69() 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
c4 + 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)

bTS is non empty V15() V18( NAT ) Function-like finite FinSequence-like