:: PNPROC_1 semantic presentation

REAL is V69() V70() V71() V75() set
NAT is V6() V7() V8() non empty V17() non finite cardinal limit_cardinal V69() V70() V71() V72() V73() V74() V75() Element of K48(REAL)
K48(REAL) is set
NAT is V6() V7() V8() non empty V17() non finite cardinal limit_cardinal V69() V70() V71() V72() V73() V74() V75() set
K48(NAT) is V17() non finite set
K48(NAT) is V17() non finite set
INT is V69() V70() V71() V72() V73() V75() set
COMPLEX is V69() V75() set
RAT is V69() V70() V71() V72() V75() set
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional V24() V25() Function-yielding finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FuncSeq-like integer ext-real V59() V60() V61() V62() V69() V70() V71() V72() V73() V74() V75() set
the Relation-like non-empty empty-yielding NAT -defined RAT -valued V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional V24() V25() Function-yielding finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FuncSeq-like integer ext-real V59() V60() V61() V62() V69() V70() V71() V72() V73() V74() V75() set is Relation-like non-empty empty-yielding NAT -defined RAT -valued V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional V24() V25() Function-yielding finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FuncSeq-like integer ext-real V59() V60() V61() V62() V69() V70() V71() V72() V73() V74() V75() set
2 is V6() V7() V8() V12() non empty V24() V25() finite cardinal integer ext-real positive V58() V69() V70() V71() V72() V73() V74() Element of NAT
1 is V6() V7() V8() V12() non empty V24() V25() finite cardinal integer ext-real positive V58() V69() V70() V71() V72() V73() V74() Element of NAT
3 is V6() V7() V8() V12() non empty V24() V25() finite cardinal integer ext-real positive V58() V69() V70() V71() V72() V73() V74() Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional V24() V25() Function-yielding finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FuncSeq-like integer ext-real V58() V59() V60() V61() V62() V69() V70() V71() V72() V73() V74() V75() Element of NAT
Seg 1 is non empty V17() finite 1 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
{1} is non empty V17() finite V36() 1 -element V69() V70() V71() V72() V73() V74() set
Seg 2 is non empty finite 2 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
{1,2} is non empty finite V36() V69() V70() V71() V72() V73() V74() set
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is set
[P,N] is V13() set
{P,N} is non empty finite set
{P} is non empty V17() finite V36() 1 -element V69() V70() V71() V72() V73() V74() set
{{P,N},{P}} is non empty finite V36() set
{[P,N]} is Relation-like non empty V17() Function-like constant finite 1 -element set
proj1 {[P,N]} is non empty V17() finite 1 -element set
{P} is non empty V17() finite V36() 1 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Seg P is finite P -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
R is set
P is Relation-like NAT -defined Function-like FinSubsequence-like set
Seq P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
proj1 P is V69() V70() V71() V72() V73() V74() set
Sgm (proj1 P) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 P)) (#) P is Relation-like NAT -defined Function-like finite set
proj2 (Sgm (proj1 P)) is finite V69() V70() V71() V72() V73() V74() set
dom {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional V24() V25() Function-yielding finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FuncSeq-like integer ext-real V59() V60() V61() V62() V69() V70() V71() V72() V73() V74() V75() Element of K48(NAT)
dom (Sgm (proj1 P)) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
proj2 {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued V6() V7() V8() V10() V11() V12() empty V17() Function-like one-to-one constant functional V24() V25() Function-yielding finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FuncSeq-like integer ext-real V59() V60() V61() V62() V63() V64() V65() V66() V69() V70() V71() V72() V73() V74() V75() set
P is Relation-like NAT -defined Function-like FinSubsequence-like set
Seq P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
proj1 P is V69() V70() V71() V72() V73() V74() set
Sgm (proj1 P) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 P)) (#) P is Relation-like NAT -defined Function-like finite set
{} (#) P is Relation-like non-empty empty-yielding NAT -defined RAT -valued V6() V7() V8() V10() V11() V12() empty Function-like one-to-one constant functional V24() V25() Function-yielding finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FuncSeq-like integer ext-real V59() V60() V61() V62() V69() V70() V71() V72() V73() V74() V75() set
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is set
[P,N] is V13() set
{P,N} is non empty finite set
{P} is non empty V17() finite V36() 1 -element V69() V70() V71() V72() V73() V74() set
{{P,N},{P}} is non empty finite V36() set
{[P,N]} is Relation-like non empty V17() Function-like constant finite 1 -element set
<*N*> is Relation-like NAT -defined non empty V17() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
R is Relation-like NAT -defined Function-like FinSubsequence-like set
Seq R is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
proj1 R is V69() V70() V71() V72() V73() V74() set
0 + 1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
Seg x is finite x -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Sgm (proj1 R) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 R)) (#) R is Relation-like NAT -defined Function-like finite set
x is Relation-like NAT -defined Function-like FinSubsequence-like set
proj1 x is V69() V70() V71() V72() V73() V74() set
{P} is non empty V17() finite V36() 1 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Seq x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
<*P*> is Relation-like NAT -defined NAT -valued non empty V17() Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V59() V60() V61() V62() V63() V64() V65() V66() Element of NAT *
NAT * is non empty functional FinSequence-membered M12( NAT )
<*P*> (#) {[P,N]} is Relation-like NAT -defined Function-like finite set
{[P,N]} . P is set
<*({[P,N]} . P)*> is Relation-like NAT -defined non empty V17() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
P is Relation-like NAT -defined Function-like FinSubsequence-like set
proj1 P is V69() V70() V71() V72() V73() V74() set
N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
Seg N is finite N -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
P is set
<*P*> is Relation-like NAT -defined non empty V17() Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
N is Relation-like NAT -defined Function-like finite FinSubsequence-like set
Seq N is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
[1,P] is V13() set
{1,P} is non empty finite set
{{1,P},{1}} is non empty finite V36() set
{[1,P]} is Relation-like non empty V17() Function-like constant finite 1 -element set
dom (Seq N) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
{1} is non empty V17() finite V36() 1 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
proj2 (Seq N) is finite set
{P} is non empty V17() finite 1 -element set
proj1 N is finite V69() V70() V71() V72() V73() V74() set
Sgm (proj1 N) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 N)) (#) N is Relation-like NAT -defined Function-like finite set
proj2 (Sgm (proj1 N)) is finite V69() V70() V71() V72() V73() V74() set
dom (Sgm (proj1 N)) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
proj2 N is finite set
R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
Seg R is finite R -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
card (proj1 N) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seg (card (proj1 N)) is finite card (proj1 N) -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
card {1} is V6() V7() V8() V12() non empty V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
x is set
{x} is non empty V17() finite 1 -element set
C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
[C,P] is V13() set
{C,P} is non empty finite set
{C} is non empty V17() finite V36() 1 -element V69() V70() V71() V72() V73() V74() set
{{C,P},{C}} is non empty finite V36() set
{[C,P]} is Relation-like non empty V17() Function-like constant finite 1 -element set
P is set
N is set
[P,N] is V13() set
{P,N} is non empty finite set
{P} is non empty V17() finite 1 -element set
{{P,N},{P}} is non empty finite V36() set
R is set
x is set
[R,x] is V13() set
{R,x} is non empty finite set
{R} is non empty V17() finite 1 -element set
{{R,x},{R}} is non empty finite V36() set
{[P,N],[R,x]} is Relation-like non empty finite set
C is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom C is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
{P,R} is non empty finite set
C . P is set
C . R is set
len C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seg (len C) is finite len C -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
1 + 1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
0 + 1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
{[P,N]} is Relation-like non empty V17() Function-like constant finite 1 -element set
P is set
[1,P] is V13() set
{1,P} is non empty finite set
{{1,P},{1}} is non empty finite V36() set
N is set
<*P,N*> is Relation-like NAT -defined non empty Function-like finite 2 -element FinSequence-like FinSubsequence-like set
[2,N] is V13() set
{2,N} is non empty finite set
{2} is non empty V17() finite V36() 1 -element V69() V70() V71() V72() V73() V74() set
{{2,N},{2}} is non empty finite V36() set
{[1,P],[2,N]} is Relation-like non empty finite set
R is Relation-like Function-like set
proj1 R is set
{1,2} is non empty finite V36() V69() V70() V71() V72() V73() V74() Element of K48(NAT)
dom <*P,N*> is non empty finite 2 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
x is set
<*P,N*> . x is set
[x,P] is V13() set
{x,P} is non empty finite set
{x} is non empty V17() finite 1 -element set
{{x,P},{x}} is non empty finite V36() set
R . x is set
<*P,N*> . x is set
[x,N] is V13() set
{x,N} is non empty finite set
{x} is non empty V17() finite 1 -element set
{{x,N},{x}} is non empty finite V36() set
R . x is set
P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R + 1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R + N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R + 0 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
0 + 1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P is Relation-like NAT -defined Function-like finite FinSubsequence-like set
card P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
Seq P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (Seq P) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
proj1 P is finite V69() V70() V71() V72() V73() V74() set
Sgm (proj1 P) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 P)) (#) P is Relation-like NAT -defined Function-like finite set
proj2 (Sgm (proj1 P)) is finite V69() V70() V71() V72() V73() V74() set
dom (Seq P) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
dom (Sgm (proj1 P)) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
N is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
Seg N is finite N -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
card (proj1 P) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
card (dom (Sgm (proj1 P))) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P is set
N is set
P /\ N is set
R is set
R is set
P /\ N is set
R is set
P is Relation-like set
proj1 P is set
N is Relation-like set
proj1 N is set
P is set
N is set
R is Relation-like set
R | P is Relation-like set
x is Relation-like set
x | N is Relation-like set
P /\ N is set
proj1 (R | P) is set
proj1 R is set
(proj1 R) /\ P is set
proj1 (x | N) is set
proj1 x is set
(proj1 x) /\ N is set
(proj1 (R | P)) /\ (proj1 (x | N)) is set
P /\ ((proj1 x) /\ N) is set
(proj1 R) /\ (P /\ ((proj1 x) /\ N)) is set
(P /\ N) /\ (proj1 x) is set
(proj1 R) /\ ((P /\ N) /\ (proj1 x)) is set
P is Relation-like NAT -defined Function-like finite FinSubsequence-like set
Seq P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (Seq P) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
proj1 P is finite V69() V70() V71() V72() V73() V74() set
Sgm (proj1 P) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
dom (Sgm (proj1 P)) is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
(Sgm (proj1 P)) (#) P is Relation-like NAT -defined Function-like finite set
proj2 (Sgm (proj1 P)) is finite V69() V70() V71() V72() V73() V74() set
P is Relation-like NAT -defined Function-like finite FinSubsequence-like set
proj2 P is finite set
Seq P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
proj2 (Seq P) is finite set
proj1 P is finite V69() V70() V71() V72() V73() V74() set
Sgm (proj1 P) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() FinSequence of NAT
(Sgm (proj1 P)) (#) P is Relation-like NAT -defined Function-like finite set
proj2 ((Sgm (proj1 P)) (#) P) is finite set
proj2 (Sgm (proj1 P)) is finite V69() V70() V71() V72() V73() V74() set
P is Relation-like Function-like set
R is Relation-like Function-like set
N is Relation-like Function-like set
proj1 P is set
proj1 N is set
x is set
P . x is set
[x,(P . x)] is V13() set
{x,(P . x)} is non empty finite set
{x} is non empty V17() finite 1 -element set
{{x,(P . x)},{x}} is non empty finite V36() set
N . x is set
[x,(N . x)] is V13() set
{x,(N . x)} is non empty finite set
{{x,(N . x)},{x}} is non empty finite V36() set
P is set
N is Relation-like set
P |` N is Relation-like set
N " P is set
N | (N " P) is Relation-like set
R is set
x is set
[R,x] is V13() set
{R,x} is non empty finite set
{R} is non empty V17() finite 1 -element set
{{R,x},{R}} is non empty finite V36() set
P is set
N is Relation-like Function-like set
P |` N is Relation-like Function-like set
N " P is set
N | (N " P) is Relation-like Function-like set
R is set
x is set
[R,x] is V13() set
{R,x} is non empty finite set
{R} is non empty V17() finite 1 -element set
{{R,x},{R}} is non empty finite V36() set
proj1 N is set
N . R is set
N . R is set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
F₁() is set
K49(F₁(),NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(F₁(),NAT)) is set
P is Relation-like Function-like set
proj1 P is set
proj2 P is set
N is set
R is set
P . R is set
F₂(R) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(F₁(),NAT))
R is set
N . R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
F₂(R) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is set
N . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
proj1 N is set
proj1 R is set
P is set
P --> 0 is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
{0} is non empty V17() functional finite V36() 1 -element V69() V70() V71() V72() V73() V74() set
K49(P,{0}) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
C is set
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
P is set
N is set
(N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(N,NAT))
K49(N,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(N,NAT)) is set
N --> 0 is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(N,NAT))
K49(N,{0}) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
(N) . P is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
(P) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
P --> 0 is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
K49(P,{0}) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is set
(P) . R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
C is set
N . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
x . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
N + R is Relation-like INT -valued RAT -valued Function-like V59() V60() V61() V62() set
N + R is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
proj1 (N + R) is set
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
N + R is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
C is set
x . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(N . C) + (R . C) is V24() V25() integer ext-real set
proj1 x is set
proj1 (N + R) is set
proj1 N is set
proj1 R is set
(proj1 N) /\ (proj1 R) is set
P /\ (proj1 R) is set
P /\ P is set
C is set
x . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(N . C) + (R . C) is V24() V25() integer ext-real set
(N + R) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
(P) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
P --> 0 is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
K49(P,{0}) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,(P)) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is set
(P) . R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(N . R) + ((P) . R) is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
C is set
x . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(N . C) - (R . C) is V24() V25() integer ext-real set
(N . C) -' (R . C) is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real non negative V58() V69() V70() V71() V72() V73() V74() Element of NAT
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
C is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
q1 is set
x . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
C . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(N . q1) - (R . q1) is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,R) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is set
N . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(P,N,R) . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() set
R . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(N . x) + (R . x) is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
(P) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
P --> 0 is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
K49(P,{0}) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,(P)) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is set
(P) . R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(N . R) - ((P) . R) is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,x,R) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,x,N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
C is set
(P,x,R) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(P,x,N) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
x . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(x . C) - (N . C) is V24() V25() integer ext-real set
(x . C) - (R . C) is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,R) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,N,R),R) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is set
(P,(P,N,R),R) . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(P,N,R) . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() set
R . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
((P,N,R) . x) - (R . x) is V24() V25() integer ext-real set
(N . x) + (R . x) is V24() V25() integer ext-real set
((N . x) + (R . x)) - (R . x) is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,R,N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,x,N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
C is set
(P,R,N) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(P,x,N) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
x . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(R . C) - (N . C) is V24() V25() integer ext-real set
(x . C) - (N . C) is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,R,N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,R,x) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,R,x),N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,R,N),x) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
C is set
(P,(P,R,x),N) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(P,(P,R,N),x) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() set
(P,R,N) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
x . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
((P,R,N) . C) + (x . C) is V24() V25() integer ext-real set
R . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(R . C) - (N . C) is V24() V25() integer ext-real set
(x . C) + ((R . C) - (N . C)) is V24() V25() integer ext-real set
(x . C) + (R . C) is V24() V25() integer ext-real set
((x . C) + (R . C)) - (N . C) is V24() V25() integer ext-real set
(P,x,R) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,x,R) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() set
((P,x,R) . C) - (N . C) is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is set
N . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,R) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,N,R),x) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,R,x) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,(P,R,x)) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
C is set
(P,(P,N,R),x) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() set
(P,N,(P,R,x)) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() set
(P,N,R) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() set
x . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
((P,N,R) . C) + (x . C) is V24() V25() integer ext-real set
N . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(N . C) + (R . C) is V24() V25() integer ext-real set
((N . C) + (R . C)) + (x . C) is V24() V25() integer ext-real set
(P,R,x) . C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() set
(N . C) + ((P,R,x) . C) is V24() V25() integer ext-real set
(R . C) + (x . C) is V24() V25() integer ext-real set
(N . C) + ((R . C) + (x . C)) is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,x) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
C is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,R,C) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
q1 is set
(P,N,x) . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() set
(P,R,C) . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() set
N . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
x . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
C . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(N . q1) + (x . q1) is V24() V25() integer ext-real set
(R . q1) + (C . q1) is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,R,N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is set
(P,R,N) . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(R . x) - (N . x) is V24() V25() integer ext-real set
(R . x) - 0 is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,R,x) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
C is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,C) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
q1 is set
(P,N,C) . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(P,R,x) . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
x . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
C . q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(R . q1) - (x . q1) is V24() V25() integer ext-real set
(N . q1) - (C . q1) is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,R,N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,R,N),N) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is set
R . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(P,(P,R,N),N) . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() set
(P,R,N) . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
N . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
((P,R,N) . x) + (N . x) is V24() V25() integer ext-real set
(R . x) - (N . x) is V24() V25() integer ext-real set
((R . x) - (N . x)) + (N . x) is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,R) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,N,R),N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is set
(P,(P,N,R),N) . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
R . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
(P,N,R) . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() set
N . x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
((P,N,R) . x) - (N . x) is V24() V25() integer ext-real set
(N . x) + (R . x) is V24() V25() integer ext-real set
((N . x) + (R . x)) - (N . x) is V24() V25() integer ext-real set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,R) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,x,N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,x,N),R) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,x,(P,N,R)) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,x,(P,N,R)),(P,N,R)) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,x,(P,N,R)),(P,N,R)),N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,(P,x,(P,N,R)),(P,N,R)),N),R) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,x,(P,N,R)),R) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,x,(P,N,R)),R),N) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,(P,x,(P,N,R)),R),N),N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,(P,(P,x,(P,N,R)),R),N),N),R) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,x,(P,N,R)),R),R) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,R,N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,x,(P,R,N)) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,x,R) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,x,R),N) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,(P,R,N)) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,N,(P,R,N)),(P,R,N)) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,x,(P,R,N)),N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,x,(P,R,N)),N),N) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
the Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT)) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
[ the Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT)), the Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))] is V13() set
{ the Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT)), the Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))} is non empty functional finite set
{ the Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))} is non empty V17() functional finite 1 -element set
{{ the Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT)), the Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))},{ the Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))}} is non empty finite V36() set
P is set
P is set
N is (P)
N `1 is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
[R,x] is V13() set
{R,x} is non empty functional finite set
{R} is non empty V17() functional finite 1 -element set
{{R,x},{R}} is non empty finite V36() set
N `2 is set
R is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
[R,x] is V13() set
{R,x} is non empty functional finite set
{R} is non empty V17() functional finite 1 -element set
{{R,x},{R}} is non empty finite V36() set
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
R is (P)
(P,R) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,(P,R)) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,R) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,N,(P,R)),(P,R)) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is (P)
(P,R) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,R) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,N,(P,R)) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,R) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x is (P)
(P,x) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,R),(P,x)) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,N,R),x) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,N,(P,R)),(P,x)) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,N,(P,R)),(P,x)),(P,R)) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,x) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,(P,N,(P,R)),(P,x)),(P,R)),(P,x)) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,N,(P,R)),(P,R)) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,x),(P,R)) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,x),(P,R)),(P,R)) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,R),(P,x)),(P,R)) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,N,R),(P,x)) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,N,R),(P,x)),(P,x)) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,N,(P,R)),(P,R)),(P,x)) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,(P,(P,N,(P,R)),(P,R)),(P,x)),(P,x)) is Relation-like INT -valued RAT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
P is set
Funcs (P,NAT) is non empty functional FUNCTION_DOMAIN of P, NAT
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is (P)
R is set
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,x,N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like Function-like set
proj1 R is set
x is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R . x is set
(P,x,N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
C is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,C,N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is Relation-like Function-like set
proj1 R is set
x is Relation-like Function-like set
proj1 x is set
C is set
R . C is set
q1 is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,q1,N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
x . C is set
P is set
Funcs (P,NAT) is non empty functional FUNCTION_DOMAIN of P, NAT
N is (P)
(P,N) is Relation-like Function-like set
proj2 (P,N) is set
R is set
proj1 (P,N) is set
x is set
(P,N) . x is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
C is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,C,N) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
P is set
K49(P,NAT) is Relation-like INT -valued RAT -valued V59() V60() V61() V62() set
K48(K49(P,NAT)) is set
N is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
R is (P)
(P,R) is Relation-like Function-like set
x is (P)
(P,N,x) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,(P,N,x),R) is Relation-like INT -valued Function-like total quasi_total V59() V60() V61() V62() Element of K48(K49(P,NAT))
(P,x) is Relation-like Function-like set
(P,x) (#) (P,R) is Relation-like Function-like set
((P,x) (#) (P,R)) . N is set
proj1 (P,x) is set
Funcs (P,NAT) is non empty functional FUNCTION_DOMAIN of P, NAT
(P,R) . (P,N,x) is set
(P,x) . N is set
(P,R) . ((P,x) . N) is set
P is set
the (P) is (P)
{ the (P)} is non empty V17() finite 1 -element set
R is set
P is set
N is non empty (P)
R is Element of N
P is set
P is set
N is non empty (P)
N * is non empty functional FinSequence-membered M12(N)
Funcs (P,NAT) is non empty functional FUNCTION_DOMAIN of P, NAT
R is Relation-like NAT -defined N -valued Function-like finite FinSequence-like FinSubsequence-like Element of N *
len R is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
dom R is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len x is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
dom x is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Seg (len x) is finite len x -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Seg (len R) is finite len R -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
C is set
proj1 x is finite V69() V70() V71() V72() V73() V74() set
x . C is set
q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
R /. q1 is Element of N
(P,(R /. q1)) is Relation-like Function-like set
C is Relation-like NAT -defined Function-like Function-yielding finite FinSequence-like FinSubsequence-like set
compose (C,(Funcs (P,NAT))) is Relation-like Function-like set
q1 is Relation-like Function-like set
len C is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
C . q2 is set
R /. q2 is Element of N
(P,(R /. q2)) is Relation-like Function-like set
x is Relation-like Function-like set
C is Relation-like Function-like set
q1 is Relation-like NAT -defined Function-like Function-yielding finite FinSequence-like FinSubsequence-like set
compose (q1,(Funcs (P,NAT))) is Relation-like Function-like set
len q1 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
q2 is Relation-like NAT -defined Function-like Function-yielding finite FinSequence-like FinSubsequence-like set
compose (q2,(Funcs (P,NAT))) is Relation-like Function-like set
len q2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real V58() V69() V70() V71() V72() V73() V74() Element of NAT
dom q1 is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Seg (len q1) is finite len q1 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
dom q2 is finite V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Seg (len q2) is finite len q2 -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
Seg (len R) is finite len R -element V69() V70() V71() V72() V73() V74() Element of K48(NAT)
fs2 is V6() V7() V8() V12() V24() V25() finite cardinal integer ext-real set
q1 . fs2 is set
R /. fs2 is Element of N
(P,(R /. fs2)) is Relation-like Function-like set
q2 . fs2 is set
P is set
Funcs (P,NAT) is non empty functional FUNCTION_DOMAIN of P, NAT
id (Funcs (P,NAT)) is Relation-like Funcs (P,NAT) -defined Funcs (P,NAT) -valued non empty Function-like one-to-one total quasi_total Element of K48(K49((Funcs (P,NAT)),(Funcs (P,NAT))))
K49((Funcs (P,NAT)),(Funcs (P,NAT))) is Relation-like set
K48(