REAL is non empty non trivial non finite V167() set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V167() Element of bool REAL
bool REAL is non empty non trivial non finite V167() set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V167() set
bool omega is non empty non trivial non finite V167() set
K135() is set
bool NAT is non empty non trivial non finite V167() set
COMPLEX is non empty non trivial non finite V167() set
RAT is non empty non trivial non finite V167() set
INT is non empty non trivial non finite V167() 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 V25() cardinal {} -element complex ext-real non positive non negative V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V164() V167() V192() V198() V199() set
{{}} is non empty trivial functional finite V25() 1 -element V167() 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 V25() 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 V25() cardinal {} -element complex ext-real non positive non negative V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V164() V167() V192() V198() V199() 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 V25() cardinal {} -element complex ext-real non positive non negative V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V164() V167() V192() V198() V199() set
[:{{}},NAT:] is non empty non trivial Relation-like non finite V167() set
[{},{}] is non empty V34() set
{[{},{}]} is non empty trivial Relation-like Function-like constant finite 1 -element V166() V167() V199() set
[:{{}},NAT:] \ {[{},{}]} is non empty non trivial Relation-like {{}} -defined NAT -valued non finite V167() Element of bool [:{{}},NAT:]
bool [:{{}},NAT:] is non empty non trivial non finite V167() set
[:{{}},NAT:] typed\ {[{},{}]} is Relation-like {{}} -defined NAT -valued Element of bool [:{{}},NAT:]
NAT \/ ([:{{}},NAT:] \ {[{},{}]}) is non empty non trivial non finite V167() set
[:REAL,REAL:] is non empty non trivial Relation-like non finite V167() set
bool [:REAL,REAL:] is non empty non trivial non finite V167() set
K293() is V47() V75() L8()
the U1 of K293() is set
<REAL,+> is V47() L8()
K299() is V47() V75() SubStr of <REAL,+>
<NAT,+> is V47() V75() V97() uniquely-decomposable SubStr of K299()
<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 V25() set
[:1,1:] is non empty Relation-like finite set
bool [:1,1:] is non empty finite V25() set
[:[:1,1:],1:] is non empty Relation-like finite set
bool [:[:1,1:],1:] is non empty finite V25() 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 V25() cardinal {} -element complex ext-real non positive non negative V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V164() V167() V192() V198() V199() Element of NAT
{0,1} is non empty finite V25() set
[:COMPLEX,COMPLEX:] is non empty non trivial Relation-like non finite V167() set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite V167() set
3 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real positive non negative V40() V41() Element of NAT
Seg 1 is non empty trivial finite 1 -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is non empty trivial finite V25() 1 -element V166() V167() Element of bool NAT
- 2 is non empty complex ext-real non positive negative V40() V41() set
X is V51() V53() eligible Language-like
TheNorSymbOf X is set
the U3 of X is Element of the U1 of X
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite V167() set
X is non empty set
X * is non empty non trivial functional non finite V25() FinSequence-membered V167() FinSequenceSet of X
[:(X *),(X *):] is non empty non trivial Relation-like non finite V167() set
X -concatenation is non empty Relation-like [:(X *),(X *):] -defined X * -valued Function-like total quasi_total Function-yielding V164() V198() V201(X * ) Element of bool [:[:(X *),(X *):],(X *):]
[:[:(X *),(X *):],(X *):] is non empty non trivial Relation-like non finite V167() set
bool [:[:(X *),(X *):],(X *):] is non empty non trivial non finite V167() set
1 -tuples_on X is non empty functional V25() FinSequence-membered V166() V167() FinSequenceSet of X
id (1 -tuples_on X) is non empty Relation-like non empty-yielding 1 -tuples_on X -defined 1 -tuples_on X -valued Function-like one-to-one total quasi_total onto bijective V155() V157() V158() V162() Function-yielding V164() V198() Element of bool [:(1 -tuples_on X),(1 -tuples_on X):]
[:(1 -tuples_on X),(1 -tuples_on X):] is non empty Relation-like set
bool [:(1 -tuples_on X),(1 -tuples_on X):] is non empty set
(X -concatenation) .: (id (1 -tuples_on X)) is functional V25() FinSequence-membered Element of bool (X *)
bool (X *) is non empty non trivial non finite V167() set
2 -tuples_on X is non empty functional V25() FinSequence-membered V166() V167() FinSequenceSet of X
chi (((X -concatenation) .: (id (1 -tuples_on X))),(2 -tuples_on X)) is non empty Relation-like 2 -tuples_on X -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:(2 -tuples_on X),BOOLEAN:]
[:(2 -tuples_on X),BOOLEAN:] is non empty Relation-like set
bool [:(2 -tuples_on X),BOOLEAN:] is non empty set
X is set
id X is Relation-like X -defined X -valued Function-like one-to-one total V155() V157() V158() V162() set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
X is V51() V53() eligible Language-like
AllSymbolsOf X is non empty non trivial non finite V167() set
the U1 of X is set
phi is ofAtomicFormula Element of AllSymbolsOf X
ar phi is complex ext-real V40() V41() Element of INT
the adicity of X is non empty Relation-like the U1 of X \ { the U3 of X} -defined INT -valued Function-like total quasi_total Element of bool [:( the U1 of X \ { the U3 of X}),INT:]
the U3 of X is Element of the U1 of X
{ the U3 of X} is non empty trivial finite 1 -element set
the U1 of X \ { the U3 of X} is non empty Element of bool the U1 of X
bool the U1 of X is non empty set
the U1 of X typed\ { the U3 of X} is Element of bool the U1 of X
[:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial Relation-like non finite V167() set
bool [:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial non finite V167() set
the adicity of X . phi is set
abs (ar phi) is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
S is non empty set
(abs (ar phi)) -tuples_on S is non empty functional V25() FinSequence-membered FinSequenceSet of S
[:((abs (ar phi)) -tuples_on S),BOOLEAN:] is non empty Relation-like set
bool [:((abs (ar phi)) -tuples_on S),BOOLEAN:] is non empty set
[:((abs (ar phi)) -tuples_on S),S:] is non empty Relation-like set
bool [:((abs (ar phi)) -tuples_on S),S:] is non empty set
the non empty Relation-like (abs (ar phi)) -tuples_on S -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:((abs (ar phi)) -tuples_on S),BOOLEAN:] is non empty Relation-like (abs (ar phi)) -tuples_on S -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:((abs (ar phi)) -tuples_on S),BOOLEAN:]
the non empty Relation-like (abs (ar phi)) -tuples_on S -defined S -valued Function-like total quasi_total Element of bool [:((abs (ar phi)) -tuples_on S),S:] is non empty Relation-like (abs (ar phi)) -tuples_on S -defined S -valued Function-like total quasi_total Element of bool [:((abs (ar phi)) -tuples_on S),S:]
X is V51() V53() eligible Language-like
AllSymbolsOf X is non empty non trivial non finite V167() set
the U1 of X is set
S is non empty set
phi is ofAtomicFormula Element of AllSymbolsOf X
ar phi is complex ext-real V40() V41() Element of INT
the adicity of X is non empty Relation-like the U1 of X \ { the U3 of X} -defined INT -valued Function-like total quasi_total Element of bool [:( the U1 of X \ { the U3 of X}),INT:]
the U3 of X is Element of the U1 of X
{ the U3 of X} is non empty trivial finite 1 -element set
the U1 of X \ { the U3 of X} is non empty Element of bool the U1 of X
bool the U1 of X is non empty set
the U1 of X typed\ { the U3 of X} is Element of bool the U1 of X
[:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial Relation-like non finite V167() set
bool [:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial non finite V167() set
the adicity of X . phi is set
abs (ar phi) is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
(abs (ar phi)) -tuples_on S is non empty functional V25() FinSequence-membered FinSequenceSet of S
S \/ BOOLEAN is non empty set
[:((abs (ar phi)) -tuples_on S),(S \/ BOOLEAN):] is non empty Relation-like set
bool [:((abs (ar phi)) -tuples_on S),(S \/ BOOLEAN):] is non empty set
I is (X,S,phi)
((abs (ar phi)) -tuples_on S) \/ {} is non empty functional V25() set
bool ((abs (ar phi)) -tuples_on S) is non empty set
bool (S \/ BOOLEAN) is non empty set
phi is functional V25() FinSequence-membered Element of bool ((abs (ar phi)) -tuples_on S)
A is Element of bool (S \/ BOOLEAN)
[:phi,A:] is Relation-like set
bool [:phi,A:] is non empty set
[:phi,A:] is Relation-like (abs (ar phi)) -tuples_on S -defined S \/ BOOLEAN -valued Element of bool [:((abs (ar phi)) -tuples_on S),(S \/ BOOLEAN):]
A2 is Relation-like phi -defined A -valued Function-like quasi_total Element of bool [:phi,A:]
h is Relation-like (abs (ar phi)) -tuples_on S -defined S \/ BOOLEAN -valued Element of bool [:((abs (ar phi)) -tuples_on S),(S \/ BOOLEAN):]
phi is functional V25() FinSequence-membered Element of bool ((abs (ar phi)) -tuples_on S)
A1 is Element of bool (S \/ BOOLEAN)
[:phi,A1:] is Relation-like set
bool [:phi,A1:] is non empty set
[:phi,A1:] is Relation-like (abs (ar phi)) -tuples_on S -defined S \/ BOOLEAN -valued Element of bool [:((abs (ar phi)) -tuples_on S),(S \/ BOOLEAN):]
A2 is Relation-like phi -defined A1 -valued Function-like quasi_total Element of bool [:phi,A1:]
h is Relation-like (abs (ar phi)) -tuples_on S -defined S \/ BOOLEAN -valued Element of bool [:((abs (ar phi)) -tuples_on S),(S \/ BOOLEAN):]
X is V51() V53() eligible Language-like
AllSymbolsOf X is non empty non trivial non finite V167() set
the U1 of X is set
phi is non relational termal own ofAtomicFormula Element of AllSymbolsOf X
ar phi is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of INT
the adicity of X is non empty Relation-like the U1 of X \ { the U3 of X} -defined INT -valued Function-like total quasi_total Element of bool [:( the U1 of X \ { the U3 of X}),INT:]
the U3 of X is Element of the U1 of X
{ the U3 of X} is non empty trivial finite 1 -element set
the U1 of X \ { the U3 of X} is non empty Element of bool the U1 of X
bool the U1 of X is non empty set
the U1 of X typed\ { the U3 of X} is Element of bool the U1 of X
[:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial Relation-like non finite V167() set
bool [:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial non finite V167() set
the adicity of X . phi is set
abs (ar phi) is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
S is non empty set
(abs (ar phi)) -tuples_on S is non empty functional V25() FinSequence-membered FinSequenceSet of S
S \/ BOOLEAN is non empty set
I is non empty Relation-like (abs (ar phi)) -tuples_on S -defined S \/ BOOLEAN -valued Function-like total quasi_total (X,S,phi)
X is V51() V53() eligible Language-like
AllSymbolsOf X is non empty non trivial non finite V167() set
the U1 of X is set
S is Element of AllSymbolsOf X
X is V51() V53() eligible Language-like
AllSymbolsOf X is non empty non trivial non finite V167() set
the U1 of X is set
S is non empty set
S \/ BOOLEAN is non empty set
OwnSymbolsOf X is non empty Element of bool (AllSymbolsOf X)
AllSymbolsOf X is non empty non trivial non finite V167() set
bool (AllSymbolsOf X) is non empty non trivial non finite V167() set
the U2 of X is Element of the U1 of X
the U3 of X is Element of the U1 of X
{ the U2 of X, the U3 of X} is non empty finite set
the U1 of X \ { the U2 of X, the U3 of X} is Element of bool the U1 of X
bool the U1 of X is non empty set
the U1 of X typed\ { the U2 of X, the U3 of X} is Element of bool the U1 of X
I is set
N is own ofAtomicFormula Element of AllSymbolsOf X
ar N is complex ext-real V40() V41() Element of INT
the adicity of X is non empty Relation-like the U1 of X \ { the U3 of X} -defined INT -valued Function-like total quasi_total Element of bool [:( the U1 of X \ { the U3 of X}),INT:]
{ the U3 of X} is non empty trivial finite 1 -element set
the U1 of X \ { the U3 of X} is non empty Element of bool the U1 of X
the U1 of X typed\ { the U3 of X} is Element of bool the U1 of X
[:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial Relation-like non finite V167() set
bool [:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial non finite V167() set
the adicity of X . N is set
abs (ar N) is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
(abs (ar N)) -tuples_on S is non empty functional V25() FinSequence-membered FinSequenceSet of S
the non empty Relation-like (abs (ar N)) -tuples_on S -defined S \/ BOOLEAN -valued Function-like total quasi_total (X,S,N) is non empty Relation-like (abs (ar N)) -tuples_on S -defined S \/ BOOLEAN -valued Function-like total quasi_total (X,S,N)
v1 is non empty Relation-like (abs (ar N)) -tuples_on S -defined S \/ BOOLEAN -valued Function-like total quasi_total (X,S,N)
I is Relation-like Function-like set
proj1 I is set
N is own ofAtomicFormula Element of AllSymbolsOf X
I . N is set
ar N is complex ext-real V40() V41() Element of INT
the adicity of X is non empty Relation-like the U1 of X \ { the U3 of X} -defined INT -valued Function-like total quasi_total Element of bool [:( the U1 of X \ { the U3 of X}),INT:]
{ the U3 of X} is non empty trivial finite 1 -element set
the U1 of X \ { the U3 of X} is non empty Element of bool the U1 of X
the U1 of X typed\ { the U3 of X} is Element of bool the U1 of X
[:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial Relation-like non finite V167() set
bool [:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial non finite V167() set
the adicity of X . N is set
abs (ar N) is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
(abs (ar N)) -tuples_on S is non empty functional V25() FinSequence-membered FinSequenceSet of S
v1 is own ofAtomicFormula Element of AllSymbolsOf X
ar v1 is complex ext-real V40() V41() Element of INT
the adicity of X . v1 is set
abs (ar v1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
(abs (ar v1)) -tuples_on S is non empty functional V25() FinSequence-membered FinSequenceSet of S
X is V51() V53() eligible Language-like
S is non empty set
phi is Relation-like Function-like set
X is V51() V53() eligible Language-like
AllSymbolsOf X is non empty non trivial non finite V167() set
the U1 of X is set
phi is own ofAtomicFormula Element of AllSymbolsOf X
ar phi is complex ext-real V40() V41() Element of INT
the adicity of X is non empty Relation-like the U1 of X \ { the U3 of X} -defined INT -valued Function-like total quasi_total Element of bool [:( the U1 of X \ { the U3 of X}),INT:]
the U3 of X is Element of the U1 of X
{ the U3 of X} is non empty trivial finite 1 -element set
the U1 of X \ { the U3 of X} is non empty Element of bool the U1 of X
bool the U1 of X is non empty set
the U1 of X typed\ { the U3 of X} is Element of bool the U1 of X
[:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial Relation-like non finite V167() set
bool [:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial non finite V167() set
the adicity of X . phi is set
abs (ar phi) is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
S is non empty set
(abs (ar phi)) -tuples_on S is non empty functional V25() FinSequence-membered FinSequenceSet of S
S \/ BOOLEAN is non empty set
I is non empty Relation-like (abs (ar phi)) -tuples_on S -defined S \/ BOOLEAN -valued Function-like total quasi_total (X,S,phi)
X is V51() V53() eligible Language-like
OwnSymbolsOf X is non empty Element of bool (AllSymbolsOf X)
AllSymbolsOf X is non empty non trivial non finite V167() set
the U1 of X is set
bool (AllSymbolsOf X) is non empty non trivial non finite V167() set
the U2 of X is Element of the U1 of X
the U3 of X is Element of the U1 of X
{ the U2 of X, the U3 of X} is non empty finite set
the U1 of X \ { the U2 of X, the U3 of X} is Element of bool the U1 of X
bool the U1 of X is non empty set
the U1 of X typed\ { the U2 of X, the U3 of X} is Element of bool the U1 of X
S is non empty set
AllSymbolsOf X is non empty non trivial non finite V167() set
AtomicFormulaSymbolsOf X is non empty Element of bool (AllSymbolsOf X)
TheNorSymbOf X is set
{(TheNorSymbOf X)} is non empty trivial finite 1 -element set
(AllSymbolsOf X) \ {(TheNorSymbOf X)} is non empty non trivial non finite V167() Element of bool (AllSymbolsOf X)
bool (AllSymbolsOf X) is non empty non trivial non finite V167() set
(AllSymbolsOf X) typed\ {(TheNorSymbOf X)} is Element of bool (AllSymbolsOf X)
v1 is Relation-like Function-like (X,S)
proj1 v1 is set
psi is set
phi is own ofAtomicFormula Element of AllSymbolsOf X
v1 . phi is set
X is V51() V53() eligible Language-like
OwnSymbolsOf X is non empty Element of bool (AllSymbolsOf X)
AllSymbolsOf X is non empty non trivial non finite V167() set
the U1 of X is set
bool (AllSymbolsOf X) is non empty non trivial non finite V167() set
the U2 of X is Element of the U1 of X
the U3 of X is Element of the U1 of X
{ the U2 of X, the U3 of X} is non empty finite set
the U1 of X \ { the U2 of X, the U3 of X} is Element of bool the U1 of X
bool the U1 of X is non empty set
the U1 of X typed\ { the U2 of X, the U3 of X} is Element of bool the U1 of X
S is non empty set
phi is Relation-like Function-like set
proj1 phi is set
X is V51() V53() eligible Language-like
S is non empty set
OwnSymbolsOf X is non empty Element of bool (AllSymbolsOf X)
AllSymbolsOf X is non empty non trivial non finite V167() set
the U1 of X is set
bool (AllSymbolsOf X) is non empty non trivial non finite V167() set
the U2 of X is Element of the U1 of X
the U3 of X is Element of the U1 of X
{ the U2 of X, the U3 of X} is non empty finite set
the U1 of X \ { the U2 of X, the U3 of X} is Element of bool the U1 of X
bool the U1 of X is non empty set
the U1 of X typed\ { the U2 of X, the U3 of X} is Element of bool the U1 of X
AllSymbolsOf X is non empty non trivial non finite V167() set
the Relation-like Function-like (X,S) is Relation-like Function-like (X,S)
the Relation-like Function-like (X,S) | (OwnSymbolsOf X) is Relation-like OwnSymbolsOf X -defined Function-like set
v1 is Relation-like Function-like set
proj1 v1 is set
proj1 the Relation-like Function-like (X,S) is set
(OwnSymbolsOf X) /\ (proj1 the Relation-like Function-like (X,S)) is Element of bool (AllSymbolsOf X)
(OwnSymbolsOf X) typed/\ (proj1 the Relation-like Function-like (X,S)) is Element of bool (OwnSymbolsOf X)
bool (OwnSymbolsOf X) is non empty set
(OwnSymbolsOf X) /\ (proj1 the Relation-like Function-like (X,S)) is set
(OwnSymbolsOf X) /\typed (proj1 the Relation-like Function-like (X,S)) is Element of bool (proj1 the Relation-like Function-like (X,S))
bool (proj1 the Relation-like Function-like (X,S)) is non empty set
S \/ BOOLEAN is non empty set
psi is own ofAtomicFormula Element of AllSymbolsOf X
v1 . psi is set
ar psi is complex ext-real V40() V41() Element of INT
the adicity of X is non empty Relation-like the U1 of X \ { the U3 of X} -defined INT -valued Function-like total quasi_total Element of bool [:( the U1 of X \ { the U3 of X}),INT:]
{ the U3 of X} is non empty trivial finite 1 -element set
the U1 of X \ { the U3 of X} is non empty Element of bool the U1 of X
the U1 of X typed\ { the U3 of X} is Element of bool the U1 of X
[:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial Relation-like non finite V167() set
bool [:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial non finite V167() set
the adicity of X . psi is set
abs (ar psi) is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
(abs (ar psi)) -tuples_on S is non empty functional V25() FinSequence-membered FinSequenceSet of S
the Relation-like Function-like (X,S) . psi is set
phi is set
psi is Relation-like Function-like (X,S)
A is own ofAtomicFormula Element of AllSymbolsOf X
psi . A is set
psi . phi is set
X is V51() V53() eligible Language-like
S is non empty set
AllSymbolsOf X is non empty non trivial non finite V167() set
the U1 of X is set
phi is Relation-like Function-like Function-yielding V164() (X,S) set
I is own ofAtomicFormula Element of AllSymbolsOf X
phi . I is Relation-like Function-like set
ar I is complex ext-real V40() V41() Element of INT
the adicity of X is non empty Relation-like the U1 of X \ { the U3 of X} -defined INT -valued Function-like total quasi_total Element of bool [:( the U1 of X \ { the U3 of X}),INT:]
the U3 of X is Element of the U1 of X
{ the U3 of X} is non empty trivial finite 1 -element set
the U1 of X \ { the U3 of X} is non empty Element of bool the U1 of X
bool the U1 of X is non empty set
the U1 of X typed\ { the U3 of X} is Element of bool the U1 of X
[:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial Relation-like non finite V167() set
bool [:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial non finite V167() set
the adicity of X . I is set
abs (ar I) is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
(abs (ar I)) -tuples_on S is non empty functional V25() FinSequence-membered FinSequenceSet of S
S \/ BOOLEAN is non empty set
N is Relation-like Function-like (X,S)
N . I is set
X is V51() V53() eligible Language-like
S is non empty set
AllSymbolsOf X is non empty non trivial non finite V167() set
the U1 of X is set
I is own ofAtomicFormula Element of AllSymbolsOf X
ar I is complex ext-real V40() V41() Element of INT
the adicity of X is non empty Relation-like the U1 of X \ { the U3 of X} -defined INT -valued Function-like total quasi_total Element of bool [:( the U1 of X \ { the U3 of X}),INT:]
the U3 of X is Element of the U1 of X
{ the U3 of X} is non empty trivial finite 1 -element set
the U1 of X \ { the U3 of X} is non empty Element of bool the U1 of X
bool the U1 of X is non empty set
the U1 of X typed\ { the U3 of X} is Element of bool the U1 of X
[:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial Relation-like non finite V167() set
bool [:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial non finite V167() set
the adicity of X . I is set
abs (ar I) is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
(abs (ar I)) -tuples_on S is non empty functional V25() FinSequence-membered FinSequenceSet of S
S \/ BOOLEAN is non empty set
phi is Relation-like Function-like Function-yielding V164() (X,S) set
N is non empty Relation-like (abs (ar I)) -tuples_on S -defined S \/ BOOLEAN -valued Function-like total quasi_total (X,S,I)
I .--> N is trivial Relation-like AllSymbolsOf X -defined {I} -defined bool [:((abs (ar I)) -tuples_on S),(S \/ BOOLEAN):] -valued Function-like one-to-one constant finite Function-yielding V164() V199() set
{I} is non empty trivial finite 1 -element set
[:((abs (ar I)) -tuples_on S),(S \/ BOOLEAN):] is non empty Relation-like set
bool [:((abs (ar I)) -tuples_on S),(S \/ BOOLEAN):] is non empty set
{I} --> N is non empty Relation-like non-empty non empty-yielding {I} -defined {N} -valued bool [:((abs (ar I)) -tuples_on S),(S \/ BOOLEAN):] -valued Function-like constant finite total quasi_total Function-yielding V164() V199() Element of bool [:{I},{N}:]
{N} is non empty trivial functional finite 1 -element V166() V167() set
[:{I},{N}:] is non empty Relation-like finite set
bool [:{I},{N}:] is non empty finite V25() set
phi +* (I .--> N) is Relation-like Function-like Function-yielding V164() set
OwnSymbolsOf X is non empty Element of bool (AllSymbolsOf X)
AllSymbolsOf X is non empty non trivial non finite V167() set
bool (AllSymbolsOf X) is non empty non trivial non finite V167() set
the U2 of X is Element of the U1 of X
{ the U2 of X, the U3 of X} is non empty finite set
the U1 of X \ { the U2 of X, the U3 of X} is Element of bool the U1 of X
the U1 of X typed\ { the U2 of X, the U3 of X} is Element of bool the U1 of X
proj1 phi is set
dom (I .--> N) is trivial finite Element of bool {I}
bool {I} is non empty finite V25() set
(proj1 phi) \/ (dom (I .--> N)) is set
A1 is own ofAtomicFormula Element of AllSymbolsOf X
(phi +* (I .--> N)) . A1 is Relation-like Function-like set
(I .--> N) . A1 is Relation-like Function-like set
ar A1 is complex ext-real V40() V41() Element of INT
the adicity of X . A1 is set
abs (ar A1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
(abs (ar A1)) -tuples_on S is non empty functional V25() FinSequence-membered FinSequenceSet of S
(phi +* (I .--> N)) . A1 is Relation-like Function-like set
A is Relation-like Function-like (X,S)
A . A1 is set
ar A1 is complex ext-real V40() V41() Element of INT
the adicity of X . A1 is set
abs (ar A1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
(abs (ar A1)) -tuples_on S is non empty functional V25() FinSequence-membered FinSequenceSet of S
X is Relation-like Function-like set
S is set
phi is set
{} .--> phi is trivial Relation-like {{}} -defined Function-like one-to-one constant finite V199() set
{{}} --> phi is non empty Relation-like {{}} -defined {phi} -valued Function-like constant finite total quasi_total V199() Element of bool [:{{}},{phi}:]
{phi} is non empty trivial finite 1 -element set
[:{{}},{phi}:] is non empty Relation-like finite set
bool [:{{}},{phi}:] is non empty finite V25() set
S .--> ({} .--> phi) is trivial Relation-like {S} -defined Function-like one-to-one constant finite Function-yielding V164() V199() set
{S} is non empty trivial finite 1 -element set
{S} --> ({} .--> phi) is non empty Relation-like {S} -defined {({} .--> phi)} -valued Function-like constant finite total quasi_total Function-yielding V164() V199() Element of bool [:{S},{({} .--> phi)}:]
{({} .--> phi)} is non empty trivial functional finite V25() 1 -element set
[:{S},{({} .--> phi)}:] is non empty Relation-like finite set
bool [:{S},{({} .--> phi)}:] is non empty finite V25() set
X +* (S .--> ({} .--> phi)) is Relation-like Function-like set
X is V51() V53() eligible Language-like
S is non empty set
AllSymbolsOf X is non empty non trivial non finite V167() set
the U1 of X is set
phi is Relation-like Function-like Function-yielding V164() (X,S) set
I is literal non operational non relational termal own ofAtomicFormula Element of AllSymbolsOf X
N is Element of S
(phi,I,N) is Relation-like Function-like set
{} .--> N is trivial Relation-like {{}} -defined S -valued Function-like one-to-one constant finite V199() set
{{}} --> N is non empty Relation-like {{}} -defined S -valued {N} -valued Function-like constant finite total quasi_total V199() Element of bool [:{{}},{N}:]
{N} is non empty trivial finite 1 -element set
[:{{}},{N}:] is non empty Relation-like finite set
bool [:{{}},{N}:] is non empty finite V25() set
I .--> ({} .--> N) is trivial Relation-like AllSymbolsOf X -defined {I} -defined Function-like one-to-one constant finite Function-yielding V164() V199() set
{I} is non empty trivial finite 1 -element set
{I} --> ({} .--> N) is non empty Relation-like {I} -defined {({} .--> N)} -valued Function-like constant finite total quasi_total Function-yielding V164() V199() Element of bool [:{I},{({} .--> N)}:]
{({} .--> N)} is non empty trivial functional finite V25() 1 -element set
[:{I},{({} .--> N)}:] is non empty Relation-like finite set
bool [:{I},{({} .--> N)}:] is non empty finite V25() set
phi +* (I .--> ({} .--> N)) is Relation-like Function-like Function-yielding V164() set
ar I 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 V25() cardinal {} -element complex ext-real non positive non negative V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V164() V167() V192() V198() V199() Element of INT
the adicity of X is non empty Relation-like the U1 of X \ { the U3 of X} -defined INT -valued Function-like total quasi_total Element of bool [:( the U1 of X \ { the U3 of X}),INT:]
the U3 of X is Element of the U1 of X
{ the U3 of X} is non empty trivial finite 1 -element set
the U1 of X \ { the U3 of X} is non empty Element of bool the U1 of X
bool the U1 of X is non empty set
the U1 of X typed\ { the U3 of X} is Element of bool the U1 of X
[:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial Relation-like non finite V167() set
bool [:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial non finite V167() set
the adicity of X . I is set
abs (ar I) 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 V25() cardinal {} -element complex ext-real non positive non negative V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V164() V167() V192() V198() V199() Element of NAT
0 -tuples_on S is non empty functional V25() FinSequence-membered V167() FinSequenceSet of S
(abs (ar I)) -tuples_on S is non empty functional V25() FinSequence-membered V167() FinSequenceSet of S
[:((abs (ar I)) -tuples_on S),S:] is non empty Relation-like set
bool [:((abs (ar I)) -tuples_on S),S:] is non empty set
{{}} --> N is non empty Relation-like {{}} -defined S -valued Function-like constant finite total quasi_total V199() Element of bool [:{{}},S:]
[:{{}},S:] is non empty Relation-like set
bool [:{{}},S:] is non empty set
S \/ BOOLEAN is non empty set
phi is non empty Relation-like (abs (ar I)) -tuples_on S -defined S -valued Function-like total quasi_total Element of bool [:((abs (ar I)) -tuples_on S),S:]
A is non empty Relation-like (abs (ar I)) -tuples_on S -defined S \/ BOOLEAN -valued Function-like total quasi_total (X,S,I)
I .--> A is trivial Relation-like AllSymbolsOf X -defined {I} -defined bool [:((abs (ar I)) -tuples_on S),(S \/ BOOLEAN):] -valued Function-like one-to-one constant finite Function-yielding V164() V199() set
[:((abs (ar I)) -tuples_on S),(S \/ BOOLEAN):] is non empty Relation-like set
bool [:((abs (ar I)) -tuples_on S),(S \/ BOOLEAN):] is non empty set
{I} --> A is non empty Relation-like non-empty non empty-yielding {I} -defined {A} -valued bool [:((abs (ar I)) -tuples_on S),(S \/ BOOLEAN):] -valued Function-like constant finite total quasi_total Function-yielding V164() V199() Element of bool [:{I},{A}:]
{A} is non empty trivial functional finite 1 -element V166() V167() set
[:{I},{A}:] is non empty Relation-like finite set
bool [:{I},{A}:] is non empty finite V25() set
phi +* (I .--> A) is Relation-like Function-like Function-yielding V164() (X,S) set
X is V51() V53() eligible Language-like
AllSymbolsOf X is non empty non trivial non finite V167() set
the U1 of X is set
S is non empty set
X is set
phi is non empty set
Funcs (X,phi) is non empty functional FUNCTION_DOMAIN of X,phi
[:S,(Funcs (X,phi)):] is non empty Relation-like set
bool [:S,(Funcs (X,phi)):] is non empty set
I is non empty Relation-like S -defined Funcs (X,phi) -valued Function-like total quasi_total Function-yielding V164() Element of bool [:S,(Funcs (X,phi)):]
X is non empty set
S is non empty set
phi is non empty set
Funcs (S,phi) is non empty functional FUNCTION_DOMAIN of S,phi
[:X,(Funcs (S,phi)):] is non empty Relation-like set
bool [:X,(Funcs (S,phi)):] is non empty set
the non empty Relation-like X -defined Funcs (S,phi) -valued Function-like total quasi_total Function-yielding V164() Element of bool [:X,(Funcs (S,phi)):] is non empty Relation-like X -defined Funcs (S,phi) -valued Function-like total quasi_total Function-yielding V164() Element of bool [:X,(Funcs (S,phi)):]
X is Relation-like Function-like Function-yielding V164() set
proj1 X is set
S is Relation-like Function-like set
phi is Relation-like Function-like set
proj1 phi is set
I is set
phi . I is set
X . I is Relation-like Function-like set
S (*) (X . I) is Relation-like Function-like set
phi is Relation-like Function-like set
proj1 phi is set
I is Relation-like Function-like set
proj1 I is set
N is set
phi . N is set
X . N is Relation-like Function-like set
S (*) (X . N) is Relation-like Function-like set
I . N is set
X 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 V25() cardinal {} -element complex ext-real non positive non negative V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V164() V167() V192() V198() V199() set
S is Relation-like Function-like set
(X,S) is Relation-like Function-like set
proj1 (X,S) is set
dom X 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 proper finite finite-yielding V25() cardinal {} -element complex ext-real non positive non negative V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V164() V167() V192() V198() V199() Element of bool NAT
X is Relation-like Function-like Function-yielding V164() set
proj1 X is set
S is Relation-like Function-like set
proj1 S is set
(proj1 X) /\ (proj1 S) is set
(proj1 X) typed/\ (proj1 S) is Element of bool (proj1 X)
bool (proj1 X) is non empty set
(proj1 X) /\typed (proj1 S) is Element of bool (proj1 S)
bool (proj1 S) is non empty set
I is Relation-like Function-like set
proj1 I is set
N is set
I . N is set
X . N is Relation-like Function-like set
S . N is set
(X . N) . (S . N) is set
I is Relation-like Function-like set
proj1 I is set
N is Relation-like Function-like set
proj1 N is set
v1 is set
I . v1 is set
X . v1 is Relation-like Function-like set
S . v1 is set
(X . v1) . (S . v1) is set
N . v1 is set
X is Relation-like Function-like Function-yielding V164() set
S 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 V25() cardinal {} -element complex ext-real non positive non negative V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V164() V167() V192() V198() V199() set
(X,S) is Relation-like Function-like set
proj1 (X,S) is set
proj1 X is set
dom S 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 proper finite finite-yielding V25() cardinal {} -element complex ext-real non positive non negative V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V164() V167() V192() V198() V199() Element of bool NAT
(proj1 X) /\ (dom S) is Relation-like finite Element of bool NAT
(proj1 X) typed/\ (dom S) is Element of bool (proj1 X)
bool (proj1 X) is non empty set
(proj1 X) /\ (dom S) is Relation-like finite set
(proj1 X) /\typed (dom S) 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 non proper finite finite-yielding V25() cardinal {} -element complex ext-real non positive non negative V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V164() V167() V192() V198() V199() Element of bool (dom S)
bool (dom S) is non empty finite V25() set
X is functional V25() FinSequence-membered set
S is Relation-like Function-like set
S is non empty set
X is non empty set
[:S,X:] is non empty Relation-like set
bool [:S,X:] is non empty set
phi is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V199() set
I is non empty Relation-like S -defined X -valued Function-like total quasi_total Element of bool [:S,X:]
I (*) phi is Relation-like NAT -defined X -valued Function-like finite FinSequence-like FinSubsequence-like V199() set
len phi is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
N is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like V199() FinSequence of S
I * N is Relation-like NAT -defined X -valued Function-like finite FinSequence-like FinSubsequence-like V199() FinSequence of X
len (I * N) is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
len N is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
v1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V199() set
X is non empty set
S is non empty set
[:X,S:] is non empty Relation-like set
bool [:X,S:] is non empty set
I is Relation-like NAT -defined X -valued Function-like finite FinSequence-like FinSubsequence-like V199() set
phi is non empty Relation-like X -defined S -valued Function-like total quasi_total Element of bool [:X,S:]
phi (*) I is Relation-like NAT -defined S -valued Function-like finite len I -element FinSequence-like FinSubsequence-like V199() set
len I is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
S is non empty set
phi is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() set
X is non empty set
[:S,X:] is non empty Relation-like set
bool [:S,X:] is non empty set
I is Relation-like NAT -defined S -valued Function-like finite phi -element FinSequence-like FinSubsequence-like V199() set
N is non empty Relation-like S -defined X -valued Function-like total quasi_total Element of bool [:S,X:]
N (*) I is Relation-like NAT -defined X -valued Function-like finite phi -element len I -element FinSequence-like FinSubsequence-like V199() set
len I is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
v1 is Relation-like NAT -defined X -valued Function-like finite FinSequence-like FinSubsequence-like V199() FinSequence of X
S is V51() V53() eligible Language-like
X is non empty set
TermSymbolsOf S is non empty set
the U1 of S is set
the U3 of S is Element of the U1 of S
{ the U3 of S} is non empty trivial finite 1 -element set
the U1 of S \ { the U3 of S} is non empty Element of bool the U1 of S
bool the U1 of S is non empty set
the U1 of S typed\ { the U3 of S} is Element of bool the U1 of S
the adicity of S is non empty Relation-like the U1 of S \ { the U3 of S} -defined INT -valued Function-like total quasi_total Element of bool [:( the U1 of S \ { the U3 of S}),INT:]
[:( the U1 of S \ { the U3 of S}),INT:] is non empty non trivial Relation-like non finite V167() set
bool [:( the U1 of S \ { the U3 of S}),INT:] is non empty non trivial non finite V167() set
the adicity of S " NAT is Element of bool ( the U1 of S \ { the U3 of S})
bool ( the U1 of S \ { the U3 of S}) is non empty set
AllSymbolsOf S is non empty non trivial non finite V167() set
(AllSymbolsOf S) * is non empty non trivial functional non finite V25() FinSequence-membered V167() FinSequenceSet of AllSymbolsOf S
((AllSymbolsOf S) *) \ {{}} is non empty non trivial functional non finite V25() FinSequence-membered V166() V167() Element of bool ((AllSymbolsOf S) *)
bool ((AllSymbolsOf S) *) is non empty non trivial non finite V167() set
((AllSymbolsOf S) *) typed\ {{}} is functional V25() FinSequence-membered Element of bool ((AllSymbolsOf S) *)
I is non empty Relation-like NAT -defined TermSymbolsOf S -valued Function-like finite FinSequence-like FinSubsequence-like V199() termal Element of ((AllSymbolsOf S) *) \ {{}}
ar I is complex ext-real V40() V41() Element of INT
S -firstChar is non empty Relation-like ((AllSymbolsOf S) *) \ {{}} -defined AllSymbolsOf S -valued Function-like total quasi_total Element of bool [:(((AllSymbolsOf S) *) \ {{}}),(AllSymbolsOf S):]
[:(((AllSymbolsOf S) *) \ {{}}),(AllSymbolsOf S):] is non empty non trivial Relation-like non finite V167() set
bool [:(((AllSymbolsOf S) *) \ {{}}),(AllSymbolsOf S):] is non empty non trivial non finite V167() set
(AllSymbolsOf S) -firstChar is non empty Relation-like ((AllSymbolsOf S) *) \ {{}} -defined AllSymbolsOf S -valued Function-like total quasi_total Element of bool [:(((AllSymbolsOf S) *) \ {{}}),(AllSymbolsOf S):]
(AllSymbolsOf S) -pr1 is non empty Relation-like [:(AllSymbolsOf S),(AllSymbolsOf S):] -defined AllSymbolsOf S -valued Function-like total quasi_total V201( AllSymbolsOf S) Element of bool [:[:(AllSymbolsOf S),(AllSymbolsOf S):],(AllSymbolsOf S):]
[:(AllSymbolsOf S),(AllSymbolsOf S):] is non empty non trivial Relation-like non finite V167() set
[:[:(AllSymbolsOf S),(AllSymbolsOf S):],(AllSymbolsOf S):] is non empty non trivial Relation-like non finite V167() set
bool [:[:(AllSymbolsOf S),(AllSymbolsOf S):],(AllSymbolsOf S):] is non empty non trivial non finite V167() set
K463((AllSymbolsOf S),(AllSymbolsOf S)) is non empty Relation-like [:(AllSymbolsOf S),(AllSymbolsOf S):] -defined AllSymbolsOf S -valued Function-like total quasi_total Element of bool [:[:(AllSymbolsOf S),(AllSymbolsOf S):],(AllSymbolsOf S):]
MultPlace ((AllSymbolsOf S) -pr1) is non empty Relation-like ((AllSymbolsOf S) *) \ {{}} -defined AllSymbolsOf S -valued Function-like total quasi_total Element of bool [:(((AllSymbolsOf S) *) \ {{}}),(AllSymbolsOf S):]
(S -firstChar) . I is non relational termal own ofAtomicFormula Element of AllSymbolsOf S
ar ((S -firstChar) . I) is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of INT
the adicity of S . ((S -firstChar) . I) is set
abs (ar I) is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
(abs (ar I)) -tuples_on X is non empty functional V25() FinSequence-membered FinSequenceSet of X
abs (ar ((S -firstChar) . I)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT
(abs (ar ((S -firstChar) . I))) -tuples_on X is non empty functional V25() FinSequence-membered FinSequenceSet of X
phi is Relation-like Function-like Function-yielding V164() (S,X) set
(S,X,phi,((S -firstChar) . I)) is non empty Relation-like (abs (ar ((S -firstChar) . I))) -tuples_on X -defined X \/ BOOLEAN -valued Function-like total quasi_total (S,X,(S -firstChar) . I)
X \/ BOOLEAN is non empty set
dom (S,X,phi,((S -firstChar) . I)) is non empty functional V25() FinSequence-membered Element of bool ((abs (ar ((S -firstChar) . I))) -tuples_on X)
bool ((abs (ar ((S -firstChar) . I))) -tuples_on X) is non empty set
X is V51() V53() eligible Language-like
TermSymbolsOf X is non empty set
the U1 of X is set
the U3 of X is Element of the U1 of X
{ the U3 of X} is non empty trivial finite 1 -element set
the U1 of X \ { the U3 of X} is non empty Element of bool the U1 of X
bool the U1 of X is non empty set
the U1 of X typed\ { the U3 of X} is Element of bool the U1 of X
the adicity of X is non empty Relation-like the U1 of X \ { the U3 of X} -defined INT -valued Function-like total quasi_total Element of bool [:( the U1 of X \ { the U3 of X}),INT:]
[:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial Relation-like non finite V167() set
bool [:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial non finite V167() set
the adicity of X " NAT is Element of bool ( the U1 of X \ { the U3 of X})
bool ( the U1 of X \ { the U3 of X}) is non empty set
AllSymbolsOf X is non empty non trivial non finite V167() set
(AllSymbolsOf X) * is non empty non trivial functional non finite V25() FinSequence-membered V167() FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V25() FinSequence-membered V166() V167() Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite V167() set
((AllSymbolsOf X) *) typed\ {{}} is functional V25() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
X -firstChar is non empty Relation-like ((AllSymbolsOf X) *) \ {{}} -defined AllSymbolsOf X -valued Function-like total quasi_total Element of bool [:(((AllSymbolsOf X) *) \ {{}}),(AllSymbolsOf X):]
[:(((AllSymbolsOf X) *) \ {{}}),(AllSymbolsOf X):] is non empty non trivial Relation-like non finite V167() set
bool [:(((AllSymbolsOf X) *) \ {{}}),(AllSymbolsOf X):] is non empty non trivial non finite V167() set
(AllSymbolsOf X) -firstChar is non empty Relation-like ((AllSymbolsOf X) *) \ {{}} -defined AllSymbolsOf X -valued Function-like total quasi_total Element of bool [:(((AllSymbolsOf X) *) \ {{}}),(AllSymbolsOf X):]
(AllSymbolsOf X) -pr1 is non empty Relation-like [:(AllSymbolsOf X),(AllSymbolsOf X):] -defined AllSymbolsOf X -valued Function-like total quasi_total V201( AllSymbolsOf X) Element of bool [:[:(AllSymbolsOf X),(AllSymbolsOf X):],(AllSymbolsOf X):]
[:(AllSymbolsOf X),(AllSymbolsOf X):] is non empty non trivial Relation-like non finite V167() set
[:[:(AllSymbolsOf X),(AllSymbolsOf X):],(AllSymbolsOf X):] is non empty non trivial Relation-like non finite V167() set
bool [:[:(AllSymbolsOf X),(AllSymbolsOf X):],(AllSymbolsOf X):] is non empty non trivial non finite V167() set
K463((AllSymbolsOf X),(AllSymbolsOf X)) is non empty Relation-like [:(AllSymbolsOf X),(AllSymbolsOf X):] -defined AllSymbolsOf X -valued Function-like total quasi_total Element of bool [:[:(AllSymbolsOf X),(AllSymbolsOf X):],(AllSymbolsOf X):]
MultPlace ((AllSymbolsOf X) -pr1) is non empty Relation-like ((AllSymbolsOf X) *) \ {{}} -defined AllSymbolsOf X -valued Function-like total quasi_total Element of bool [:(((AllSymbolsOf X) *) \ {{}}),(AllSymbolsOf X):]
S is non empty trivial Relation-like NAT -defined TermSymbolsOf X -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like V199() termal 0 -termal Element of ((AllSymbolsOf X) *) \ {{}}
(X -firstChar) . S is literal non operational non relational termal own ofAtomicFormula Element of AllSymbolsOf X
<*((X -firstChar) . S)*> is non empty trivial Relation-like NAT -defined AllSymbolsOf X -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like V199() FinSequence of AllSymbolsOf X
[1,((X -firstChar) . S)] is non empty V34() set
{[1,((X -firstChar) . S)]} is non empty trivial Relation-like Function-like constant finite 1 -element V166() V167() V199() set
((AllSymbolsOf X) *) * is non empty non trivial functional non finite V25() FinSequence-membered V167() FinSequenceSet of (AllSymbolsOf X) *
X -multiCat is non empty Relation-like ((AllSymbolsOf X) *) * -defined (AllSymbolsOf X) * -valued Function-like total quasi_total Function-yielding V164() V198() Element of bool [:(((AllSymbolsOf X) *) *),((AllSymbolsOf X) *):]
[:(((AllSymbolsOf X) *) *),((AllSymbolsOf X) *):] is non empty non trivial Relation-like non finite V167() set
bool [:(((AllSymbolsOf X) *) *),((AllSymbolsOf X) *):] is non empty non trivial non finite V167() set
(AllSymbolsOf X) -multiCat is non empty Relation-like ((AllSymbolsOf X) *) * -defined (AllSymbolsOf X) * -valued Function-like total quasi_total Function-yielding V164() V198() Element of bool [:(((AllSymbolsOf X) *) *),((AllSymbolsOf X) *):]
{} .--> {} is trivial Relation-like {{}} -defined Function-like one-to-one constant finite Function-yielding V164() V199() set
{{}} --> {} is non empty Relation-like empty-yielding {{}} -defined INT -valued {{}} -valued Function-like constant finite total quasi_total Function-yielding V164() V199() Element of bool [:{{}},{{}}:]
[:{{}},{{}}:] is non empty Relation-like finite set
bool [:{{}},{{}}:] is non empty finite V25() set
(AllSymbolsOf X) -concatenation is non empty Relation-like [:((AllSymbolsOf X) *),((AllSymbolsOf X) *):] -defined (AllSymbolsOf X) * -valued Function-like total quasi_total Function-yielding V164() V198() V201((AllSymbolsOf X) * ) Element of bool [:[:((AllSymbolsOf X) *),((AllSymbolsOf X) *):],((AllSymbolsOf X) *):]
[:((AllSymbolsOf X) *),((AllSymbolsOf X) *):] is non empty non trivial Relation-like non finite V167() set
[:[:((AllSymbolsOf X) *),((AllSymbolsOf X) *):],((AllSymbolsOf X) *):] is non empty non trivial Relation-like non finite V167() set
bool [:[:((AllSymbolsOf X) *),((AllSymbolsOf X) *):],((AllSymbolsOf X) *):] is non empty non trivial non finite V167() set
MultPlace ((AllSymbolsOf X) -concatenation) is non empty Relation-like (((AllSymbolsOf X) *) *) \ {{}} -defined (AllSymbolsOf X) * -valued Function-like total quasi_total Function-yielding V164() V198() Element of bool [:((((AllSymbolsOf X) *) *) \ {{}}),((AllSymbolsOf X) *):]
(((AllSymbolsOf X) *) *) \ {{}} is non empty non trivial functional non finite V25() FinSequence-membered V166() V167() Element of bool (((AllSymbolsOf X) *) *)
bool (((AllSymbolsOf X) *) *) is non empty non trivial non finite V167() set
(((AllSymbolsOf X) *) *) typed\ {{}} is functional V25() FinSequence-membered Element of bool (((AllSymbolsOf X) *) *)
[:((((AllSymbolsOf X) *) *) \ {{}}),((AllSymbolsOf X) *):] is non empty non trivial Relation-like non finite V167() set
bool [:((((AllSymbolsOf X) *) *) \ {{}}),((AllSymbolsOf X) *):] is non empty non trivial non finite V167() set
({} .--> {}) +* (MultPlace ((AllSymbolsOf X) -concatenation)) is non empty Relation-like Function-like Function-yielding V164() set
SubTerms S is empty trivial Relation-like non-empty empty-yielding NAT -defined (proj2 S) * -valued AllTermsOf X -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V25() cardinal {} -element abs (ar S) -element complex ext-real non positive non negative V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V164() V167() V192() V198() V199() Element of (AllTermsOf X) *
proj2 S is non empty trivial finite 1 -element set
(proj2 S) * is non empty non trivial functional non finite V25() FinSequence-membered V167() FinSequenceSet of proj2 S
AllTermsOf X is non empty functional V25() FinSequence-membered AllSymbolsOf X -prefix X -prefix Element of bool ((AllSymbolsOf X) *)
X -termsOfMaxDepth is Relation-like Function-like set
proj2 (X -termsOfMaxDepth) is set
union (proj2 (X -termsOfMaxDepth)) is set
ar S is complex ext-real V40() V41() Element of INT
ar ((X -firstChar) . S) 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 V25() cardinal {} -element complex ext-real non positive non negative V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V164() V167() V192() V198() V199() Element of INT
the adicity of X . ((X -firstChar) . 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
(AllTermsOf X) * is non empty non trivial functional non finite V25() FinSequence-membered V167() Element of bool (((AllSymbolsOf X) *) *)
(X -multiCat) . (SubTerms S) is Relation-like NAT -defined AllSymbolsOf X -valued Function-like finite FinSequence-like FinSubsequence-like V199() Element of (AllSymbolsOf X) *
phi 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 V25() cardinal {} -element complex ext-real non positive non negative V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V164() V167() V192() V198() V199() set
<*((X -firstChar) . S)*> ^ phi is non empty Relation-like NAT -defined Function-like finite 1 + {} -element FinSequence-like FinSubsequence-like V199() set
1 + {} is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real positive non negative V40() V41() set
<*((X -firstChar) . S)*> null phi is Relation-like NAT -defined phi \/ (proj1 <*((X -firstChar) . S)*>) -defined Seg (1 + phi) -defined phi \/ (proj2 <*((X -firstChar) . S)*>) -valued Function-like finite len <*((X -firstChar) . S)*> -element total FinSequence-like FinSubsequence-like V199() set
proj1 <*((X -firstChar) . S)*> is non empty trivial finite 1 -element set
phi \/ (proj1 <*((X -firstChar) . S)*>) is non empty finite set
1 + phi is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real positive non negative V40() V41() set
Seg (1 + phi) is non empty finite 1 + phi -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real non negative V40() V41() Element of NAT : ( 1 <= b1 & b1 <= 1 + phi ) } is set
proj2 <*((X -firstChar) . S)*> is non empty trivial finite 1 -element set
phi \/ (proj2 <*((X -firstChar) . S)*>) is non empty finite set
len <*((X -firstChar) . S)*> is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real positive non negative V40() V41() Element of NAT
<*((X -firstChar) . S)*> \typed/ phi is Relation-like NAT -defined finite Element of bool (<*((X -firstChar) . S)*> \/ phi)
<*((X -firstChar) . S)*> \/ phi is non empty Relation-like NAT -defined finite set
bool (<*((X -firstChar) . S)*> \/ phi) is non empty finite V25() set
phi ^ <*((X -firstChar) . S)*> is non empty Relation-like NAT -defined Function-like finite {} + 1 -element {} + 1 -element FinSequence-like FinSubsequence-like V199() set
{} + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real positive non negative V40() V41() set
{} + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal complex ext-real positive non negative V40() V41() Element of NAT
X is V51() V53() eligible Language-like
AllTermsOf X is non empty functional V25() FinSequence-membered V166() V167() AllSymbolsOf X -prefix X -prefix Element of K365((((AllSymbolsOf X) *) \ {{}}))
AllSymbolsOf X is non empty non trivial non finite V167() set
the U1 of X is set
(AllSymbolsOf X) * is non empty non trivial functional non finite V25() FinSequence-membered V167() FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V25() FinSequence-membered V166() V167() Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite V167() set
((AllSymbolsOf X) *) typed\ {{}} is functional V25() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
bool (((AllSymbolsOf X) *) \ {{}}) is non empty non trivial non finite V167() set
K365((((AllSymbolsOf X) *) \ {{}})) is non empty non trivial non finite V167() Element of bool (bool (((AllSymbolsOf X) *) \ {{}}))
bool (bool (((AllSymbolsOf X) *) \ {{}})) is non empty non trivial non finite V167() set
X -termsOfMaxDepth is Relation-like Function-like set
proj2 (X -termsOfMaxDepth) is set
union (proj2 (X -termsOfMaxDepth)) is set
X -firstChar is non empty Relation-like ((AllSymbolsOf X) *) \ {{}} -defined AllSymbolsOf X -valued Function-like total quasi_total Element of bool [:(((AllSymbolsOf X) *) \ {{}}),(AllSymbolsOf X):]
[:(((AllSymbolsOf X) *) \ {{}}),(AllSymbolsOf X):] is non empty non trivial Relation-like non finite V167() set
bool [:(((AllSymbolsOf X) *) \ {{}}),(AllSymbolsOf X):] is non empty non trivial non finite V167() set
(AllSymbolsOf X) -firstChar is non empty Relation-like ((AllSymbolsOf X) *) \ {{}} -defined AllSymbolsOf X -valued Function-like total quasi_total Element of bool [:(((AllSymbolsOf X) *) \ {{}}),(AllSymbolsOf X):]
(AllSymbolsOf X) -pr1 is non empty Relation-like [:(AllSymbolsOf X),(AllSymbolsOf X):] -defined AllSymbolsOf X -valued Function-like total quasi_total V201( AllSymbolsOf X) Element of bool [:[:(AllSymbolsOf X),(AllSymbolsOf X):],(AllSymbolsOf X):]
[:(AllSymbolsOf X),(AllSymbolsOf X):] is non empty non trivial Relation-like non finite V167() set
[:[:(AllSymbolsOf X),(AllSymbolsOf X):],(AllSymbolsOf X):] is non empty non trivial Relation-like non finite V167() set
bool [:[:(AllSymbolsOf X),(AllSymbolsOf X):],(AllSymbolsOf X):] is non empty non trivial non finite V167() set
K463((AllSymbolsOf X),(AllSymbolsOf X)) is non empty Relation-like [:(AllSymbolsOf X),(AllSymbolsOf X):] -defined AllSymbolsOf X -valued Function-like total quasi_total Element of bool [:[:(AllSymbolsOf X),(AllSymbolsOf X):],(AllSymbolsOf X):]
MultPlace ((AllSymbolsOf X) -pr1) is non empty Relation-like ((AllSymbolsOf X) *) \ {{}} -defined AllSymbolsOf X -valued Function-like total quasi_total Element of bool [:(((AllSymbolsOf X) *) \ {{}}),(AllSymbolsOf X):]
X -subTerms is non empty Relation-like AllTermsOf X -defined (AllTermsOf X) * -valued Function-like total quasi_total Function-yielding V164() V198() Element of bool [:(AllTermsOf X),((AllTermsOf X) *):]
(AllTermsOf X) * is non empty non trivial functional non finite V25() FinSequence-membered V167() Element of bool ((((AllSymbolsOf X) *) \ {{}}) *)
(((AllSymbolsOf X) *) \ {{}}) * is non empty non trivial functional non finite V25() FinSequence-membered V167() FinSequenceSet of ((AllSymbolsOf X) *) \ {{}}
bool ((((AllSymbolsOf X) *) \ {{}}) *) is non empty non trivial non finite V167() set
[:(AllTermsOf X),((AllTermsOf X) *):] is non empty non trivial Relation-like non finite V167() set
bool [:(AllTermsOf X),((AllTermsOf X) *):] is non empty non trivial non finite V167() set
S is non empty set
[:(AllTermsOf X),S:] is non empty Relation-like set
bool [:(AllTermsOf X),S:] is non empty set
Funcs ((AllTermsOf X),S) is non empty functional FUNCTION_DOMAIN of AllTermsOf X,S
phi is Relation-like Function-like Function-yielding V164() (X,S) set
phi (*) (X -firstChar) is Relation-like ((AllSymbolsOf X) *) \ {{}} -defined Function-like Function-yielding V164() set
dom (phi (*) (X -firstChar)) is functional V25() FinSequence-membered V166() Element of bool (((AllSymbolsOf X) *) \ {{}})
AllSymbolsOf X is non empty non trivial non finite V167() set
AtomicTermsOf X is functional V25() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
LettersOf X is non empty non trivial non finite V167() set
the U3 of X is Element of the U1 of X
{ the U3 of X} is non empty trivial finite 1 -element set
the U1 of X \ { the U3 of X} is non empty Element of bool the U1 of X
bool the U1 of X is non empty set
the U1 of X typed\ { the U3 of X} is Element of bool the U1 of X
the adicity of X is non empty Relation-like the U1 of X \ { the U3 of X} -defined INT -valued Function-like total quasi_total Element of bool [:( the U1 of X \ { the U3 of X}),INT:]
[:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial Relation-like non finite V167() set
bool [:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial non finite V167() set
{0} is non empty trivial functional finite V25() 1 -element V167() Element of bool NAT
0 * is non empty functional V25() FinSequence-membered