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

<%c

K232(E) is non empty functional M11(E)

bNFA ^ <%c

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

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

len c

proj1 c

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

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

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

len c

proj1 c

FA ^ c

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

<%FA%> ^ c

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

len c

proj1 c

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

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

FA ^ c

c

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

proj1 (FA ^ c

len c

proj1 c

1 + (len c

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

proj1 (c

len c

proj1 c

1 + (len c

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

x is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega

bNFA is Element of the carrier of FA

[bNFA,c

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

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

<%c

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

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

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

the carrier of (FA,c

[: the carrier of (FA,c

[:[: the carrier of (FA,c

bool [:[: the carrier of (FA,c

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

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

[: the carrier of (FA,c

[:[: the carrier of (FA,c

bool [:[: the carrier of (FA,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

Es is finite Element of bool the non empty finite set

(E,FA, the non empty finite set ,c

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

(E,FA,c

the carrier of (E,FA,c

bool the carrier of (E,FA,c

[: the carrier of (E,FA,c

[:[: the carrier of (E,FA,c

bool [:[: the carrier of (E,FA,c

the Tran of (E,FA,c

u is V15() V18([: 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

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

the carrier of c

the Tran of c

[: the carrier of c

[:[: the carrier of c

bool [:[: the carrier of c

transition-system(# the carrier of c

the of c

bool the carrier of c

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

the of bNFA is Element of bool the carrier of bNFA

{ b

{ b

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

the carrier of c

bool the carrier of c

the of c

FA -succ_of ( the of c

x is Element of bool the carrier of c

(E,bNFA,c

{ b

Es is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega

Es -succ_of ( the 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

Es is finite Element of bool the non empty finite set

(E,FA, the non empty finite set ,c

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

(E,FA,c

the carrier of (E,FA,c

[: the carrier of (E,FA,c

[:[: the carrier of (E,FA,c

bool [:[: the carrier of (E,FA,c

the Tran of (E,FA,c

the of (E,FA,c

bool the carrier of (E,FA,c

{ b

{ b

Es is V15() V18([: 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

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

c

the carrier of c

the Tran of c

[: the carrier of c

[:[: the carrier of c

bool [:[: the carrier of c

the of c

bool the carrier of c

(E,(Lex E), the carrier of c

the of c

{ b

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

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

the of bNFA is Element of bool the carrier of bNFA

{ b

{ b

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

the carrier of c

bool the carrier of c

the of c

x is Element of bool the carrier of c

(E,bNFA,c

{ b

FA -succ_of (x,c

Es is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega

Es -succ_of (x,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

( b

{ b

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

(E,bNFA,c

the carrier of c

the of c

bool the carrier of c

the of c

{ b

( b

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

(E,bNFA,c

the carrier of c

the of c

bool the carrier of c

the of c

{ b

( b

FA -succ_of ( the 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

( b

(E,FA,bNFA, the of bNFA) is functional Element of bool (E ^omega)

{ b

c

c

c

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

( b

(E,FA,bNFA, the of bNFA) is functional Element of bool (E ^omega)

{ b

c

c

c

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

==>.-relation c

the carrier of c

[: the carrier of c

[:[: the carrier of c

bool [:[: the carrier of c

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

u is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega

[Es,u] is V26() Element of [: the carrier of c

v is Element of the carrier of c

bTS is V8() V15() V18( NAT ) Function-like finite V67() Element of E ^omega

[v,bTS] is V26() Element of [: the carrier of c

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

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

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