:: FOMODEL2 semantic presentation

REAL is non empty non trivial non finite V167() set

bool REAL is non empty non trivial non finite 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 non empty trivial functional finite V25() 1 -element V167() set

is non empty non trivial Relation-like non finite V167() set
is non empty V34() set

bool is non empty non trivial non finite V167() set

NAT \/ () is non empty non trivial non finite V167() set
is non empty non trivial Relation-like non finite V167() set
bool 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()

{{},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,1} is non empty finite V25() set
is non empty non trivial Relation-like non finite V167() set
bool is non empty non trivial non finite V167() set

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

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

[:(),():] is non empty Relation-like set
bool [:(),():] is non empty set
() .: (id ()) 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 ((() .: (id ())),()) is non empty Relation-like 2 -tuples_on X -defined BOOLEAN -valued Function-like total quasi_total boolean-valued Element of bool [:(),BOOLEAN:]
[:(),BOOLEAN:] is non empty Relation-like set
bool [:(),BOOLEAN:] is non empty set
X is 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

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

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

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)) -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),():] is non empty Relation-like set
bool [:((abs (ar phi)) -tuples_on S),():] 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 () is non empty set
phi is functional V25() FinSequence-membered Element of bool ((abs (ar phi)) -tuples_on S)
A is Element of bool ()
[: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),():]

h is Relation-like (abs (ar phi)) -tuples_on S -defined S \/ BOOLEAN -valued Element of bool [:((abs (ar phi)) -tuples_on S),():]
phi is functional V25() FinSequence-membered Element of bool ((abs (ar phi)) -tuples_on S)
A1 is Element of bool ()
[: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),():]
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),():]
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

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

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 is non empty non trivial non finite V167() set
bool () 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

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

proj1 I is set

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)) -tuples_on S is non empty functional V25() FinSequence-membered FinSequenceSet of S

ar v1 is complex ext-real V40() V41() Element of INT
the adicity of X . v1 is set

(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

X is V51() V53() eligible Language-like
AllSymbolsOf X is non empty non trivial non finite V167() set
the U1 of X is set

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

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 is non empty non trivial non finite V167() set
the U1 of X is set
bool () 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 ()

{()} is non empty trivial finite 1 -element set
() \ {()} is non empty non trivial non finite V167() Element of bool ()
bool () is non empty non trivial non finite V167() set
() typed\ {()} is Element of bool ()
v1 is Relation-like Function-like (X,S)
proj1 v1 is set
psi is set

v1 . phi is set
X is V51() V53() eligible Language-like
OwnSymbolsOf X is non empty Element of bool ()
AllSymbolsOf X is non empty non trivial non finite V167() set
the U1 of X is set
bool () 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

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 is non empty non trivial non finite V167() set
the U1 of X is set
bool () 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)

proj1 v1 is set
proj1 the Relation-like Function-like (X,S) is set
() /\ (proj1 the Relation-like Function-like (X,S)) is Element of bool ()
() typed/\ (proj1 the Relation-like Function-like (X,S)) is Element of bool ()
bool () is non empty set
() /\ (proj1 the Relation-like Function-like (X,S)) is set
() /\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

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

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

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

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)) -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} is non empty trivial finite 1 -element set
[:((abs (ar I)) -tuples_on S),():] is non empty Relation-like set
bool [:((abs (ar I)) -tuples_on S),():] is non empty set

{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

OwnSymbolsOf X is non empty Element of bool ()
AllSymbolsOf X is non empty non trivial non finite V167() set
bool () 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

(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)) -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)) -tuples_on S is non empty functional V25() FinSequence-membered FinSequenceSet of S

S is set
phi is set

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

N is Element of S
(phi,I,N) is Relation-like Function-like set

{N} is non empty trivial finite 1 -element set
is non empty Relation-like finite set
bool is non empty finite V25() set

{I} is non empty trivial finite 1 -element set

{()} is non empty trivial functional finite V25() 1 -element set
[:{I},{()}:] is non empty Relation-like finite set
bool [:{I},{()}:] is non empty finite V25() set
phi +* (I .--> ()) is Relation-like Function-like Function-yielding V164() set

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

[:,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)

[:((abs (ar I)) -tuples_on S),():] is non empty Relation-like set
bool [:((abs (ar I)) -tuples_on S),():] is non empty set

{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)):]

proj1 X is set

proj1 phi is set
I is set
phi . I is set

S (*) (X . I) is Relation-like Function-like set

proj1 phi is set

proj1 I is set
N is set
phi . N is set

S (*) (X . N) is Relation-like Function-like set
I . N is set

(X,S) is Relation-like Function-like set
proj1 (X,S) is set

proj1 X is set

proj1 S is set
() /\ () is set
() typed/\ () is Element of bool ()
bool () is non empty set
() /\typed () is Element of bool ()
bool () is non empty set

proj1 I is set
N is set
I . N is set

S . N is set
(X . N) . (S . N) is set

proj1 I is set

proj1 N is set
v1 is set
I . v1 is set

S . v1 is set
(X . v1) . (S . v1) is set
N . v1 is set

(X,S) is Relation-like Function-like set
proj1 (X,S) is set
proj1 X is set

() /\ (dom S) is Relation-like finite Element of bool NAT
() typed/\ (dom S) is Element of bool ()
bool () is non empty set
() /\ (dom S) is Relation-like finite set

bool (dom S) is non empty finite V25() 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

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

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

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
() * is non empty non trivial functional non finite V25() FinSequence-membered V167() FinSequenceSet of AllSymbolsOf S
(() *) \ is non empty non trivial functional non finite V25() FinSequence-membered V166() V167() Element of bool (() *)
bool (() *) is non empty non trivial non finite V167() set
(() *) typed\ is functional V25() FinSequence-membered Element of bool (() *)

ar I is complex ext-real V40() V41() Element of INT

[:((() *) \ ),():] is non empty non trivial Relation-like non finite V167() set
bool [:((() *) \ ),():] is non empty non trivial non finite V167() set

[:(),():] is non empty non trivial Relation-like non finite V167() set
[:[:(),():],():] is non empty non trivial Relation-like non finite V167() set
bool [:[:(),():],():] is non empty non trivial non finite V167() set

MultPlace (() -pr1) is non empty Relation-like (() *) \ -defined AllSymbolsOf S -valued Function-like total quasi_total Element of bool [:((() *) \ ),():]
() . I is non relational termal own ofAtomicFormula Element of AllSymbolsOf S

the adicity of S . (() . I) is set

(abs (ar I)) -tuples_on X is non empty functional V25() FinSequence-membered FinSequenceSet of X

(abs (ar (() . 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,(() . I)) is non empty Relation-like (abs (ar (() . I))) -tuples_on X -defined X \/ BOOLEAN -valued Function-like total quasi_total (S,X,() . I)
X \/ BOOLEAN is non empty set
dom (S,X,phi,(() . I)) is non empty functional V25() FinSequence-membered Element of bool ((abs (ar (() . I))) -tuples_on X)
bool ((abs (ar (() . 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
() * is non empty non trivial functional non finite V25() FinSequence-membered V167() FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V25() FinSequence-membered V166() V167() Element of bool (() *)
bool (() *) is non empty non trivial non finite V167() set
(() *) typed\ is functional V25() FinSequence-membered Element of bool (() *)

[:((() *) \ ),():] is non empty non trivial Relation-like non finite V167() set
bool [:((() *) \ ),():] is non empty non trivial non finite V167() set

[:(),():] is non empty non trivial Relation-like non finite V167() set
[:[:(),():],():] is non empty non trivial Relation-like non finite V167() set
bool [:[:(),():],():] is non empty non trivial non finite V167() set

MultPlace (() -pr1) is non empty Relation-like (() *) \ -defined AllSymbolsOf X -valued Function-like total quasi_total Element of bool [:((() *) \ ),():]

[1,(() . S)] is non empty V34() set
{[1,(() . S)]} is non empty trivial Relation-like Function-like constant finite 1 -element V166() V167() V199() set
(() *) * is non empty non trivial functional non finite V25() FinSequence-membered V167() FinSequenceSet of () *
X -multiCat is non empty Relation-like (() *) * -defined () * -valued Function-like total quasi_total Function-yielding V164() V198() Element of bool [:((() *) *),(() *):]
[:((() *) *),(() *):] is non empty non trivial Relation-like non finite V167() set
bool [:((() *) *),(() *):] is non empty non trivial non finite V167() set
() -multiCat is non empty Relation-like (() *) * -defined () * -valued Function-like total quasi_total Function-yielding V164() V198() Element of bool [:((() *) *),(() *):]

bool is non empty finite V25() set
() -concatenation is non empty Relation-like [:(() *),(() *):] -defined () * -valued Function-like total quasi_total Function-yielding V164() V198() V201(() * ) Element of bool [:[:(() *),(() *):],(() *):]
[:(() *),(() *):] is non empty non trivial Relation-like non finite V167() set
[:[:(() *),(() *):],(() *):] is non empty non trivial Relation-like non finite V167() set
bool [:[:(() *),(() *):],(() *):] is non empty non trivial non finite V167() set
MultPlace () is non empty Relation-like ((() *) *) \ -defined () * -valued Function-like total quasi_total Function-yielding V164() V198() Element of bool [:(((() *) *) \ ),(() *):]
((() *) *) \ is non empty non trivial functional non finite V25() FinSequence-membered V166() V167() Element of bool ((() *) *)
bool ((() *) *) is non empty non trivial non finite V167() set
((() *) *) typed\ is functional V25() FinSequence-membered Element of bool ((() *) *)
[:(((() *) *) \ ),(() *):] is non empty non trivial Relation-like non finite V167() set
bool [:(((() *) *) \ ),(() *):] is non empty non trivial non finite V167() set

proj2 S is non empty trivial finite 1 -element set
() * is non empty non trivial functional non finite V25() FinSequence-membered V167() FinSequenceSet of proj2 S

proj2 () is set
union () is set
ar S is complex ext-real V40() V41() Element of INT

the adicity of X . (() . S) is set

() * is non empty non trivial functional non finite V25() FinSequence-membered V167() Element of bool ((() *) *)

<*(() . S)*> null phi is Relation-like NAT -defined phi \/ (proj1 <*(() . S)*>) -defined Seg (1 + phi) -defined phi \/ (proj2 <*(() . S)*>) -valued Function-like finite len <*(() . S)*> -element total FinSequence-like FinSubsequence-like V199() set
proj1 <*(() . S)*> is non empty trivial finite 1 -element set
phi \/ (proj1 <*(() . S)*>) is non empty finite 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 <*(() . S)*> is non empty trivial finite 1 -element set
phi \/ (proj2 <*(() . S)*>) is non empty finite set

<*(() . S)*> \typed/ phi is Relation-like NAT -defined finite Element of bool (<*(() . S)*> \/ phi)
<*(() . S)*> \/ phi is non empty Relation-like NAT -defined finite set
bool (<*(() . S)*> \/ phi) is non empty finite V25() set

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 is non empty non trivial non finite V167() set
the U1 of X is set
() * is non empty non trivial functional non finite V25() FinSequence-membered V167() FinSequenceSet of AllSymbolsOf X
(() *) \ is non empty non trivial functional non finite V25() FinSequence-membered V166() V167() Element of bool (() *)
bool (() *) is non empty non trivial non finite V167() set
(() *) typed\ is functional V25() FinSequence-membered Element of bool (() *)
bool ((() *) \ ) is non empty non trivial non finite V167() set
K365(((() *) \ )) is non empty non trivial non finite V167() Element of bool (bool ((() *) \ ))
bool (bool ((() *) \ )) is non empty non trivial non finite V167() set

proj2 () is set
union () is set

[:((() *) \ ),():] is non empty non trivial Relation-like non finite V167() set
bool [:((() *) \ ),():] is non empty non trivial non finite V167() set

[:(),():] is non empty non trivial Relation-like non finite V167() set
[:[:(),():],():] is non empty non trivial Relation-like non finite V167() set
bool [:[:(),():],():] is non empty non trivial non finite V167() set

MultPlace (() -pr1) is non empty Relation-like (() *) \ -defined AllSymbolsOf X -valued Function-like total quasi_total Element of bool [:((() *) \ ),():]

() * is non empty non trivial functional non finite V25() FinSequence-membered V167() Element of bool (((() *) \ ) *)
((() *) \ ) * is non empty non trivial functional non finite V25() FinSequence-membered V167() FinSequenceSet of (() *) \
bool (((() *) \ ) *) is non empty non trivial non finite V167() set
[:(),(() *):] is non empty non trivial Relation-like non finite V167() set
bool [:(),(() *):] is non empty non trivial non finite V167() set
S is non empty set
[:(),S:] is non empty Relation-like set
bool [:(),S:] is non empty set
Funcs ((),S) is non empty functional FUNCTION_DOMAIN of AllTermsOf X,S
phi is Relation-like Function-like Function-yielding V164() (X,S) set

dom (phi (*) ()) is functional V25() FinSequence-membered V166() Element of bool ((() *) \ )
AllSymbolsOf X is non empty non trivial non finite V167() set

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
is non empty trivial functional finite V25() 1 -element V167() Element of bool NAT
0 * is non empty functional V25() FinSequence-membered