:: STIRL2_1 semantic presentation

REAL is V50() V51() V52() V56() V68() V69() V71() set
NAT is epsilon-transitive epsilon-connected ordinal non empty non trivial V50() V51() V52() V53() V54() V55() V56() non finite V66() V68() cardinal limit_cardinal Element of bool REAL
bool REAL is non empty set
RAT is V50() V51() V52() V53() V56() set
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty Function-like one-to-one constant functional V33() V34() integer ext-real non positive non negative V40() V41() V42() V43() V50() V51() V52() V53() V54() V55() V56() finite finite-yielding V61() V68() V69() V70() V71() cardinal {} -element V88() V92() set
the Relation-like non-empty empty-yielding NAT -defined RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty Function-like one-to-one constant functional V33() V34() integer ext-real non positive non negative V40() V41() V42() V43() V50() V51() V52() V53() V54() V55() V56() finite finite-yielding V61() V68() V69() V70() V71() cardinal {} -element V88() V92() set is Relation-like non-empty empty-yielding NAT -defined RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty Function-like one-to-one constant functional V33() V34() integer ext-real non positive non negative V40() V41() V42() V43() V50() V51() V52() V53() V54() V55() V56() finite finite-yielding V61() V68() V69() V70() V71() cardinal {} -element V88() V92() set
COMPLEX is V50() V56() set
INT is V50() V51() V52() V53() V54() V56() set
[:COMPLEX,COMPLEX:] is Relation-like V40() set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like V40() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:REAL,REAL:] is Relation-like V40() V41() V42() set
bool [:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is Relation-like V40() V41() V42() set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is Relation-like RAT -valued V40() V41() V42() set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued V40() V41() V42() set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is Relation-like RAT -valued INT -valued V40() V41() V42() set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued V40() V41() V42() set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V40() V41() V42() V43() non finite V92() set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V40() V41() V42() V43() non finite V92() set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
NAT is epsilon-transitive epsilon-connected ordinal non empty non trivial V50() V51() V52() V53() V54() V55() V56() non finite V66() V68() cardinal limit_cardinal set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
[:COMPLEX,REAL:] is Relation-like V40() V41() V42() set
bool [:COMPLEX,REAL:] is non empty set
1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() integer V36() ext-real positive non negative V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() cardinal Element of NAT
{{},1} is non empty V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() set
2 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() integer V36() ext-real positive non negative V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() cardinal Element of NAT
3 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() integer V36() ext-real positive non negative V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() cardinal Element of NAT
union {} is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
dom {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty Function-like one-to-one constant functional V33() V34() integer ext-real non positive non negative V40() V41() V42() V43() V50() V51() V52() V53() V54() V55() V56() finite finite-yielding V61() V68() V69() V70() V71() cardinal {} -element V88() V92() set
rng {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty trivial Function-like one-to-one constant functional V33() V34() integer ext-real non positive non negative V40() V41() V42() V43() V44() V45() V46() V47() V50() V51() V52() V53() V54() V55() V56() finite finite-yielding V61() V68() V69() V70() V71() cardinal {} -element V84() V88() V92() set
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty Function-like one-to-one constant functional V33() V34() integer V36() ext-real non positive non negative V40() V41() V42() V43() V50() V51() V52() V53() V54() V55() V56() finite finite-yielding V61() V68() V69() V70() V71() cardinal {} -element V88() V92() Element of NAT
card {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty Function-like one-to-one constant functional V33() V34() integer ext-real non positive non negative V40() V41() V42() V43() V50() V51() V52() V53() V54() V55() V56() finite finite-yielding V61() V68() V69() V70() V71() cardinal {} -element V88() V92() set
{{}} is non empty trivial functional V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element set
addnat is Relation-like [:NAT,NAT:] -defined NAT -valued non empty Function-like V24([:NAT,NAT:]) quasi_total V32( NAT ) V40() V41() V42() V43() V92() V93( NAT ) V94( NAT ) Element of bool [:[:NAT,NAT:],NAT:]
K497(NAT,addnat) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
2 ! is V33() V34() ext-real Element of REAL
Ne is non empty V50() V51() V52() V53() V54() V55() V66() V68() Element of bool NAT
min Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
min* Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ke is ext-real set
Ne is non empty V50() V51() V52() V53() V54() V55() V66() V68() Element of bool NAT
min Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ke is non empty V50() V51() V52() V53() V54() V55() V66() V68() Element of bool NAT
min Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
min ((min Ne),(min Ke)) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ne \/ Ke is non empty V50() V51() V52() V53() V54() V55() V66() V68() Element of bool NAT
min (Ne \/ Ke) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
min ((min Ke),(min Ne)) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ke \/ Ne is non empty V50() V51() V52() V53() V54() V55() V66() V68() Element of bool NAT
I1 is ext-real set
Ne is V50() V51() V52() V53() V54() V55() V68() Element of bool NAT
min* Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ke is V50() V51() V52() V53() V54() V55() V68() Element of bool NAT
min* Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
min ((min* Ne),(min* Ke)) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ne \/ Ke is V50() V51() V52() V53() V54() V55() V68() Element of bool NAT
min* (Ne \/ Ke) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
I1 is non empty V50() V51() V52() V53() V54() V55() V66() V68() Element of bool NAT
min I1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
F is non empty V50() V51() V52() V53() V54() V55() V66() V68() Element of bool NAT
F \/ I1 is non empty V50() V51() V52() V53() V54() V55() V66() V68() Element of bool NAT
min (F \/ I1) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
min F is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ne is V50() V51() V52() V53() V54() V55() V68() Element of bool NAT
min* Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ke is V50() V51() V52() V53() V54() V55() V68() Element of bool NAT
Ne /\ Ke is V50() V51() V52() V53() V54() V55() V68() Element of bool NAT
Ne \ Ke is V50() V51() V52() V53() V54() V55() V68() Element of bool NAT
min* (Ne \ Ke) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
{Ne} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool NAT
min* {Ne} is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
min {Ne} is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
{Ne,Ke} is non empty V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() Element of bool NAT
min* {Ne,Ke} is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
min (Ne,Ke) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
min {Ne,Ke} is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
{Ne} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool NAT
min {Ne} is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
{Ke} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool NAT
{Ne} \/ {Ke} is non empty V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() Element of bool NAT
min {Ke} is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
min ((min {Ne}),(min {Ke})) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
{Ne,Ke,F} is non empty V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() Element of bool NAT
min* {Ne,Ke,F} is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
min (Ke,F) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
min (Ne,(min (Ke,F))) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
min {Ne,Ke,F} is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
{Ne} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool NAT
{Ke,F} is non empty V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() Element of bool NAT
{Ne} \/ {Ke,F} is non empty V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() Element of bool NAT
min {Ne} is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
min {Ke,F} is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
min ((min {Ne}),(min {Ke,F})) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
Ke is set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT : not Ne <= b₁ } is set
F is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of Ne
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
Ne - 1 is V33() V34() integer V36() ext-real Element of INT
Ke is non empty V50() V51() V52() V53() V54() V55() V66() V68() Element of bool NAT
min* Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT : not Ne <= b₁ } is set
F is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
Ke - 1 is V33() V34() integer V36() ext-real Element of INT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT : not Ke <= b₁ } is set
F is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
(Ke - 1) + 1 is V33() V34() integer V36() ext-real Element of INT
F is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
min* Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT : not Ne <= b₁ } is set
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
Ne - 1 is V33() V34() integer V36() ext-real Element of INT
Ke is non empty V50() V51() V52() V53() V54() V55() V66() V68() Element of bool NAT
min* Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
Ne - 1 is V33() V34() integer V36() ext-real Element of INT
{(Ne - 1)} is non empty trivial V50() V51() V52() V53() V54() finite V66() V67() V68() V69() V70() 1 -element Element of bool REAL
Ke is non empty V50() V51() V52() V53() V54() V55() V66() V68() Element of bool NAT
min* Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
F is set
I1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
Ne - 1 is V33() V34() integer V36() ext-real Element of INT
Ke is V50() V51() V52() V53() V54() V55() V68() Element of bool NAT
min* Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
Ke is set
[:Ne,Ke:] is Relation-like set
bool [:Ne,Ke:] is non empty set
F is Relation-like Ne -defined Ke -valued Function-like quasi_total finite Element of bool [:Ne,Ke:]
I1 is set
F " I1 is finite set
I2 is set
F " I1 is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ne
bool Ne is non empty finite V61() set
Ne is set
Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
[:Ne,Ke:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() V92() set
bool [:Ne,Ke:] is non empty set
F is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() V92() Element of bool [:Ne,Ke:]
I1 is set
F . I1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
dom F is Element of bool Ne
bool Ne is non empty set
rng F is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ke
bool Ke is non empty finite V61() set
dom F is Element of bool Ne
bool Ne is non empty set
dom F is Element of bool Ne
bool Ne is non empty set
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
[:Ne,Ke:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ne,Ke:] is non empty finite V61() set
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
[:Ne,Ke:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ne,Ke:] is non empty finite V61() set
F is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:]
I1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
I2 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
{I2} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ne,Ke,F,{I2}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ne,Ke,F,{I2}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
{I1} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ne,Ke,F,{I1}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ne,Ke,F,{I1}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
rng F is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ke
bool Ke is non empty finite V61() set
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
[:Ke,Ne:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ke,Ne:] is non empty finite V61() set
Ke - 1 is V33() V34() integer V36() ext-real Element of INT
F is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
{F} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
I1 is Relation-like Ke -defined Ne -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ke,Ne:]
(Ke,Ne,I1,{F}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ke,Ne,I1,{F}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
I2 is set
dom I1 is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ke
bool Ke is non empty finite V61() set
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
[:Ne,Ke:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ne,Ke:] is non empty finite V61() set
F is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:]
rng F is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ke
bool Ke is non empty finite V61() set
dom F is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ne
bool Ne is non empty finite V61() set
card Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
card Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
[:Ne,Ke:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ne,Ke:] is non empty finite V61() set
F is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:]
rng F is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ke
bool Ke is non empty finite V61() set
I1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
{I1} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ne,Ke,F,{I1}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ne,Ke,F,{I1}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
I1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() integer V36() ext-real positive non negative V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() cardinal Element of NAT
{(I1 + 1)} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ne,Ke,F,{(I1 + 1)}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ne,Ke,F,{(I1 + 1)}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
{(I1 + 1)} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool NAT
(Ne,Ke,F,{(I1 + 1)}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ne,Ke,F,{(I1 + 1)}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
{0} is non empty trivial functional V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ne,Ke,F,{0}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ne,Ke,F,{0}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
I1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
{I1} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ne,Ke,F,{I1}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ne,Ke,F,{I1}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
[:Ke,Ne:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ke,Ne:] is non empty finite V61() set
Ke - Ne is V33() V34() integer V36() ext-real Element of INT
F is Relation-like Ke -defined Ne -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ke,Ne:]
I1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
{I1} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ke,Ne,F,{I1}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ke,Ne,F,{I1}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
(Ke - Ne) + I1 is V33() V34() integer V36() ext-real Element of INT
Ne - 1 is V33() V34() integer V36() ext-real Element of INT
I1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
I1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() integer V36() ext-real positive non negative V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() cardinal Element of NAT
rng F is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ne
bool Ne is non empty finite V61() set
P1 is V33() V34() integer ext-real set
{P1} is non empty trivial V50() V51() V52() V53() V54() finite V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ke,Ne,F,{P1}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ke,Ne,F,{P1}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
(Ke - Ne) + P1 is V33() V34() integer V36() ext-real Element of INT
P1 - 1 is V33() V34() integer V36() ext-real Element of INT
{(P1 - 1)} is non empty trivial V50() V51() V52() V53() V54() finite V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ke,Ne,F,{(P1 - 1)}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ke,Ne,F,{(P1 - 1)}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
(Ke - Ne) + (P1 - 1) is V33() V34() integer V36() ext-real Element of INT
P2 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
P2 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() integer V36() ext-real positive non negative V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() cardinal Element of NAT
{(P2 + 1)} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool NAT
(Ke,Ne,F,{(P2 + 1)}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ke,Ne,F,{(P2 + 1)}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
{P2} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool NAT
(Ke,Ne,F,{P2}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ke,Ne,F,{P2}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
I2 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
I2 + P2 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
(I2 + P2) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() integer V36() ext-real positive non negative V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() cardinal Element of NAT
{I1} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ke,Ne,F,{I1}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ke,Ne,F,{I1}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
(Ke - Ne) + I1 is V33() V34() integer V36() ext-real Element of INT
{I1} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool NAT
(Ke,Ne,F,{I1}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ke,Ne,F,{I1}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ke - 1 is V33() V34() integer V36() ext-real Element of INT
I2 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
{I2} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ke,Ne,F,{I2}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ke,Ne,F,{I2}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
(Ke - Ne) + I2 is V33() V34() integer V36() ext-real Element of INT
I2 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
{I2} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ke,Ne,F,{I2}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ke,Ne,F,{I2}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
(Ke - Ne) + I2 is V33() V34() integer V36() ext-real Element of INT
I1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
{I1} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ke,Ne,F,{I1}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ke,Ne,F,{I1}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
(Ke - Ne) + I1 is V33() V34() integer V36() ext-real Element of INT
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
id Ne is Relation-like Ne -defined Ne -valued RAT -valued INT -valued Function-like one-to-one V24(Ne) quasi_total V40() V41() V42() V43() V44() V46() finite V92() Element of bool [:Ne,Ne:]
[:Ne,Ne:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ne,Ne:] is non empty finite V61() set
Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
[:Ne,Ke:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ne,Ke:] is non empty finite V61() set
F is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:]
I1 is set
(Ne,Ke,F,I1) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of Ke
dom F is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ne
bool Ne is non empty finite V61() set
I1 is set
I2 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
rng F is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ke
bool Ke is non empty finite V61() set
dom F is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ne
bool Ne is non empty finite V61() set
{I2} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool NAT
(Ne,Ke,F,{I2}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
P2 is set
(Ne,Ke,F,P2) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of Ke
min* (Ne,Ke,F,{I2}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ne - Ke is V33() V34() integer V36() ext-real Element of INT
(Ne - Ke) + I2 is V33() V34() integer V36() ext-real Element of INT
P1 is non empty V50() V51() V52() V53() V54() V55() V66() V68() Element of bool NAT
min* P1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
(Ne,Ke,F,I2) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of Ke
(Ne,Ke,F,I1) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of Ke
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
[:Ke,Ne:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ke,Ne:] is non empty finite V61() set
id Ke is Relation-like Ke -defined Ke -valued RAT -valued INT -valued Function-like one-to-one V24(Ke) quasi_total V40() V41() V42() V43() V44() V46() finite V92() Element of bool [:Ke,Ke:]
[:Ke,Ke:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ke,Ke:] is non empty finite V61() set
F is Relation-like Ke -defined Ne -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ke,Ne:]
I1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
rng F is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ne
bool Ne is non empty finite V61() set
I2 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
{I1} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ke,Ne,F,{I1}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
dom F is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ke
bool Ke is non empty finite V61() set
P1 is set
(Ke,Ne,F,P1) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of Ne
P2 is set
{P2} is non empty trivial finite 1 -element set
min* (Ke,Ne,F,{I1}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
{I2} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ke,Ne,F,{I2}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
P2 is set
(Ke,Ne,F,P2) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of Ne
F is set
{F} is non empty trivial finite 1 -element set
min* (Ke,Ne,F,{I2}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
I1 is set
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
[:Ne,Ke:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ne,Ke:] is non empty finite V61() set
dom {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty proper Function-like one-to-one constant functional V33() V34() integer ext-real non positive non negative V40() V41() V42() V43() V50() V51() V52() V53() V54() V55() V56() finite finite-yielding V61() V68() V69() V70() V71() cardinal {} -element V88() V92() Element of bool NAT
rng {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty trivial Function-like one-to-one constant functional V33() V34() integer ext-real non positive non negative V40() V41() V42() V43() V44() V45() V46() V47() V50() V51() V52() V53() V54() V55() V56() finite finite-yielding V61() V68() V69() V70() V71() cardinal {} -element V84() V88() V92() Element of bool RAT
bool RAT is non empty set
I1 is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:]
{0} is non empty trivial functional V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool NAT
F is Relation-like Function-like set
dom F is set
rng F is set
[:Ne,{0}:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ne,{0}:] is non empty finite V61() set
I1 is Relation-like Ne -defined {0} -valued Function-like V24(Ne) quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,{0}:]
rng I1 is trivial functional V50() V51() V52() V53() V54() V55() finite V61() V68() V69() V70() Element of bool {0}
bool {0} is non empty finite V61() set
I2 is set
I2 is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:]
rng I2 is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ke
bool Ke is non empty finite V61() set
P1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
P2 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
{P2} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ne,Ke,I2,{P2}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ne,Ke,I2,{P2}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
{P1} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ne,Ke,I2,{P1}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ne,Ke,I2,{P1}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
F is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:]
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
[:Ne,Ke:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ne,Ke:] is non empty finite V61() set
dom {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty proper Function-like one-to-one constant functional V33() V34() integer ext-real non positive non negative V40() V41() V42() V43() V50() V51() V52() V53() V54() V55() V56() finite finite-yielding V61() V68() V69() V70() V71() cardinal {} -element V88() V92() Element of bool NAT
rng {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty trivial Function-like one-to-one constant functional V33() V34() integer ext-real non positive non negative V40() V41() V42() V43() V44() V45() V46() V47() V50() V51() V52() V53() V54() V55() V56() finite finite-yielding V61() V68() V69() V70() V71() cardinal {} -element V84() V88() V92() Element of bool RAT
bool RAT is non empty set
I1 is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:]
Ke - 1 is V33() V34() integer V36() ext-real Element of INT
I2 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() integer V36() ext-real positive non negative V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() cardinal Element of NAT
I1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() integer V36() ext-real positive non negative V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() cardinal Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
P1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of I2
min (P1,F) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
F + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() integer V36() ext-real positive non negative V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() cardinal Element of NAT
[:I2,I1:] is Relation-like RAT -valued INT -valued non empty V40() V41() V42() V43() finite V92() set
bool [:I2,I1:] is non empty finite V61() set
P1 is Relation-like I2 -defined I1 -valued non empty Function-like V24(I2) quasi_total V40() V41() V42() V43() finite V92() Element of bool [:I2,I1:]
P2 is set
F + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() integer V36() ext-real positive non negative V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() cardinal Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
dom P1 is non empty V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() Element of bool I2
bool I2 is non empty finite V61() set
min (F,F) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
(I2,I1,P1,F) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of I1
rng P1 is non empty V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() Element of bool I1
bool I1 is non empty finite V61() set
P2 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
{P2} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(I2,I1,P1,{P2}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (I2,I1,P1,{P2}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
min (P2,F) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
(I2,I1,P1,P2) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of I1
F is set
domF is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
(I2,I1,P1,domF) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of I1
min (domF,F) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
(I2,I1,P1,F) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of I1
min (F,P2) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
P2 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
F is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
{P2} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(I2,I1,P1,{P2}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (I2,I1,P1,{P2}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
{F} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(I2,I1,P1,{F}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (I2,I1,P1,{F}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
F is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:]
F₁() is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
F₂() is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
[:F₁(),F₂():] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:F₁(),F₂():] is non empty finite V61() set
{ b₁ where b₁ is Relation-like F₁() -defined F₂() -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:F₁(),F₂():] : P₁[b₁] } is set
{{}} is non empty trivial functional V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
Ke is set
F is Relation-like F₁() -defined F₂() -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:F₁(),F₂():]
Funcs (F₁(),F₂()) is functional set
Ke is set
F is Relation-like F₁() -defined F₂() -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:F₁(),F₂():]
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
[:Ne,Ke:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ne,Ke:] is non empty finite V61() set
{ b₁ where b₁ is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:] : ( b₁ is onto & b₁ is (Ne,Ke) ) } is set
{ b₁ where b₁ is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:] : S₁[b₁] } is set
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
[:Ne,Ke:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ne,Ke:] is non empty finite V61() set
{ b₁ where b₁ is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:] : ( b₁ is onto & b₁ is (Ne,Ke) ) } is set
card { b₁ where b₁ is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:] : ( b₁ is onto & b₁ is (Ne,Ke) ) } is epsilon-transitive epsilon-connected ordinal cardinal set
I1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
card I1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
[:Ne,Ke:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ne,Ke:] is non empty finite V61() set
{ b₁ where b₁ is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:] : ( b₁ is onto & b₁ is (Ne,Ke) ) } is set
card { b₁ where b₁ is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:] : ( b₁ is onto & b₁ is (Ne,Ke) ) } is epsilon-transitive epsilon-connected ordinal cardinal set
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
(Ne,<