:: MULTOP_1 semantic presentation

f is V1() Function-like set

a is set

b is set

c is set

[a,b,c] is V15() V16() set

K83(a,b) is V15() set

K83(K83(a,b),c) is V15() set

f . [a,b,c] is set

f is non empty set

a is non empty set

b is non empty set

[:f,a,b:] is non empty set

c is non empty set

[:[:f,a,b:],c:] is non empty set

bool [:[:f,a,b:],c:] is non empty set

d is V1() V4([:f,a,b:]) V5(c) Function-like V18([:f,a,b:],c) Element of bool [:[:f,a,b:],c:]

c

z1 is Element of a

y1 is Element of b

(d,c

[c

K83(c

K83(K83(c

d . [c

[c

d . [c

f is non empty set

a is set

b is set

c is set

[:a,b,c:] is set

[:[:a,b,c:],f:] is set

bool [:[:a,b,c:],f:] is non empty set

d is V1() V4([:a,b,c:]) V5(f) Function-like V18([:a,b,c:],f) Element of bool [:[:a,b,c:],f:]

c

z1 is set

d . z1 is set

c

y1 is set

x1 is set

t is set

[y1,x1,t] is V15() V16() set

K83(y1,x1) is V15() set

K83(K83(y1,x1),t) is V15() set

f is non empty set

a is non empty set

b is non empty set

[:f,a,b:] is non empty set

c is non empty set

[:[:f,a,b:],c:] is non empty set

bool [:[:f,a,b:],c:] is non empty set

d is V1() V4([:f,a,b:]) V5(c) Function-like V18([:f,a,b:],c) Element of bool [:[:f,a,b:],c:]

c

z1 is set

y1 is set

x1 is set

[z1,y1,x1] is V15() V16() set

K83(z1,y1) is V15() set

K83(K83(z1,y1),x1) is V15() set

d . [z1,y1,x1] is set

c

f is non empty set

a is non empty set

b is non empty set

[:f,a,b:] is non empty set

c is non empty set

[:[:f,a,b:],c:] is non empty set

bool [:[:f,a,b:],c:] is non empty set

d is V1() V4([:f,a,b:]) V5(c) Function-like V18([:f,a,b:],c) Element of bool [:[:f,a,b:],c:]

c

z1 is Element of f

y1 is Element of a

x1 is Element of b

[z1,y1,x1] is V15() V16() Element of [:f,a,b:]

K83(z1,y1) is V15() set

K83(K83(z1,y1),x1) is V15() set

d . [z1,y1,x1] is Element of c

c

(f,a,b,c,d,z1,y1,x1) is Element of c

[z1,y1,x1] is V15() V16() set

d . [z1,y1,x1] is set

(f,a,b,c,c

c

F

F

F

F

[:F

[:[:F

bool [:[:F

f is Element of [:F

a is set

b is set

c is set

[a,b,c] is V15() V16() set

K83(a,b) is V15() set

K83(K83(a,b),c) is V15() set

z1 is Element of F

c

d is Element of F

y1 is Element of F

x1 is Element of F

t is Element of F

x is Element of F

[x1,t,x] is V15() V16() Element of [:F

K83(x1,t) is V15() set

K83(K83(x1,t),x) is V15() set

f is V1() V4([:F

a is Element of F

b is Element of F

c is Element of F

[a,b,c] is V15() V16() Element of [:F

K83(a,b) is V15() set

K83(K83(a,b),c) is V15() set

f . [a,b,c] is Element of F

F

[:F

[:[:F

bool [:[:F

f is Element of F

a is Element of F

b is Element of F

c is Element of F

d is Element of F

f is V1() V4([:F

a is Element of F

b is Element of F

c is Element of F

(F

[a,b,c] is V15() V16() set

K83(a,b) is V15() set

K83(K83(a,b),c) is V15() set

f . [a,b,c] is set

F

F

F

F

[:F

[:[:F

bool [:[:F

f is Element of F

a is Element of F

b is Element of F

F

f is V1() V4([:F

F

F

F

F

[:F

[:[:F

bool [:[:F

f is V1() V4([:F

a is Element of F

b is Element of F

c is Element of F

(F

[a,b,c] is V15() V16() set

K83(a,b) is V15() set

K83(K83(a,b),c) is V15() set

f . [a,b,c] is set

F

f is V1() Function-like set

a is set

b is set

c is set

d is set

[a,b,c,d] is V15() V16() V17() set

[a,b,c] is V15() V16() set

K83(a,b) is V15() set

K83(K83(a,b),c) is V15() set

K83([a,b,c],d) is V15() set

f . [a,b,c,d] is set

f is non empty set

a is non empty set

b is non empty set

c is non empty set

[:f,a,b,c:] is non empty set

d is non empty set

[:[:f,a,b,c:],d:] is non empty set

bool [:[:f,a,b,c:],d:] is non empty set

c

z1 is Element of f

y1 is Element of a

x1 is Element of b

t is Element of c

(c

[z1,y1,x1,t] is V15() V16() V17() set

[z1,y1,x1] is V15() V16() set

K83(z1,y1) is V15() set

K83(K83(z1,y1),x1) is V15() set

K83([z1,y1,x1],t) is V15() set

c

[z1,y1,x1,t] is V15() V16() V17() Element of [:f,a,b,c:]

c

f is non empty set

a is set

b is set

c is set

d is set

[:a,b,c,d:] is set

[:[:a,b,c,d:],f:] is set

bool [:[:a,b,c,d:],f:] is non empty set

c

z1 is V1() V4([:a,b,c,d:]) V5(f) Function-like V18([:a,b,c,d:],f) Element of bool [:[:a,b,c,d:],f:]

y1 is set

c

z1 . y1 is set

x1 is set

t is set

x is set

y is set

[x1,t,x,y] is V15() V16() V17() set

[x1,t,x] is V15() V16() set

K83(x1,t) is V15() set

K83(K83(x1,t),x) is V15() set

K83([x1,t,x],y) is V15() set

f is non empty set

a is non empty set

b is non empty set

c is non empty set

[:f,a,b,c:] is non empty set

d is non empty set

[:[:f,a,b,c:],d:] is non empty set

bool [:[:f,a,b,c:],d:] is non empty set

c

z1 is V1() V4([:f,a,b,c:]) V5(d) Function-like V18([:f,a,b,c:],d) Element of bool [:[:f,a,b,c:],d:]

y1 is set

x1 is set

t is set

x is set

[y1,x1,t,x] is V15() V16() V17() set

[y1,x1,t] is V15() V16() set

K83(y1,x1) is V15() set

K83(K83(y1,x1),t) is V15() set

K83([y1,x1,t],x) is V15() set

c

z1 . [y1,x1,t,x] is set

f is non empty set

a is non empty set

b is non empty set

c is non empty set

[:f,a,b,c:] is non empty set

d is non empty set

[:[:f,a,b,c:],d:] is non empty set

bool [:[:f,a,b,c:],d:] is non empty set

c

z1 is V1() V4([:f,a,b,c:]) V5(d) Function-like V18([:f,a,b,c:],d) Element of bool [:[:f,a,b,c:],d:]

y1 is Element of f

x1 is Element of a

t is Element of b

x is Element of c

[y1,x1,t,x] is V15() V16() V17() Element of [:f,a,b,c:]

[y1,x1,t] is V15() V16() set

K83(y1,x1) is V15() set

K83(K83(y1,x1),t) is V15() set

K83([y1,x1,t],x) is V15() set

c

z1 . [y1,x1,t,x] is Element of d

(f,a,b,c,d,c

[y1,x1,t,x] is V15() V16() V17() set

c

(f,a,b,c,d,z1,y1,x1,t,x) is Element of d

z1 . [y1,x1,t,x] is set

F

F

F

F

F

[:F

[:[:F

bool [:[:F

f is Element of [:F

a is set

b is set

c is set

d is set

[a,b,c,d] is V15() V16() V17() set

[a,b,c] is V15() V16() set

K83(a,b) is V15() set

K83(K83(a,b),c) is V15() set

K83([a,b,c],d) is V15() set

x1 is Element of F

y1 is Element of F

z1 is Element of F

c

t is Element of F

x is Element of F

y is Element of F

z is Element of F

s is Element of F

[x,y,z,s] is V15() V16() V17() Element of [:F

[x,y,z] is V15() V16() set

K83(x,y) is V15() set

K83(K83(x,y),z) is V15() set

K83([x,y,z],s) is V15() set

f is V1() V4([:F

a is Element of F

b is Element of F

c is Element of F

d is Element of F

[a,b,c,d] is V15() V16() V17() Element of [:F

[a,b,c] is V15() V16() set

K83(a,b) is V15() set

K83(K83(a,b),c) is V15() set

K83([a,b,c],d) is V15() set

f . [a,b,c,d] is Element of F

F

[:F

[:[:F

bool [:[:F

f is Element of F

a is Element of F

b is Element of F

c is Element of F

d is Element of F

c

f is V1() V4([:F

a is Element of F

b is Element of F

c is Element of F

d is Element of F

(F

[a,b,c,d] is V15() V16() V17() set

[a,b,c] is V15() V16() set

K83(a,b) is V15() set

K83(K83(a,b),c) is V15() set

K83([a,b,c],d) is V15() set

f . [a,b,c,d] is set

F

F

F

F

F

[:F

[:[:F

bool [:[:F

f is Element of F

a is Element of F

b is Element of F

c is Element of F

F

f is V1() V4([:F

F

[:F

[:[:F

bool [:[:F

f is V1() V4([:F

a is Element of F

b is Element of F

c is Element of F

d is Element of F

(F

[a,b,c,d] is V15() V16() V17() set

[a,b,c] is V15() V16() set

K83(a,b) is V15() set

K83(K83(a,b),c) is V15() set

K83([a,b,c],d) is V15() set

f . [a,b,c,d] is set

F