begin
scheme
Fraenkel59{
F1()
-> set ,
F2(
set )
-> set ,
P1[
set ],
P2[
set ] } :
{ F2(v) where v is Element of F1() : P1[v] } c= { F2(u) where u is Element of F1() : P2[u] }
provided
A1:
for
v being
Element of
F1() st
P1[
v] holds
P2[
v]
scheme
Fraenkel599{
F1()
-> set ,
F2()
-> set ,
F3(
set ,
set )
-> set ,
P1[
set ,
set ],
P2[
set ,
set ] } :
{ F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } c= { F3(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2] }
provided
A1:
for
u being
Element of
F1()
for
v being
Element of
F2() st
P1[
u,
v] holds
P2[
u,
v]
scheme
Fraenkel69{
F1()
-> set ,
F2(
set )
-> set ,
P1[
set ],
P2[
set ] } :
{ F2(v1) where v1 is Element of F1() : P1[v1] } = { F2(v2) where v2 is Element of F1() : P2[v2] }
provided
A1:
for
v being
Element of
F1() holds
(
P1[
v] iff
P2[
v] )
scheme
Fraenkel699{
F1()
-> set ,
F2()
-> set ,
F3(
set ,
set )
-> set ,
P1[
set ,
set ],
P2[
set ,
set ] } :
{ F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } = { F3(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2] }
provided
A1:
for
u being
Element of
F1()
for
v being
Element of
F2() holds
(
P1[
u,
v] iff
P2[
u,
v] )
scheme
FraenkelF9{
F1()
-> set ,
F2(
set )
-> set ,
F3(
set )
-> set ,
P1[
set ] } :
{ F2(v1) where v1 is Element of F1() : P1[v1] } = { F3(v2) where v2 is Element of F1() : P1[v2] }
provided
A1:
for
v being
Element of
F1() holds
F2(
v)
= F3(
v)
scheme
FraenkelF9R{
F1()
-> set ,
F2(
set )
-> set ,
F3(
set )
-> set ,
P1[
set ] } :
{ F2(v1) where v1 is Element of F1() : P1[v1] } = { F3(v2) where v2 is Element of F1() : P1[v2] }
provided
A1:
for
v being
Element of
F1() st
P1[
v] holds
F2(
v)
= F3(
v)
scheme
FraenkelF99{
F1()
-> set ,
F2()
-> set ,
F3(
set ,
set )
-> set ,
F4(
set ,
set )
-> set ,
P1[
set ,
set ] } :
{ F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } = { F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2] }
provided
A1:
for
u being
Element of
F1()
for
v being
Element of
F2() holds
F3(
u,
v)
= F4(
u,
v)
scheme
FraenkelF699{
F1()
-> set ,
F2()
-> set ,
F3(
set ,
set )
-> set ,
P1[
set ,
set ],
P2[
set ,
set ] } :
{ F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } = { F3(v2,u2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2] }
provided
A1:
for
u being
Element of
F1()
for
v being
Element of
F2() holds
(
P1[
u,
v] iff
P2[
u,
v] )
and A2:
for
u being
Element of
F1()
for
v being
Element of
F2() holds
F3(
u,
v)
= F3(
v,
u)
scheme
RelevantArgs{
F1()
-> set ,
F2()
-> set ,
F3()
-> set ,
F4()
-> Function of
F1(),
F2(),
F5()
-> Function of
F1(),
F2(),
P1[
set ],
P2[
set ] } :
{ (F4() . u9) where u9 is Element of F1() : ( P1[u9] & u9 in F3() ) } = { (F5() . v9) where v9 is Element of F1() : ( P2[v9] & v9 in F3() ) }
provided
A1:
F4()
| F3()
= F5()
| F3()
and A2:
for
u being
Element of
F1() st
u in F3() holds
(
P1[
u] iff
P2[
u] )
scheme
Gen199{
F1()
-> set ,
F2()
-> set ,
F3(
set ,
set )
-> set ,
P1[
set ,
set ],
P2[
set ] } :
for
s being
Element of
F1()
for
t being
Element of
F2() st
P1[
s,
t] holds
P2[
F3(
s,
t)]
provided
A1:
for
st1 being
set st
st1 in { F3(s1,t1) where s1 is Element of F1(), t1 is Element of F2() : P1[s1,t1] } holds
P2[
st1]
scheme
Gen199A{
F1()
-> set ,
F2()
-> set ,
F3(
set ,
set )
-> set ,
P1[
set ,
set ],
P2[
set ] } :
for
st1 being
set st
st1 in { F3(s1,t1) where s1 is Element of F1(), t1 is Element of F2() : P1[s1,t1] } holds
P2[
st1]
provided
A1:
for
s being
Element of
F1()
for
t being
Element of
F2() st
P1[
s,
t] holds
P2[
F3(
s,
t)]
scheme
Gen299{
F1()
-> set ,
F2()
-> set ,
F3()
-> set ,
F4(
set ,
set )
-> Element of
F3(),
P1[
set ,
set ],
P2[
set ] } :
{ st1 where st1 is Element of F3() : ( st1 in { F4(s1,t1) where s1 is Element of F1(), t1 is Element of F2() : P1[s1,t1] } & P2[st1] ) } = { F4(s2,t2) where s2 is Element of F1(), t2 is Element of F2() : ( P1[s2,t2] & P2[F4(s2,t2)] ) }
scheme
Gen39{
F1()
-> set ,
F2(
set )
-> set ,
P1[
set ],
P2[
set ] } :
{ F2(s) where s is Element of F1() : ( s in { s1 where s1 is Element of F1() : P2[s1] } & P1[s] ) } = { F2(s2) where s2 is Element of F1() : ( P2[s2] & P1[s2] ) }
scheme
Gen399{
F1()
-> set ,
F2()
-> set ,
F3(
set ,
set )
-> set ,
P1[
set ,
set ],
P2[
set ] } :
{ F3(s,t) where s is Element of F1(), t is Element of F2() : ( s in { s1 where s1 is Element of F1() : P2[s1] } & P1[s,t] ) } = { F3(s2,t2) where s2 is Element of F1(), t2 is Element of F2() : ( P2[s2] & P1[s2,t2] ) }
scheme
Gen499{
F1()
-> set ,
F2()
-> set ,
F3(
set ,
set )
-> set ,
P1[
set ,
set ],
P2[
set ,
set ] } :
{ F3(s,t) where s is Element of F1(), t is Element of F2() : P1[s,t] } c= { F3(s1,t1) where s1 is Element of F1(), t1 is Element of F2() : P2[s1,t1] }
provided
A1:
for
s being
Element of
F1()
for
t being
Element of
F2() st
P1[
s,
t] holds
ex
s9 being
Element of
F1() st
(
P2[
s9,
t] &
F3(
s,
t)
= F3(
s9,
t) )
scheme
FrEqua1{
F1()
-> set ,
F2()
-> set ,
F3(
set ,
set )
-> set ,
F4()
-> Element of
F2(),
P1[
set ,
set ],
P2[
set ,
set ] } :
{ F3(s,t) where s is Element of F1(), t is Element of F2() : P2[s,t] } = { F3(s9,F4()) where s9 is Element of F1() : P1[s9,F4()] }
provided
A1:
for
s being
Element of
F1()
for
t being
Element of
F2() holds
(
P2[
s,
t] iff (
t = F4() &
P1[
s,
t] ) )
scheme
FrEqua2{
F1()
-> set ,
F2()
-> set ,
F3(
set ,
set )
-> set ,
F4()
-> Element of
F2(),
P1[
set ,
set ] } :
{ F3(s,t) where s is Element of F1(), t is Element of F2() : ( t = F4() & P1[s,t] ) } = { F3(s9,F4()) where s9 is Element of F1() : P1[s9,F4()] }
scheme
Finiteness{
F1()
-> non
empty set ,
F2()
-> Element of
Fin F1(),
P1[
Element of
F1(),
Element of
F1()] } :
for
x being
Element of
F1() st
x in F2() holds
ex
y being
Element of
F1() st
(
y in F2() &
P1[
y,
x] & ( for
z being
Element of
F1() st
z in F2() &
P1[
z,
y] holds
P1[
y,
z] ) )
provided
A1:
for
x being
Element of
F1() holds
P1[
x,
x]
and A2:
for
x,
y,
z being
Element of
F1() st
P1[
x,
y] &
P1[
y,
z] holds
P1[
x,
z]