:: AMI_2 semantic presentation

REAL is non empty non trivial V31() set

bool REAL is non trivial V31() set

1 is non empty ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
{{},1} is non empty V31() V35() countable set

bool omega is non trivial V31() set
bool NAT is non trivial V31() set
COMPLEX is non empty non trivial V31() set
RAT is non empty non trivial V31() set
INT is non empty non trivial V31() set
9 is non empty ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT

SCM-Data-Loc is non empty set
K80(NAT,1) is non empty trivial V31() V35() 1 -element countable Element of bool NAT

is non trivial V31() set
bool is non trivial V31() set
[:1,1:] is V31() countable set
bool [:1,1:] is V31() V35() countable set
[:[:1,1:],1:] is V31() countable set
bool [:[:1,1:],1:] is V31() V35() countable set
2 is non empty ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
3 is non empty ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT

is non empty trivial V31() 1 -element countable set
\/ SCM-Data-Loc is non empty set
() is set
bool () is set
() is non empty Element of bool ()
x is Element of ()
x is set
y is set
[x,y] is V1() set
{x,y} is non empty V31() countable set
{x} is non empty trivial V31() 1 -element countable set
{{x,y},{x}} is non empty V31() V35() countable set
[:(),2:] is set
bool [:(),2:] is set
is non empty trivial V31() V35() 1 -element countable set
{1} is non empty trivial V31() V35() 1 -element countable set
\/ {1} is non empty V31() V35() countable set
{0,1} is non empty V31() V35() countable set
{1} \/ is non empty V31() V35() countable set
x is Element of ()
x is non empty Relation-like () -defined 2 -valued Function-like V17(()) V18((),2) Element of bool [:(),2:]
y is Element of ()
x . y is ordinal Element of 2
x is non empty Relation-like () -defined 2 -valued Function-like V17(()) V18((),2) Element of bool [:(),2:]
y is non empty Relation-like () -defined 2 -valued Function-like V17(()) V18((),2) Element of bool [:(),2:]
z is Element of ()
x . z is ordinal Element of 2
y . z is ordinal Element of 2
z is Element of ()
x . z is ordinal Element of 2
y . z is ordinal Element of 2
z is Element of ()
x . z is ordinal Element of 2
y . z is ordinal Element of 2
z is Element of ()
x . z is ordinal Element of 2
y . z is ordinal Element of 2
() is non empty Relation-like () -defined 2 -valued Function-like V17(()) V18((),2) Element of bool [:(),2:]

(() * ()) . NAT is set
proj1 () is set
() . NAT is set
() . (() . NAT) is set
() . 0 is set
x is Element of ()
(() * ()) . x is set
proj1 () is set
() . x is ordinal Element of 2
() . (() . x) is set
() . 1 is set
proj1 () is set

proj2 () is set
proj1 () is set
proj1 (() * ()) is set
y is set
(() * ()) . y is set
x is Element of ()
(() * ()) . x is set
product (() * ()) is non empty functional with_common_domain product-like set
pi ((product (() * ())),NAT) is set
x is Element of ()
pi ((product (() * ())),x) is set
(() * ()) . x is set
x is Relation-like Function-like () * () -compatible Element of product (() * ())
x . NAT is set
x is Relation-like Function-like () * () -compatible Element of product (() * ())

{y} is non empty trivial V31() V35() 1 -element countable set

z is set
proj1 () is V31() countable set
(x +* ()) . NAT is set
() . NAT is set
(x +* ()) . z is set
(() * ()) . z is set
proj1 () is V31() countable set
(x +* ()) . z is set
x . z is set
(() * ()) . z is set
proj1 x is set
proj1 (x +* ()) is set
proj1 () is V31() countable set
() \/ (proj1 ()) is non empty set
() \/ is non empty set
x is Relation-like Function-like () * () -compatible Element of product (() * ())

(x,y) is Relation-like Function-like () * () -compatible Element of product (() * ())

{y} is non empty trivial V31() V35() 1 -element countable set

(x,y) . NAT is set
proj1 () is V31() countable set
() . NAT is set
x is Relation-like Function-like () * () -compatible Element of product (() * ())

(x,y) is Relation-like Function-like () * () -compatible Element of product (() * ())

{y} is non empty trivial V31() V35() 1 -element countable set

z is Element of ()
(x,y) . z is set
x . z is set
proj1 () is V31() countable set
(() * ()) . z is set
x is Relation-like Function-like () * () -compatible Element of product (() * ())

(x,y) is Relation-like Function-like () * () -compatible Element of product (() * ())

{y} is non empty trivial V31() V35() 1 -element countable set

(x,y) . z is set
x . z is set
proj1 () is V31() countable set
x is Relation-like Function-like () * () -compatible Element of product (() * ())
y is Element of ()
z is V86() integer V111() ext-real set

{y} is non empty trivial V31() 1 -element countable set
{y} --> z is non empty Relation-like {y} -defined {z} -valued Function-like constant V17({y}) V18({y},{z}) V31() countable Element of bool [:{y},{z}:]
{z} is non empty trivial V31() 1 -element countable set
[:{y},{z}:] is V31() countable set
bool [:{y},{z}:] is V31() V35() countable set
x +* (y .--> z) is Relation-like Function-like set
k is set
proj1 (y .--> z) is V31() countable set
(x +* (y .--> z)) . y is set
(y .--> z) . y is set
(x +* (y .--> z)) . k is set
(() * ()) . k is set
proj1 (y .--> z) is V31() countable set
(x +* (y .--> z)) . k is set
x . k is set
(() * ()) . k is set
proj1 x is set
proj1 (x +* (y .--> z)) is set
proj1 (y .--> z) is V31() countable set
() \/ (proj1 (y .--> z)) is non empty set
() \/ {y} is non empty set
x is Relation-like Function-like () * () -compatible Element of product (() * ())
x . NAT is set
y is Element of ()
z is V86() integer V111() ext-real set
(x,y,z) is Relation-like Function-like () * () -compatible Element of product (() * ())

{y} is non empty trivial V31() 1 -element countable set
{y} --> z is non empty Relation-like {y} -defined {z} -valued Function-like constant V17({y}) V18({y},{z}) V31() countable Element of bool [:{y},{z}:]
{z} is non empty trivial V31() 1 -element countable set
[:{y},{z}:] is V31() countable set
bool [:{y},{z}:] is V31() V35() countable set
x +* (y .--> z) is Relation-like Function-like set
(x,y,z) . NAT is set
proj1 (y .--> z) is V31() countable set
(() * ()) . y is set
x is Relation-like Function-like () * () -compatible Element of product (() * ())
y is Element of ()
z is V86() integer V111() ext-real set
(x,y,z) is Relation-like Function-like () * () -compatible Element of product (() * ())

{y} is non empty trivial V31() 1 -element countable set
{y} --> z is non empty Relation-like {y} -defined {z} -valued Function-like constant V17({y}) V18({y},{z}) V31() countable Element of bool [:{y},{z}:]
{z} is non empty trivial V31() 1 -element countable set
[:{y},{z}:] is V31() countable set
bool [:{y},{z}:] is V31() V35() countable set
x +* (y .--> z) is Relation-like Function-like set
(x,y,z) . y is set
proj1 (y .--> z) is V31() countable set
(y .--> z) . y is set
x is Relation-like Function-like () * () -compatible Element of product (() * ())
y is Element of ()
z is V86() integer V111() ext-real set
(x,y,z) is Relation-like Function-like () * () -compatible Element of product (() * ())

{y} is non empty trivial V31() 1 -element countable set
{y} --> z is non empty Relation-like {y} -defined {z} -valued Function-like constant V17({y}) V18({y},{z}) V31() countable Element of bool [:{y},{z}:]
{z} is non empty trivial V31() 1 -element countable set
[:{y},{z}:] is V31() countable set
bool [:{y},{z}:] is V31() V35() countable set
x +* (y .--> z) is Relation-like Function-like set
k is Element of ()
(x,y,z) . k is set
x . k is set
proj1 (y .--> z) is V31() countable set
x is Relation-like Function-like () * () -compatible Element of product (() * ())
y is Element of ()
x . y is set
pi ((product (() * ())),y) is set
SCM-Instr is non empty set
x is Element of SCM-Instr
y is Relation-like Function-like () * () -compatible Element of product (() * ())

y . () is V86() integer V111() ext-real set
(y,(),(y . ())) is Relation-like Function-like () * () -compatible Element of product (() * ())

{()} is non empty trivial V31() 1 -element countable set
{()} --> (y . ()) is non empty Relation-like {()} -defined {(y . ())} -valued Function-like constant V17({()}) V18({()},{(y . ())}) V31() countable Element of bool [:{()},{(y . ())}:]
{(y . ())} is non empty trivial V31() 1 -element countable set
[:{()},{(y . ())}:] is V31() countable set
bool [:{()},{(y . ())}:] is V31() V35() countable set
y +* (() .--> (y . ())) is Relation-like Function-like set

y . NAT is set

((y,(),(y . ())),(succ (y))) is Relation-like Function-like () * () -compatible Element of product (() * ())

--> (succ (y)) is non empty Relation-like -defined {(succ (y))} -valued Function-like constant V17() V18(,{(succ (y))}) V31() Cardinal-yielding countable V102() Element of bool [:,{(succ (y))}:]
{(succ (y))} is non empty trivial V31() V35() 1 -element countable set
[:,{(succ (y))}:] is V31() countable set
bool [:,{(succ (y))}:] is V31() V35() countable set
(y,(),(y . ())) +* (NAT .--> (succ (y))) is Relation-like Function-like set
y . () is V86() integer V111() ext-real set
(y . ()) + (y . ()) is V86() integer V111() ext-real set
(y,(),((y . ()) + (y . ()))) is Relation-like Function-like () * () -compatible Element of product (() * ())
() .--> ((y . ()) + (y . ())) is Relation-like SCM-Data-Loc -defined {()} -defined Function-like one-to-one V31() countable set
{()} --> ((y . ()) + (y . ())) is non empty Relation-like {()} -defined {((y . ()) + (y . ()))} -valued Function-like constant V17({()}) V18({()},{((y . ()) + (y . ()))}) V31() countable Element of bool [:{()},{((y . ()) + (y . ()))}:]
{((y . ()) + (y . ()))} is non empty trivial V31() 1 -element countable set
[:{()},{((y . ()) + (y . ()))}:] is V31() countable set
bool [:{()},{((y . ()) + (y . ()))}:] is V31() V35() countable set
y +* (() .--> ((y . ()) + (y . ()))) is Relation-like Function-like set
((y,(),((y . ()) + (y . ()))),(succ (y))) is Relation-like Function-like () * () -compatible Element of product (() * ())
(y,(),((y . ()) + (y . ()))) +* (NAT .--> (succ (y))) is Relation-like Function-like set
(y . ()) - (y . ()) is V86() integer V111() ext-real set
(y,(),((y . ()) - (y . ()))) is Relation-like Function-like () * () -compatible Element of product (() * ())
() .--> ((y . ()) - (y . ())) is Relation-like SCM-Data-Loc -defined {()} -defined Function-like one-to-one V31() countable set
{()} --> ((y . ()) - (y . ())) is non empty Relation-like {()} -defined {((y . ()) - (y . ()))} -valued Function-like constant V17({()}) V18({()},{((y . ()) - (y . ()))}) V31() countable Element of bool [:{()},{((y . ()) - (y . ()))}:]
{((y . ()) - (y . ()))} is non empty trivial V31() 1 -element countable set
[:{()},{((y . ()) - (y . ()))}:] is V31() countable set
bool [:{()},{((y . ()) - (y . ()))}:] is V31() V35() countable set
y +* (() .--> ((y . ()) - (y . ()))) is Relation-like Function-like set
((y,(),((y . ()) - (y . ()))),(succ (y))) is Relation-like Function-like () * () -compatible Element of product (() * ())
(y,(),((y . ()) - (y . ()))) +* (NAT .--> (succ (y))) is Relation-like Function-like set
4 is non empty ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
(y . ()) * (y . ()) is V86() integer V111() ext-real set
(y,(),((y . ()) * (y . ()))) is Relation-like Function-like () * () -compatible Element of product (() * ())
() .--> ((y . ()) * (y . ())) is Relation-like SCM-Data-Loc -defined {()} -defined Function-like one-to-one V31() countable set
{()} --> ((y . ()) * (y . ())) is non empty Relation-like {()} -defined {((y . ()) * (y . ()))} -valued Function-like constant V17({()}) V18({()},{((y . ()) * (y . ()))}) V31() countable Element of bool [:{()},{((y . ()) * (y . ()))}:]
{((y . ()) * (y . ()))} is non empty trivial V31() 1 -element countable set
[:{()},{((y . ()) * (y . ()))}:] is V31() countable set
bool [:{()},{((y . ()) * (y . ()))}:] is V31() V35() countable set
y +* (() .--> ((y . ()) * (y . ()))) is Relation-like Function-like set
((y,(),((y . ()) * (y . ()))),(succ (y))) is Relation-like Function-like () * () -compatible Element of product (() * ())
(y,(),((y . ()) * (y . ()))) +* (NAT .--> (succ (y))) is Relation-like Function-like set
5 is non empty ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
(y . ()) div (y . ()) is V86() integer V111() ext-real set
(y,(),((y . ()) div (y . ()))) is Relation-like Function-like () * () -compatible Element of product (() * ())
() .--> ((y . ()) div (y . ())) is Relation-like SCM-Data-Loc -defined {()} -defined Function-like one-to-one V31() countable set
{()} --> ((y . ()) div (y . ())) is non empty Relation-like {()} -defined {((y . ()) div (y . ()))} -valued Function-like constant V17({()}) V18({()},{((y . ()) div (y . ()))}) V31() countable Element of bool [:{()},{((y . ()) div (y . ()))}:]
{((y . ()) div (y . ()))} is non empty trivial V31() 1 -element countable set
[:{()},{((y . ()) div (y . ()))}:] is V31() countable set
bool [:{()},{((y . ()) div (y . ()))}:] is V31() V35() countable set
y +* (() .--> ((y . ()) div (y . ()))) is Relation-like Function-like set
(y . ()) mod (y . ()) is V86() integer V111() ext-real set
((y,(),((y . ()) div (y . ()))),(),((y . ()) mod (y . ()))) is Relation-like Function-like () * () -compatible Element of product (() * ())
() .--> ((y . ()) mod (y . ())) is Relation-like SCM-Data-Loc -defined {()} -defined Function-like one-to-one V31() countable set
{()} is non empty trivial V31() 1 -element countable set
{()} --> ((y . ()) mod (y . ())) is non empty Relation-like {()} -defined {((y . ()) mod (y . ()))} -valued Function-like constant V17({()}) V18({()},{((y . ()) mod (y . ()))}) V31() countable Element of bool [:{()},{((y . ()) mod (y . ()))}:]
{((y . ()) mod (y . ()))} is non empty trivial V31() 1 -element countable set
[:{()},{((y . ()) mod (y . ()))}:] is V31() countable set
bool [:{()},{((y . ()) mod (y . ()))}:] is V31() V35() countable set
(y,(),((y . ()) div (y . ()))) +* (() .--> ((y . ()) mod (y . ()))) is Relation-like Function-like set
(((y,(),((y . ()) div (y . ()))),(),((y . ()) mod (y . ()))),(succ (y))) is Relation-like Function-like () * () -compatible Element of product (() * ())
((y,(),((y . ()) div (y . ()))),(),((y . ()) mod (y . ()))) +* (NAT .--> (succ (y))) is Relation-like Function-like set
6 is non empty ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT

(y,()) is Relation-like Function-like () * () -compatible Element of product (() * ())

{()} is non empty trivial V31() V35() 1 -element countable set

7 is non empty ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT

y . () is V86() integer V111() ext-real set

IFEQ ((y . ()),0,(),(succ (y))) is ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of omega
(y,(IFEQ ((y . ()),0,(),(succ (y))))) is Relation-like Function-like () * () -compatible Element of product (() * ())
NAT .--> (IFEQ ((y . ()),0,(),(succ (y)))) is Relation-like -defined Function-like one-to-one V31() Cardinal-yielding countable set
--> (IFEQ ((y . ()),0,(),(succ (y)))) is non empty Relation-like -defined {(IFEQ ((y . ()),0,(),(succ (y))))} -valued Function-like constant V17() V18(,{(IFEQ ((y . ()),0,(),(succ (y))))}) V31() Cardinal-yielding countable V102() Element of bool [:,{(IFEQ ((y . ()),0,(),(succ (y))))}:]
{(IFEQ ((y . ()),0,(),(succ (y))))} is non empty trivial V31() V35() 1 -element countable set
[:,{(IFEQ ((y . ()),0,(),(succ (y))))}:] is V31() countable set
bool [:,{(IFEQ ((y . ()),0,(),(succ (y))))}:] is V31() V35() countable set
y +* (NAT .--> (IFEQ ((y . ()),0,(),(succ (y))))) is Relation-like Function-like set
8 is non empty ordinal natural V31() cardinal countable V86() integer V111() ext-real Element of NAT
IFGT ((y . ()),0,(),(succ (y))) is ordinal natural V31() cardinal countable V86() integer V111() ext-real set
(y,(IFGT ((y . ()),0,(),(succ (y))))) is Relation-like Function-like () * () -compatible Element of product (() * ())
NAT .--> (IFGT ((y . ()),0,(),(succ (y)))) is Relation-like -defined Function-like one-to-one V31() Cardinal-yielding countable set
--> (IFGT ((y . ()),0,(),(succ (y)))) is non empty Relation-like -defined {(IFGT ((y . ()),0,(),(succ (y))))} -valued Function-like constant V17() V18(,{(IFGT ((y . ()),0,(),(succ (y))))}) V31() Cardinal-yielding countable V102() Element of bool [:,{(IFGT ((y . ()),0,(),(succ (y))))}:]
{(IFGT ((y . ()),0,(),(succ (y))))} is non empty trivial V31() V35() 1 -element countable set
[:,{(IFGT ((y . ()),0,(),(succ (y))))}:] is V31() countable set
bool [:,{(IFGT ((y . ()),0,(),(succ (y))))}:] is V31() V35() countable set
y +* (NAT .--> (IFGT ((y . ()),0,(),(succ (y))))) is Relation-like Function-like set
k is Element of ()
c5 is Element of ()
<*k,c5*> is set
[1,{},<*k,c5*>] is V1() V2() set
[1,{}] is V1() set
{1,{}} is non empty V31() V35() countable set
{1} is non empty trivial V31() V35() 1 -element countable set
{{1,{}},{1}} is non empty V31() V35() countable set
[[1,{}],<*k,c5*>] is V1() set
{[1,{}],<*k,c5*>} is non empty V31() countable set
{[1,{}]} is non empty trivial Function-like V31() 1 -element countable set
{{[1,{}],<*k,c5*>},{[1,{}]}} is non empty V31() V35() countable set
y is Element of ()
c7 is Element of ()
<*y,c7*> is set
[2,{},<*y,c7*>] is V1() V2() set
[2,{}] is V1() set
{2,{}} is non empty V31() V35() countable set
{2} is non empty trivial V31() V35() 1 -element countable set
{{2,{}},{2}} is non empty V31() V35() countable set
[[2,{}],<*y,c7*>] is V1() set
{[2,{}],<*y,c7*>} is non empty V31() countable set
{[2,{}]} is non empty trivial Function-like V31() 1 -element countable set
{{[2,{}],<*y,c7*>},{[2,{}]}} is non empty V31() V35() countable set
z is Relation-like Function-like () * () -compatible Element of product (() * ())
c9 is Element of ()
c10 is Element of ()
<*c9,c10*> is set
[1,{},<*c9,c10*>] is V1() V2() set
[[1,{}],<*c9,c10*>] is V1() set
{[1,{}],<*c9,c10*>} is non empty V31() countable set
{{[1,{}],<*c9,c10*>},{[1,{}]}} is non empty V31() V35() countable set
c11 is Element of ()
c12 is Element of ()
<*c11,c12*> is set
[3,{},<*c11,c12*>] is V1() V2() set
[3,{}] is V1() set
{3,{}} is non empty V31() V35() countable set
{3} is non empty trivial V31() V35() 1 -element countable set
{{3,{}},{3}} is non empty V31() V35() countable set
[[3,{}],<*c11,c12*>] is V1() set
{[3,{}],<*c11,c12*>} is non empty V31() countable set
{[3,{}]} is non empty trivial Function-like V31() 1 -element countable set
{{[3,{}],<*c11,c12*>},{[3,{}]}} is non empty V31() V35() countable set
c8 is Relation-like Function-like () * () -compatible Element of product (() * ())
c14 is Element of ()
c15 is Element of ()
<*c14,c15*> is set
[1,{},<*c14,c15*>] is V1() V2() set
[[1,{}],<*c14,c15*>] is V1() set
{[1,{}],<*c14,c15*>} is non empty V31() countable set
{{[1,{}],<*c14,c15*>},{[1,{}]}} is non empty V31() V35() countable set
c16 is Element of ()
c17 is Element of ()
<*c16,c17*> is set
[4,{},<*c16,c17*>] is V1() V2() set
[4,{}] is V1() set
{4,{}} is non empty V31() V35() countable set
{4} is non empty trivial V31() V35() 1 -element countable set
{{4,{}},{4}} is non empty V31() V35() countable set
[[4,{}],<*c16,c17*>] is V1() set
{[4,{}],<*c16,c17*>} is non empty V31() countable set
{[4,{}]} is non empty trivial Function-like V31() 1 -element countable set
{{[4,{}],<*c16,c17*>},{[4,{}]}} is non empty V31() V35() countable set
c13 is Relation-like Function-like () * () -compatible Element of product (() * ())
c19 is Element of ()
c20 is Element of ()
<*c19,c20*> is set
[1,{},<*c19,c20*>] is V1() V2() set
[[1,{}],<*c19,c20*>] is V1() set
{[1,{}],<*c19,c20*>} is non empty V31() countable set
{{[1,{}],<*c19,c20*>},{[1,{}]}} is non empty V31() V35() countable set
c21 is Element of ()
c22 is Element of ()
<*c21,c22*> is set
[5,{},<*c21,c22*>] is V1() V2() set
[5,{}] is V1() set
{5,{}} is non empty V31() V35() countable set
{5} is non empty trivial V31() V35() 1 -element countable set
{{5,{}},{5}} is non empty V31() V35() countable set
[[5,{}],<*c21,c22*>] is V1() set
{[5,{}],<*c21,c22*>} is non empty V31() countable set
{[5,{}]} is non empty trivial Function-like V31() 1 -element countable set
{{[5,{}],<*c21,c22*>},{[5,{}]}} is non empty V31() V35() countable set
c18 is Relation-like Function-like () * () -compatible Element of product (() * ())
c24 is Element of ()
c25 is Element of ()
<*c24,c25*> is set
[1,{},<*c24,c25*>] is V1() V2() set
[[1,{}],<*c24,c25*>] is V1() set
{[1,{}],<*c24,c25*>} is non empty V31() countable set
{{[1,{}],<*c24,c25*>},{[1,{}]}} is non empty V31() V35() countable set

[6,<*c26*>,{}] is V1() V2() set
[6,<*c26*>] is V1() set
{6,<*c26*>} is non empty V31() countable set
{6} is non empty trivial V31() V35() 1 -element countable set
{{6,<*c26*>},{6}} is non empty V31() V35() countable set
[[6,<*c26*>],{}] is V1() set
{[6,<*c26*>],{}} is non empty V31() countable set
{[6,<*c26*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[6,<*c26*>],{}},{[6,<*c26*>]}} is non empty V31() V35() countable set
c23 is Relation-like Function-like () * () -compatible Element of product (() * ())
c28 is Element of ()
c29 is Element of ()
<*c28,c29*> is set
[1,{},<*c28,c29*>] is V1() V2() set
[[1,{}],<*c28,c29*>] is V1() set
{[1,{}],<*c28,c29*>} is non empty V31() countable set
{{[1,{}],<*c28,c29*>},{[1,{}]}} is non empty V31() V35() countable set

c31 is Element of ()

[7,<*c30*>,<*c31*>] is V1() V2() set
[7,<*c30*>] is V1() set
{7,<*c30*>} is non empty V31() countable set
{7} is non empty trivial V31() V35() 1 -element countable set
{{7,<*c30*>},{7}} is non empty V31() V35() countable set
[[7,<*c30*>],<*c31*>] is V1() set
{[7,<*c30*>],<*c31*>} is non empty V31() countable set
{[7,<*c30*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[7,<*c30*>],<*c31*>},{[7,<*c30*>]}} is non empty V31() V35() countable set
c27 is Relation-like Function-like () * () -compatible Element of product (() * ())
c33 is Element of ()
c34 is Element of ()
<*c33,c34*> is set
[1,{},<*c33,c34*>] is V1() V2() set
[[1,{}],<*c33,c34*>] is V1() set
{[1,{}],<*c33,c34*>} is non empty V31() countable set
{{[1,{}],<*c33,c34*>},{[1,{}]}} is non empty V31() V35() countable set

c36 is Element of ()

[8,<*c35*>,<*c36*>] is V1() V2() set
[8,<*c35*>] is V1() set
{8,<*c35*>} is non empty V31() countable set
{8} is non empty trivial V31() V35() 1 -element countable set
{{8,<*c35*>},{8}} is non empty V31() V35() countable set
[[8,<*c35*>],<*c36*>] is V1() set
{[8,<*c35*>],<*c36*>} is non empty V31() countable set
{[8,<*c35*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[8,<*c35*>],<*c36*>},{[8,<*c35*>]}} is non empty V31() V35() countable set
c32 is Relation-like Function-like () * () -compatible Element of product (() * ())
c38 is Element of ()
c39 is Element of ()
<*c38,c39*> is set
[2,{},<*c38,c39*>] is V1() V2() set
[[2,{}],<*c38,c39*>] is V1() set
{[2,{}],<*c38,c39*>} is non empty V31() countable set
{{[2,{}],<*c38,c39*>},{[2,{}]}} is non empty V31() V35() countable set
c40 is Element of ()
c41 is Element of ()
<*c40,c41*> is set
[3,{},<*c40,c41*>] is V1() V2() set
[[3,{}],<*c40,c41*>] is V1() set
{[3,{}],<*c40,c41*>} is non empty V31() countable set
{{[3,{}],<*c40,c41*>},{[3,{}]}} is non empty V31() V35() countable set
c37 is Relation-like Function-like () * () -compatible Element of product (() * ())
c43 is Element of ()
c44 is Element of ()
<*c43,c44*> is set
[2,{},<*c43,c44*>] is V1() V2() set
[[2,{}],<*c43,c44*>] is V1() set
{[2,{}],<*c43,c44*>} is non empty V31() countable set
{{[2,{}],<*c43,c44*>},{[2,{}]}} is non empty V31() V35() countable set
c45 is Element of ()
c46 is Element of ()
<*c45,c46*> is set
[4,{},<*c45,c46*>] is V1() V2() set
[[4,{}],<*c45,c46*>] is V1() set
{[4,{}],<*c45,c46*>} is non empty V31() countable set
{{[4,{}],<*c45,c46*>},{[4,{}]}} is non empty V31() V35() countable set
c42 is Relation-like Function-like () * () -compatible Element of product (() * ())
c48 is Element of ()
c49 is Element of ()
<*c48,c49*> is set
[2,{},<*c48,c49*>] is V1() V2() set
[[2,{}],<*c48,c49*>] is V1() set
{[2,{}],<*c48,c49*>} is non empty V31() countable set
{{[2,{}],<*c48,c49*>},{[2,{}]}} is non empty V31() V35() countable set
c50 is Element of ()
c51 is Element of ()
<*c50,c51*> is set
[5,{},<*c50,c51*>] is V1() V2() set
[[5,{}],<*c50,c51*>] is V1() set
{[5,{}],<*c50,c51*>} is non empty V31() countable set
{{[5,{}],<*c50,c51*>},{[5,{}]}} is non empty V31() V35() countable set
c47 is Relation-like Function-like () * () -compatible Element of product (() * ())
c53 is Element of ()
c54 is Element of ()
<*c53,c54*> is set
[2,{},<*c53,c54*>] is V1() V2() set
[[2,{}],<*c53,c54*>] is V1() set
{[2,{}],<*c53,c54*>} is non empty V31() countable set
{{[2,{}],<*c53,c54*>},{[2,{}]}} is non empty V31() V35() countable set

[6,<*c55*>,{}] is V1() V2() set
[6,<*c55*>] is V1() set
{6,<*c55*>} is non empty V31() countable set
{{6,<*c55*>},{6}} is non empty V31() V35() countable set
[[6,<*c55*>],{}] is V1() set
{[6,<*c55*>],{}} is non empty V31() countable set
{[6,<*c55*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[6,<*c55*>],{}},{[6,<*c55*>]}} is non empty V31() V35() countable set
c52 is Relation-like Function-like () * () -compatible Element of product (() * ())
c57 is Element of ()
c58 is Element of ()
<*c57,c58*> is set
[2,{},<*c57,c58*>] is V1() V2() set
[[2,{}],<*c57,c58*>] is V1() set
{[2,{}],<*c57,c58*>} is non empty V31() countable set
{{[2,{}],<*c57,c58*>},{[2,{}]}} is non empty V31() V35() countable set

c60 is Element of ()

[7,<*c59*>,<*c60*>] is V1() V2() set
[7,<*c59*>] is V1() set
{7,<*c59*>} is non empty V31() countable set
{{7,<*c59*>},{7}} is non empty V31() V35() countable set
[[7,<*c59*>],<*c60*>] is V1() set
{[7,<*c59*>],<*c60*>} is non empty V31() countable set
{[7,<*c59*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[7,<*c59*>],<*c60*>},{[7,<*c59*>]}} is non empty V31() V35() countable set
c56 is Relation-like Function-like () * () -compatible Element of product (() * ())
c62 is Element of ()
c63 is Element of ()
<*c62,c63*> is set
[2,{},<*c62,c63*>] is V1() V2() set
[[2,{}],<*c62,c63*>] is V1() set
{[2,{}],<*c62,c63*>} is non empty V31() countable set
{{[2,{}],<*c62,c63*>},{[2,{}]}} is non empty V31() V35() countable set

c65 is Element of ()

[8,<*c64*>,<*c65*>] is V1() V2() set
[8,<*c64*>] is V1() set
{8,<*c64*>} is non empty V31() countable set
{{8,<*c64*>},{8}} is non empty V31() V35() countable set
[[8,<*c64*>],<*c65*>] is V1() set
{[8,<*c64*>],<*c65*>} is non empty V31() countable set
{[8,<*c64*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[8,<*c64*>],<*c65*>},{[8,<*c64*>]}} is non empty V31() V35() countable set
c61 is Relation-like Function-like () * () -compatible Element of product (() * ())
c67 is Element of ()
c68 is Element of ()
<*c67,c68*> is set
[3,{},<*c67,c68*>] is V1() V2() set
[[3,{}],<*c67,c68*>] is V1() set
{[3,{}],<*c67,c68*>} is non empty V31() countable set
{{[3,{}],<*c67,c68*>},{[3,{}]}} is non empty V31() V35() countable set
c69 is Element of ()
c70 is Element of ()
<*c69,c70*> is set
[4,{},<*c69,c70*>] is V1() V2() set
[[4,{}],<*c69,c70*>] is V1() set
{[4,{}],<*c69,c70*>} is non empty V31() countable set
{{[4,{}],<*c69,c70*>},{[4,{}]}} is non empty V31() V35() countable set
c66 is Relation-like Function-like () * () -compatible Element of product (() * ())
c72 is Element of ()
c73 is Element of ()
<*c72,c73*> is set
[3,{},<*c72,c73*>] is V1() V2() set
[[3,{}],<*c72,c73*>] is V1() set
{[3,{}],<*c72,c73*>} is non empty V31() countable set
{{[3,{}],<*c72,c73*>},{[3,{}]}} is non empty V31() V35() countable set
c74 is Element of ()
c75 is Element of ()
<*c74,c75*> is set
[5,{},<*c74,c75*>] is V1() V2() set
[[5,{}],<*c74,c75*>] is V1() set
{[5,{}],<*c74,c75*>} is non empty V31() countable set
{{[5,{}],<*c74,c75*>},{[5,{}]}} is non empty V31() V35() countable set
c71 is Relation-like Function-like () * () -compatible Element of product (() * ())
c77 is Element of ()
c78 is Element of ()
<*c77,c78*> is set
[3,{},<*c77,c78*>] is V1() V2() set
[[3,{}],<*c77,c78*>] is V1() set
{[3,{}],<*c77,c78*>} is non empty V31() countable set
{{[3,{}],<*c77,c78*>},{[3,{}]}} is non empty V31() V35() countable set

[6,<*c79*>,{}] is V1() V2() set
[6,<*c79*>] is V1() set
{6,<*c79*>} is non empty V31() countable set
{{6,<*c79*>},{6}} is non empty V31() V35() countable set
[[6,<*c79*>],{}] is V1() set
{[6,<*c79*>],{}} is non empty V31() countable set
{[6,<*c79*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[6,<*c79*>],{}},{[6,<*c79*>]}} is non empty V31() V35() countable set
c76 is Relation-like Function-like () * () -compatible Element of product (() * ())
c81 is Element of ()
c82 is Element of ()
<*c81,c82*> is set
[3,{},<*c81,c82*>] is V1() V2() set
[[3,{}],<*c81,c82*>] is V1() set
{[3,{}],<*c81,c82*>} is non empty V31() countable set
{{[3,{}],<*c81,c82*>},{[3,{}]}} is non empty V31() V35() countable set

c84 is Element of ()

[7,<*c83*>,<*c84*>] is V1() V2() set
[7,<*c83*>] is V1() set
{7,<*c83*>} is non empty V31() countable set
{{7,<*c83*>},{7}} is non empty V31() V35() countable set
[[7,<*c83*>],<*c84*>] is V1() set
{[7,<*c83*>],<*c84*>} is non empty V31() countable set
{[7,<*c83*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[7,<*c83*>],<*c84*>},{[7,<*c83*>]}} is non empty V31() V35() countable set
c80 is Relation-like Function-like () * () -compatible Element of product (() * ())
c86 is Element of ()
c87 is Element of ()
<*c86,c87*> is set
[3,{},<*c86,c87*>] is V1() V2() set
[[3,{}],<*c86,c87*>] is V1() set
{[3,{}],<*c86,c87*>} is non empty V31() countable set
{{[3,{}],<*c86,c87*>},{[3,{}]}} is non empty V31() V35() countable set

c89 is Element of ()

[8,<*c88*>,<*c89*>] is V1() V2() set
[8,<*c88*>] is V1() set
{8,<*c88*>} is non empty V31() countable set
{{8,<*c88*>},{8}} is non empty V31() V35() countable set
[[8,<*c88*>],<*c89*>] is V1() set
{[8,<*c88*>],<*c89*>} is non empty V31() countable set
{[8,<*c88*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[8,<*c88*>],<*c89*>},{[8,<*c88*>]}} is non empty V31() V35() countable set
c85 is Relation-like Function-like () * () -compatible Element of product (() * ())
c91 is Element of ()
c92 is Element of ()
<*c91,c92*> is set
[4,{},<*c91,c92*>] is V1() V2() set
[[4,{}],<*c91,c92*>] is V1() set
{[4,{}],<*c91,c92*>} is non empty V31() countable set
{{[4,{}],<*c91,c92*>},{[4,{}]}} is non empty V31() V35() countable set
c93 is Element of ()
c94 is Element of ()
<*c93,c94*> is set
[5,{},<*c93,c94*>] is V1() V2() set
[[5,{}],<*c93,c94*>] is V1() set
{[5,{}],<*c93,c94*>} is non empty V31() countable set
{{[5,{}],<*c93,c94*>},{[5,{}]}} is non empty V31() V35() countable set
c90 is Relation-like Function-like () * () -compatible Element of product (() * ())
c96 is Element of ()
c97 is Element of ()
<*c96,c97*> is set
[4,{},<*c96,c97*>] is V1() V2() set
[[4,{}],<*c96,c97*>] is V1() set
{[4,{}],<*c96,c97*>} is non empty V31() countable set
{{[4,{}],<*c96,c97*>},{[4,{}]}} is non empty V31() V35() countable set

[6,<*c98*>,{}] is V1() V2() set
[6,<*c98*>] is V1() set
{6,<*c98*>} is non empty V31() countable set
{{6,<*c98*>},{6}} is non empty V31() V35() countable set
[[6,<*c98*>],{}] is V1() set
{[6,<*c98*>],{}} is non empty V31() countable set
{[6,<*c98*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[6,<*c98*>],{}},{[6,<*c98*>]}} is non empty V31() V35() countable set
c95 is Relation-like Function-like () * () -compatible Element of product (() * ())
c100 is Element of ()
c101 is Element of ()
<*c100,c101*> is set
[4,{},<*c100,c101*>] is V1() V2() set
[[4,{}],<*c100,c101*>] is V1() set
{[4,{}],<*c100,c101*>} is non empty V31() countable set
{{[4,{}],<*c100,c101*>},{[4,{}]}} is non empty V31() V35() countable set

c103 is Element of ()

[7,<*c102*>,<*c103*>] is V1() V2() set
[7,<*c102*>] is V1() set
{7,<*c102*>} is non empty V31() countable set
{{7,<*c102*>},{7}} is non empty V31() V35() countable set
[[7,<*c102*>],<*c103*>] is V1() set
{[7,<*c102*>],<*c103*>} is non empty V31() countable set
{[7,<*c102*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[7,<*c102*>],<*c103*>},{[7,<*c102*>]}} is non empty V31() V35() countable set
c99 is Relation-like Function-like () * () -compatible Element of product (() * ())
c105 is Element of ()
c106 is Element of ()
<*c105,c106*> is set
[4,{},<*c105,c106*>] is V1() V2() set
[[4,{}],<*c105,c106*>] is V1() set
{[4,{}],<*c105,c106*>} is non empty V31() countable set
{{[4,{}],<*c105,c106*>},{[4,{}]}} is non empty V31() V35() countable set

c108 is Element of ()

[8,<*c107*>,<*c108*>] is V1() V2() set
[8,<*c107*>] is V1() set
{8,<*c107*>} is non empty V31() countable set
{{8,<*c107*>},{8}} is non empty V31() V35() countable set
[[8,<*c107*>],<*c108*>] is V1() set
{[8,<*c107*>],<*c108*>} is non empty V31() countable set
{[8,<*c107*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[8,<*c107*>],<*c108*>},{[8,<*c107*>]}} is non empty V31() V35() countable set
c104 is Relation-like Function-like () * () -compatible Element of product (() * ())
c110 is Element of ()
c111 is Element of ()
<*c110,c111*> is set
[5,{},<*c110,c111*>] is V1() V2() set
[[5,{}],<*c110,c111*>] is V1() set
{[5,{}],<*c110,c111*>} is non empty V31() countable set
{{[5,{}],<*c110,c111*>},{[5,{}]}} is non empty V31() V35() countable set

[6,<*c112*>,{}] is V1() V2() set
[6,<*c112*>] is V1() set
{6,<*c112*>} is non empty V31() countable set
{{6,<*c112*>},{6}} is non empty V31() V35() countable set
[[6,<*c112*>],{}] is V1() set
{[6,<*c112*>],{}} is non empty V31() countable set
{[6,<*c112*>]} is non empty trivial Function-like V31() 1 -element countable set
{{[6,<*c112*>],{}},{[6,<*c112*>]}} is non empty V31() V35() countable set
c109 is Relation-like Function-like () * () -compatible Element of product (() * ())
c114 is Element of ()
c115 is Element of ()
<*c114,c115*> is set
[5,{},<*c114,c115*>] is V1() V2() set
[[5,{}],<*c114,c115*>] is V1() set
{[5,{}],<*c114,c115*>} is non empty V31() countable set
{{[5,{}],<*c114,c115*>},{[5,{}]}} is non empty V31() V35() countable set

c117 is Element of ()

[7,<*c116*>,<*c117*>] is V1() V2() set
[7,<*c116*>] is V1() set
{7,<*c116*>} is non empty V31() countable