:: POLYFORM semantic presentation

REAL is non empty non trivial non finite set
NAT is V6() V7() V8() non empty non trivial non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty non trivial non finite V137() set
NAT is V6() V7() V8() non empty non trivial non finite cardinal limit_cardinal set
bool NAT is non empty non trivial non finite V137() set
bool NAT is non empty non trivial non finite V137() set
COMPLEX is non empty non trivial non finite set
RAT is non empty non trivial non finite set
INT is non empty non trivial non finite set
{} is V1() non-empty empty-yielding V4( NAT ) V5( RAT ) V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V38() V58() integer V148() V149() V150() V151() FinSequence-yielding finite-support Function-yielding V182() set
the V1() non-empty empty-yielding V4( NAT ) V5( RAT ) V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V38() V58() integer V148() V149() V150() V151() FinSequence-yielding finite-support Function-yielding V182() set is V1() non-empty empty-yielding V4( NAT ) V5( RAT ) V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V38() V58() integer V148() V149() V150() V151() FinSequence-yielding finite-support Function-yielding V182() set
2 is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() integer Element of NAT
1 is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() integer Element of NAT
K197(NAT) is V135() set
Z_2 is non empty non degenerated non trivial V72() V92() V96() V98() V100() right-distributive left-distributive right_unital well-unital V106() left_unital V116() V117() V118() L11()
the carrier of Z_2 is non empty non trivial set
[:COMPLEX,COMPLEX:] is V1() non empty non trivial non finite set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite V137() set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is V1() non empty non trivial non finite set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite V137() set
[:REAL,REAL:] is V1() non empty non trivial non finite set
bool [:REAL,REAL:] is non empty non trivial non finite V137() set
[:[:REAL,REAL:],REAL:] is V1() non empty non trivial non finite set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite V137() set
[:RAT,RAT:] is V1() non empty non trivial non finite set
bool [:RAT,RAT:] is non empty non trivial non finite V137() set
[:[:RAT,RAT:],RAT:] is V1() non empty non trivial non finite set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite V137() set
[:INT,INT:] is V1() non empty non trivial non finite set
bool [:INT,INT:] is non empty non trivial non finite V137() set
[:[:INT,INT:],INT:] is V1() non empty non trivial non finite set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite V137() set
[:NAT,NAT:] is V1() non empty non trivial non finite set
[:[:NAT,NAT:],NAT:] is V1() non empty non trivial non finite set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite V137() set
0 is V1() non-empty empty-yielding V4( NAT ) V5( RAT ) V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V38() V58() integer V148() V149() V150() V151() FinSequence-yielding finite-support Function-yielding V182() Element of NAT
{0,1,2} is non empty finite set
[:{0,1,2},{0,1,2}:] is V1() non empty finite set
[:[:{0,1,2},{0,1,2}:],{0,1,2}:] is V1() non empty finite set
bool [:[:{0,1,2},{0,1,2}:],{0,1,2}:] is non empty finite V28() V137() set
bool [:{0,1,2},{0,1,2}:] is non empty finite V28() V137() set
K582() is non empty V74() L8()
the carrier of K582() is non empty set
3 is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() integer Element of NAT
K49({}) is V1() non-empty empty-yielding V4( NAT ) V5( RAT ) V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V38() V58() integer V148() V149() V150() V151() FinSequence-yielding finite-support Function-yielding V182() set
rng {} is V1() non-empty empty-yielding V4( NAT ) V5( RAT ) V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty trivial finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V38() V58() integer V136() V148() V149() V150() V151() V152() V153() V154() V155() V158() V159() V160() V161() V163() FinSequence-yielding finite-support Function-yielding V182() set
Seg 1 is non empty trivial finite 1 -element Element of bool NAT
{ b₁ where b₁ is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT : ( 1 <= b₁ & b₁ <= 1 ) } is set
[#] Z_2 is non empty non proper Element of bool the carrier of Z_2
bool the carrier of Z_2 is non empty V137() set
{{},1} is non empty finite V28() set
0. Z_2 is V51( Z_2 ) Element of the carrier of Z_2
the ZeroF of Z_2 is Element of the carrier of Z_2
1. Z_2 is V51( Z_2 ) Element of the carrier of Z_2
the OneF of Z_2 is Element of the carrier of Z_2
<*> INT is V1() non-empty empty-yielding V4( NAT ) V5( INT ) V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty proper finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V38() V58() integer V148() V149() V150() V151() FinSequence-yielding finite-support Function-yielding V182() FinSequence of INT
[:NAT,INT:] is V1() non empty non trivial non finite set
K581((<*> INT)) is ext-real V38() V58() integer Element of INT
- 1 is non empty ext-real non positive negative V38() V58() integer set
p is set
s is set
c is set
{s,c} is non empty finite set
b is set
a is set
{b,a} is non empty finite set
b is set
a is set
{b,a} is non empty finite set
b is set
p is ext-real V38() V58() integer set
s is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
p is ext-real V38() V58() integer set
s is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer set
p * s is ext-real V38() V58() integer set
(2,0) is V1() non-empty empty-yielding V4( NAT ) V5( RAT ) V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V38() V58() integer V148() V149() V150() V151() FinSequence-yielding finite-support Function-yielding V182() even Element of INT
(2,0) + 1 is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() integer non even set
(2,1) is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() integer even Element of INT
(2,1) is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() integer even Element of INT
(2,1) + 1 is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() integer non even set
4 is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() integer Element of NAT
(2,2) is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() integer even Element of INT
p is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer set
(- 1) |^ p is ext-real V38() V58() set
s is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
(- 1) |^ s is ext-real V38() V58() set
(- 1) to_power s is ext-real V38() V58() set
p is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer set
(- 1) |^ p is ext-real V38() V58() set
s is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
(- 1) |^ s is ext-real V38() V58() set
(- 1) to_power s is ext-real V38() V58() set
p is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer set
(- 1) |^ p is ext-real V38() V58() set
p is ext-real V38() V58() integer set
s is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer set
p |^ s is ext-real V38() V58() set
c is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
- c is ext-real non positive V38() V58() integer set
b is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
b |^ s is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of REAL
a is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
c |^ s is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of REAL
(- 1) |^ s is ext-real V38() V58() set
((- 1),c) is ext-real non positive V38() V58() integer Element of INT
a is ext-real V38() V58() integer Element of INT
b is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
(a,b) is ext-real V38() V58() integer Element of INT
0 + 1 is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() integer set
p is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
p is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
s is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
p ^ s is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
len (p ^ s) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
c is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
s ^ c is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
p ^ (s ^ c) is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
len (p ^ (s ^ c)) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
(p ^ s) ^ c is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
len ((p ^ s) ^ c) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
p is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer set
p + 2 is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() integer set
p + 1 is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() integer set
((- 1),2) is ext-real V38() V58() integer Element of INT
1 + 1 is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() integer set
((- 1),(1 + 1)) is ext-real V38() V58() integer Element of INT
((- 1),1) is ext-real V38() V58() integer Element of INT
((- 1),1) * ((- 1),1) is ext-real V38() V58() integer set
((- 1),1) * (- 1) is ext-real V38() V58() integer set
(- 1) * (- 1) is non empty ext-real positive non negative V38() V58() integer set
p is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer set
((- 1),p) is ext-real V38() V58() integer Element of INT
p + 2 is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() integer set
((- 1),(p + 2)) is ext-real V38() V58() integer Element of INT
((- 1),p) * ((- 1),2) is ext-real V38() V58() integer set
p is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like V148() V149() V150() finite-support FinSequence of INT
len p is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
Sum p is V38() set
s is ext-real V38() V58() integer Element of INT
<*s*> is V1() V4( NAT ) V5( INT ) Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V148() V149() V150() V152() V153() V154() V155() finite-support Element of INT *
INT * is functional non empty FinSequence-membered FinSequenceSet of INT
[1,s] is set
{1,s} is non empty finite set
{1} is non empty trivial finite V28() 1 -element set
{{1,s},{1}} is non empty finite V28() set
{[1,s]} is V1() Function-like constant non empty trivial finite 1 -element finite-support set
p ^ <*s*> is V1() V4( NAT ) V5( INT ) Function-like non empty finite FinSequence-like FinSubsequence-like V148() V149() V150() finite-support FinSequence of INT
len (p ^ <*s*>) is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() integer Element of NAT
Sum (p ^ <*s*>) is V38() set
b is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like V148() V149() V150() finite-support FinSequence of INT
len b is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
a is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like V148() V149() V150() finite-support FinSequence of INT
len a is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
b . 1 is ext-real V38() V58() integer set
a . (len (p ^ <*s*>)) is ext-real V38() V58() integer set
(b . 1) + (a . (len (p ^ <*s*>))) is ext-real V38() V58() integer set
(Sum p) + s is V38() set
b is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer set
(p ^ <*s*>) . b is ext-real V38() V58() integer set
b . b is ext-real V38() V58() integer set
a . b is ext-real V38() V58() integer set
(b . b) + (a . b) is ext-real V38() V58() integer set
b | (len p) is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like V148() V149() V150() finite-support FinSequence of INT
Seg (len p) is finite len p -element Element of bool NAT
{ b₁ where b₁ is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT : ( 1 <= b₁ & b₁ <= len p ) } is set
K5(b,(Seg (len p))) is V1() V4( NAT ) V4( Seg (len p)) V4( NAT ) V5( INT ) Function-like finite FinSubsequence-like V148() V149() V150() finite-support set
(b | (len p)) . 1 is ext-real V38() V58() integer set
n9 is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
a | (len p) is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like V148() V149() V150() finite-support FinSequence of INT
K5(a,(Seg (len p))) is V1() V4( NAT ) V4( Seg (len p)) V4( NAT ) V5( INT ) Function-like finite FinSubsequence-like V148() V149() V150() finite-support set
a . (len p) is ext-real V38() V58() integer set
(a | (len p)) . (len p) is ext-real V38() V58() integer set
apcson is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer set
(a | (len p)) . apcson is ext-real V38() V58() integer set
apcson + 1 is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() integer set
(b | (len p)) . (apcson + 1) is ext-real V38() V58() integer set
- ((b | (len p)) . (apcson + 1)) is ext-real V38() V58() integer set
b is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
(a | (len p)) . b is ext-real V38() V58() integer set
a . b is ext-real V38() V58() integer set
b + 1 is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() integer set
(b | (len p)) . (b + 1) is ext-real V38() V58() integer set
b . (b + 1) is ext-real V38() V58() integer set
apcson is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer set
p . apcson is ext-real V38() V58() integer set
(b | (len p)) . apcson is ext-real V38() V58() integer set
(a | (len p)) . apcson is ext-real V38() V58() integer set
((b | (len p)) . apcson) + ((a | (len p)) . apcson) is ext-real V38() V58() integer set
dom p is finite Element of bool NAT
b is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
p . b is ext-real V38() V58() integer set
(p ^ <*s*>) . b is ext-real V38() V58() integer set
b . b is ext-real V38() V58() integer set
a . b is ext-real V38() V58() integer set
(b . b) + (a . b) is ext-real V38() V58() integer set
(b | (len p)) . b is ext-real V38() V58() integer set
((b | (len p)) . b) + (a . b) is ext-real V38() V58() integer set
(a | (len p)) . b is ext-real V38() V58() integer set
((b | (len p)) . b) + ((a | (len p)) . b) is ext-real V38() V58() integer set
len <*s*> is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() integer Element of NAT
(len p) + 1 is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() integer set
0 + (len p) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer set
b . ((len p) + 1) is ext-real V38() V58() integer set
- (b . ((len p) + 1)) is ext-real V38() V58() integer set
(p ^ <*s*>) . ((len p) + 1) is ext-real V38() V58() integer set
- ((a | (len p)) . (len p)) is ext-real V38() V58() integer set
(- ((a | (len p)) . (len p))) + (a . (len (p ^ <*s*>))) is ext-real V38() V58() integer set
len (a | (len p)) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
len (b | (len p)) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
((b | (len p)) . 1) + ((a | (len p)) . (len p)) is ext-real V38() V58() integer set
<*> INT is V1() non-empty empty-yielding V4( NAT ) V5( INT ) V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V38() V58() integer V148() V149() V150() V151() FinSequence-yielding finite-support Function-yielding V182() Element of INT *
INT * is functional non empty FinSequence-membered FinSequenceSet of INT
len (<*> INT) is V1() non-empty empty-yielding V4( NAT ) V5( RAT ) V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V38() V58() integer V148() V149() V150() V151() FinSequence-yielding finite-support Function-yielding V182() Element of NAT
Sum (<*> INT) is V38() set
p is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like V148() V149() V150() finite-support FinSequence of INT
len p is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
s is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like V148() V149() V150() finite-support FinSequence of INT
len s is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
p . 1 is ext-real V38() V58() integer set
s . (len (<*> INT)) is ext-real V38() V58() integer set
(p . 1) + (s . (len (<*> INT))) is ext-real V38() V58() integer set
c is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like V148() V149() V150() finite-support FinSequence of INT
len c is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
p is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like V148() V149() V150() finite-support FinSequence of INT
len p is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
s is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like V148() V149() V150() finite-support FinSequence of INT
len s is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
Sum c is V38() set
p . 1 is ext-real V38() V58() integer set
s . (len c) is ext-real V38() V58() integer set
(p . 1) + (s . (len c)) is ext-real V38() V58() integer set
p is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
s is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
p ^ s is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
c is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
(p ^ s) ^ c is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
len ((p ^ s) ^ c) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
len p is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
len s is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
(len p) + (len s) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer set
len c is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
((len p) + (len s)) + (len c) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer set
len (p ^ s) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
(len (p ^ s)) + (len c) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer set
p is set
<*p*> is V1() V4( NAT ) Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like finite-support set
[1,p] is set
{1,p} is non empty finite set
{1} is non empty trivial finite V28() 1 -element set
{{1,p},{1}} is non empty finite V28() set
{[1,p]} is V1() Function-like constant non empty trivial finite 1 -element finite-support set
s is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
<*p*> ^ s is V1() V4( NAT ) Function-like non empty finite FinSequence-like FinSubsequence-like finite-support set
c is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
(<*p*> ^ s) ^ c is V1() V4( NAT ) Function-like non empty finite FinSequence-like FinSubsequence-like finite-support set
((<*p*> ^ s) ^ c) . 1 is set
s ^ c is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
<*p*> ^ (s ^ c) is V1() V4( NAT ) Function-like non empty finite FinSequence-like FinSubsequence-like finite-support set
p is set
<*p*> is V1() V4( NAT ) Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like finite-support set
[1,p] is set
{1,p} is non empty finite set
{1} is non empty trivial finite V28() 1 -element set
{{1,p},{1}} is non empty finite V28() set
{[1,p]} is V1() Function-like constant non empty trivial finite 1 -element finite-support set
s is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
c is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
s ^ c is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
(s ^ c) ^ <*p*> is V1() V4( NAT ) Function-like non empty finite FinSequence-like FinSubsequence-like finite-support set
len s is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
len c is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
(len s) + (len c) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer set
((len s) + (len c)) + 1 is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() integer set
((s ^ c) ^ <*p*>) . (((len s) + (len c)) + 1) is set
len (s ^ c) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
(len (s ^ c)) + 1 is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() integer set
((s ^ c) ^ <*p*>) . ((len (s ^ c)) + 1) is set
p is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
len p is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
s is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
p ^ s is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
len (p ^ s) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
c is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
(p ^ s) ^ c is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
b is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer set
((p ^ s) ^ c) . b is set
b - (len p) is ext-real V38() V58() integer set
s . (b - (len p)) is set
(len p) - (len p) is ext-real V38() V58() integer set
len s is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
(len p) + (len s) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer set
((len p) + (len s)) - (len p) is ext-real V38() V58() integer set
b is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer set
Seg (len s) is finite len s -element Element of bool NAT
{ b₁ where b₁ is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT : ( 1 <= b₁ & b₁ <= len s ) } is set
dom s is finite Element of bool NAT
s ^ c is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
p ^ (s ^ c) is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
len (p ^ (s ^ c)) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
(p ^ (s ^ c)) . b is set
(s ^ c) . (b - (len p)) is set
n is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
(s ^ c) . n is set
s . n is set
p is ext-real V38() V58() integer set
<*p*> is V1() V4( NAT ) Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like finite-support set
[1,p] is set
{1,p} is non empty finite set
{1} is non empty trivial finite V28() 1 -element set
{{1,p},{1}} is non empty finite V28() set
{[1,p]} is V1() Function-like constant non empty trivial finite 1 -element finite-support set
<*p*> is V1() V4( NAT ) Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like finite-support set
rng <*p*> is non empty trivial finite 1 -element set
{p} is non empty trivial finite 1 -element set
p is ext-real V38() V58() integer set
s is ext-real V38() V58() integer set
<*p,s*> is V1() V4( NAT ) Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like finite-support set
<*p*> is V1() V4( NAT ) Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like finite-support set
[1,p] is set
{1,p} is non empty finite set
{{1,p},{1}} is non empty finite V28() set
{[1,p]} is V1() Function-like constant non empty trivial finite 1 -element finite-support set
<*s*> is V1() V4( NAT ) Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like finite-support set
[1,s] is set
{1,s} is non empty finite set
{{1,s},{1}} is non empty finite V28() set
{[1,s]} is V1() Function-like constant non empty trivial finite 1 -element finite-support set
<*p*> ^ <*s*> is V1() V4( NAT ) Function-like non empty finite K132(1,1) -element FinSequence-like FinSubsequence-like finite-support set
K132(1,1) is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() integer Element of NAT
rng <*p,s*> is non empty finite set
{p,s} is non empty finite set
p is ext-real V38() V58() integer set
s is ext-real V38() V58() integer set
c is ext-real V38() V58() integer set
<*p,s,c*> is V1() V4( NAT ) Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like finite-support set
<*p*> is V1() V4( NAT ) Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like finite-support set
[1,p] is set
{1,p} is non empty finite set
{{1,p},{1}} is non empty finite V28() set
{[1,p]} is V1() Function-like constant non empty trivial finite 1 -element finite-support set
<*s*> is V1() V4( NAT ) Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like finite-support set
[1,s] is set
{1,s} is non empty finite set
{{1,s},{1}} is non empty finite V28() set
{[1,s]} is V1() Function-like constant non empty trivial finite 1 -element finite-support set
<*p*> ^ <*s*> is V1() V4( NAT ) Function-like non empty finite K132(1,1) -element FinSequence-like FinSubsequence-like finite-support set
<*c*> is V1() V4( NAT ) Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like finite-support set
[1,c] is set
{1,c} is non empty finite set
{{1,c},{1}} is non empty finite V28() set
{[1,c]} is V1() Function-like constant non empty trivial finite 1 -element finite-support set
(<*p*> ^ <*s*>) ^ <*c*> is V1() V4( NAT ) Function-like non empty finite K132(K132(1,1),1) -element FinSequence-like FinSubsequence-like finite-support set
K132(K132(1,1),1) is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() integer Element of NAT
rng <*p,s,c*> is non empty finite set
{p,s,c} is non empty finite set
p is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like V148() V149() V150() finite-support FinSequence of INT
s is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like V148() V149() V150() finite-support FinSequence of INT
p ^ s is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
p is ext-real V38() V58() integer set
(p) is V1() V4( NAT ) V5( INT ) Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V148() V149() V150() V152() V153() V154() V155() finite-support FinSequence of INT
[1,p] is set
{1,p} is non empty finite set
{{1,p},{1}} is non empty finite V28() set
{[1,p]} is V1() Function-like constant non empty trivial finite 1 -element finite-support set
s is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like V148() V149() V150() finite-support FinSequence of INT
((p),s) is V1() V4( NAT ) V5( INT ) Function-like non empty finite FinSequence-like FinSubsequence-like V148() V149() V150() finite-support FinSequence of INT
Sum ((p),s) is V38() set
Sum s is V38() set
p + (Sum s) is V38() set
c is ext-real V38() V58() integer Element of INT
(c) is V1() V4( NAT ) V5( INT ) Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V148() V149() V150() V152() V153() V154() V155() finite-support FinSequence of INT
[1,c] is set
{1,c} is non empty finite set
{{1,c},{1}} is non empty finite V28() set
{[1,c]} is V1() Function-like constant non empty trivial finite 1 -element finite-support set
((c),s) is V1() V4( NAT ) V5( INT ) Function-like non empty finite FinSequence-like FinSubsequence-like V148() V149() V150() finite-support FinSequence of INT
Sum ((c),s) is V38() set
Sum (c) is V38() set
(Sum s) + (Sum (c)) is V38() set
(s,(c)) is V1() V4( NAT ) V5( INT ) Function-like non empty finite FinSequence-like FinSubsequence-like V148() V149() V150() finite-support FinSequence of INT
Sum (s,(c)) is V38() set
c + (Sum s) is V38() set
p is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like V148() V149() V150() finite-support FinSequence of INT
s is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like V148() V149() V150() finite-support FinSequence of INT
(p,s) is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like V148() V149() V150() finite-support FinSequence of INT
c is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like V148() V149() V150() finite-support FinSequence of INT
((p,s),c) is V1() V4( NAT ) V5( INT ) Function-like finite FinSequence-like FinSubsequence-like V148() V149() V150() finite-support FinSequence of INT
Sum ((p,s),c) is V38() set
Sum p is V38() set
Sum s is V38() set
(Sum p) + (Sum s) is V38() set
Sum c is V38() set
((Sum p) + (Sum s)) + (Sum c) is V38() set
Sum (p,s) is V38() set
(Sum (p,s)) + (Sum c) is V38() set
p is Element of the carrier of Z_2
<*p*> is V1() V4( NAT ) V5( the carrier of Z_2) Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like finite-support Element of the carrier of Z_2 *
the carrier of Z_2 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of Z_2
[1,p] is set
{1,p} is non empty finite set
{{1,p},{1}} is non empty finite V28() set
{[1,p]} is V1() Function-like constant non empty trivial finite 1 -element finite-support set
Sum <*p*> is Element of the carrier of Z_2
the U5 of Z_2 is V1() V4([: the carrier of Z_2, the carrier of Z_2:]) V5( the carrier of Z_2) Function-like non empty V39([: the carrier of Z_2, the carrier of Z_2:]) quasi_total Element of bool [:[: the carrier of Z_2, the carrier of Z_2:], the carrier of Z_2:]
[: the carrier of Z_2, the carrier of Z_2:] is V1() non empty set
[:[: the carrier of Z_2, the carrier of Z_2:], the carrier of Z_2:] is V1() non empty set
bool [:[: the carrier of Z_2, the carrier of Z_2:], the carrier of Z_2:] is non empty V137() set
K392( the carrier of Z_2,<*p*>, the U5 of Z_2) is Element of the carrier of Z_2
{(0. Z_2),(1. Z_2)} is non empty finite set
p is set
s is set
[:p,s:] is V1() set
[:p,s:] --> (1. Z_2) is V1() V4([:p,s:]) V5( the carrier of Z_2) Function-like constant V39([:p,s:]) quasi_total Element of bool [:[:p,s:], the carrier of Z_2:]
[:[:p,s:], the carrier of Z_2:] is V1() set
bool [:[:p,s:], the carrier of Z_2:] is non empty set
Funcs ([:p,s:],{(0. Z_2),(1. Z_2)}) is functional non empty FUNCTION_DOMAIN of [:p,s:],{(0. Z_2),(1. Z_2)}
rng ([:p,s:] --> (1. Z_2)) is trivial finite Element of bool the carrier of Z_2
{(1. Z_2)} is non empty trivial finite 1 -element set
dom ([:p,s:] --> (1. Z_2)) is V1() V4(p) V5(s) Element of bool [:p,s:]
bool [:p,s:] is non empty set
<*> {} is V1() non-empty empty-yielding V4( NAT ) V5( {} ) V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V38() V58() integer V148() V149() V150() V151() FinSequence-yielding finite-support Function-yielding V182() Element of {} *
{} * is functional non empty FinSequence-membered FinSequenceSet of {}
bool [:NAT,INT:] is non empty non trivial non finite V137() set
({}) is V1() V4( NAT ) V5( INT ) Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V148() V149() V150() V152() V153() V154() V155() FinSequence-yielding finite-support Function-yielding V182() FinSequence of INT
[1,{}] is set
{1,{}} is non empty finite V28() set
{{1,{}},{1}} is non empty finite V28() set
{[1,{}]} is V1() Function-like constant non empty trivial finite 1 -element finite-support set
<*({})*> is V1() V4( NAT ) V5( bool [:NAT,INT:]) Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Function-yielding V182() Element of (bool [:NAT,INT:]) *
(bool [:NAT,INT:]) * is functional non empty FinSequence-membered FinSequenceSet of bool [:NAT,INT:]
[1,({})] is set
{1,({})} is non empty finite V28() set
{{1,({})},{1}} is non empty finite V28() set
{[1,({})]} is V1() Function-like constant non empty trivial finite 1 -element finite-support set
s is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Function-yielding V182() set
p is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support Function-yielding V182() set
(s,p) is () ()
c is () ()
len s is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
len p is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
1 - 1 is ext-real V38() V58() integer set
b is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer set
p . b is V1() Function-like set
s . b is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
rng (s . b) is finite set
b + 1 is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() integer set
s . (b + 1) is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
rng (s . (b + 1)) is finite set
[:(rng (s . b)),(rng (s . (b + 1))):] is V1() finite set
Funcs ([:(rng (s . b)),(rng (s . (b + 1))):],{(0. Z_2),(1. Z_2)}) is functional non empty FUNCTION_DOMAIN of [:(rng (s . b)),(rng (s . (b + 1))):],{(0. Z_2),(1. Z_2)}
b is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer set
the of c is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Function-yielding V182() set
len the of c is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
the of c . b is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
p is () () () ()
the of p is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Function-yielding V182() set
len the of p is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
s is ext-real V38() V58() integer set
{{}} is functional non empty trivial finite V28() 1 -element set
p is () () () ()
(p) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
the of p is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Function-yielding V182() set
len the of p is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
s + 1 is ext-real V38() V58() integer set
the of p . (s + 1) is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
rng ( the of p . (s + 1)) is finite set
{p} is non empty trivial finite 1 -element set
(- 1) + 1 is ext-real V38() V58() integer set
b is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
b + 1 is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() integer set
the of p . (b + 1) is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
b is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
rng b is finite set
b is finite set
a is finite set
p is () () () ()
(p) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
the of p is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Function-yielding V182() set
len the of p is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
s is ext-real V38() V58() integer set
s + 1 is ext-real V38() V58() integer set
(- 1) + 1 is ext-real V38() V58() integer set
c is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
p is () () () ()
(p) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
the of p is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Function-yielding V182() set
len the of p is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
s is ext-real V38() V58() integer set
(p,s) is finite set
s + 1 is ext-real V38() V58() integer set
the of p . (s + 1) is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
rng ( the of p . (s + 1)) is finite set
b is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
n is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer set
the of p . n is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
{p} is non empty trivial finite 1 -element set
p is () () () ()
(p) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
the of p is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Function-yielding V182() set
len the of p is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
s is ext-real V38() V58() integer set
s - 1 is ext-real V38() V58() integer set
p is () () () ()
s is ext-real V38() V58() integer set
s - 1 is ext-real V38() V58() integer set
(p,(s - 1)) is finite set
(p,s) is finite set
[:(p,(s - 1)),(p,s):] is V1() finite set
Funcs ([:(p,(s - 1)),(p,s):],{(0. Z_2),(1. Z_2)}) is functional non empty FUNCTION_DOMAIN of [:(p,(s - 1)),(p,s):],{(0. Z_2),(1. Z_2)}
(p,0) is finite set
[:{{}},(p,0):] is V1() finite set
[:{{}},(p,0):] --> (1. Z_2) is V1() V4([:{{}},(p,0):]) V5( the carrier of Z_2) Function-like constant finite V39([:{{}},(p,0):]) quasi_total finite-support Element of bool [:[:{{}},(p,0):], the carrier of Z_2:]
[:[:{{}},(p,0):], the carrier of Z_2:] is V1() set
bool [:[:{{}},(p,0):], the carrier of Z_2:] is non empty set
(p) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
the of p is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Function-yielding V182() set
len the of p is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
the of p is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support Function-yielding V182() set
the of p . s is V1() Function-like set
(p) - 1 is ext-real V38() V58() integer set
(p,((p) - 1)) is finite set
{p} is non empty trivial finite 1 -element set
[:(p,((p) - 1)),{p}:] is V1() finite set
[:(p,((p) - 1)),{p}:] --> (1. Z_2) is V1() V4([:(p,((p) - 1)),{p}:]) V5( the carrier of Z_2) Function-like constant finite V39([:(p,((p) - 1)),{p}:]) quasi_total finite-support Element of bool [:[:(p,((p) - 1)),{p}:], the carrier of Z_2:]
[:[:(p,((p) - 1)),{p}:], the carrier of Z_2:] is V1() set
bool [:[:(p,((p) - 1)),{p}:], the carrier of Z_2:] is non empty set
0 - 1 is non empty ext-real non positive negative V38() V58() integer set
[:[:(p,(s - 1)),(p,s):],{(0. Z_2),(1. Z_2)}:] is V1() finite set
bool [:[:(p,(s - 1)),(p,s):],{(0. Z_2),(1. Z_2)}:] is non empty finite V28() set
b is V1() Function-like set
a is V1() V4([:(p,(s - 1)),(p,s):]) V5({(0. Z_2),(1. Z_2)}) Function-like finite V39([:(p,(s - 1)),(p,s):]) quasi_total finite-support Element of bool [:[:(p,(s - 1)),(p,s):],{(0. Z_2),(1. Z_2)}:]
b is V1() V4([:(p,(s - 1)),(p,s):]) V5({(0. Z_2),(1. Z_2)}) Function-like V39([:(p,(s - 1)),(p,s):]) quasi_total finite-support Element of Funcs ([:(p,(s - 1)),(p,s):],{(0. Z_2),(1. Z_2)})
[:[:(p,(s - 1)),(p,s):],{(0. Z_2),(1. Z_2)}:] is V1() finite set
bool [:[:(p,(s - 1)),(p,s):],{(0. Z_2),(1. Z_2)}:] is non empty finite V28() set
b is V1() Function-like set
a is V1() V4([:(p,(s - 1)),(p,s):]) V5({(0. Z_2),(1. Z_2)}) Function-like finite V39([:(p,(s - 1)),(p,s):]) quasi_total finite-support Element of bool [:[:(p,(s - 1)),(p,s):],{(0. Z_2),(1. Z_2)}:]
b is V1() V4([:(p,(s - 1)),(p,s):]) V5({(0. Z_2),(1. Z_2)}) Function-like V39([:(p,(s - 1)),(p,s):]) quasi_total finite-support Element of Funcs ([:(p,(s - 1)),(p,s):],{(0. Z_2),(1. Z_2)})
s + 1 is ext-real V38() V58() integer set
the of p . (s + 1) is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
rng ( the of p . (s + 1)) is finite set
1 - 1 is ext-real V38() V58() integer set
(s - 1) + 1 is ext-real V38() V58() integer set
the of p . ((s - 1) + 1) is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
rng ( the of p . ((s - 1) + 1)) is finite set
a is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer set
the of p . a is V1() Function-like set
b is V1() V4([:(p,(s - 1)),(p,s):]) V5({(0. Z_2),(1. Z_2)}) Function-like V39([:(p,(s - 1)),(p,s):]) quasi_total finite-support Element of Funcs ([:(p,(s - 1)),(p,s):],{(0. Z_2),(1. Z_2)})
[:{{}},{p}:] is V1() non empty finite set
[:{{}},{p}:] --> (1. Z_2) is V1() V4([:{{}},{p}:]) V5( the carrier of Z_2) Function-like constant non empty finite V39([:{{}},{p}:]) quasi_total finite-support Element of bool [:[:{{}},{p}:], the carrier of Z_2:]
[:[:{{}},{p}:], the carrier of Z_2:] is V1() non empty set
bool [:[:{{}},{p}:], the carrier of Z_2:] is non empty V137() set
Funcs ([:{{}},{p}:],{(0. Z_2),(1. Z_2)}) is functional non empty FUNCTION_DOMAIN of [:{{}},{p}:],{(0. Z_2),(1. Z_2)}
b is V1() V4([:{{}},{p}:]) V5({(0. Z_2),(1. Z_2)}) Function-like V39([:{{}},{p}:]) quasi_total finite-support Element of Funcs ([:{{}},{p}:],{(0. Z_2),(1. Z_2)})
a is V1() V4([:(p,(s - 1)),(p,s):]) V5({(0. Z_2),(1. Z_2)}) Function-like V39([:(p,(s - 1)),(p,s):]) quasi_total finite-support Element of Funcs ([:(p,(s - 1)),(p,s):],{(0. Z_2),(1. Z_2)})
Funcs ([:{{}},(p,0):],{(0. Z_2),(1. Z_2)}) is functional non empty FUNCTION_DOMAIN of [:{{}},(p,0):],{(0. Z_2),(1. Z_2)}
b is V1() V4([:{{}},(p,0):]) V5({(0. Z_2),(1. Z_2)}) Function-like V39([:{{}},(p,0):]) quasi_total finite-support Element of Funcs ([:{{}},(p,0):],{(0. Z_2),(1. Z_2)})
a is V1() V4([:(p,(s - 1)),(p,s):]) V5({(0. Z_2),(1. Z_2)}) Function-like V39([:(p,(s - 1)),(p,s):]) quasi_total finite-support Element of Funcs ([:(p,(s - 1)),(p,s):],{(0. Z_2),(1. Z_2)})
[:{{}},{p}:] is V1() non empty finite set
[:{{}},{p}:] --> (1. Z_2) is V1() V4([:{{}},{p}:]) V5( the carrier of Z_2) Function-like constant non empty finite V39([:{{}},{p}:]) quasi_total finite-support Element of bool [:[:{{}},{p}:], the carrier of Z_2:]
[:[:{{}},{p}:], the carrier of Z_2:] is V1() non empty set
bool [:[:{{}},{p}:], the carrier of Z_2:] is non empty V137() set
Funcs ([:{{}},{p}:],{(0. Z_2),(1. Z_2)}) is functional non empty FUNCTION_DOMAIN of [:{{}},{p}:],{(0. Z_2),(1. Z_2)}
b is V1() V4([:{{}},{p}:]) V5({(0. Z_2),(1. Z_2)}) Function-like V39([:{{}},{p}:]) quasi_total finite-support Element of Funcs ([:{{}},{p}:],{(0. Z_2),(1. Z_2)})
a is V1() V4([:(p,(s - 1)),(p,s):]) V5({(0. Z_2),(1. Z_2)}) Function-like V39([:(p,(s - 1)),(p,s):]) quasi_total finite-support Element of Funcs ([:(p,(s - 1)),(p,s):],{(0. Z_2),(1. Z_2)})
Funcs ([:(p,((p) - 1)),{p}:],{(0. Z_2),(1. Z_2)}) is functional non empty FUNCTION_DOMAIN of [:(p,((p) - 1)),{p}:],{(0. Z_2),(1. Z_2)}
b is V1() V4([:(p,((p) - 1)),{p}:]) V5({(0. Z_2),(1. Z_2)}) Function-like V39([:(p,((p) - 1)),{p}:]) quasi_total finite-support Element of Funcs ([:(p,((p) - 1)),{p}:],{(0. Z_2),(1. Z_2)})
a is V1() V4([:(p,(s - 1)),(p,s):]) V5({(0. Z_2),(1. Z_2)}) Function-like V39([:(p,(s - 1)),(p,s):]) quasi_total finite-support Element of Funcs ([:(p,(s - 1)),(p,s):],{(0. Z_2),(1. Z_2)})
b is V1() V4([:(p,(s - 1)),(p,s):]) V5({(0. Z_2),(1. Z_2)}) Function-like V39([:(p,(s - 1)),(p,s):]) quasi_total finite-support Element of Funcs ([:(p,(s - 1)),(p,s):],{(0. Z_2),(1. Z_2)})
a is V1() V4([:(p,(s - 1)),(p,s):]) V5({(0. Z_2),(1. Z_2)}) Function-like V39([:(p,(s - 1)),(p,s):]) quasi_total finite-support Element of Funcs ([:(p,(s - 1)),(p,s):],{(0. Z_2),(1. Z_2)})
s is ext-real V38() V58() integer set
<*> {} is V1() non-empty empty-yielding V4( NAT ) V5( {} ) V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V38() V58() integer V148() V149() V150() V151() FinSequence-yielding finite-support Function-yielding V182() Element of {} *
{} * is functional non empty FinSequence-membered FinSequenceSet of {}
({}) is V1() V4( NAT ) V5( INT ) Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V148() V149() V150() V152() V153() V154() V155() FinSequence-yielding finite-support Function-yielding V182() FinSequence of INT
[1,{}] is set
{1,{}} is non empty finite V28() set
{{1,{}},{1}} is non empty finite V28() set
{[1,{}]} is V1() Function-like constant non empty trivial finite 1 -element finite-support set
p is () () () ()
(p) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
the of p is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Function-yielding V182() set
len the of p is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
s + 1 is ext-real V38() V58() integer set
the of p . (s + 1) is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
<*p*> is V1() V4( NAT ) Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like finite-support set
[1,p] is set
{1,p} is non empty finite set
{{1,p},{1}} is non empty finite V28() set
{[1,p]} is V1() Function-like constant non empty trivial finite 1 -element finite-support set
b is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
a is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
p is () () () ()
s is ext-real V38() V58() integer set
(p,s) is finite set
card (p,s) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
p is () () () ()
(p,0) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
(p,0) is finite set
card (p,0) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
(p,1) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
(p,1) is finite set
card (p,1) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
(p,2) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
(p,2) is finite set
card (p,2) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
p is () () () ()
s is ext-real V38() V58() integer set
(p,s) is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
dom (p,s) is finite Element of bool NAT
(p,s) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
(p,s) is finite set
card (p,s) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
Seg (p,s) is finite (p,s) -element Element of bool NAT
{ b₁ where b₁ is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT : ( 1 <= b₁ & b₁ <= (p,s) ) } is set
the of p is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Function-yielding V182() set
(p) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
len the of p is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
len (p,s) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
s + 1 is ext-real V38() V58() integer set
a is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer set
the of p . a is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
b is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
the of p . (s + 1) is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
rng ( the of p . (s + 1)) is finite set
dom b is finite Element of bool NAT
card (dom b) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
len b is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
<*p*> is V1() V4( NAT ) Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like finite-support set
[1,p] is set
{1,p} is non empty finite set
{{1,p},{1}} is non empty finite V28() set
{[1,p]} is V1() Function-like constant non empty trivial finite 1 -element finite-support set
len (p,s) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
{p} is non empty trivial finite 1 -element set
(p) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
len the of p is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
(p) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
len the of p is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
p is () () () ()
s is ext-real V38() V58() integer set
(p,s) is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
len (p,s) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
(p,s) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
(p,s) is finite set
card (p,s) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
dom (p,s) is finite Element of bool NAT
Seg (p,s) is finite (p,s) -element Element of bool NAT
{ b₁ where b₁ is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT : ( 1 <= b₁ & b₁ <= (p,s) ) } is set
p is () () () ()
s is ext-real V38() V58() integer set
(p,s) is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
rng (p,s) is finite set
(p,s) is finite set
the of p is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support Function-yielding V182() set
(p) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
len the of p is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
s + 1 is ext-real V38() V58() integer set
the of p . (s + 1) is V1() V4( NAT ) Function-like finite FinSequence-like FinSubsequence-like finite-support set
rng ( the of p . (s + 1)) is finite set
{p} is non empty trivial finite 1 -element set
<*p*> is V1() V4( NAT ) Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like finite-support set
[1,p] is set
{1,p} is non empty finite set
{{1,p},{1}} is non empty finite V28() set
{[1,p]} is V1() Function-like constant non empty trivial finite 1 -element finite-support set
(p) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
len the of p is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
(p) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
len the of p is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
p is () () () ()
(p,(- 1)) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
(p,(- 1)) is finite set
card (p,(- 1)) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
s is ext-real V38() V58() integer set
(p,s) is finite set
p is () () () ()
(p) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() integer Element of NAT
the of p is V1() V4( NAT ) Function-like finite FinSequence-like