### The Mizar article:

### Schemes

**by****Stanislaw T. Czuba**

- Received December 17, 1990
Copyright (c) 1990 Association of Mizar Users

- MML identifier: SCHEMS_1
- [ 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 A1: for a holds P[a] proof consider a; P[a] by A1; hence thesis; end; scheme Schemat1a {P[set],T[]} : (for a holds P[a]) & T[] provided A1: for a holds (P[a] & T[]) by A1; scheme Schemat1b {P[set],T[]} : for a holds (P[a] & T[]) provided A1: (for a holds P[a]) & T[] by A1; scheme Schemat2a {P[set], T[]} : (ex a st P[a]) or T[] provided A1: ex a st (P[a] or T[]) by A1; scheme Schemat2b {P[set], T[]} : ex a st (P[a] or T[]) provided A1: (ex a st P[a]) or T[] by A1; scheme Schemat3 {S[set,set]} : for b ex a st S[a,b] provided A1: ex a st for b holds S[a,b] proof consider a such that A2:for b holds S[a,b] by A1; now let b; S[a,b] by A2; hence ex a st S[a,b]; end; hence thesis; end; scheme Schemat4a {P[set],Q[set]} : (ex a st P[a]) or (ex a st Q[a]) provided A1: ex a st (P[a] or Q[a]) by A1; scheme Schemat4b {P[set],Q[set]} : ex a st (P[a] or Q[a]) provided A1: (ex a st P[a]) or (ex a st Q[a]) by A1; scheme Schemat5 {P[set],Q[set]} : (ex a st P[a]) & (ex a st Q[a]) provided A1: ex a st (P[a] & Q[a]) by A1; scheme Schemat6a {P[set],Q[set]} : (for a holds P[a]) & (for a holds Q[a]) provided A1: for a holds (P[a] & Q[a]) by A1; scheme Schemat6b {P[set],Q[set]} : for a holds (P[a] & Q[a]) provided A1: (for a holds P[a]) & (for a holds Q[a]) by A1; scheme Schemat7 {P[set],Q[set]} : for a holds (P[a] or Q[a]) provided A1: (for a holds P[a]) or (for a holds Q[a]) by A1; scheme Schemat8 {P[set],Q[set]} : (for a holds P[a]) implies (for a holds Q[a]) provided A1: for a holds P[a] implies Q[a] proof assume A2:for a holds P[a]; now let a; (P[a] implies Q[a]) & P[a] by A1,A2; hence Q[a]; end; hence thesis; end; scheme Schemat9 {P[set],Q[set]} : (for a holds P[a]) iff (for a holds Q[a]) provided A1: for a holds (P[a] iff Q[a]) proof thus (for a holds P[a]) implies (for a holds Q[a]) proof assume A2:for a holds P[a]; now let a; (P[a] iff Q[a]) & P[a] by A1,A2; hence Q[a]; end; hence thesis; end; assume A3:for a holds Q[a]; now let a; (P[a] iff Q[a]) & Q[a] by A1,A3; hence P[a]; end; hence thesis; end; scheme Schemat10b {T[]} : for a holds T[] provided A1: T[] by A1; scheme Schemat11a {P[set],T[]} : (for a holds P[a]) or T[] provided A1: for a holds (P[a] or T[]) by A1; scheme Schemat11b {P[set],T[]} : for a holds (P[a] or T[]) provided A1: (for a holds P[a]) or T[] by A1; scheme Schemat12a {P[set],T[]} : ex a st (T[] & P[a]) provided A1: T[] & (ex a st P[a]) by A1; scheme Schemat12b {P[set],T[]} : T[] & (ex a st P[a]) provided A1: ex a st (T[] & P[a]) by A1; scheme Schemat13a {P[set],T[]} : for a holds (T[] implies P[a]) provided A1: T[] implies (for a holds P[a]) by A1; scheme Schemat13b {P[set],T[]} : T[] implies (for a holds P[a]) provided A1: for a holds (T[] implies P[a]) by A1; scheme Schemat14 {P[set],T[]} : ex a st (T[] implies P[a]) provided A1: T[] implies (ex a st P[a]) by A1; scheme Schemat17 {P[set],T[]} : (for a holds P[a]) implies T[] provided A1: for a holds (P[a] implies T[]) proof assume A2:for a holds P[a]; now let a; P[a] by A2; hence T[] by A1; end; hence thesis; end; scheme Schemat18a {P[set],Q[set]} : ex a st (for b holds (P[a] or Q[b])) provided A1: (ex a st P[a]) or (for b holds Q[b]) proof now A2:now given a such that A3:P[a]; for b holds (P[a] or Q[b]) by A3; hence thesis; end; now assume A4:for b holds Q[b]; consider a; for b holds (P[a] or Q[b]) by A4; hence thesis; end; hence thesis by A1,A2; end; hence thesis; end; scheme Schemat18b {P[set],Q[set]} : (ex a st P[a]) or (for b holds Q[b]) provided A1: ex a st for b holds (P[a] or Q[b]) proof consider a such that A2:for b holds (P[a] or Q[b]) by A1; (ex b st not Q[b]) implies P[a] by A2; hence thesis; end; scheme Schemat19a {P[set],Q[set]} : for b holds (ex a st (P[a] or Q[b])) provided A1: (ex a st P[a]) or (for b holds Q[b]) by A1; scheme Schemat19b {P[set],Q[set]} : (ex a st P[a]) or (for b holds Q[b]) provided A1: for b holds (ex a st (P[a] or Q[b])) by A1; scheme Schemat20b {P[set],Q[set]} : ex a st (for b holds (P[a] or Q[b])) provided A1: for b ex a st (P[a] or Q[b]) proof defpred X[set] means P[$1]; defpred Y[set] means Q[$1]; A2: for b ex a st (X[a] or Y[b]) by A1; A3:(ex a st X[a]) or (for b holds Y[b]) from Schemat19b(A2); ex a st (for b holds (X[a] or Y[b])) from Schemat18a(A3); hence thesis; end; scheme Schemat21a {P[set],Q[set]} : ex a st for b holds P[a] & Q[b] provided A1: (ex a st P[a]) & (for b holds Q[b]) by A1; scheme Schemat21b {P[set],Q[set]} : (ex a st P[a]) & (for b holds Q[b]) provided A1: ex a st for b holds P[a] & Q[b] by A1; scheme Schemat22a {P[set],Q[set]} : for b ex a st (P[a] & Q[b]) provided A1: (ex a st P[a]) & (for b holds Q[b]) proof now let b; A2:Q[b] by A1; consider a such that A3:P[a] by A1; thus ex a st P[a] & Q[b] by A2,A3; end; hence thesis; end; scheme Schemat22b {P[set],Q[set]} : (ex a st P[a]) & (for b holds Q[b]) provided A1: for b ex a st P[a] & Q[b] proof assume A2:(for a holds not P[a]) or (ex b st not Q[b]); A3:now given b such that A4:not Q[b]; now let d; assume d = b; ex a st P[a] & Q[b] by A1; hence contradiction by A4; end; hence thesis; end; now assume A5:for a holds not P[a]; now let b; consider a such that A6:P[a] & Q[b] by A1; thus thesis by A5,A6; end; hence thesis; end; hence thesis by A2,A3; end; scheme Schemat23b {P[set],Q[set]} : ex a st for b holds P[a] & Q[b] provided A1: for b ex a st P[a] & Q[b] proof defpred X[set] means P[$1]; defpred Y[set] means Q[$1]; A2: for b ex a st X[a] & Y[b] by A1; A3: (ex a st X[a]) & (for b holds Y[b]) from Schemat22b(A2); ex a st for b holds (X[a] & Y[b]) from Schemat21a(A3); hence thesis; end; scheme Schemat24a {S[set,set],Q[set]} : for a ex b st (S[a,b] implies Q[a]) provided A1: for a holds ((for b holds S[a,b]) implies Q[a]) by A1; scheme Schemat24b {S[set,set],Q[set]} : for a holds ((for b holds S[a,b]) implies Q[a]) provided A1: for a ex b st (S[a,b] implies Q[a]) by A1; scheme Schemat25a {S[set,set],Q[set]} : for a,b holds (S[a,b] implies Q[a]) provided A1: for a holds ((ex b st S[a,b]) implies Q[a]) by A1; scheme Schemat25b {S[set,set],Q[set]} : for a holds ((ex b st S[a,b]) implies Q[a]) provided A1: for a,b holds (S[a,b] implies Q[a]) by A1; scheme Schemat27 {S[set,set]} : for a holds S[a,a] provided A1: for a,b holds S[a,b] by A1; scheme Schemat28 {S[set,set]} : ex b st for a holds S[a,b] provided A1: for a,b holds S[a,b] proof now let b; for a holds S[a,b] by A1; hence thesis; end; hence thesis; end; scheme Schemat30 {S[set,set]} : ex a st S[a,a] provided A1: ex a st for b holds S[a,b] proof consider a such that A2:for b holds S[a,b] by A1; S[a,a] by A2; hence thesis; end; scheme Schemat31 {S[set,set]} : for a ex b st S[b,a] provided A1: for a holds S[a,a] proof let a; S[a,a] by A1; hence thesis; end; scheme Schemat33 {S[set,set]} : for a ex b st S[a,b] provided A1: for a holds S[a,a] proof let a; S[a,a] by A1; hence thesis; end; scheme Schemat36 {S[set,set]} : ex a,b st S[a,b] provided A1: for b ex a st S[a,b] proof consider b; ex a st S[a,b] by A1; hence thesis; end; scheme Schemat37 {S[set,set]} : ex a,b st S[a,b] provided A1: ex a st S[a,a] by A1;

Back to top