:: FOMODEL3 semantic presentation

REAL is non empty non trivial non finite V166() set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V166() Element of bool REAL
bool REAL is non empty non trivial non finite V166() set
BOOLEAN is non empty set
0 is empty trivial Relation-like non-empty empty-yielding NAT -defined {{}} -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding finite-membered cardinal {} -element complex ext-real non positive non negative V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V164() V166() V192() FinSequence-yielding finite-support Element of NAT
{} is empty trivial Relation-like non-empty empty-yielding NAT -defined {{}} -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding finite-membered cardinal {} -element complex ext-real non positive non negative V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V164() V166() V192() FinSequence-yielding finite-support set
{{}} is non empty trivial functional finite finite-membered 1 -element V166() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real positive non negative V40() V41() Element of NAT
{} * is non empty functional finite-membered FinSequence-membered FinSequenceSet of {}
the empty trivial Relation-like non-empty empty-yielding NAT -defined {{}} -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding finite-membered cardinal {} -element complex ext-real non positive non negative V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V164() V166() V192() FinSequence-yielding finite-support set is empty trivial Relation-like non-empty empty-yielding NAT -defined {{}} -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding finite-membered cardinal {} -element complex ext-real non positive non negative V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V164() V166() V192() FinSequence-yielding finite-support set
{0,1} is non empty finite finite-membered set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V166() set
bool omega is non empty non trivial non finite V166() set
bool NAT is non empty non trivial non finite V166() set
COMPLEX is non empty non trivial non finite V166() set
RAT is non empty non trivial non finite V166() set
INT is non empty non trivial non finite V166() set
[:{{}},NAT:] is non empty non trivial Relation-like non finite V166() set
[{},{}] is non empty set
{[{},{}]} is non empty trivial Relation-like Function-like constant finite 1 -element V165() V166() finite-support set
[:{{}},NAT:] \ {[{},{}]} is non empty non trivial Relation-like {{}} -defined NAT -valued non finite V166() Element of bool [:{{}},NAT:]
bool [:{{}},NAT:] is non empty non trivial non finite V166() set
[:{{}},NAT:] typed\ {[{},{}]} is Relation-like {{}} -defined NAT -valued Element of bool [:{{}},NAT:]
NAT \/ ([:{{}},NAT:] \ {[{},{}]}) is non empty non trivial non finite V166() set
[:REAL,REAL:] is non empty non trivial Relation-like non finite V166() set
bool [:REAL,REAL:] is non empty non trivial non finite V166() set
K281() is V47() V75() L8()
the U1 of K281() is set
<REAL,+> is V47() L8()
K287() is V47() V75() SubStr of <REAL,+>
<NAT,+> is V47() V75() V97() uniquely-decomposable SubStr of K287()
<REAL,*> is V47() V75() V97() V99() V101() L8()
<NAT,*> is V47() V75() V97() uniquely-decomposable SubStr of <REAL,*>
2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real positive non negative V40() V41() Element of NAT
{{},1} is non empty finite finite-membered set
K368(NAT) is V173() set
[:COMPLEX,COMPLEX:] is non empty non trivial Relation-like non finite V166() set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite V166() set
[:1,1:] is non empty Relation-like finite set
bool [:1,1:] is non empty finite finite-membered set
[:[:1,1:],1:] is non empty Relation-like finite set
bool [:[:1,1:],1:] is non empty finite finite-membered set
3 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real positive non negative V40() V41() Element of NAT
dom {} is empty trivial Relation-like non-empty empty-yielding NAT -defined {{}} -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding finite-membered cardinal {} -element complex ext-real non positive non negative V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V164() V166() V192() FinSequence-yielding finite-support set
rng {} is empty trivial Relation-like non-empty empty-yielding NAT -defined {{}} -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding finite-membered cardinal {} -element complex ext-real non positive non negative V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V164() V165() V166() V192() FinSequence-yielding finite-support set
len {} is empty trivial Relation-like non-empty empty-yielding NAT -defined {{}} -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding finite-membered cardinal {} -element complex ext-real non positive non negative V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V164() V166() V192() FinSequence-yielding finite-support Element of NAT
- 2 is non empty finite complex ext-real non positive negative V40() V41() set
TRUE is boolean Element of BOOLEAN
FALSE is boolean Element of BOOLEAN
U is V51() V53() eligible Language-like
AllSymbolsOf U is non empty non trivial non finite V166() set
the U1 of U is set
(AllSymbolsOf U) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of AllSymbolsOf U
((AllSymbolsOf U) *) \ {{}} is non empty non trivial functional non finite finite-membered FinSequence-membered V165() V166() Element of bool ((AllSymbolsOf U) *)
bool ((AllSymbolsOf U) *) is non empty non trivial non finite V166() set
((AllSymbolsOf U) *) typed\ {{}} is functional finite-membered FinSequence-membered Element of bool ((AllSymbolsOf U) *)
((AllSymbolsOf U) *) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of (AllSymbolsOf U) *
(((AllSymbolsOf U) *) \ {{}}) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() Element of bool (((AllSymbolsOf U) *) *)
bool (((AllSymbolsOf U) *) *) is non empty non trivial non finite V166() set
u is Element of AllSymbolsOf U
<*u*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like finite-support Element of ((AllSymbolsOf U) *) \ {{}}
AllSymbolsOf U is non empty non trivial non finite V166() set
(AllSymbolsOf U) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of AllSymbolsOf U
((AllSymbolsOf U) *) \ {{}} is non empty non trivial functional non finite finite-membered FinSequence-membered V165() V166() Element of bool ((AllSymbolsOf U) *)
bool ((AllSymbolsOf U) *) is non empty non trivial non finite V166() set
((AllSymbolsOf U) *) typed\ {{}} is functional finite-membered FinSequence-membered Element of bool ((AllSymbolsOf U) *)
[1,u] is non empty set
{[1,u]} is non empty trivial Relation-like Function-like constant finite 1 -element V165() V166() finite-support set
U -multiCat is non empty Relation-like ((AllSymbolsOf U) *) * -defined (AllSymbolsOf U) * -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding Element of bool [:(((AllSymbolsOf U) *) *),((AllSymbolsOf U) *):]
((AllSymbolsOf U) *) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of (AllSymbolsOf U) *
[:(((AllSymbolsOf U) *) *),((AllSymbolsOf U) *):] is non empty non trivial Relation-like non finite V166() set
bool [:(((AllSymbolsOf U) *) *),((AllSymbolsOf U) *):] is non empty non trivial non finite V166() set
(AllSymbolsOf U) -multiCat is non empty Relation-like ((AllSymbolsOf U) *) * -defined (AllSymbolsOf U) * -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding Element of bool [:(((AllSymbolsOf U) *) *),((AllSymbolsOf U) *):]
{} .--> {} is trivial Relation-like {{}} -defined Function-like one-to-one constant finite Function-yielding V164() finite-support set
{{}} --> {} is non empty Relation-like empty-yielding {{}} -defined INT -valued {{}} -valued Function-like constant finite total quasi_total Function-yielding V164() finite-support Element of bool [:{{}},{{}}:]
[:{{}},{{}}:] is non empty Relation-like finite set
bool [:{{}},{{}}:] is non empty finite finite-membered set
(AllSymbolsOf U) -concatenation is non empty Relation-like [:((AllSymbolsOf U) *),((AllSymbolsOf U) *):] -defined (AllSymbolsOf U) * -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding V233((AllSymbolsOf U) * ) Element of bool [:[:((AllSymbolsOf U) *),((AllSymbolsOf U) *):],((AllSymbolsOf U) *):]
[:((AllSymbolsOf U) *),((AllSymbolsOf U) *):] is non empty non trivial Relation-like non finite V166() set
[:[:((AllSymbolsOf U) *),((AllSymbolsOf U) *):],((AllSymbolsOf U) *):] is non empty non trivial Relation-like non finite V166() set
bool [:[:((AllSymbolsOf U) *),((AllSymbolsOf U) *):],((AllSymbolsOf U) *):] is non empty non trivial non finite V166() set
MultPlace ((AllSymbolsOf U) -concatenation) is non empty Relation-like (((AllSymbolsOf U) *) *) \ {{}} -defined (AllSymbolsOf U) * -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding Element of bool [:((((AllSymbolsOf U) *) *) \ {{}}),((AllSymbolsOf U) *):]
(((AllSymbolsOf U) *) *) \ {{}} is non empty non trivial functional non finite finite-membered FinSequence-membered V165() V166() Element of bool (((AllSymbolsOf U) *) *)
bool (((AllSymbolsOf U) *) *) is non empty non trivial non finite V166() set
(((AllSymbolsOf U) *) *) typed\ {{}} is functional finite-membered FinSequence-membered Element of bool (((AllSymbolsOf U) *) *)
[:((((AllSymbolsOf U) *) *) \ {{}}),((AllSymbolsOf U) *):] is non empty non trivial Relation-like non finite V166() set
bool [:((((AllSymbolsOf U) *) *) \ {{}}),((AllSymbolsOf U) *):] is non empty non trivial non finite V166() set
({} .--> {}) +* (MultPlace ((AllSymbolsOf U) -concatenation)) is non empty Relation-like Function-like Function-yielding V164() set
S is Relation-like NAT -defined ((AllSymbolsOf U) *) \ {{}} -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V164() FinSequence-yielding finite-support Element of (((AllSymbolsOf U) *) \ {{}}) *
(U -multiCat) . S is Relation-like NAT -defined AllSymbolsOf U -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (AllSymbolsOf U) *
<*u*> ^ ((U -multiCat) . S) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
E is Relation-like NAT -defined AllSymbolsOf U -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (AllSymbolsOf U) *
i is Relation-like NAT -defined AllSymbolsOf U -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of AllSymbolsOf U
E ^ i is Relation-like NAT -defined AllSymbolsOf U -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of AllSymbolsOf U
x is Relation-like NAT -defined AllSymbolsOf U -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of AllSymbolsOf U
U is V51() V53() eligible Language-like
AllSymbolsOf U is non empty non trivial non finite V166() set
the U1 of U is set
S is non relational termal own ofAtomicFormula Element of AllSymbolsOf U
ar S is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of INT
the adicity of U is non empty Relation-like the U1 of U \ { the U3 of U} -defined INT -valued Function-like total quasi_total Element of bool [:( the U1 of U \ { the U3 of U}),INT:]
the U3 of U is Element of the U1 of U
{ the U3 of U} is non empty trivial finite 1 -element set
the U1 of U \ { the U3 of U} is non empty Element of bool the U1 of U
bool the U1 of U is non empty set
the U1 of U typed\ { the U3 of U} is Element of bool the U1 of U
[:( the U1 of U \ { the U3 of U}),INT:] is non empty non trivial Relation-like non finite V166() set
bool [:( the U1 of U \ { the U3 of U}),INT:] is non empty non trivial non finite V166() set
the adicity of U . S is set
abs (ar S) is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
AllSymbolsOf U is non empty non trivial non finite V166() set
(AllSymbolsOf U) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of AllSymbolsOf U
((AllSymbolsOf U) *) \ {{}} is non empty non trivial functional non finite finite-membered FinSequence-membered V165() V166() Element of bool ((AllSymbolsOf U) *)
bool ((AllSymbolsOf U) *) is non empty non trivial non finite V166() set
((AllSymbolsOf U) *) typed\ {{}} is functional finite-membered FinSequence-membered Element of bool ((AllSymbolsOf U) *)
K335((((AllSymbolsOf U) *) \ {{}})) is non empty non trivial non finite V166() Element of bool (bool (((AllSymbolsOf U) *) \ {{}}))
bool (((AllSymbolsOf U) *) \ {{}}) is non empty non trivial non finite V166() set
bool (bool (((AllSymbolsOf U) *) \ {{}})) is non empty non trivial non finite V166() set
U -termsOfMaxDepth is non empty Relation-like NAT -defined K335((((AllSymbolsOf U) *) \ {{}})) -valued Function-like total quasi_total Element of bool [:NAT,K335((((AllSymbolsOf U) *) \ {{}})):]
[:NAT,K335((((AllSymbolsOf U) *) \ {{}})):] is non empty non trivial Relation-like non finite V166() set
bool [:NAT,K335((((AllSymbolsOf U) *) \ {{}})):] is non empty non trivial non finite V166() set
u is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
(U -termsOfMaxDepth) . u is non empty functional finite-membered FinSequence-membered V165() V166() AllSymbolsOf U -prefix U -prefix Element of K335((((AllSymbolsOf U) *) \ {{}}))
(((AllSymbolsOf U) *) \ {{}}) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of ((AllSymbolsOf U) *) \ {{}}
((U -termsOfMaxDepth) . u) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() Element of bool ((((AllSymbolsOf U) *) \ {{}}) *)
bool ((((AllSymbolsOf U) *) \ {{}}) *) is non empty non trivial non finite V166() set
l is Relation-like NAT -defined (U -termsOfMaxDepth) . u -valued Function-like finite abs (ar S) -element FinSequence-like FinSubsequence-like Function-yielding V164() FinSequence-yielding finite-support Element of ((U -termsOfMaxDepth) . u) *
(U,S,l) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support Element of ((AllSymbolsOf U) *) \ {{}}
<*S*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like finite-support Element of ((AllSymbolsOf U) *) \ {{}}
[1,S] is non empty set
{[1,S]} is non empty trivial Relation-like Function-like constant finite 1 -element V165() V166() finite-support set
(AllSymbolsOf U) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of AllSymbolsOf U
((AllSymbolsOf U) *) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of (AllSymbolsOf U) *
U -multiCat is non empty Relation-like ((AllSymbolsOf U) *) * -defined (AllSymbolsOf U) * -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding Element of bool [:(((AllSymbolsOf U) *) *),((AllSymbolsOf U) *):]
((AllSymbolsOf U) *) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of (AllSymbolsOf U) *
[:(((AllSymbolsOf U) *) *),((AllSymbolsOf U) *):] is non empty non trivial Relation-like non finite V166() set
bool [:(((AllSymbolsOf U) *) *),((AllSymbolsOf U) *):] is non empty non trivial non finite V166() set
(AllSymbolsOf U) -multiCat is non empty Relation-like ((AllSymbolsOf U) *) * -defined (AllSymbolsOf U) * -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding Element of bool [:(((AllSymbolsOf U) *) *),((AllSymbolsOf U) *):]
(AllSymbolsOf U) -concatenation is non empty Relation-like [:((AllSymbolsOf U) *),((AllSymbolsOf U) *):] -defined (AllSymbolsOf U) * -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding V233((AllSymbolsOf U) * ) Element of bool [:[:((AllSymbolsOf U) *),((AllSymbolsOf U) *):],((AllSymbolsOf U) *):]
[:((AllSymbolsOf U) *),((AllSymbolsOf U) *):] is non empty non trivial Relation-like non finite V166() set
[:[:((AllSymbolsOf U) *),((AllSymbolsOf U) *):],((AllSymbolsOf U) *):] is non empty non trivial Relation-like non finite V166() set
bool [:[:((AllSymbolsOf U) *),((AllSymbolsOf U) *):],((AllSymbolsOf U) *):] is non empty non trivial non finite V166() set
MultPlace ((AllSymbolsOf U) -concatenation) is non empty Relation-like (((AllSymbolsOf U) *) *) \ {{}} -defined (AllSymbolsOf U) * -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding Element of bool [:((((AllSymbolsOf U) *) *) \ {{}}),((AllSymbolsOf U) *):]
(((AllSymbolsOf U) *) *) \ {{}} is non empty non trivial functional non finite finite-membered FinSequence-membered V165() V166() Element of bool (((AllSymbolsOf U) *) *)
bool (((AllSymbolsOf U) *) *) is non empty non trivial non finite V166() set
(((AllSymbolsOf U) *) *) typed\ {{}} is functional finite-membered FinSequence-membered Element of bool (((AllSymbolsOf U) *) *)
[:((((AllSymbolsOf U) *) *) \ {{}}),((AllSymbolsOf U) *):] is non empty non trivial Relation-like non finite V166() set
bool [:((((AllSymbolsOf U) *) *) \ {{}}),((AllSymbolsOf U) *):] is non empty non trivial non finite V166() set
({} .--> {}) +* (MultPlace ((AllSymbolsOf U) -concatenation)) is non empty Relation-like Function-like Function-yielding V164() set
(U -multiCat) . l is Relation-like NAT -defined AllSymbolsOf U -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (AllSymbolsOf U) *
<*S*> ^ ((U -multiCat) . l) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
u + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real positive non negative V40() V41() Element of NAT
LettersOf U is non empty non trivial non finite V166() Element of bool (AllSymbolsOf U)
bool (AllSymbolsOf U) is non empty non trivial non finite V166() set
{0} is non empty trivial functional finite finite-membered 1 -element V166() Element of bool NAT
0 * is non empty functional finite-membered FinSequence-membered FinSequenceSet of 0
{0} is non empty trivial functional finite finite-membered 1 -element V166() set
the adicity of U " {0} is Element of bool ( the U1 of U \ { the U3 of U})
bool ( the U1 of U \ { the U3 of U}) is non empty set
AtomicTermsOf U is functional finite-membered FinSequence-membered Element of bool ((AllSymbolsOf U) *)
LettersOf U is non empty non trivial non finite V166() set
1 -tuples_on (LettersOf U) is non empty functional finite-membered FinSequence-membered V165() V166() FinSequenceSet of LettersOf U
{ (Compound (b₁,((U -termsOfMaxDepth) . u))) where b₁ is ofAtomicFormula Element of AllSymbolsOf U : b₁ is operational } is set
bool ((AllSymbolsOf U) *) is non empty non trivial non finite V166() set
((AllSymbolsOf U) *) \ {{}} is non empty non trivial functional non finite finite-membered FinSequence-membered V165() V166() Element of bool ((AllSymbolsOf U) *)
((AllSymbolsOf U) *) typed\ {{}} is functional finite-membered FinSequence-membered Element of bool ((AllSymbolsOf U) *)
I is functional finite-membered FinSequence-membered Element of bool ((AllSymbolsOf U) *)
I * is non empty functional finite-membered FinSequence-membered Element of bool (((AllSymbolsOf U) *) *)
bool (((AllSymbolsOf U) *) *) is non empty non trivial non finite V166() set
j is Relation-like NAT -defined (AllSymbolsOf U) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V164() FinSequence-yielding finite-support Element of ((AllSymbolsOf U) *) *
(U -multiCat) . j is Relation-like NAT -defined AllSymbolsOf U -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (AllSymbolsOf U) *
<*S*> ^ ((U -multiCat) . j) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
rng j is finite set
Compound (S,((U -termsOfMaxDepth) . u)) is functional finite-membered FinSequence-membered V165() Element of K335((((AllSymbolsOf U) *) \ {{}}))
K395((AllSymbolsOf U),S) is non empty trivial Relation-like NAT -defined AllSymbolsOf U -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like finite-support Element of 1 -tuples_on (AllSymbolsOf U)
1 -tuples_on (AllSymbolsOf U) is non empty functional finite-membered FinSequence-membered V165() V166() FinSequenceSet of AllSymbolsOf U
{ (K395((AllSymbolsOf U),S) ^ ((U -multiCat) . b₁)) where b₁ is Relation-like NAT -defined (AllSymbolsOf U) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V164() FinSequence-yielding finite-support Element of ((AllSymbolsOf U) *) * : ( rng b₁ c= (U -termsOfMaxDepth) . u & b₁ is abs (ar S) -element ) } is set
Jj is literal non operational non relational termal own ofAtomicFormula Element of AllSymbolsOf U
ar Jj is empty trivial Relation-like non-empty empty-yielding NAT -defined {{}} -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding finite-membered cardinal {} -element complex ext-real non positive non negative V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V164() V166() V192() FinSequence-yielding finite-support Element of INT
the adicity of U . Jj is set
jJ is empty trivial Relation-like non-empty empty-yielding NAT -defined {{}} -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding finite-membered cardinal 0 -element complex ext-real non positive non negative V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V164() V166() V192() FinSequence-yielding finite-support set
<*S*> ^ jJ is non empty Relation-like NAT -defined Function-like finite 1 + 0 -element 1 + 0 -element FinSequence-like FinSubsequence-like finite-support set
1 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real positive non negative V40() V41() set
1 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real positive non negative V40() V41() Element of NAT
<*S*> null jJ is Relation-like NAT -defined jJ \/ (dom <*S*>) -defined Seg (1 + jJ) -defined jJ \/ (rng <*S*>) -valued Function-like finite len <*S*> -element total FinSequence-like FinSubsequence-like finite-support set
dom <*S*> is non empty trivial finite 1 -element set
jJ \/ (dom <*S*>) is non empty finite set
1 + jJ is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real positive non negative V40() V41() set
Seg (1 + jJ) is non empty finite 1 + jJ -element Element of bool NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT : ( 1 <= b₁ & b₁ <= 1 + jJ ) } is set
rng <*S*> is non empty trivial finite 1 -element set
jJ \/ (rng <*S*>) is non empty finite set
len <*S*> is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real positive non negative V40() V41() Element of NAT
<*S*> \typed/ jJ is Relation-like NAT -defined finite Element of bool (<*S*> \/ jJ)
<*S*> \/ jJ is non empty Relation-like NAT -defined finite set
bool (<*S*> \/ jJ) is non empty finite finite-membered set
jJ ^ <*S*> is non empty Relation-like NAT -defined Function-like finite 0 + 1 -element 0 + 1 -element FinSequence-like FinSubsequence-like finite-support set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real positive non negative V40() V41() set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real positive non negative V40() V41() Element of NAT
jJ is literal Element of LettersOf U
<*jJ*> is non empty trivial Relation-like NAT -defined TermSymbolsOf U -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like finite-support termal 0 -termal Element of ((AllSymbolsOf U) *) \ {{}}
TermSymbolsOf U is non empty set
the adicity of U " NAT is Element of bool ( the U1 of U \ { the U3 of U})
[1,jJ] is non empty set
{[1,jJ]} is non empty trivial Relation-like Function-like constant finite 1 -element V165() V166() finite-support set
(U -termsOfMaxDepth) . 0 is non empty functional finite-membered FinSequence-membered V165() V166() AllSymbolsOf U -prefix U -prefix Element of K335((((AllSymbolsOf U) *) \ {{}}))
0 + (u + 1) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real positive non negative V40() V41() Element of NAT
(U -termsOfMaxDepth) . (0 + (u + 1)) is non empty functional finite-membered FinSequence-membered V165() V166() AllSymbolsOf U -prefix U -prefix Element of K335((((AllSymbolsOf U) *) \ {{}}))
g is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support Element of ((AllSymbolsOf U) *) \ {{}}
union { (Compound (b₁,((U -termsOfMaxDepth) . u))) where b₁ is ofAtomicFormula Element of AllSymbolsOf U : b₁ is operational } is set
(union { (Compound (b₁,((U -termsOfMaxDepth) . u))) where b₁ is ofAtomicFormula Element of AllSymbolsOf U : b₁ is operational } ) \/ ((U -termsOfMaxDepth) . u) is non empty set
(U -termsOfMaxDepth) . (u + 1) is non empty functional finite-membered FinSequence-membered V165() V166() AllSymbolsOf U -prefix U -prefix Element of K335((((AllSymbolsOf U) *) \ {{}}))
Jj is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support Element of ((AllSymbolsOf U) *) \ {{}}
U is set
u is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() set
S is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() set
u + S is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() set
l is V51() V53() eligible Language-like
AllSymbolsOf l is non empty non trivial non finite V166() set
the U1 of l is set
(AllSymbolsOf l) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of AllSymbolsOf l
((AllSymbolsOf l) *) \ {{}} is non empty non trivial functional non finite finite-membered FinSequence-membered V165() V166() Element of bool ((AllSymbolsOf l) *)
bool ((AllSymbolsOf l) *) is non empty non trivial non finite V166() set
((AllSymbolsOf l) *) typed\ {{}} is functional finite-membered FinSequence-membered Element of bool ((AllSymbolsOf l) *)
K335((((AllSymbolsOf l) *) \ {{}})) is non empty non trivial non finite V166() Element of bool (bool (((AllSymbolsOf l) *) \ {{}}))
bool (((AllSymbolsOf l) *) \ {{}}) is non empty non trivial non finite V166() set
bool (bool (((AllSymbolsOf l) *) \ {{}})) is non empty non trivial non finite V166() set
l -termsOfMaxDepth is non empty Relation-like NAT -defined K335((((AllSymbolsOf l) *) \ {{}})) -valued Function-like total quasi_total Element of bool [:NAT,K335((((AllSymbolsOf l) *) \ {{}})):]
[:NAT,K335((((AllSymbolsOf l) *) \ {{}})):] is non empty non trivial Relation-like non finite V166() set
bool [:NAT,K335((((AllSymbolsOf l) *) \ {{}})):] is non empty non trivial non finite V166() set
(l -termsOfMaxDepth) . (u + S) is non empty functional finite-membered FinSequence-membered V165() V166() AllSymbolsOf l -prefix l -prefix Element of K335((((AllSymbolsOf l) *) \ {{}}))
(l -termsOfMaxDepth) . u is non empty functional finite-membered FinSequence-membered V165() V166() AllSymbolsOf l -prefix l -prefix Element of K335((((AllSymbolsOf l) *) \ {{}}))
U is set
u is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() set
S is V51() V53() eligible Language-like
AllSymbolsOf S is non empty non trivial non finite V166() set
the U1 of S is set
(AllSymbolsOf S) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of AllSymbolsOf S
((AllSymbolsOf S) *) \ {{}} is non empty non trivial functional non finite finite-membered FinSequence-membered V165() V166() Element of bool ((AllSymbolsOf S) *)
bool ((AllSymbolsOf S) *) is non empty non trivial non finite V166() set
((AllSymbolsOf S) *) typed\ {{}} is functional finite-membered FinSequence-membered Element of bool ((AllSymbolsOf S) *)
K335((((AllSymbolsOf S) *) \ {{}})) is non empty non trivial non finite V166() Element of bool (bool (((AllSymbolsOf S) *) \ {{}}))
bool (((AllSymbolsOf S) *) \ {{}}) is non empty non trivial non finite V166() set
bool (bool (((AllSymbolsOf S) *) \ {{}})) is non empty non trivial non finite V166() set
S -termsOfMaxDepth is non empty Relation-like NAT -defined K335((((AllSymbolsOf S) *) \ {{}})) -valued Function-like total quasi_total Element of bool [:NAT,K335((((AllSymbolsOf S) *) \ {{}})):]
[:NAT,K335((((AllSymbolsOf S) *) \ {{}})):] is non empty non trivial Relation-like non finite V166() set
bool [:NAT,K335((((AllSymbolsOf S) *) \ {{}})):] is non empty non trivial non finite V166() set
(S -termsOfMaxDepth) . u is non empty functional finite-membered FinSequence-membered V165() V166() AllSymbolsOf S -prefix S -prefix Element of K335((((AllSymbolsOf S) *) \ {{}}))
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT : not U in (S -termsOfMaxDepth) . b₁ } is set
E is set
i is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
(S -termsOfMaxDepth) . i is non empty functional finite-membered FinSequence-membered V165() V166() AllSymbolsOf S -prefix S -prefix Element of K335((((AllSymbolsOf S) *) \ {{}}))
x is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() set
u + x is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() set
U is V51() V53() eligible Language-like
AllTermsOf U is non empty functional finite-membered FinSequence-membered V165() V166() AllSymbolsOf U -prefix U -prefix Element of K335((((AllSymbolsOf U) *) \ {{}}))
AllSymbolsOf U is non empty non trivial non finite V166() set
the U1 of U is set
(AllSymbolsOf U) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of AllSymbolsOf U
((AllSymbolsOf U) *) \ {{}} is non empty non trivial functional non finite finite-membered FinSequence-membered V165() V166() Element of bool ((AllSymbolsOf U) *)
bool ((AllSymbolsOf U) *) is non empty non trivial non finite V166() set
((AllSymbolsOf U) *) typed\ {{}} is functional finite-membered FinSequence-membered Element of bool ((AllSymbolsOf U) *)
bool (((AllSymbolsOf U) *) \ {{}}) is non empty non trivial non finite V166() set
K335((((AllSymbolsOf U) *) \ {{}})) is non empty non trivial non finite V166() Element of bool (bool (((AllSymbolsOf U) *) \ {{}}))
bool (bool (((AllSymbolsOf U) *) \ {{}})) is non empty non trivial non finite V166() set
U -termsOfMaxDepth is Relation-like Function-like set
rng (U -termsOfMaxDepth) is set
union (rng (U -termsOfMaxDepth)) is set
(((AllSymbolsOf U) *) \ {{}}) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of ((AllSymbolsOf U) *) \ {{}}
(AllTermsOf U) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() Element of bool ((((AllSymbolsOf U) *) \ {{}}) *)
bool ((((AllSymbolsOf U) *) \ {{}}) *) is non empty non trivial non finite V166() set
U -termsOfMaxDepth is non empty Relation-like NAT -defined K335((((AllSymbolsOf U) *) \ {{}})) -valued Function-like total quasi_total Element of bool [:NAT,K335((((AllSymbolsOf U) *) \ {{}})):]
[:NAT,K335((((AllSymbolsOf U) *) \ {{}})):] is non empty non trivial Relation-like non finite V166() set
bool [:NAT,K335((((AllSymbolsOf U) *) \ {{}})):] is non empty non trivial non finite V166() set
l is Relation-like NAT -defined AllTermsOf U -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V164() FinSequence-yielding finite-support Element of (AllTermsOf U) *
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT : not l . a₁ in (U -termsOfMaxDepth) . b₁ } is set
dom l is finite Element of bool NAT
{ H₁(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT : b₁ in dom l } is set
i is set
x is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
l . x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT : not l . x in (U -termsOfMaxDepth) . b₁ } is set
rng l is finite set
O is non empty set
[:O,(AllTermsOf U):] is non empty Relation-like set
bool [:O,(AllTermsOf U):] is non empty set
UU is non empty Relation-like non empty-yielding O -defined AllTermsOf U -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding Element of bool [:O,(AllTermsOf U):]
III is Element of O
UU . III is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support termal Element of AllTermsOf U
E is Relation-like Function-like set
X is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
E . X is set
i is finite finite-membered set
union i is finite set
x is finite set
NAT \ x is non empty non trivial non finite V166() Element of bool REAL
NAT typed\ x is Element of bool NAT
NAT \ x is non empty non trivial non finite V166() Element of bool NAT
O is set
UU is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
(U -termsOfMaxDepth) . UU is non empty functional finite-membered FinSequence-membered V165() V166() AllSymbolsOf U -prefix U -prefix Element of K335((((AllSymbolsOf U) *) \ {{}}))
((U -termsOfMaxDepth) . UU) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() Element of bool ((((AllSymbolsOf U) *) \ {{}}) *)
III is set
l . III is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT : not l . III in (U -termsOfMaxDepth) . b₁ } is set
X is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
l . X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT : not l . X in (U -termsOfMaxDepth) . b₁ } is set
[:(dom l),((U -termsOfMaxDepth) . UU):] is Relation-like set
bool [:(dom l),((U -termsOfMaxDepth) . UU):] is non empty set
U is V51() V53() eligible Language-like
AllSymbolsOf U is non empty non trivial non finite V166() set
the U1 of U is set
u is non relational termal own ofAtomicFormula Element of AllSymbolsOf U
ar u is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of INT
the adicity of U is non empty Relation-like the U1 of U \ { the U3 of U} -defined INT -valued Function-like total quasi_total Element of bool [:( the U1 of U \ { the U3 of U}),INT:]
the U3 of U is Element of the U1 of U
{ the U3 of U} is non empty trivial finite 1 -element set
the U1 of U \ { the U3 of U} is non empty Element of bool the U1 of U
bool the U1 of U is non empty set
the U1 of U typed\ { the U3 of U} is Element of bool the U1 of U
[:( the U1 of U \ { the U3 of U}),INT:] is non empty non trivial Relation-like non finite V166() set
bool [:( the U1 of U \ { the U3 of U}),INT:] is non empty non trivial non finite V166() set
the adicity of U . u is set
abs (ar u) is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
AllTermsOf U is non empty functional finite-membered FinSequence-membered V165() V166() AllSymbolsOf U -prefix U -prefix Element of K335((((AllSymbolsOf U) *) \ {{}}))
AllSymbolsOf U is non empty non trivial non finite V166() set
(AllSymbolsOf U) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of AllSymbolsOf U
((AllSymbolsOf U) *) \ {{}} is non empty non trivial functional non finite finite-membered FinSequence-membered V165() V166() Element of bool ((AllSymbolsOf U) *)
bool ((AllSymbolsOf U) *) is non empty non trivial non finite V166() set
((AllSymbolsOf U) *) typed\ {{}} is functional finite-membered FinSequence-membered Element of bool ((AllSymbolsOf U) *)
bool (((AllSymbolsOf U) *) \ {{}}) is non empty non trivial non finite V166() set
K335((((AllSymbolsOf U) *) \ {{}})) is non empty non trivial non finite V166() Element of bool (bool (((AllSymbolsOf U) *) \ {{}}))
bool (bool (((AllSymbolsOf U) *) \ {{}})) is non empty non trivial non finite V166() set
U -termsOfMaxDepth is Relation-like Function-like set
rng (U -termsOfMaxDepth) is set
union (rng (U -termsOfMaxDepth)) is set
(((AllSymbolsOf U) *) \ {{}}) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of ((AllSymbolsOf U) *) \ {{}}
(AllTermsOf U) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() Element of bool ((((AllSymbolsOf U) *) \ {{}}) *)
bool ((((AllSymbolsOf U) *) \ {{}}) *) is non empty non trivial non finite V166() set
S is Relation-like NAT -defined AllTermsOf U -valued Function-like finite abs (ar u) -element FinSequence-like FinSubsequence-like Function-yielding V164() FinSequence-yielding finite-support Element of (AllTermsOf U) *
(U,u,S) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support Element of ((AllSymbolsOf U) *) \ {{}}
<*u*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like finite-support Element of ((AllSymbolsOf U) *) \ {{}}
[1,u] is non empty set
{[1,u]} is non empty trivial Relation-like Function-like constant finite 1 -element V165() V166() finite-support set
(AllSymbolsOf U) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of AllSymbolsOf U
((AllSymbolsOf U) *) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of (AllSymbolsOf U) *
U -multiCat is non empty Relation-like ((AllSymbolsOf U) *) * -defined (AllSymbolsOf U) * -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding Element of bool [:(((AllSymbolsOf U) *) *),((AllSymbolsOf U) *):]
((AllSymbolsOf U) *) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of (AllSymbolsOf U) *
[:(((AllSymbolsOf U) *) *),((AllSymbolsOf U) *):] is non empty non trivial Relation-like non finite V166() set
bool [:(((AllSymbolsOf U) *) *),((AllSymbolsOf U) *):] is non empty non trivial non finite V166() set
(AllSymbolsOf U) -multiCat is non empty Relation-like ((AllSymbolsOf U) *) * -defined (AllSymbolsOf U) * -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding Element of bool [:(((AllSymbolsOf U) *) *),((AllSymbolsOf U) *):]
(AllSymbolsOf U) -concatenation is non empty Relation-like [:((AllSymbolsOf U) *),((AllSymbolsOf U) *):] -defined (AllSymbolsOf U) * -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding V233((AllSymbolsOf U) * ) Element of bool [:[:((AllSymbolsOf U) *),((AllSymbolsOf U) *):],((AllSymbolsOf U) *):]
[:((AllSymbolsOf U) *),((AllSymbolsOf U) *):] is non empty non trivial Relation-like non finite V166() set
[:[:((AllSymbolsOf U) *),((AllSymbolsOf U) *):],((AllSymbolsOf U) *):] is non empty non trivial Relation-like non finite V166() set
bool [:[:((AllSymbolsOf U) *),((AllSymbolsOf U) *):],((AllSymbolsOf U) *):] is non empty non trivial non finite V166() set
MultPlace ((AllSymbolsOf U) -concatenation) is non empty Relation-like (((AllSymbolsOf U) *) *) \ {{}} -defined (AllSymbolsOf U) * -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding Element of bool [:((((AllSymbolsOf U) *) *) \ {{}}),((AllSymbolsOf U) *):]
(((AllSymbolsOf U) *) *) \ {{}} is non empty non trivial functional non finite finite-membered FinSequence-membered V165() V166() Element of bool (((AllSymbolsOf U) *) *)
bool (((AllSymbolsOf U) *) *) is non empty non trivial non finite V166() set
(((AllSymbolsOf U) *) *) typed\ {{}} is functional finite-membered FinSequence-membered Element of bool (((AllSymbolsOf U) *) *)
[:((((AllSymbolsOf U) *) *) \ {{}}),((AllSymbolsOf U) *):] is non empty non trivial Relation-like non finite V166() set
bool [:((((AllSymbolsOf U) *) *) \ {{}}),((AllSymbolsOf U) *):] is non empty non trivial non finite V166() set
({} .--> {}) +* (MultPlace ((AllSymbolsOf U) -concatenation)) is non empty Relation-like Function-like Function-yielding V164() set
(U -multiCat) . S is Relation-like NAT -defined AllSymbolsOf U -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (AllSymbolsOf U) *
<*u*> ^ ((U -multiCat) . S) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
U -termsOfMaxDepth is non empty Relation-like NAT -defined K335((((AllSymbolsOf U) *) \ {{}})) -valued Function-like total quasi_total Element of bool [:NAT,K335((((AllSymbolsOf U) *) \ {{}})):]
[:NAT,K335((((AllSymbolsOf U) *) \ {{}})):] is non empty non trivial Relation-like non finite V166() set
bool [:NAT,K335((((AllSymbolsOf U) *) \ {{}})):] is non empty non trivial non finite V166() set
E is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
(U -termsOfMaxDepth) . E is non empty functional finite-membered FinSequence-membered V165() V166() AllSymbolsOf U -prefix U -prefix Element of K335((((AllSymbolsOf U) *) \ {{}}))
((U -termsOfMaxDepth) . E) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() Element of bool ((((AllSymbolsOf U) *) \ {{}}) *)
i is Relation-like NAT -defined (U -termsOfMaxDepth) . E -valued Function-like finite abs (ar u) -element FinSequence-like FinSubsequence-like Function-yielding V164() FinSequence-yielding finite-support Element of ((U -termsOfMaxDepth) . E) *
(U,u,i) is non empty Relation-like NAT -defined TermSymbolsOf U -valued Function-like finite FinSequence-like FinSubsequence-like finite-support termal E + 1 -termal Element of ((AllSymbolsOf U) *) \ {{}}
TermSymbolsOf U is non empty set
the adicity of U " NAT is Element of bool ( the U1 of U \ { the U3 of U})
bool ( the U1 of U \ { the U3 of U}) is non empty set
E + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real positive non negative V40() V41() Element of NAT
(U -multiCat) . i is Relation-like NAT -defined AllSymbolsOf U -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (AllSymbolsOf U) *
<*u*> ^ ((U -multiCat) . i) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
x is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support Element of ((AllSymbolsOf U) *) \ {{}}
U is V51() V53() eligible Language-like
AllSymbolsOf U is non empty non trivial non finite V166() set
the U1 of U is set
u is low-compounding relational ofAtomicFormula Element of AllSymbolsOf U
ar u is non empty finite complex ext-real non positive negative V40() V41() Element of INT
the adicity of U is non empty Relation-like the U1 of U \ { the U3 of U} -defined INT -valued Function-like total quasi_total Element of bool [:( the U1 of U \ { the U3 of U}),INT:]
the U3 of U is Element of the U1 of U
{ the U3 of U} is non empty trivial finite 1 -element set
the U1 of U \ { the U3 of U} is non empty Element of bool the U1 of U
bool the U1 of U is non empty set
the U1 of U typed\ { the U3 of U} is Element of bool the U1 of U
[:( the U1 of U \ { the U3 of U}),INT:] is non empty non trivial Relation-like non finite V166() set
bool [:( the U1 of U \ { the U3 of U}),INT:] is non empty non trivial non finite V166() set
the adicity of U . u is set
abs (ar u) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real positive non negative V40() V41() Element of NAT
AllTermsOf U is non empty functional finite-membered FinSequence-membered V165() V166() AllSymbolsOf U -prefix U -prefix Element of K335((((AllSymbolsOf U) *) \ {{}}))
AllSymbolsOf U is non empty non trivial non finite V166() set
(AllSymbolsOf U) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of AllSymbolsOf U
((AllSymbolsOf U) *) \ {{}} is non empty non trivial functional non finite finite-membered FinSequence-membered V165() V166() Element of bool ((AllSymbolsOf U) *)
bool ((AllSymbolsOf U) *) is non empty non trivial non finite V166() set
((AllSymbolsOf U) *) typed\ {{}} is functional finite-membered FinSequence-membered Element of bool ((AllSymbolsOf U) *)
bool (((AllSymbolsOf U) *) \ {{}}) is non empty non trivial non finite V166() set
K335((((AllSymbolsOf U) *) \ {{}})) is non empty non trivial non finite V166() Element of bool (bool (((AllSymbolsOf U) *) \ {{}}))
bool (bool (((AllSymbolsOf U) *) \ {{}})) is non empty non trivial non finite V166() set
U -termsOfMaxDepth is Relation-like Function-like set
rng (U -termsOfMaxDepth) is set
union (rng (U -termsOfMaxDepth)) is set
(((AllSymbolsOf U) *) \ {{}}) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of ((AllSymbolsOf U) *) \ {{}}
(AllTermsOf U) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() Element of bool ((((AllSymbolsOf U) *) \ {{}}) *)
bool ((((AllSymbolsOf U) *) \ {{}}) *) is non empty non trivial non finite V166() set
S is Relation-like NAT -defined AllTermsOf U -valued Function-like finite abs (ar u) -element FinSequence-like FinSubsequence-like Function-yielding V164() FinSequence-yielding finite-support Element of (AllTermsOf U) *
(U,u,S) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support Element of ((AllSymbolsOf U) *) \ {{}}
<*u*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like finite-support Element of ((AllSymbolsOf U) *) \ {{}}
[1,u] is non empty set
{[1,u]} is non empty trivial Relation-like Function-like constant finite 1 -element V165() V166() finite-support set
(AllSymbolsOf U) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of AllSymbolsOf U
((AllSymbolsOf U) *) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of (AllSymbolsOf U) *
U -multiCat is non empty Relation-like ((AllSymbolsOf U) *) * -defined (AllSymbolsOf U) * -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding Element of bool [:(((AllSymbolsOf U) *) *),((AllSymbolsOf U) *):]
((AllSymbolsOf U) *) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of (AllSymbolsOf U) *
[:(((AllSymbolsOf U) *) *),((AllSymbolsOf U) *):] is non empty non trivial Relation-like non finite V166() set
bool [:(((AllSymbolsOf U) *) *),((AllSymbolsOf U) *):] is non empty non trivial non finite V166() set
(AllSymbolsOf U) -multiCat is non empty Relation-like ((AllSymbolsOf U) *) * -defined (AllSymbolsOf U) * -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding Element of bool [:(((AllSymbolsOf U) *) *),((AllSymbolsOf U) *):]
(AllSymbolsOf U) -concatenation is non empty Relation-like [:((AllSymbolsOf U) *),((AllSymbolsOf U) *):] -defined (AllSymbolsOf U) * -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding V233((AllSymbolsOf U) * ) Element of bool [:[:((AllSymbolsOf U) *),((AllSymbolsOf U) *):],((AllSymbolsOf U) *):]
[:((AllSymbolsOf U) *),((AllSymbolsOf U) *):] is non empty non trivial Relation-like non finite V166() set
[:[:((AllSymbolsOf U) *),((AllSymbolsOf U) *):],((AllSymbolsOf U) *):] is non empty non trivial Relation-like non finite V166() set
bool [:[:((AllSymbolsOf U) *),((AllSymbolsOf U) *):],((AllSymbolsOf U) *):] is non empty non trivial non finite V166() set
MultPlace ((AllSymbolsOf U) -concatenation) is non empty Relation-like (((AllSymbolsOf U) *) *) \ {{}} -defined (AllSymbolsOf U) * -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding Element of bool [:((((AllSymbolsOf U) *) *) \ {{}}),((AllSymbolsOf U) *):]
(((AllSymbolsOf U) *) *) \ {{}} is non empty non trivial functional non finite finite-membered FinSequence-membered V165() V166() Element of bool (((AllSymbolsOf U) *) *)
bool (((AllSymbolsOf U) *) *) is non empty non trivial non finite V166() set
(((AllSymbolsOf U) *) *) typed\ {{}} is functional finite-membered FinSequence-membered Element of bool (((AllSymbolsOf U) *) *)
[:((((AllSymbolsOf U) *) *) \ {{}}),((AllSymbolsOf U) *):] is non empty non trivial Relation-like non finite V166() set
bool [:((((AllSymbolsOf U) *) *) \ {{}}),((AllSymbolsOf U) *):] is non empty non trivial non finite V166() set
({} .--> {}) +* (MultPlace ((AllSymbolsOf U) -concatenation)) is non empty Relation-like Function-like Function-yielding V164() set
(U -multiCat) . S is Relation-like NAT -defined AllSymbolsOf U -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (AllSymbolsOf U) *
<*u*> ^ ((U -multiCat) . S) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
l is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support Element of ((AllSymbolsOf U) *) \ {{}}
U is V51() V53() eligible Language-like
AllSymbolsOf U is non empty non trivial non finite V166() set
the U1 of U is set
(AllSymbolsOf U) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of AllSymbolsOf U
((AllSymbolsOf U) *) \ {{}} is non empty non trivial functional non finite finite-membered FinSequence-membered V165() V166() Element of bool ((AllSymbolsOf U) *)
bool ((AllSymbolsOf U) *) is non empty non trivial non finite V166() set
((AllSymbolsOf U) *) typed\ {{}} is functional finite-membered FinSequence-membered Element of bool ((AllSymbolsOf U) *)
(((AllSymbolsOf U) *) \ {{}}) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() Element of bool (((AllSymbolsOf U) *) *)
((AllSymbolsOf U) *) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of (AllSymbolsOf U) *
bool (((AllSymbolsOf U) *) *) is non empty non trivial non finite V166() set
[:((((AllSymbolsOf U) *) \ {{}}) *),(((AllSymbolsOf U) *) \ {{}}):] is non empty non trivial Relation-like non finite V166() set
bool [:((((AllSymbolsOf U) *) \ {{}}) *),(((AllSymbolsOf U) *) \ {{}}):] is non empty non trivial non finite V166() set
u is Element of AllSymbolsOf U
AllSymbolsOf U is non empty non trivial non finite V166() set
(AllSymbolsOf U) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of AllSymbolsOf U
((AllSymbolsOf U) *) \ {{}} is non empty non trivial functional non finite finite-membered FinSequence-membered V165() V166() Element of bool ((AllSymbolsOf U) *)
bool ((AllSymbolsOf U) *) is non empty non trivial non finite V166() set
((AllSymbolsOf U) *) typed\ {{}} is functional finite-membered FinSequence-membered Element of bool ((AllSymbolsOf U) *)
l is non empty Relation-like non empty-yielding (((AllSymbolsOf U) *) \ {{}}) * -defined ((AllSymbolsOf U) *) \ {{}} -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding Element of bool [:((((AllSymbolsOf U) *) \ {{}}) *),(((AllSymbolsOf U) *) \ {{}}):]
II is Relation-like NAT -defined ((AllSymbolsOf U) *) \ {{}} -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V164() FinSequence-yielding finite-support Element of (((AllSymbolsOf U) *) \ {{}}) *
l . II is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support Element of ((AllSymbolsOf U) *) \ {{}}
(U,u,II) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support Element of ((AllSymbolsOf U) *) \ {{}}
<*u*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like finite-support Element of ((AllSymbolsOf U) *) \ {{}}
[1,u] is non empty set
{[1,u]} is non empty trivial Relation-like Function-like constant finite 1 -element V165() V166() finite-support set
U -multiCat is non empty Relation-like ((AllSymbolsOf U) *) * -defined (AllSymbolsOf U) * -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding Element of bool [:(((AllSymbolsOf U) *) *),((AllSymbolsOf U) *):]
((AllSymbolsOf U) *) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of (AllSymbolsOf U) *
[:(((AllSymbolsOf U) *) *),((AllSymbolsOf U) *):] is non empty non trivial Relation-like non finite V166() set
bool [:(((AllSymbolsOf U) *) *),((AllSymbolsOf U) *):] is non empty non trivial non finite V166() set
(AllSymbolsOf U) -multiCat is non empty Relation-like ((AllSymbolsOf U) *) * -defined (AllSymbolsOf U) * -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding Element of bool [:(((AllSymbolsOf U) *) *),((AllSymbolsOf U) *):]
(AllSymbolsOf U) -concatenation is non empty Relation-like [:((AllSymbolsOf U) *),((AllSymbolsOf U) *):] -defined (AllSymbolsOf U) * -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding V233((AllSymbolsOf U) * ) Element of bool [:[:((AllSymbolsOf U) *),((AllSymbolsOf U) *):],((AllSymbolsOf U) *):]
[:((AllSymbolsOf U) *),((AllSymbolsOf U) *):] is non empty non trivial Relation-like non finite V166() set
[:[:((AllSymbolsOf U) *),((AllSymbolsOf U) *):],((AllSymbolsOf U) *):] is non empty non trivial Relation-like non finite V166() set
bool [:[:((AllSymbolsOf U) *),((AllSymbolsOf U) *):],((AllSymbolsOf U) *):] is non empty non trivial non finite V166() set
MultPlace ((AllSymbolsOf U) -concatenation) is non empty Relation-like (((AllSymbolsOf U) *) *) \ {{}} -defined (AllSymbolsOf U) * -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding Element of bool [:((((AllSymbolsOf U) *) *) \ {{}}),((AllSymbolsOf U) *):]
(((AllSymbolsOf U) *) *) \ {{}} is non empty non trivial functional non finite finite-membered FinSequence-membered V165() V166() Element of bool (((AllSymbolsOf U) *) *)
bool (((AllSymbolsOf U) *) *) is non empty non trivial non finite V166() set
(((AllSymbolsOf U) *) *) typed\ {{}} is functional finite-membered FinSequence-membered Element of bool (((AllSymbolsOf U) *) *)
[:((((AllSymbolsOf U) *) *) \ {{}}),((AllSymbolsOf U) *):] is non empty non trivial Relation-like non finite V166() set
bool [:((((AllSymbolsOf U) *) *) \ {{}}),((AllSymbolsOf U) *):] is non empty non trivial non finite V166() set
({} .--> {}) +* (MultPlace ((AllSymbolsOf U) -concatenation)) is non empty Relation-like Function-like Function-yielding V164() set
(U -multiCat) . II is Relation-like NAT -defined AllSymbolsOf U -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (AllSymbolsOf U) *
<*u*> ^ ((U -multiCat) . II) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
l is non empty Relation-like non empty-yielding (((AllSymbolsOf U) *) \ {{}}) * -defined ((AllSymbolsOf U) *) \ {{}} -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding Element of bool [:((((AllSymbolsOf U) *) \ {{}}) *),(((AllSymbolsOf U) *) \ {{}}):]
II is non empty Relation-like non empty-yielding (((AllSymbolsOf U) *) \ {{}}) * -defined ((AllSymbolsOf U) *) \ {{}} -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding Element of bool [:((((AllSymbolsOf U) *) \ {{}}) *),(((AllSymbolsOf U) *) \ {{}}):]
E is Relation-like NAT -defined ((AllSymbolsOf U) *) \ {{}} -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V164() FinSequence-yielding finite-support Element of (((AllSymbolsOf U) *) \ {{}}) *
l . E is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support Element of ((AllSymbolsOf U) *) \ {{}}
(U,u,E) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support Element of ((AllSymbolsOf U) *) \ {{}}
AllSymbolsOf U is non empty non trivial non finite V166() set
(AllSymbolsOf U) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of AllSymbolsOf U
((AllSymbolsOf U) *) \ {{}} is non empty non trivial functional non finite finite-membered FinSequence-membered V165() V166() Element of bool ((AllSymbolsOf U) *)
bool ((AllSymbolsOf U) *) is non empty non trivial non finite V166() set
((AllSymbolsOf U) *) typed\ {{}} is functional finite-membered FinSequence-membered Element of bool ((AllSymbolsOf U) *)
<*u*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like finite-support Element of ((AllSymbolsOf U) *) \ {{}}
[1,u] is non empty set
{[1,u]} is non empty trivial Relation-like Function-like constant finite 1 -element V165() V166() finite-support set
U -multiCat is non empty Relation-like ((AllSymbolsOf U) *) * -defined (AllSymbolsOf U) * -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding Element of bool [:(((AllSymbolsOf U) *) *),((AllSymbolsOf U) *):]
((AllSymbolsOf U) *) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of (AllSymbolsOf U) *
[:(((AllSymbolsOf U) *) *),((AllSymbolsOf U) *):] is non empty non trivial Relation-like non finite V166() set
bool [:(((AllSymbolsOf U) *) *),((AllSymbolsOf U) *):] is non empty non trivial non finite V166() set
(AllSymbolsOf U) -multiCat is non empty Relation-like ((AllSymbolsOf U) *) * -defined (AllSymbolsOf U) * -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding Element of bool [:(((AllSymbolsOf U) *) *),((AllSymbolsOf U) *):]
(AllSymbolsOf U) -concatenation is non empty Relation-like [:((AllSymbolsOf U) *),((AllSymbolsOf U) *):] -defined (AllSymbolsOf U) * -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding V233((AllSymbolsOf U) * ) Element of bool [:[:((AllSymbolsOf U) *),((AllSymbolsOf U) *):],((AllSymbolsOf U) *):]
[:((AllSymbolsOf U) *),((AllSymbolsOf U) *):] is non empty non trivial Relation-like non finite V166() set
[:[:((AllSymbolsOf U) *),((AllSymbolsOf U) *):],((AllSymbolsOf U) *):] is non empty non trivial Relation-like non finite V166() set
bool [:[:((AllSymbolsOf U) *),((AllSymbolsOf U) *):],((AllSymbolsOf U) *):] is non empty non trivial non finite V166() set
MultPlace ((AllSymbolsOf U) -concatenation) is non empty Relation-like (((AllSymbolsOf U) *) *) \ {{}} -defined (AllSymbolsOf U) * -valued Function-like total quasi_total Function-yielding V164() FinSequence-yielding Element of bool [:((((AllSymbolsOf U) *) *) \ {{}}),((AllSymbolsOf U) *):]
(((AllSymbolsOf U) *) *) \ {{}} is non empty non trivial functional non finite finite-membered FinSequence-membered V165() V166() Element of bool (((AllSymbolsOf U) *) *)
bool (((AllSymbolsOf U) *) *) is non empty non trivial non finite V166() set
(((AllSymbolsOf U) *) *) typed\ {{}} is functional finite-membered FinSequence-membered Element of bool (((AllSymbolsOf U) *) *)
[:((((AllSymbolsOf U) *) *) \ {{}}),((AllSymbolsOf U) *):] is non empty non trivial Relation-like non finite V166() set
bool [:((((AllSymbolsOf U) *) *) \ {{}}),((AllSymbolsOf U) *):] is non empty non trivial non finite V166() set
({} .--> {}) +* (MultPlace ((AllSymbolsOf U) -concatenation)) is non empty Relation-like Function-like Function-yielding V164() set
(U -multiCat) . E is Relation-like NAT -defined AllSymbolsOf U -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (AllSymbolsOf U) *
<*u*> ^ ((U -multiCat) . E) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
II . E is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support Element of ((AllSymbolsOf U) *) \ {{}}
U is V51() V53() eligible Language-like
AllSymbolsOf U is non empty non trivial non finite V166() set
the U1 of U is set
AllTermsOf U is non empty functional finite-membered FinSequence-membered V165() V166() AllSymbolsOf U -prefix U -prefix Element of K335((((AllSymbolsOf U) *) \ {{}}))
AllSymbolsOf U is non empty non trivial non finite V166() set
(AllSymbolsOf U) * is non empty non trivial functional non finite finite-membered FinSequence-membered V166() FinSequenceSet of AllSymbolsOf U
((AllSymbolsOf U) *) \ {{}} is non empty non trivial functional non finite finite-membered FinSequence-membered V165() V166() Element of bool ((