Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

Schemes

by
Stanislaw T. Czuba

MML identifier: SCHEMS_1
[ Mizar article, MML identifier index ]

```environ

constructors XBOOLE_0;
clusters XBOOLE_0;

begin

reserve a,b,d for set;

scheme Schemat0 {P[set]} :
ex a st P[a]
provided
for a holds P[a];

scheme Schemat1a {P[set],T[]} :
(for a holds P[a]) & T[]
provided
for a holds (P[a] & T[]);

scheme Schemat1b {P[set],T[]} :
for a holds (P[a] & T[])
provided
(for a holds P[a]) & T[];

scheme Schemat2a {P[set], T[]} :
(ex a st P[a]) or T[]
provided
ex a st (P[a] or T[]);

scheme Schemat2b {P[set], T[]} :
ex a st (P[a] or T[])
provided
(ex a st P[a]) or T[];

scheme Schemat3 {S[set,set]} :
for b ex a st S[a,b]
provided
ex a st for b holds S[a,b];

scheme Schemat4a {P[set],Q[set]} :
(ex a st P[a]) or (ex a st Q[a])
provided
ex a st (P[a] or Q[a]);

scheme Schemat4b {P[set],Q[set]} :
ex a st (P[a] or Q[a])
provided
(ex a st P[a]) or (ex a st Q[a]);

scheme Schemat5 {P[set],Q[set]} :
(ex a st P[a]) & (ex a st Q[a])
provided
ex a st (P[a] & Q[a]);

scheme Schemat6a {P[set],Q[set]} :
(for a holds P[a]) & (for a holds Q[a])
provided
for a holds (P[a] & Q[a]);

scheme Schemat6b {P[set],Q[set]} :
for a holds (P[a] & Q[a])
provided
(for a holds P[a]) & (for a holds Q[a]);

scheme Schemat7 {P[set],Q[set]} :
for a holds (P[a] or Q[a])
provided
(for a holds P[a]) or (for a holds Q[a]);

scheme Schemat8 {P[set],Q[set]} :
(for a holds P[a]) implies (for a holds Q[a])
provided
for a holds P[a] implies Q[a];

scheme Schemat9 {P[set],Q[set]} :
(for a holds P[a]) iff (for a holds Q[a])
provided
for a holds (P[a] iff Q[a]);

scheme Schemat10b {T[]} :
for a holds T[]
provided
T[];

scheme Schemat11a {P[set],T[]} :
(for a holds P[a]) or T[]
provided
for a holds (P[a] or T[]);

scheme Schemat11b {P[set],T[]} :
for a holds (P[a] or T[])
provided
(for a holds P[a]) or T[];

scheme Schemat12a {P[set],T[]} :
ex a st (T[] & P[a])
provided
T[] & (ex a st P[a]);

scheme Schemat12b {P[set],T[]} :
T[] & (ex a st P[a])
provided
ex a st (T[] & P[a]);

scheme Schemat13a {P[set],T[]} :
for a holds (T[] implies P[a])
provided
T[] implies (for a holds P[a]);

scheme Schemat13b {P[set],T[]} :
T[] implies (for a holds P[a])
provided
for a holds (T[] implies P[a]);

scheme Schemat14 {P[set],T[]} :
ex a st (T[] implies P[a])
provided
T[] implies (ex a st P[a]);

scheme Schemat17 {P[set],T[]} :
(for a holds P[a]) implies T[]
provided
for a holds (P[a] implies T[]);

scheme Schemat18a {P[set],Q[set]} :
ex a st (for b holds (P[a] or Q[b]))
provided
(ex a st P[a]) or (for b holds Q[b]);

scheme Schemat18b {P[set],Q[set]} :
(ex a st P[a]) or (for b holds Q[b])
provided
ex a st for b holds (P[a] or Q[b]);

scheme Schemat19a {P[set],Q[set]} :
for b holds (ex a st (P[a] or Q[b]))
provided
(ex a st P[a]) or (for b holds Q[b]);

scheme Schemat19b {P[set],Q[set]} :
(ex a st P[a]) or (for b holds Q[b])
provided
for b holds (ex a st (P[a] or Q[b]));

scheme Schemat20b {P[set],Q[set]} :
ex a st (for b holds (P[a] or Q[b]))
provided
for b ex a st (P[a] or Q[b]);

scheme Schemat21a {P[set],Q[set]} :
ex a st for b holds P[a] & Q[b]
provided
(ex a st P[a]) & (for b holds Q[b]);

scheme Schemat21b {P[set],Q[set]} :
(ex a st P[a]) & (for b holds Q[b])
provided
ex a st for b holds P[a] & Q[b];

scheme Schemat22a {P[set],Q[set]} :
for b ex a st (P[a] & Q[b])
provided
(ex a st P[a]) & (for b holds Q[b]);

scheme Schemat22b {P[set],Q[set]} :
(ex a st P[a]) & (for b holds Q[b])
provided
for b ex a st P[a] & Q[b];

scheme Schemat23b {P[set],Q[set]} :
ex a st for b holds P[a] & Q[b]
provided
for b ex a st P[a] & Q[b];

scheme Schemat24a {S[set,set],Q[set]} :
for a ex b st (S[a,b] implies Q[a])
provided
for a holds ((for b holds S[a,b]) implies Q[a]);

scheme Schemat24b {S[set,set],Q[set]} :
for a holds ((for b holds S[a,b]) implies Q[a])
provided
for a ex b st (S[a,b] implies Q[a]);

scheme Schemat25a {S[set,set],Q[set]} :
for a,b holds (S[a,b] implies Q[a])
provided
for a holds ((ex b st S[a,b]) implies Q[a]);

scheme Schemat25b {S[set,set],Q[set]} :
for a holds ((ex b st S[a,b]) implies Q[a])
provided
for a,b holds (S[a,b] implies Q[a]);

scheme Schemat27 {S[set,set]} :
for a holds S[a,a]
provided
for a,b holds S[a,b];

scheme Schemat28 {S[set,set]} :
ex b st for a holds S[a,b]
provided
for a,b holds S[a,b];

scheme Schemat30 {S[set,set]} :
ex a st S[a,a]
provided
ex a st for b holds S[a,b];

scheme Schemat31 {S[set,set]} :
for a ex b st S[b,a]
provided
for a holds S[a,a];

scheme Schemat33 {S[set,set]} :
for a ex b st S[a,b]
provided
for a holds S[a,a];

scheme Schemat36 {S[set,set]} :
ex a,b st S[a,b]
provided
for b ex a st S[a,b];

scheme Schemat37 {S[set,set]} :
ex a,b st S[a,b]
provided
ex a st S[a,a];

```