:: A First Order Language
:: by Piotr Rudnicki and Andrzej Trybulec
::
:: Received August 8, 1989
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, SUBSET_1, ZFMISC_1, TARSKI, XXREAL_0,
MARGREL1, MCART_1, ARYTM_3, NAT_1, FINSEQ_1, RELAT_1, ORDINAL4, CARD_1,
REALSET1, XBOOLEAN, BVFUNC_2, ZF_LANG, CLASSES2, FUNCT_1, FUNCOP_1,
RCOMP_1, QC_LANG1, WELLORD1, RELAT_2, MEMBER_1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, SUBSET_1, CARD_1,
ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, MCART_1, RELAT_1, FUNCT_1,
RELSET_1, NAT_1, FUNCT_2, FUNCOP_1, FINSEQ_1, WELLORD1, WELLORD2,
RELAT_2;
constructors ENUMSET1, FUNCOP_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, RELSET_1,
WELLORD1, WELLORD2, RELAT_2, XTUPLE_0, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0,
FINSEQ_1, XTUPLE_0, NAT_1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0, CARD_1;
equalities FINSEQ_1;
expansions TARSKI, XBOOLE_0, FINSEQ_1;
theorems ZFMISC_1, SUBSET_1, TARSKI, FINSEQ_1, MCART_1, NAT_1, FUNCT_1,
FUNCT_2, RELSET_1, XBOOLE_0, XBOOLE_1, FUNCOP_1, XXREAL_0, ORDINAL1,
CARD_1, RELAT_1, WELLORD1, WELLORD2, RELAT_2, ORDERS_1;
schemes NAT_1, FUNCT_2, CLASSES1, XBOOLE_0;
begin :: Preliminaries
theorem
for D1 being non empty set, D2 being set, k being Element of D1 holds
[: {k}, D2 :] c= [: D1, D2 :]
proof
let D1 be non empty set, D2 be set, k be Element of D1;
{k} is Subset of D1 by SUBSET_1:41;
hence thesis by ZFMISC_1:95;
end;
theorem
for D1 being non empty set, D2 being set, k1, k2, k3 being
Element of D1 holds [: {k1, k2, k3}, D2 :] c= [: D1, D2 :]
proof
let D1 be non empty set, D2 be set, k1, k2, k3 be Element of D1;
{k1, k2, k3} is Subset of D1 by SUBSET_1:35;
hence thesis by ZFMISC_1:95;
end;
definition
mode QC-alphabet -> set means :Def1:
it is non empty set & ex X being set st NAT c= X & it = [: NAT, X :];
existence
proof
[: NAT, NAT :] = [: NAT, NAT :];
hence thesis;
end;
end;
registration
cluster -> non empty Relation-like for QC-alphabet;
coherence
proof
let A be QC-alphabet;
ex X being set st NAT c= X & A = [: NAT, X :] by Def1;
hence thesis by Def1;
end;
end;
reserve A for QC-alphabet;
reserve k,n,m for Nat;
definition
let A be QC-alphabet;
func QC-symbols(A) -> non empty set equals
rng A;
coherence;
end;
definition let A be QC-alphabet;
mode QC-symbol of A is Element of QC-symbols(A);
end;
theorem Th3: NAT c= QC-symbols(A) & 0 in QC-symbols(A)
proof
consider X being set such that A1: NAT c= X & A = [: NAT, X :] by Def1;
thus A2: NAT c= QC-symbols(A) by A1,RELAT_1:160;
thus 0 in QC-symbols(A) by A2;
end;
registration let A be QC-alphabet;
cluster QC-symbols(A) -> non empty;
coherence;
end;
definition let A be QC-alphabet;
func QC-variables(A) -> set equals
[: {6}, NAT :] \/ [: {4,5}, QC-symbols(A) :];
coherence;
end;
registration
let A be QC-alphabet;
cluster QC-variables(A) -> non empty;
coherence;
end;
Lm1: [: {4}, QC-symbols(A) :] c= QC-variables(A) &
[: {5}, QC-symbols(A) :] c= QC-variables(A) &
[: {6}, NAT :] c= QC-variables(A)
proof
{5} c= {4,5} by ZFMISC_1:7;
then
A1: [: {5}, QC-symbols(A) :] c= [: {4,5}, QC-symbols(A) :] by ZFMISC_1:96;
{4} c= {4,5} by ZFMISC_1:7;
then [: {4}, QC-symbols(A) :] c= [: {4,5}, QC-symbols(A) :] by ZFMISC_1:96;
hence thesis by A1,XBOOLE_1:10;
end;
theorem Th4:
QC-variables(A) c= [: NAT, QC-symbols(A) :]
proof
{ 6 } c= NAT & NAT c= QC-symbols(A) by Th3,ZFMISC_1:31;
then
A1: [: { 6 }, NAT :] c= [: NAT, QC-symbols(A) :] by ZFMISC_1:96;
{4, 5} c= NAT & QC-symbols(A) c= QC-symbols(A) by ZFMISC_1:32;
then [: {4,5}, QC-symbols(A) :] c= [: NAT, QC-symbols(A) :] by ZFMISC_1:96;
hence thesis by A1,XBOOLE_1:8;
end;
definition
let A be QC-alphabet;
mode QC-variable of A is Element of QC-variables(A);
func bound_QC-variables(A) -> Subset of QC-variables(A) equals
[: {4}, QC-symbols(A) :];
coherence by Lm1;
func fixed_QC-variables(A) -> Subset of QC-variables(A) equals
[: {5}, QC-symbols(A) :];
coherence by Lm1;
func free_QC-variables(A) -> Subset of QC-variables(A) equals
[: {6}, NAT :];
coherence by Lm1;
func QC-pred_symbols(A) -> set equals
{ [n, x] where x is QC-symbol of A : 7 <= n };
coherence;
end;
registration
let A be QC-alphabet;
cluster bound_QC-variables(A) -> non empty;
coherence;
cluster fixed_QC-variables(A) -> non empty;
coherence;
cluster free_QC-variables(A) -> non empty;
coherence;
cluster QC-pred_symbols(A) -> non empty;
coherence
proof
0 is QC-symbol of A by Th3;
then [7, 0] in { [n, x] where x is QC-symbol of A: 7 <= n };
hence thesis;
end;
end;
theorem
A = [: NAT, QC-symbols(A) :]
proof
consider X being set such that A1: NAT c= X & A = [: NAT, X :] by Def1;
X <> {} by A1;
hence A = [: NAT, QC-symbols(A) :] by A1,RELAT_1:160;
end;
theorem Th6:
QC-pred_symbols(A) c= [: NAT, QC-symbols(A) :]
proof
let y be object;
assume y in QC-pred_symbols(A);
then consider k being Nat, x being QC-symbol of A such that
A1: y = [k, x] & 7 <= k;
k in NAT by ORDINAL1:def 12;
hence thesis by ZFMISC_1:def 2,A1;
end;
definition
let A be QC-alphabet;
mode QC-pred_symbol of A is Element of QC-pred_symbols(A);
end;
definition
let A be QC-alphabet;
let P be Element of QC-pred_symbols(A);
func the_arity_of P -> Nat means
:Def8:
P`1 = 7+it;
existence
proof
P in {[k, x] where x is QC-symbol of A : 7 <= k};
then consider k being Nat, x being QC-symbol of A such that
A1: P = [k, x] and
A2: 7 <= k;
consider w being Nat such that
A3: k=7+w by A2,NAT_1:10;
thus thesis by A1,A3;
end;
uniqueness;
end;
reserve P for QC-pred_symbol of A;
definition
let A,k;
func k-ary_QC-pred_symbols(A) -> Subset of QC-pred_symbols(A) equals
{ P : the_arity_of P = k };
coherence
proof
set Y = {7+k};
[: {7+k}, QC-symbols(A) :] c= QC-pred_symbols(A)
proof
let y be object;
assume
A1: y in [: {7+k}, QC-symbols(A) :];
reconsider y1 = y`1 as Nat by MCART_1:12,A1;
reconsider y2 = y`2 as QC-symbol of A by A1,MCART_1:12;
y`1 = 7+k by A1,MCART_1:12;
then 7 <= y1 by NAT_1:12;
then [y1, y2] in { [m, x] where x is QC-symbol of A : 7 <= m };
hence thesis by A1,MCART_1:21;
end;
then reconsider X = [: Y, QC-symbols(A) :] as Subset of QC-pred_symbols(A);
X = { P : the_arity_of P = k }
proof
thus X c= { P : the_arity_of P = k }
proof
let x be object;
assume
A2: x in X;
then reconsider Q = x as QC-pred_symbol of A;
x`1 in Y by A2,MCART_1:10;
then x`1 = 7+k by TARSKI:def 1;
then the_arity_of Q = k by Def8;
hence thesis;
end;
let x be object;
assume x in { P : the_arity_of P = k };
then consider P such that
A3: x = P and
A4: the_arity_of P = k;
P`1 = 7+k by A4,Def8;
then
A5: P`1 in Y by TARSKI:def 1;
A6: QC-pred_symbols(A) c= [: NAT, QC-symbols(A) :] by Th6;
then P in [: NAT, QC-symbols(A) :];
then P`2 in QC-symbols(A) by MCART_1:10;
then [P`1, P`2] in X by A5,ZFMISC_1:87;
hence thesis by A3,A6,MCART_1:21;
end;
hence thesis;
end;
end;
registration
let k, A;
cluster k-ary_QC-pred_symbols(A) -> non empty;
coherence
proof
set Y = {7+k};
[: {7+k}, QC-symbols(A) :] c= QC-pred_symbols(A)
proof
let x be object;
assume
A1: x in [: {7+k}, QC-symbols(A) :];
reconsider x1 = x`1 as Nat by MCART_1:12,A1;
reconsider x2 = x`2 as QC-symbol of A by A1,MCART_1:12;
x`1 = 7+k by A1,MCART_1:12;
then 7 <= x1 by NAT_1:12;
then [x1, x2] in { [m, y] where y is QC-symbol of A : 7 <= m };
hence thesis by A1,MCART_1:21;
end;
then reconsider X = [: Y, QC-symbols(A) :] as
non empty Subset of QC-pred_symbols(A);
X = { P : the_arity_of P = k }
proof
thus X c= { P : the_arity_of P = k }
proof
let x be object;
assume
A2: x in X;
then reconsider Q = x as QC-pred_symbol of A;
x`1 in Y by A2,MCART_1:10;
then x`1 = 7+k by TARSKI:def 1;
then the_arity_of Q = k by Def8;
hence thesis;
end;
let x be object;
assume x in { P : the_arity_of P = k };
then consider P such that
A3: x = P and
A4: the_arity_of P = k;
P`1 = 7+k by A4,Def8;
then
A5: P`1 in Y by TARSKI:def 1;
A6: QC-pred_symbols(A) c= [: NAT, QC-symbols(A) :] by Th6;
then P in [: NAT, QC-symbols(A) :];
then P`2 in QC-symbols(A) by MCART_1:10;
then [P`1, P`2] in X by A5,ZFMISC_1:87;
hence thesis by A3,A6,MCART_1:21;
end;
hence thesis;
end;
end;
definition
let A be QC-alphabet;
mode bound_QC-variable of A is Element of bound_QC-variables(A);
mode fixed_QC-variable of A is Element of fixed_QC-variables(A);
mode free_QC-variable of A is Element of free_QC-variables(A);
let k;
mode QC-pred_symbol of k, A is Element of k-ary_QC-pred_symbols(A);
end;
registration
let k be Nat;
let A be QC-alphabet;
cluster k-element for FinSequence of QC-variables(A);
existence
proof
consider p being FinSequence of QC-variables(A) such that
A1: len p = k by FINSEQ_1:19;
take p;
thus len p = k by A1;
end;
end;
definition
let k be Nat;
let A be QC-alphabet;
mode QC-variable_list of k, A is k-element FinSequence of QC-variables(A);
end;
definition
let A be QC-alphabet;
let D be set;
attr D is A-closed means
:Def10:
D is Subset of [:NAT, QC-symbols(A):]* & :: Includes atomic formulae
(for k being Nat, p being (QC-pred_symbol of k,A),
ll being QC-variable_list of k,A holds <*p*>^ll in D) &
:: Is closed under VERUM, 'not', '&', and quantification
<*[0, 0]*> in D &
(for p being FinSequence of [:NAT,QC-symbols(A):]
st p in D holds <*[1, 0]*>^p in D) &
(for p, q being FinSequence of [:NAT, QC-symbols(A):] st p in D &
q in D holds <*[2, 0]*>^p^q in D) &
(for x being bound_QC-variable of A,
p being FinSequence of [:NAT, QC-symbols(A):]
st p in D holds <*[3, 0]*>^<*x*>^p in D);
end;
Lm2: for k being Nat, x being QC-symbol of A
holds <*[k, x]*> is FinSequence of [:NAT, QC-symbols(A):]
proof
let k;
let x be QC-symbol of A;
k in NAT by ORDINAL1:def 12;
then [k, x] in [:NAT, QC-symbols(A):] by ZFMISC_1:def 2;
then rng <*[k, x]*> = {[k, x]} &
{[k, x]} c= [:NAT, QC-symbols(A):] by FINSEQ_1:39,ZFMISC_1:31;
hence thesis by FINSEQ_1:def 4;
end;
Lm3: for k being Nat, p being (QC-pred_symbol of k,A), ll being (
QC-variable_list of k,A) holds <*p*>^ll is FinSequence of [:NAT,QC-symbols(A):]
proof
let k be Nat, p be (QC-pred_symbol of k,A),
ll be QC-variable_list of k,A;
QC-variables(A) c= [:NAT,QC-symbols(A):] by Th4;
then
A1: rng ll c= [:NAT,QC-symbols(A):];
QC-pred_symbols(A) c= [:NAT,QC-symbols(A):] by Th6;
then k-ary_QC-pred_symbols(A) c= [:NAT,QC-symbols(A):];
then rng <*p*> c= [:NAT,QC-symbols(A):];
then rng <*p*> \/ rng ll c= [:NAT,QC-symbols(A):] by A1,XBOOLE_1:8;
then rng (<*p*>^ll) c= [:NAT,QC-symbols(A):] by FINSEQ_1:31;
hence thesis by FINSEQ_1:def 4;
end;
Lm4: for x being bound_QC-variable of A,
p being FinSequence of [:NAT, QC-symbols(A):] holds
<*[3, 0]*>^<*x*>^p is FinSequence of [:NAT, QC-symbols(A):]
proof
A1: 0 is QC-symbol of A by Th3;
reconsider y = <*[3, 0]*> as FinSequence of [:NAT,QC-symbols(A):] by A1,Lm2;
let x be bound_QC-variable of A, p be FinSequence of [:NAT, QC-symbols(A):];
QC-variables(A) c= [: NAT, QC-symbols(A) :] by Th4;
then bound_QC-variables(A) c= [:NAT,QC-symbols(A):];
then rng <*x*> c= [:NAT,QC-symbols(A):];
then reconsider z = <*x*> as FinSequence of
[:NAT, QC-symbols(A):] by FINSEQ_1:def 4;
y^z^p is FinSequence of [:NAT, QC-symbols(A):];
hence thesis;
end;
definition
let A be QC-alphabet;
func QC-WFF(A) -> non empty set means
:Def11:
it is A-closed & for D being non empty set st D is A-closed holds it c= D;
existence
proof
0 is QC-symbol of A by Th3;
then <*[0, 0]*> is FinSequence of [:NAT, QC-symbols(A):] by Lm2;
then
A1: <*[0, 0]*> in [:NAT, QC-symbols(A):]* by FINSEQ_1:def 11;
defpred P[object] means
for D being non empty set st D is A-closed holds $1
in D;
consider D0 being set such that
A2: for x being object holds x in D0 iff x in [:NAT, QC-symbols(A):]* & P[x]
from
XBOOLE_0:sch 1;
A3: for D being non empty set st D is A-closed holds <*[0, 0]*> in D;
then reconsider D0 as non empty set by A2,A1;
take D0;
D0 c= [:NAT, QC-symbols(A):]*
by A2;
hence D0 is Subset of [:NAT, QC-symbols(A):]*;
thus for k being Nat, p being (QC-pred_symbol of k,A), ll being
QC-variable_list of k,A holds <*p*>^ll in D0
proof
let k be Nat, p be (QC-pred_symbol of k,A), ll be
QC-variable_list of k,A;
<*p*>^ll is FinSequence of [:NAT, QC-symbols(A):] by Lm3;
then
A4: <*p*>^ll in [:NAT, QC-symbols(A):]* by FINSEQ_1:def 11;
for D being non empty set st D is A-closed holds <*p*>^ll in D;
hence thesis by A2,A4;
end;
thus <*[0, 0]*> in D0 by A2,A1,A3;
thus for p being FinSequence of [:NAT, QC-symbols(A):]
st p in D0 holds <*[1, 0]*>^p
in D0
proof
A5: 0 is QC-symbol of A by Th3;
reconsider h = <*[1, 0]*> as
FinSequence of [:NAT, QC-symbols(A):] by Lm2,A5;
let p be FinSequence of [:NAT, QC-symbols(A):];
assume
A6: p in D0;
A7: for D being non empty set st D is A-closed holds <*[1, 0]*>^p in D
proof
let D be non empty set;
assume
A8: D is A-closed;
then p in D by A2,A6;
hence thesis by A8;
end;
h^p is FinSequence of [:NAT, QC-symbols(A):];
then <*[1, 0]*>^p in [:NAT, QC-symbols(A):]* by FINSEQ_1:def 11;
hence thesis by A2,A7;
end;
thus for p, q being FinSequence of [:NAT, QC-symbols(A):]
st p in D0 & q in D0 holds
<*[2, 0]*>^p^q in D0
proof
A9: 0 is QC-symbol of A by Th3;
reconsider h = <*[2, 0]*> as FinSequence
of [:NAT, QC-symbols(A):] by A9,Lm2;
let p, q be FinSequence of [:NAT, QC-symbols(A):] such that
A10: p in D0 & q in D0;
A11: for D being non empty set st D is A-closed holds <*[2, 0]*>^p^q in D
proof
let D be non empty set;
assume
A12: D is A-closed;
then p in D & q in D by A2,A10;
hence thesis by A12;
end;
h^p^q is FinSequence of [:NAT, QC-symbols(A):];
then <*[2, 0]*>^p^q in [:NAT, QC-symbols(A):]* by FINSEQ_1:def 11;
hence thesis by A2,A11;
end;
thus for x being bound_QC-variable of A,
p being FinSequence of [:NAT, QC-symbols(A):] st
p in D0 holds <*[3, 0]*>^<*x*>^p in D0
proof
let x be bound_QC-variable of A,
p be FinSequence of [:NAT, QC-symbols(A):];
assume
A13: p in D0;
A14: for D being non empty set st D is A-closed holds <*[3, 0]*>^<*x*>^
p in D
proof
let D be non empty set;
assume
A15: D is A-closed;
then p in D by A2,A13;
hence thesis by A15;
end;
<*[3, 0]*>^<*x*>^p is FinSequence of [:NAT, QC-symbols(A):] by Lm4;
then <*[3, 0]*>^<*x*>^p in [:NAT, QC-symbols(A):]* by FINSEQ_1:def 11;
hence thesis by A2,A14;
end;
let D be non empty set such that
A16: D is A-closed;
let x be object;
assume x in D0;
hence thesis by A2,A16;
end;
uniqueness;
end;
theorem
QC-WFF(A) is A-closed by Def11;
registration
let A be QC-alphabet;
cluster A-closed non empty for set;
existence
proof
QC-WFF(A) is A-closed by Def11;
hence thesis;
end;
end;
definition
let A be QC-alphabet;
mode QC-formula of A is Element of QC-WFF(A);
end;
definition
let A be QC-alphabet;
let P be QC-pred_symbol of A;
let l be FinSequence of QC-variables(A);
assume
A1: the_arity_of P = len l;
func P!l -> Element of QC-WFF(A) equals :Def12:
<*P*>^l;
coherence
proof
set k = len l;
set QCP = {Q where Q is QC-pred_symbol of A: the_arity_of Q = k };
P in QCP by A1;
then reconsider P as QC-pred_symbol of k, A;
reconsider l as QC-variable_list of k, A by CARD_1:def 7;
A2: QC-WFF(A) is A-closed non empty set by Def11;
for D being A-closed non empty set st not contradiction holds
<*P*>^l in D by Def10;
hence thesis by A2;
end;
end;
theorem Th8:
for k being Nat, p being QC-pred_symbol of k, A, ll be
QC-variable_list of k, A holds p!ll = <*p*>^ll
proof
let k be Nat, p be QC-pred_symbol of k, A,
ll be QC-variable_list of k, A;
set QCP = {Q where Q is QC-pred_symbol of A: the_arity_of Q = k };
p in QCP;
then
A1: ex Q being QC-pred_symbol of A st p = Q & the_arity_of Q = k;
len ll = k by CARD_1:def 7;
hence thesis by A1,Def12;
end;
Lm5: QC-WFF(A) is Subset of [:NAT, QC-symbols(A):]*
proof
A1: QC-WFF(A) is A-closed non empty set by Def11;
thus thesis by A1,Def10;
end;
definition
let A be QC-alphabet;
let p be Element of QC-WFF(A);
func @p -> FinSequence of [:NAT, QC-symbols(A):] equals
p;
coherence
proof
QC-WFF(A) is Subset of [:NAT, QC-symbols(A):]* &
p in QC-WFF(A) by Lm5;
hence thesis by FINSEQ_1:def 11;
end;
end;
definition
let A be QC-alphabet;
func VERUM(A) -> QC-formula of A equals
<*[0, 0]*>;
coherence
proof
QC-WFF(A) is A-closed non empty set by Def11;
hence thesis by Def10;
end;
let p be Element of QC-WFF(A);
func 'not' p -> QC-formula of A equals
<*[1, 0]*>^@p;
coherence
proof
QC-WFF(A) is A-closed non empty set by Def11;
hence thesis by Def10;
end;
let q be Element of QC-WFF(A);
func p '&' q -> QC-formula of A equals
<*[2, 0]*>^@p^@q;
coherence
proof
QC-WFF(A) is A-closed non empty set by Def11;
hence thesis by Def10;
end;
end;
definition
let A be QC-alphabet;
let x be bound_QC-variable of A, p be Element of QC-WFF(A);
func All(x, p) -> QC-formula of A equals
<*[3, 0]*>^<*x*>^@p;
coherence
proof
QC-WFF(A) is A-closed non empty set by Def11;
hence thesis by Def10;
end;
end;
reserve F for Element of QC-WFF(A);
scheme
QCInd { A() -> QC-alphabet, Prop[Element of QC-WFF(A())] }:
for F being Element of QC-WFF(A()) holds Prop[F]
provided
A1: for k being Nat, P being (QC-pred_symbol of k, A()), ll being
QC-variable_list of k, A() holds Prop[P!ll] and
A2: Prop[VERUM(A())] and
A3: for p being Element of QC-WFF(A()) st Prop[p] holds Prop['not' p] and
A4: for p, q being Element of QC-WFF(A()) st Prop[p] & Prop[q] holds Prop[p
'&' q] and
A5: for x being bound_QC-variable of A(),
p being Element of QC-WFF(A()) st Prop[p]
holds Prop[All(x, p)]
proof
VERUM(A()) in { F where F is Element of QC-WFF(A()) : Prop[F] } by A2;
then reconsider X = { F where F is Element of QC-WFF(A()) : Prop[F] }
as non empty set;
A6: for k being Nat, P being (QC-pred_symbol of k, A()), ll being
QC-variable_list of k,A() holds <*P*>^ll in X
proof
let k be Nat, P be (QC-pred_symbol of k, A()), ll be
QC-variable_list of k, A();
Prop[P!ll] by A1;
then P!ll in X;
hence thesis by Th8;
end;
A7: for x being bound_QC-variable of A(),
p being FinSequence of [:NAT, QC-symbols(A()):]
st p in X holds <*[3, 0]*>^<*x*>^p in X
proof
let x be bound_QC-variable of A(),
p be FinSequence of [:NAT, QC-symbols(A()):];
assume p in X;
then consider p9 being Element of QC-WFF(A()) such that
A8: p = p9 and
A9: Prop[p9];
Prop[All(x, p9)] by A5,A9;
hence thesis by A8;
end;
A10: for p, q being FinSequence of [:NAT, QC-symbols(A()):]
st p in X & q in X holds <*[2, 0]*>^p^q in X
proof
let p, q be FinSequence of [:NAT, QC-symbols(A()):];
assume p in X;
then consider p9 being Element of QC-WFF(A()) such that
A11: p = p9 and
A12: Prop[p9];
assume q in X;
then consider q9 being Element of QC-WFF(A()) such that
A13: q = q9 and
A14: Prop[q9];
Prop[p9 '&' q9] by A4,A12,A14;
hence thesis by A11,A13;
end;
A15: for p being FinSequence of [:NAT, QC-symbols(A()):]
st p in X holds <*[1, 0]*>^p in X
proof
let p be FinSequence of [:NAT, QC-symbols(A()):];
assume p in X;
then consider p9 being Element of QC-WFF(A()) such that
A16: p = p9 and
A17: Prop[p9];
Prop['not' p9] by A3,A17;
hence thesis by A16;
end;
let F9 be Element of QC-WFF(A());
A18: X c= [:NAT, QC-symbols(A()):]*
proof
let x be object;
assume x in X;
then consider p being Element of QC-WFF(A()) such that
A19: x = p and
Prop[p];
p = @p;
hence thesis by A19,FINSEQ_1:def 11;
end;
A20: <*[0, 0]*> in X by A2;
X is A()-closed by A6,A18,A20,A15,A10,A7;
then QC-WFF(A()) c= X by Def11;
then F9 in X;
then ex F99 being Element of QC-WFF(A()) st F9 = F99 & Prop[F99];
hence thesis;
end;
definition
let A be QC-alphabet;
let F be Element of QC-WFF(A);
attr F is atomic means
:Def18:
ex k being Nat, p being (
QC-pred_symbol of k, A), ll being QC-variable_list of k, A st F = p!ll;
attr F is negative means
:Def19:
ex p being Element of QC-WFF(A) st F = 'not' p;
attr F is conjunctive means
:Def20:
ex p, q being Element of QC-WFF(A) st F = p '&' q;
attr F is universal means
:Def21:
ex x being bound_QC-variable of A,
p being Element of QC-WFF(A) st F = All(x, p);
end;
theorem Th9:
for F being Element of QC-WFF(A) holds F = VERUM(A) or F is atomic or
F is negative or F is conjunctive or F is universal
proof
defpred P[Element of QC-WFF(A)] means $1 = VERUM(A) or $1 is atomic or $1 is
negative or $1 is conjunctive or $1 is universal;
A1: P[VERUM(A)];
A2: for p being Element of QC-WFF(A) st P[p] holds P['not' p] by Def19;
A3: for x being bound_QC-variable of A,
p being Element of QC-WFF(A) st P[p] holds P[All(x, p)] by Def21;
A4: for p, q being Element of QC-WFF(A)
st P[p] & P[q] holds P[p '&' q] by Def20;
A5: for k being Nat, p being (QC-pred_symbol of k, A), ll being
QC-variable_list of k,A holds P[p!ll] by Def18;
thus for F being Element of QC-WFF(A)
holds P[F] from QCInd (A5, A1, A2, A4, A3);
end;
theorem Th10:
for F being Element of QC-WFF(A) holds 1 <= len @F
proof
let F be Element of QC-WFF(A);
now
per cases by Th9;
suppose
F = VERUM(A);
hence thesis by FINSEQ_1:39;
end;
suppose
F is atomic;
then consider
k being Nat, p being (QC-pred_symbol of k, A), ll being
QC-variable_list of k, A such that
A1: F = p!ll;
@F = <*p*>^ll by A1,Th8;
then len @F = len <*p*> + len ll by FINSEQ_1:22
.= 1 + len ll by FINSEQ_1:39;
hence thesis by NAT_1:11;
end;
suppose
F is negative;
then consider p being Element of QC-WFF(A) such that
A2: F = 'not' p;
len @F = len <*[1, 0]*> + len @p by A2,FINSEQ_1:22
.= 1 + len @p by FINSEQ_1:39;
hence thesis by NAT_1:11;
end;
suppose
F is conjunctive;
then consider p, q being Element of QC-WFF(A) such that
A3: F = p '&' q;
@F = <*[2, 0]*>^(@p^@q) by A3,FINSEQ_1:32;
then len @F = len <*[2, 0]*> + len (@p^@q) by FINSEQ_1:22
.= 1 + len (@p^@q) by FINSEQ_1:39;
hence thesis by NAT_1:11;
end;
suppose
F is universal;
then consider
x being bound_QC-variable of A, p being Element of QC-WFF(A) such that
A4: F = All(x, p);
@F = <*[3, 0]*>^(<*x*>^@p) by A4,FINSEQ_1:32;
then len @F = len <*[3, 0]*> + len (<*x*>^@p) by FINSEQ_1:22
.= 1 + len (<*x*>^@p) by FINSEQ_1:39;
hence thesis by NAT_1:11;
end;
end;
hence thesis;
end;
reserve Q for QC-pred_symbol of A;
theorem Th11:
for k being Nat, P being QC-pred_symbol of k, A holds
the_arity_of P = k
proof
let k be Nat, P be QC-pred_symbol of k, A;
reconsider P as Element of k-ary_QC-pred_symbols(A);
P in { Q : the_arity_of Q = k };
then ex Q st P = Q & the_arity_of Q = k;
hence thesis;
end;
reserve F, G for (Element of QC-WFF(A)), s for FinSequence;
theorem Th12:
((@F.1)`1 = 0 implies F = VERUM(A)) & ((@F.1)`1 = 1 implies F is
negative) & ((@F.1)`1 = 2 implies F is conjunctive) & ((@F.1)`1 = 3 implies F
is universal) & ((ex k being Nat
st @F.1 is QC-pred_symbol of k, A)
implies F is atomic)
proof
A1: now
per cases by Th9;
case
F is atomic;
then consider
k being Nat, P being (QC-pred_symbol of k, A), ll being
QC-variable_list of k, A such that
A2: F = P!ll;
@F = <*P*>^ll by A2,Th8;
then @F.1 = P by FINSEQ_1:41;
hence ex k being Nat st @F.1 is QC-pred_symbol of k, A;
end;
case
F = VERUM(A);
hence (@F.1)`1 = [0,0]`1
.= 0;
end;
case
F is negative;
then ex p being Element of QC-WFF(A) st F = 'not' p;
then @F.1 = [1, 0] by FINSEQ_1:41;
hence (@F.1)`1 = 1;
end;
case
F is conjunctive;
then consider p, q being Element of QC-WFF(A) such that
A3: F = p '&' q;
@F = <*[2, 0]*>^(@p^@q) by A3,FINSEQ_1:32;
then @F.1 = [2, 0] by FINSEQ_1:41;
hence (@F.1)`1 = 2;
end;
case
F is universal;
then consider
x being bound_QC-variable of A, p being Element of QC-WFF(A) such that
A4: F = All(x, p);
@F = <*[3, 0]*>^(<*x*>^@p) by A4,FINSEQ_1:32;
then @F.1 = [3, 0] by FINSEQ_1:41;
hence (@F.1)`1 = 3;
end;
end;
now
let k be Nat, P be QC-pred_symbol of k, A;
reconsider P9 = P as QC-pred_symbol of A;
P9`1 = 7+the_arity_of P9 by Def8;
hence P`1 <> 0 & P`1 <> 1 & P`1 <> 2 & P`1 <> 3 by NAT_1:11;
end;
hence thesis by A1;
end;
theorem Th13:
@F = @G^s implies @F = @G
proof
defpred P[set] means for F,G,s st len @F = $1 & @F = @G^s holds @F = @G;
A1: for n being Nat st for k being Nat st k < n holds P[k] holds P[n]
proof
let n be Nat such that
A2: for k being Nat st k < n holds for F, G, s st len @F = k & @F = @G
^s holds @F = @G;
let F, G be (Element of QC-WFF(A)), s be FinSequence such that
A3: len @F = n and
A4: @F = @G^s;
dom @G = Seg len @G & 1 <= len @G by Th10,FINSEQ_1:def 3;
then 1 in dom @G;
then
A5: @F.1 = @G.1 by A4,FINSEQ_1:def 7;
A6: len (@G^s) = len @G + len s by FINSEQ_1:22;
now
per cases by Th9;
suppose
A7: F = VERUM(A);
A8: 1 <= len @G by Th10;
A9: len @F = 1 by A7,FINSEQ_1:39;
then len @G <= 1 by A4,A6,NAT_1:11;
then 1 + 0 = 1 + len s by A4,A6,A9,A8,XXREAL_0:1;
then s = {};
hence thesis by A4,FINSEQ_1:34;
end;
suppose
F is atomic;
then consider
k being Nat, P being (QC-pred_symbol of k, A), ll
being QC-variable_list of k, A such that
A10: F = P!ll;
A11: @F = <*P*>^ll by A10,Th8;
then
A12: @G.1 = P by A5,FINSEQ_1:41;
then G is atomic by Th12;
then consider
k9 being Nat, P9 being (QC-pred_symbol of k9, A), ll9
being QC-variable_list of k9, A such that
A13: G = P9!ll9;
A14: @G = <*P9*>^ll9 by A13,Th8;
then
A15: @G.1 = P9 by FINSEQ_1:41;
then <*P*>^ll = <*P*>^(ll9^s) by A4,A11,A12,A14,FINSEQ_1:32;
then ll = ll9^s by FINSEQ_1:33;
then
A16: len ll + 0 = len ll9 + len s by FINSEQ_1:22;
len ll9 = k9 by CARD_1:def 7
.= the_arity_of P by A12,A15,Th11
.= k by Th11
.= len ll by CARD_1:def 7;
then s = {} by A16;
hence thesis by A4,FINSEQ_1:34;
end;
suppose
F is negative;
then consider p being Element of QC-WFF(A) such that
A17: F = 'not' p;
@F.1 = [1, 0] by A17,FINSEQ_1:41;
then (@G.1)`1 = 1 by A5;
then G is negative by Th12;
then consider p9 being Element of QC-WFF(A) such that
A18: G = 'not' p9;
<*[1, 0]*>^@p = <*[1, 0]*>^(@p9^s) by A4,A17,A18,FINSEQ_1:32;
then
A19: @p = @p9^s by FINSEQ_1:33;
len @F = len @p + len <*[1, 0]*> by A17,FINSEQ_1:22
.= len @p + 1 by FINSEQ_1:40;
then len @p < len @F by NAT_1:13;
then @p = @p9 by A2,A3,A19;
then @p9^{} = @p9^s by A19,FINSEQ_1:34;
then s = {} by FINSEQ_1:33;
hence thesis by A4,FINSEQ_1:34;
end;
suppose
F is conjunctive;
then consider p, q being Element of QC-WFF(A) such that
A20: F = p '&' q;
A21: @F = <*[2, 0]*>^(@p^@q) by A20,FINSEQ_1:32;
then
A22: len @F = len (@p^@q) + len <*[2, 0]*> by FINSEQ_1:22
.= len (@p^@q) + 1 by FINSEQ_1:40;
then
A23: len @F = len @p + len @q + 1 by FINSEQ_1:22;
@F.1 = [2, 0] by A21,FINSEQ_1:41;
then (@G.1)`1 = 2 by A5;
then G is conjunctive by Th12;
then consider p9, q9 being Element of QC-WFF(A) such that
A24: G = p9 '&' q9;
A25: len @p9 <= len @p9 + len (@q9^s) by NAT_1:11;
A26: @G = <*[2, 0]*>^(@p9^@q9) by A24,FINSEQ_1:32;
then <*[2, 0]*>^(@p^@q) = <*[2, 0]*>^(@p9^@q9^s) by A4,A21,FINSEQ_1:32;
then
A27: @p^@q = @p9^@q9^s by FINSEQ_1:33
.= @p9^(@q9^s) by FINSEQ_1:32;
then len @F = len @p9 + len (@q9^s) + 1 by A22,FINSEQ_1:22;
then
A28: len @p9 < len @F by A25,NAT_1:13;
len @q <= len @p + len @q by NAT_1:11;
then
A29: len @q < len @F by A23,NAT_1:13;
len @p <= len @p + len @q by NAT_1:11;
then
A30: len @p < len @F by A23,NAT_1:13;
len @p <= len @p9 or len @p9 <= len @p;
then consider a, b, c, d being FinSequence such that
A31: a = @p & b = @p9 or a = @p9 & b = @p and
A32: len a <= len b & a^c = b^d by A27;
ex t being FinSequence st a^t = b by A32,FINSEQ_1:47;
then
A33: @p = @p9 by A2,A3,A31,A30,A28;
then @q = @q9^s by A27,FINSEQ_1:33;
hence thesis by A2,A3,A21,A26,A33,A29;
end;
suppose
F is universal;
then consider
x being bound_QC-variable of A, p being Element of QC-WFF(A) such
that
A34: F = All(x, p);
A35: @F = <*[3, 0]*>^(<*x*>^@p) by A34,FINSEQ_1:32;
then len @F = len (<*x*>^@p) + len <*[3, 0]*> by FINSEQ_1:22
.= len (<*x*>^@p) + 1 by FINSEQ_1:40
.= len <*x*> + len @p + 1 by FINSEQ_1:22
.= 1 + len @p + 1 by FINSEQ_1:40;
then len @p + 1 <= len @F by NAT_1:13;
then
A36: len @p < len @F by NAT_1:13;
@F.1 = [3, 0] by A35,FINSEQ_1:41;
then (@G.1)`1 = 3 by A5;
then G is universal by Th12;
then consider
x9 being bound_QC-variable of A,p9 being Element of QC-WFF(A) such that
A37: G = All(x9, p9);
<*[3, 0]*>^<*x*>^@p = <*[3, 0]*>^(<*x9*>^@p9)^s by A4,A34,A37,
FINSEQ_1:32
.= <*[3, 0]*>^(<*x9*>^@p9^s) by FINSEQ_1:32;
then
A38: <*x*>^@p = <*x9*>^@p9^s by A34,A35,FINSEQ_1:33
.= <*x9*>^(@p9^s) by FINSEQ_1:32;
then
A39: x = (<*x9*>^(@p9^s)).1 by FINSEQ_1:41
.= x9 by FINSEQ_1:41;
then @p = @p9^s by A38,FINSEQ_1:33;
hence thesis by A2,A3,A34,A37,A39,A36;
end;
end;
hence thesis;
end;
A40: for n being Nat holds P[n] from NAT_1:sch 4(A1);
thus thesis by A40;
end;
definition
let A be QC-alphabet;
let F be Element of QC-WFF(A) such that
A1: F is atomic;
func the_pred_symbol_of F -> QC-pred_symbol of A means
:Def22:
ex k being Nat, ll being (QC-variable_list of k, A),
P being QC-pred_symbol of k, A st it = P
& F = P!ll;
existence
by A1;
uniqueness
proof
let P1, P2 be QC-pred_symbol of A;
given k1 being Nat, ll1 being (QC-variable_list of k1, A), P19
being QC-pred_symbol of k1, A such that
A2: P1 = P19 & F = P19!ll1;
given k2 being Nat, ll2 being (QC-variable_list of k2, A), P29
being QC-pred_symbol of k2, A such that
A3: P2 = P29 & F = P29!ll2;
A4: <*P1*>^ll1 = F by A2,Th8
.= <*P2*>^ll2 by A3,Th8;
thus P1 = (<*P1*>^ll1).1 by FINSEQ_1:41
.= P2 by A4,FINSEQ_1:41;
end;
end;
definition
let A be QC-alphabet;
let F be Element of QC-WFF(A) such that
A1: F is atomic;
func the_arguments_of F -> FinSequence of QC-variables(A) means
:Def23:
ex k
being Nat, P being (QC-pred_symbol of k, A),
ll being QC-variable_list
of k, A st it = ll & F = P!ll;
existence
by A1;
uniqueness
proof
let ll1, ll2 be FinSequence of QC-variables(A);
given k1 being Nat, P1 being (QC-pred_symbol of k1, A),
ll19 being
QC-variable_list of k1, A such that
A2: ll1 = ll19 and
A3: F = P1!ll19;
A4: F = <*P1*>^ll19 by A3,Th8;
given k2 being Nat, P2 being (QC-pred_symbol of k2, A),
ll29 being QC-variable_list of k2, A such that
A5: ll2 = ll29 and
A6: F = P2!ll29;
A7: F = <*P2*>^ll29 by A6,Th8;
P1 = the_pred_symbol_of F by A1,A3,Def22
.= P2 by A1,A6,Def22;
hence thesis by A2,A5,A4,A7,FINSEQ_1:33;
end;
end;
definition
let A be QC-alphabet;
let F be Element of QC-WFF(A) such that
A1: F is negative;
func the_argument_of F -> QC-formula of A means
:Def24:
F = 'not' it;
existence by A1;
uniqueness by FINSEQ_1:33;
end;
definition
let A be QC-alphabet;
let F be Element of QC-WFF(A) such that
A1: F is conjunctive;
func the_left_argument_of F -> QC-formula of A means
:Def25:
ex q being Element of QC-WFF(A) st F = it '&' q;
existence by A1;
uniqueness
proof
let p1, p2 be QC-formula of A;
given q1 being Element of QC-WFF(A) such that
A2: F = p1 '&' q1;
given q2 being Element of QC-WFF(A) such that
A3: F = p2 '&' q2;
<*[2, 0]*>^(@p1^@q1) = p2 '&' q2 by A2,A3,FINSEQ_1:32
.= <*[2, 0]*>^(@p2^@q2) by FINSEQ_1:32;
then
A4: @p1^@q1 = @p2^@q2 by FINSEQ_1:33;
len @p1 <= len @p2 or len @p2 <= len @p1;
then consider a, b, c, d being FinSequence such that
A5: a = @p1 & b = @p2 or a = @p2 & b = @p1 and
A6: len a <= len b & a^c = b^d by A4;
ex t being FinSequence st a^t = b by A6,FINSEQ_1:47;
hence thesis by A5,Th13;
end;
end;
definition
let A be QC-alphabet;
let F be Element of QC-WFF(A) such that
A1: F is conjunctive;
func the_right_argument_of F -> QC-formula of A means
:Def26:
ex p being Element of QC-WFF(A) st F = p '&' it;
existence
by A1;
uniqueness
proof
let q1, q2 be QC-formula of A;
given p1 being Element of QC-WFF(A) such that
A2: F = p1 '&' q1;
given p2 being Element of QC-WFF(A) such that
A3: F = p2 '&' q2;
<*[2, 0]*>^(@p1^@q1) = p2 '&' q2 by A2,A3,FINSEQ_1:32
.= <*[2, 0]*>^(@p2^@q2) by FINSEQ_1:32;
then
A4: @p1^@q1 = @p2^@q2 by FINSEQ_1:33;
p1 = the_left_argument_of F by A1,A2,Def25
.= p2 by A1,A3,Def25;
hence thesis by A4,FINSEQ_1:33;
end;
end;
definition
let A be QC-alphabet;
let F be Element of QC-WFF(A) such that
A1: F is universal;
func bound_in F -> bound_QC-variable of A means
:Def27:
ex p being Element of QC-WFF(A) st F = All(it, p);
existence by A1;
uniqueness
proof
let x1, x2 be bound_QC-variable of A;
given p1 being Element of QC-WFF(A) such that
A2: F = All(x1, p1);
given p2 being Element of QC-WFF(A) such that
A3: F = All(x2, p2);
<*[3, 0]*>^(<*x1*>^@p1) = All(x2, p2) by A2,A3,FINSEQ_1:32
.= <*[3, 0]*>^(<*x2*>^@p2) by FINSEQ_1:32;
then
A4: <*x1*>^@p1 = <*x2*>^@p2 by FINSEQ_1:33;
thus x1 = (<*x1*>^@p1).1 by FINSEQ_1:41
.= x2 by A4,FINSEQ_1:41;
end;
func the_scope_of F -> QC-formula of A means
:Def28:
ex x being bound_QC-variable of A st F = All(x, it);
existence
by A1;
uniqueness
proof
let p1, p2 be QC-formula of A;
given x1 being bound_QC-variable of A such that
A5: F = All(x1, p1);
given x2 being bound_QC-variable of A such that
A6: F = All(x2, p2);
<*[3, 0]*>^(<*x1*>^@p1) = All(x2, p2) by A5,A6,FINSEQ_1:32
.= <*[3, 0]*>^(<*x2*>^@p2) by FINSEQ_1:32;
then
A7: <*x1*>^@p1 = <*x2*>^@p2 by FINSEQ_1:33;
x1 = (<*x1*>^@p1).1 by FINSEQ_1:41
.= x2 by A7,FINSEQ_1:41;
hence thesis by A7,FINSEQ_1:33;
end;
end;
reserve p for Element of QC-WFF(A);
theorem Th14:
p is negative implies len @the_argument_of p < len @p
proof
assume
A1: p is negative;
then consider q being Element of QC-WFF(A) such that
A2: p = 'not' q;
len @p = len <*[1, 0]*> + len @q by A2,FINSEQ_1:22
.= len @q + 1 by FINSEQ_1:40;
then len @q < len @p by NAT_1:13;
hence thesis by A1,A2,Def24;
end;
theorem Th15:
p is conjunctive implies len @the_left_argument_of p < len @p &
len @the_right_argument_of p < len @p
proof
assume
A1: p is conjunctive;
then consider l, q being Element of QC-WFF(A) such that
A2: p = l '&' q;
p = <*[2, 0]*>^(@l^@q) by A2,FINSEQ_1:32;
then
A3: len @p = len <*[2, 0]*> + len (@l^@q) by FINSEQ_1:22
.= len (@l^@q) + 1 by FINSEQ_1:40;
A4: len @q + len @l = len (@l^@q) by FINSEQ_1:22;
then len @q <= len (@l^@q) by NAT_1:11;
then
A5: len @q < len @p by A3,NAT_1:13;
len @l <= len (@l^@q) by A4,NAT_1:11;
then len @l < len @p by A3,NAT_1:13;
hence thesis by A1,A2,A5,Def25,Def26;
end;
theorem Th16:
p is universal implies len @the_scope_of p < len @p
proof
assume
A1: p is universal;
then consider x being bound_QC-variable of A, q being Element of QC-WFF(A)
such that
A2: p = All(x, q);
len @q + len <*x*> = len (<*x*>^@q) by FINSEQ_1:22;
then
A3: len @q <= len (<*x*>^@q) by NAT_1:11;
p = <*[3, 0]*>^(<*x*>^@q) by A2,FINSEQ_1:32;
then len @p = len <*[3, 0]*> + len (<*x*>^@q) by FINSEQ_1:22
.= len (<*x*>^@q) + 1 by FINSEQ_1:40;
then len @q < len @p by A3,NAT_1:13;
hence thesis by A1,A2,Def28;
end;
scheme
QCInd2 { A() -> QC-alphabet, P[Element of QC-WFF(A())] }:
for p being Element of QC-WFF(A()) holds P[p]
provided
A1: for p being Element of QC-WFF(A()) holds (p is atomic implies P[p]) & P[
VERUM(A())] & (p is negative & P[the_argument_of p] implies P[p]) & (p is
conjunctive & P[the_left_argument_of p] & P[the_right_argument_of p] implies P[
p]) & (p is universal & P[the_scope_of p] implies P[p])
proof
A2: now
let x be bound_QC-variable of A(), p be Element of QC-WFF(A()) such that
A3: P[p];
A4: All(x, p) is universal;
then p = the_scope_of All(x, p) by Def28;
hence P[All(x, p)] by A1,A3,A4;
end;
A5: now
let p be Element of QC-WFF(A()) such that
A6: P[p];
A7: 'not' p is negative;
then p= the_argument_of 'not' p by Def24;
hence P['not' p] by A1,A6,A7;
end;
A8: now
let p, q be Element of QC-WFF(A()) such that
A9: ( P[p])& P[q];
A10: p '&' q is conjunctive;
then
p = the_left_argument_of (p '&' q) & q = the_right_argument_of (p '&'
q) by Def25,Def26;
hence P[p '&' q] by A1,A9,A10;
end;
A11: for k be Nat, P be (QC-pred_symbol of k, A()), ll be
QC-variable_list of k, A() holds P[P!ll] by A1,Def18;
A12: P[VERUM(A())] by A1;
thus for p be Element of QC-WFF(A())
holds P[p] from QCInd (A11, A12, A5, A8, A2);
end;
reserve F for Element of QC-WFF(A);
theorem Th17:
for k being Nat, P being QC-pred_symbol of k, A holds P
`1 <> 0 & P`1 <> 1 & P`1 <> 2 & P`1 <> 3
proof
let k be Nat, P be QC-pred_symbol of k, A;
reconsider P9 = P as QC-pred_symbol of A;
P9`1 = 7+the_arity_of P9 by Def8;
hence thesis by NAT_1:11;
end;
theorem Th18:
(@VERUM(A).1)`1 = 0 & (F is atomic implies
ex k being Nat st @F.1 is QC-pred_symbol of k, A)
& (F is negative implies (@F.1)`1 = 1) &
(F is conjunctive implies (@F.1)`1 = 2) & (F is universal implies (@F.1)`1 = 3)
proof
thus (@VERUM(A).1)`1 = [0,0]`1
.= 0;
thus F is atomic implies ex k being Nat st @F.1 is QC-pred_symbol
of k, A
proof
assume F is atomic;
then consider
k being Nat, P being (QC-pred_symbol of k, A), ll being
QC-variable_list of k, A such that
A1: F = P!ll;
@F = <*P*>^ll by A1,Th8;
then @F.1 = P by FINSEQ_1:41;
hence thesis;
end;
thus F is negative implies (@F.1)`1 = 1
proof
assume F is negative;
then ex p being Element of QC-WFF(A) st F = 'not' p;
then @F.1 = [1, 0] by FINSEQ_1:41;
hence thesis;
end;
thus F is conjunctive implies (@F.1)`1 = 2
proof
assume F is conjunctive;
then consider p, q being Element of QC-WFF(A) such that
A2: F = p '&' q;
@F = <*[2, 0]*>^(@p^@q) by A2,FINSEQ_1:32;
then @F.1 = [2, 0] by FINSEQ_1:41;
hence thesis;
end;
thus F is universal implies (@F.1)`1 = 3
proof
assume F is universal;
then consider
x being bound_QC-variable of A, p being Element of QC-WFF(A) such that
A3: F = All(x, p);
@F = <*[3, 0]*>^(<*x*>^@p) by A3,FINSEQ_1:32;
then @F.1 = [3, 0] by FINSEQ_1:41;
hence thesis;
end;
end;
theorem Th19:
F is atomic implies (@F.1)`1 <> 0 & (@F.1)`1 <> 1 & (@F.1)`1 <>
2 & (@F.1)`1 <> 3
proof
assume F is atomic;
then ex k being Nat st @F.1 is QC-pred_symbol of k, A by Th18;
hence thesis by Th17;
end;
reserve p for Element of QC-WFF(A);
theorem Th20:
not (VERUM(A) is atomic or VERUM(A) is negative or VERUM(A) is
conjunctive or VERUM(A) is universal)
& not (ex p st p is atomic & p is negative
or p is atomic & p is conjunctive or p is atomic & p is universal or p is
negative & p is conjunctive or p is negative & p is universal or p is
conjunctive & p is universal)
proof
(@VERUM(A).1)`1 = 0;
hence not (VERUM(A) is atomic or VERUM(A)
is negative or VERUM(A) is conjunctive or
VERUM(A) is universal) by Th18,Th19;
let p be Element of QC-WFF(A);
A1: p is conjunctive implies (@p.1)`1 = 2 by Th18;
A2: p is universal implies (@p.1)`1 = 3 by Th18;
p is negative implies (@p.1)`1 = 1 by Th18;
hence thesis by A1,A2,Th19;
end;
scheme
QCFuncEx { Al() -> QC-alphabet, D() -> non empty set,
V() -> (Element of D()),
A(Element of QC-WFF(Al())) -> (Element of D()),
N(Element of D()) -> (Element of D()),
C((Element of D()), Element of D()) -> (Element of D()),
Q((Element of QC-WFF(Al())), Element of D()) -> Element of D()} :
ex F being Function of QC-WFF(Al()), D() st F.VERUM(Al()) = V()
& for p being Element of QC-WFF(Al()) holds
(p is atomic implies F.p = A(p)) & (p is
negative implies F.p = N(F.the_argument_of p))
& (p is conjunctive implies F.p =
C(F.the_left_argument_of p, F.the_right_argument_of p))
& (p is universal implies F.p = Q(p, F.the_scope_of p))
proof
defpred Pfn[Function of QC-WFF(Al()), D(), Nat]
means $1.VERUM(Al()) = V()
& for p being Element of QC-WFF(Al()) st len @p <= $2 holds
(p is atomic implies $1.p = A(p))
& (p is negative implies $1.p = N($1.the_argument_of p))
& (p is conjunctive implies $1.p = C($1.the_left_argument_of p,
$1.the_right_argument_of p))
& (p is universal implies $1.p = Q(p, $1.the_scope_of p));
defpred Pfgp[(Element of D()), (Function of QC-WFF(Al()), D()),
Element of QC-WFF(Al())]
means ($3 = VERUM(Al()) implies $1 = V())
& ($3 is atomic implies $1 = A($3))
& ($3 is negative implies $1 = N($2.the_argument_of $3))
& ($3 is conjunctive implies $1 = C($2.the_left_argument_of $3,
$2.the_right_argument_of $3))
& ($3 is universal implies $1 = Q($3, $2.the_scope_of $3));
defpred S[Nat] means ex F being Function of QC-WFF(Al()), D()
st Pfn[F, $1];
defpred Qfn[object, object] means ex p being Element of QC-WFF(Al())
st p = $1 & for g being Function of QC-WFF(Al()), D()
st Pfn[g, len @p qua Nat] holds $2 = g.p;
A1: for n be Nat st S[n] holds S[n+1]
proof
let n be Nat;
given F being Function of QC-WFF(Al()), D() such that
A2: Pfn[F, n];
defpred R[Element of QC-WFF(Al()),Element of D()] means
(len @$1 <> n+1 implies $2 = F.$1) & (len @$1 = n+1 implies Pfgp[$2,F,$1]);
A3: for p be Element of QC-WFF(Al()) ex y be Element of D() st R[p,y]
proof
let p be Element of QC-WFF(Al());
now
per cases by Th9;
case
len @p <> n+1;
take y = F.p;
thus y =F.p;
end;
case
A4: len @p = n+1 & p = VERUM(Al());
take y = V();
thus Pfgp[y, F, p] by A4,Th20;
end;
case
A5: len @p = n+1 & p is atomic;
take y = A(p);
thus Pfgp[y, F, p] by A5,Th20;
end;
case
A6: len @p = n+1 & p is negative;
take y = N(F.the_argument_of p);
thus Pfgp[y, F, p] by A6,Th20;
end;
case
A7: len @p = n+1 & p is conjunctive;
take y = C(F.the_left_argument_of p, F.the_right_argument_of p);
thus Pfgp[y, F, p] by A7,Th20;
end;
case
A8: len @p = n+1 & p is universal;
take y = Q(p, F.the_scope_of p);
thus Pfgp[y, F, p] by A8,Th20;
end;
end;
hence thesis;
end;
consider G being Function of QC-WFF(Al()), D() such that
A9: for p being Element of QC-WFF(Al()) holds R[p,G.p] from FUNCT_2:sch 3 (
A3);
take H = G;
thus Pfn[H, n+1]
proof
thus H.VERUM(Al()) = V()
proof
per cases;
suppose
len @VERUM(Al()) <> n+1;
hence thesis by A2,A9;
end;
suppose
len @VERUM(Al()) = n+1;
hence thesis by A9;
end;
end;
let p be Element of QC-WFF(Al()) such that
A10: len @p <= n+1;
thus p is atomic implies H.p = A(p)
proof
now
per cases;
suppose
len @p <> n+1;
then len @p <= n & H.p = F.p by A9,A10,NAT_1:8;
hence thesis by A2;
end;
suppose
len @p = n+1;
hence thesis by A9;
end;
end;
hence thesis;
end;
thus p is negative implies H.p = N(H.the_argument_of p)
proof
assume
A11: p is negative;
then len @the_argument_of p <> n+1 by A10,Th14;
then
A12: H.the_argument_of p = F.the_argument_of p by A9;
now
per cases;
suppose
len @p <> n+1;
then len @p <= n & H.p = F.p by A9,A10,NAT_1:8;
hence thesis by A2,A11,A12;
end;
suppose
len @p = n+1;
hence thesis by A9,A11,A12;
end;
end;
hence thesis;
end;
thus p is conjunctive implies H.p = C(H.the_left_argument_of p, H.
the_right_argument_of p)
proof
assume
A13: p is conjunctive;
then len @the_right_argument_of p <> n+1 by A10,Th15;
then
A14: H.the_right_argument_of p = F.the_right_argument_of p by A9;
len @the_left_argument_of p <> n+1 by A10,A13,Th15;
then
A15: H.the_left_argument_of p = F.the_left_argument_of p by A9;
now
per cases;
suppose
len @p <> n+1;
then len @p <= n & H.p = F.p by A9,A10,NAT_1:8;
hence thesis by A2,A13,A15,A14;
end;
suppose
len @p = n+1;
hence thesis by A9,A13,A15,A14;
end;
end;
hence thesis;
end;
thus p is universal implies H.p = Q(p, H.the_scope_of p)
proof
assume
A16: p is universal;
then len @the_scope_of p <> n+1 by A10,Th16;
then
A17: H.the_scope_of p = F.the_scope_of p by A9;
now
per cases;
suppose
len @p <> n+1;
then len @p <= n & H.p = F.p by A9,A10,NAT_1:8;
hence thesis by A2,A16,A17;
end;
suppose
len @p = n+1;
hence thesis by A9,A16,A17;
end;
end;
hence thesis;
end;
end;
end;
A18: S[0]
proof
reconsider F = QC-WFF(Al()) --> V() as Function of QC-WFF(Al()), D();
take F;
thus F.VERUM(Al()) = V() by FUNCOP_1:7;
let p be Element of QC-WFF(Al()) such that
A19: len @p <= 0;
1 <= len @p by Th10;
hence thesis by A19;
end;
A20: for n being Nat holds S[n] from NAT_1:sch 2(A18, A1);
then
A21: ex G being Function of QC-WFF(Al()), D()
st Pfn[G, len @VERUM(Al()) qua Nat];
A22: for x being object st x in QC-WFF(Al()) ex y being object st Qfn[x, y]
proof
let x be object;
assume x in QC-WFF(Al());
then reconsider x9 = x as Element of QC-WFF(Al());
consider F being Function of QC-WFF(Al()), D() such that
A23: Pfn[F, len @x9 qua Nat] by A20;
take F.x, x9;
thus x = x9;
let G be Function of QC-WFF(Al()), D() such that
A24: Pfn[G, len @x9 qua Nat];
defpred Prop[Element of QC-WFF(Al())]
means len @$1 <= len@x9 implies F.$1 = G.$1;
A25: now
let p be Element of QC-WFF(Al());
thus p is atomic implies Prop[p]
proof
assume
A26: p is atomic & len @p <= len@x9;
hence F.p = A(p) by A23
.= G.p by A24,A26;
end;
thus Prop[VERUM(Al())] by A23,A24;
thus p is negative & Prop[the_argument_of p] implies Prop[p]
proof
assume that
A27: p is negative and
A28: Prop[the_argument_of p] and
A29: len @p <= len @x9;
len @the_argument_of p < len @p by A27,Th14;
hence F.p = N(G.the_argument_of p) by A23,A27,A28,A29,XXREAL_0:2
.= G.p by A24,A27,A29;
end;
thus p is conjunctive & Prop[the_left_argument_of p] & Prop[
the_right_argument_of p] implies Prop[p]
proof
assume that
A30: p is conjunctive and
A31: ( Prop[the_left_argument_of p])& Prop[the_right_argument_of p ] and
A32: len @p <= len @x9;
len @the_left_argument_of p < len @p & len @the_right_argument_of
p < len @p by A30,Th15;
hence F.p = C(G.the_left_argument_of p, G.the_right_argument_of p) by
A23,A30,A31,A32,XXREAL_0:2
.= G.p by A24,A30,A32;
end;
thus p is universal & Prop[the_scope_of p] implies Prop[p]
proof
assume that
A33: p is universal and
A34: Prop[the_scope_of p] and
A35: len @p <= len @x9;
len @the_scope_of p < len @p by A33,Th16;
hence F.p = Q(p, G.the_scope_of p) by A23,A33,A34,A35,XXREAL_0:2
.= G.p by A24,A33,A35;
end;
end;
for p being Element of QC-WFF(Al()) holds Prop[p] from QCInd2 (A25);
hence thesis;
end;
consider F being Function such that
A36: dom F = QC-WFF(Al()) and
A37: for x being object st x in QC-WFF(Al()) holds Qfn[x, F.x]
from CLASSES1:sch
1 (A22);
rng F c= D()
proof
let y be object;
assume y in rng F;
then consider x being object such that
A38: x in QC-WFF(Al()) & y = F.x by A36,FUNCT_1:def 3;
consider p being Element of QC-WFF(Al()) such that
p = x and
A39: for g being Function of QC-WFF(Al()), D() st Pfn[g, len @p qua Element
of NAT] holds y = g.p by A37,A38;
consider G being Function of QC-WFF(Al()), D() such that
A40: Pfn[G, len @p qua Nat] by A20;
y = G.p by A39,A40;
hence thesis;
end;
then reconsider F as Function of QC-WFF(Al()), D()
by A36,FUNCT_2:def 1,RELSET_1:4;
take F;
Qfn[VERUM(Al()), F.VERUM(Al())] by A37;
hence F.VERUM(Al()) = V() by A21;
let p be Element of QC-WFF(Al());
consider p1 being Element of QC-WFF(Al()) such that
A41: p1 = p and
A42: for g being Function of QC-WFF(Al()), D() st Pfn[g, len @p1 qua Element
of NAT] holds F.p = g.p1 by A37;
consider G being Function of QC-WFF(Al()), D() such that
A43: Pfn[G, len @p1 qua Nat] by A20;
set p9 = the_scope_of p;
A44: ex p1 being Element of QC-WFF(Al()) st p1 = p9 & for g being Function of
QC-WFF(Al()), D() st Pfn[g, len @p1 qua Nat]
holds F.p9 = g.p1 by A37;
A45: F.p = G.p by A41,A42,A43;
hence p is atomic implies F.p = A(p) by A41,A43;
A46: for k being Nat st k < len @p holds Pfn[G, k]
proof
let k be Nat;
assume
A47: k < len @p;
thus G.VERUM(Al()) = V() by A43;
let p9 be Element of QC-WFF(Al());
assume len @p9 <= k;
then len @p9 <= len@p by A47,XXREAL_0:2;
hence thesis by A41,A43;
end;
thus p is negative implies F.p = N(F.the_argument_of p)
proof
set p9 = the_argument_of p;
set k = len @p9;
A48: ex p1 being Element of QC-WFF(Al()) st p1 = p9 & for g being Function of
QC-WFF(Al()), D() st Pfn[g, len @p1 qua Nat]
holds F.p9 = g.p1 by A37;
assume
A49: p is negative;
then k < len @p by Th14;
then Pfn[G, k qua Nat] by A46;
then F.p9 = G.p9 by A48;
hence thesis by A41,A43,A45,A49;
end;
thus p is conjunctive implies F.p = C(F.the_left_argument_of p, F.
the_right_argument_of p)
proof
set p99 = the_right_argument_of p;
set p9 = the_left_argument_of p;
set k9 = len @p9;
set k99 = len @p99;
A50: ex p2 being Element of QC-WFF(Al()) st p2 = p99
& for g being Function of QC-WFF(Al()), D()
st Pfn[g, len @p2 qua Nat] holds F.p99 = g.p2 by A37;
assume
A51: p is conjunctive;
then k9 < len @p by Th15;
then
A52: Pfn[G, k9 qua Nat] by A46;
k99 < len @p by A51,Th15;
then Pfn[G, k99 qua Nat] by A46;
then
A53: F.p99 = G.p99 by A50;
ex p1 being Element of QC-WFF(Al()) st p1 = p9 & for g being Function of
QC-WFF(Al()), D() st Pfn[g, len @p1 qua Nat]
holds F.p9 = g.p1 by A37;
then F.p9 = G.p9 by A52;
hence thesis by A41,A43,A45,A51,A53;
end;
set k = len @p9;
assume
A54: p is universal;
then k < len @p by Th16;
then Pfn[G, k qua Nat] by A46;
then F.p9 = G.p9 by A44;
hence thesis by A41,A43,A45,A54;
end;
reserve j,k for Nat;
definition
let A be QC-alphabet;
let ll be FinSequence of QC-variables(A);
func still_not-bound_in ll -> Subset of bound_QC-variables(A) equals
{ ll.k : 1
<= k & k <= len ll & ll.k in bound_QC-variables(A) };
coherence
proof
set IT = { ll.k : 1 <= k & k <= len ll & ll.k in bound_QC-variables(A) };
now
let x be object;
assume x in IT;
then
ex k being Nat st x = ll.k & 1 <= k & k <= len ll & ll.k
in bound_QC-variables(A);
hence x in bound_QC-variables(A);
end;
hence thesis by TARSKI:def 3;
end;
end;
reserve k for Nat;
definition
let A be QC-alphabet;
let p be QC-formula of A;
func still_not-bound_in p -> Subset of bound_QC-variables(A) means
ex F being Function of QC-WFF(A), bool bound_QC-variables(A)
st it = F.p & for p being Element
of QC-WFF(A) holds F.VERUM(A) = {}
& (p is atomic implies F.p = { (the_arguments_of p
).k : 1 <= k & k <= len the_arguments_of p & (the_arguments_of p).k in
bound_QC-variables(A) })
& (p is negative implies F.p = F.the_argument_of p) & (p
is conjunctive implies F.p = (F.the_left_argument_of p) \/ (F.
the_right_argument_of p)) & (p is universal implies F.p = (F.the_scope_of p) \
{bound_in p});
existence
proof
deffunc Q(Element of QC-WFF(A), Subset of bound_QC-variables(A)) = $2 \ {
bound_in $1};
deffunc C(Subset of bound_QC-variables(A),
Subset of bound_QC-variables(A)) = $1
\/ $2;
deffunc N(Subset of bound_QC-variables(A)) = $1;
deffunc A(Element of QC-WFF(A)) = still_not-bound_in (the_arguments_of $1);
reconsider Emp = {} as Subset of bound_QC-variables(A) by XBOOLE_1:2;
consider F being Function of QC-WFF(A), bool bound_QC-variables(A)
such that A1: F.VERUM(A) = Emp & for p being Element of QC-WFF(A)
holds (p is atomic implies F.p = A(p)) & (p is negative implies F.p
= N(F.the_argument_of p)) & (p is conjunctive implies F.p =
C(F.the_left_argument_of p,F.the_right_argument_of p))
& (p is universal implies F.p = Q(p,F.the_scope_of p)) from QCFuncEx;
take F.p, F;
thus F.p = F.p;
let p be Element of QC-WFF(A);
thus F.VERUM(A) = {} by A1;
thus p is atomic implies F.p = { (the_arguments_of p).k : 1 <= k & k <=
len the_arguments_of p & (the_arguments_of p).k in bound_QC-variables(A) }
proof
assume p is atomic;
then F.p = still_not-bound_in (the_arguments_of p) by A1;
hence thesis;
end;
thus p is negative implies F.p = F.the_argument_of p by A1;
thus p is conjunctive implies F.p = (F.the_left_argument_of p) \/ (F.
the_right_argument_of p) by A1;
assume p is universal;
hence thesis by A1;
end;
uniqueness
proof
let IT,IT9 be Subset of bound_QC-variables(A);
given F1 being Function of QC-WFF(A), bool bound_QC-variables(A) such that
A2: IT = F1.p and
A3: for p being Element of QC-WFF(A) holds F1.VERUM(A) = {} & (p is atomic
implies F1.p = { (the_arguments_of p).k : 1 <= k & k <= len the_arguments_of p
& (the_arguments_of p).k in bound_QC-variables(A) })
& (p is negative implies F1.p = F1.the_argument_of p)
& (p is conjunctive implies F1.p = (F1.the_left_argument_of p)
\/ (F1.the_right_argument_of p))
& (p is universal implies F1.p = (F1.the_scope_of p) \ {bound_in p});
given F2 being Function of QC-WFF(A), bool bound_QC-variables(A) such that
A4: IT9 = F2.p and
A5: for p being Element of QC-WFF(A) holds F2.VERUM(A) = {} & (p is atomic
implies F2.p = { (the_arguments_of p).k : 1 <= k & k <= len the_arguments_of p
& (the_arguments_of p).k in bound_QC-variables(A) })
& (p is negative implies F2.p
= F2.the_argument_of p) & (p is conjunctive implies F2.p = (F2.
the_left_argument_of p) \/ (F2.the_right_argument_of p)) & (p is universal
implies F2.p = (F2.the_scope_of p) \ {bound_in p});
defpred Prop[Element of QC-WFF(A)] means F1.$1 = F2.$1;
A6: for k being Nat, P being (QC-pred_symbol of k, A), ll being
QC-variable_list of k, A holds Prop[P!ll]
proof
let k be Nat, P be (QC-pred_symbol of k, A), ll be
QC-variable_list of k, A;
A7: P!ll is atomic;
then
A8: the_arguments_of P!ll = ll by Def23;
hence F1.(P!ll) = { ll.j : 1 <= j & j <= len ll & ll.j in
bound_QC-variables(A) } by A3,A7
.= F2.(P!ll) by A5,A7,A8;
end;
A9: for p being Element of QC-WFF(A) st Prop[p] holds Prop['not' p]
proof
let p be Element of QC-WFF(A) such that
A10: F1.p = F2.p;
A11: 'not' p is negative;
then
A12: the_argument_of 'not' p = p by Def24;
hence F1.'not' p = F2.p by A3,A10,A11
.= F2.'not' p by A5,A11,A12;
end;
A13: for x being bound_QC-variable of A, p being Element of QC-WFF(A)
holds Prop[p] implies Prop[All(x, p)]
proof
let x be bound_QC-variable of A, p be Element of QC-WFF(A) such that
A14: F1.p = F2.p;
A15: All(x,p) is universal;
then
A16: the_scope_of All(x, p) = p & bound_in All(x, p) = x by Def27,Def28;
hence F1.All(x, p) = (F2.p) \ { x } by A3,A14,A15
.= F2.All(x, p) by A5,A15,A16;
end;
A17: for p, q being Element of QC-WFF(A) st Prop[p] & Prop[q]
holds Prop[p '&' q]
proof
let p, q be Element of QC-WFF(A) such that
A18: F1.p = F2.p & F1.q = F2.q;
A19: p '&' q is conjunctive;
then
A20: the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q
) = q by Def25,Def26;
hence F1.(p '&' q) = (F2.p) \/ (F2.q) by A3,A18,A19
.= F2.(p '&' q) by A5,A19,A20;
end;
A21: Prop[VERUM(A)] by A3,A5;
for p be Element of QC-WFF(A) holds Prop[p] from QCInd(A6,A21,A9, A17,
A13);
hence thesis by A2,A4;
end;
end;
definition
let A be QC-alphabet;
let p be QC-formula of A;
attr p is closed means
still_not-bound_in p = {};
end;
reserve s,t,u,v for QC-symbol of A;
definition
let A;
mode Relation of A -> Relation means :Def32:
it well_orders QC-symbols(A) \ NAT;
existence by WELLORD2:17;
end;
definition
let A,s,t;
pred s <= t means :Def33:
ex n,m st n = s & m = t & n <= m if s in NAT & t in NAT,
[s,t] in the Relation of A if not s in NAT & not t in NAT
otherwise t in NAT;
consistency;
end;
definition
let A,s,t;
pred s < t means
s <= t & s <> t;
end;
theorem Th21:
s <= t & t <= u implies s <= u
proof
set R = the Relation of A;
R well_orders QC-symbols(A) \ NAT by Def32;
then
A1: R is_transitive_in QC-symbols(A) \ NAT by WELLORD1:def 5;
assume
A2: s <= t & t <= u;
per cases;
suppose
A3: s in NAT;
then
A4: t in NAT by A2,Def33;
then
A5: u in NAT by A2,Def33;
consider m,n such that
A6: s = m & t = n & m <= n by A2,A3,A4,Def33;
consider k,j such that
A7: t = k & u = j & k <= j by A2,A4,A5,Def33;
m <= j by A6,A7,XXREAL_0:2;
hence s <= u by A6,A7,Def33,A3,A5;
end;
suppose
A8: not s in NAT;
per cases;
suppose t in NAT;
then u in NAT by A2,Def33;
hence thesis by A8,Def33;
end;
suppose
A9: not t in NAT;
per cases;
suppose u in NAT;
hence thesis by A8,Def33;
end;
suppose
A10: not u in NAT;
then
A11: s in QC-symbols(A) \ NAT & t in QC-symbols(A) \ NAT & u in
QC-symbols(A) \ NAT by A8,A9,XBOOLE_0:def 5;
[s,t] in R & [t,u] in R by A2,A8,A9,A10,Def33;
then [s,u] in R by A1,A11,RELAT_2:def 8;
hence thesis by A8,A10,Def33;
end;
end;
end;
end;
theorem Th22:
t <= t
proof
set R = the Relation of A;
R well_orders QC-symbols(A) \ NAT by Def32;
then
A1: R is_reflexive_in QC-symbols(A) \ NAT by WELLORD1:def 5;
per cases;
suppose t in NAT;
hence thesis by Def33;
end;
suppose
A2: not t in NAT;
then t in QC-symbols(A) \ NAT by XBOOLE_0:def 5;
then [t,t] in the Relation of A by A1,RELAT_2:def 1;
hence thesis by A2,Def33;
end;
end;
theorem Th23:
t <= u & u <= t implies u = t
proof
set R = the Relation of A;
R well_orders QC-symbols(A) \ NAT by Def32;
then
A1: R is_antisymmetric_in QC-symbols(A) \ NAT by WELLORD1:def 5;
assume
A2: t <= u & u <= t;
per cases;
suppose
A3: t in NAT & u in NAT;
then consider n,m such that
A4: t = n & u = m & n <= m by A2,Def33;
consider k,j such that
A5: u = k & t = j & k <= j by A2,A3,Def33;
thus thesis by A4,A5,XXREAL_0:1;
end;
suppose not t in NAT or not u in NAT;
then per cases;
suppose not t in NAT;
then
A6: not t in NAT & not u in NAT by A2,Def33;
then
A7: t in QC-symbols(A) \ NAT & u in QC-symbols(A) \ NAT
by XBOOLE_0:def 5;
[t,u] in R & [u,t] in R by A2,A6,Def33;
hence u = t by A1,A7,RELAT_2:def 4;
end;
suppose not u in NAT;
then
A8: not t in NAT & not u in NAT by A2,Def33;
then
A9: t in QC-symbols(A) \ NAT & u in QC-symbols(A) \ NAT
by XBOOLE_0:def 5;
[t,u] in R & [u,t] in R by A2,A8,Def33;
hence u = t by A1,A9,RELAT_2:def 4;
end;
end;
end;
theorem Th24:
t <= u or u <= t
proof
set R = the Relation of A;
R well_orders QC-symbols(A) \ NAT by Def32;
then R is_connected_in QC-symbols(A) \ NAT & R is_reflexive_in
QC-symbols(A) \ NAT by WELLORD1:def 5;
then
A1: R is_strongly_connected_in QC-symbols(A) \ NAT by ORDERS_1:7;
per cases;
suppose
A2: t in NAT & u in NAT;
then consider n,m such that
A3: n = t & m = u;
n <= m or m <= n;
hence thesis by A3,Def33,A2;
end;
suppose not t in NAT or not u in NAT;
then per cases;
suppose
A4: not t in NAT;
per cases;
suppose u in NAT;
hence thesis by A4,Def33;
end;
suppose
A5: not u in NAT;
then t in QC-symbols(A) \NAT & u in QC-symbols(A) \NAT
by A4,XBOOLE_0:def 5;
then [t,u] in R or [u,t] in R by A1,RELAT_2:def 7;
hence thesis by A4,A5,Def33;
end;
end;
suppose
A6: not u in NAT;
per cases;
suppose t in NAT;
hence thesis by A6,Def33;
end;
suppose
A7: not t in NAT;
then t in QC-symbols(A) \NAT & u in QC-symbols(A) \NAT
by A6,XBOOLE_0:def 5;
then [u,t] in R or [t,u] in R by A1,RELAT_2:def 7;
hence thesis by A6,A7,Def33;
end;
end;
end;
end;
theorem Th25:
s < t iff not t <= s
by Th23,Th24;
theorem
s < t or s = t or t < s
by Th25;
definition
let A;
let Y be non empty Subset of QC-symbols(A);
func min Y -> QC-symbol of A means :Def35:
it in Y & for t st t in Y holds it <= t;
existence
proof
per cases;
suppose Y c= NAT;
then reconsider Y as non empty Subset of NAT;
set y = min* Y;
NAT c= QC-symbols(A) by Th3;
then reconsider yp = y as QC-symbol of A;
take yp;
for t st t in Y holds yp <= t
proof
let t;
assume
A1: t in Y;
reconsider t as Nat by A1;
y <= t by A1,NAT_1:def 1;
hence thesis by A1,Def33;
end;
hence thesis by NAT_1:def 1;
end;
suppose not Y c= NAT;
then consider a being object such that
A2: a in Y & not a in NAT;
set R = the Relation of A;
R well_orders QC-symbols(A) \ NAT & Y \ NAT <> {}
by A2,Def32,XBOOLE_0:def 5;
then consider y being object such that
A3: (y in Y \ NAT &
(for b being object st b in Y \ NAT holds [y,b] in R))
by WELLORD1:5,XBOOLE_1:33;
reconsider y as QC-symbol of A by A3;
A4: not y in NAT & y in Y by A3,XBOOLE_0:def 5;
for s st s in Y holds y <= s
proof
let s;
assume
A5: s in Y;
per cases;
suppose s in NAT;
hence thesis by A4,Def33;
end;
suppose
A6: not s in NAT;
then s in Y \ NAT by A5,XBOOLE_0:def 5;
then [y,s] in R by A3;
hence thesis by A4,A6,Def33;
end;
end;
hence thesis by A4;
end;
end;
uniqueness
proof
let t,u such that
A7: (t in Y & for s st s in Y holds t <= s) &
(u in Y & for s st s in Y holds u <= s);
t <= u & u <= t by A7;
hence thesis by Th23;
end;
end;
definition
let A;
func 0(A) -> QC-symbol of A means
for t holds it <= t;
existence
proof
QC-symbols(A) c= QC-symbols(A);
then reconsider symb = QC-symbols(A) as non empty Subset of QC-symbols(A);
set z = min symb;
take z;
thus thesis by Def35;
end;
uniqueness
proof
let s,t such that
A1: (for u holds s <= u) & (for u holds t <= u);
s <= t & t <= s by A1;
hence thesis by Th23;
end;
end;
definition
let A,s;
func Seg s -> non empty Subset of QC-symbols(A) equals
{ t : s < t };
coherence
proof
set e = { t : s < t };
A1: e c= QC-symbols(A)
proof
let a be object;
assume a in e;
then consider t such that
A2: a = t & s < t;
thus thesis by A2;
end;
ex a being set st a in e
proof
per cases;
suppose
A3: s in NAT;
then consider n such that
A4: s = n;
reconsider a = n+1 as Nat;
NAT c= QC-symbols(A) by Th3;
then reconsider b = a as QC-symbol of A;
not n = a & n <= a by NAT_1:19;
then s <= b & not s = b by A4,Def33,A3;
then s < b;
then b in { t : s < t };
hence thesis;
end;
suppose
A5: not s in NAT;
reconsider a = 0 as QC-symbol of A by Th3;
not s = a & s <= a by A5,Def33;
then s < a;
then a in e;
hence thesis;
end;
end;
hence thesis by A1;
end;
end;
definition
let A,s;
func s++ -> QC-symbol of A equals
min (Seg s);
coherence;
end;
theorem Th27:
s < s++
proof
s++ in Seg s by Def35;
then consider t such that
A1: t = s++ & s < t;
thus thesis by A1;
end;
theorem
for Y1,Y2 being non empty Subset of QC-symbols(A) st Y1 c= Y2 holds
min Y2 <= min Y1
proof
let Y1,Y2 be non empty Subset of QC-symbols(A) such that
A1: Y1 c= Y2;
min Y1 in Y1 by Def35;
hence min Y2 <= min Y1 by A1,Def35;
end;
theorem Th29:
s <= t & t < v implies s < v
by Th21,Th25;
theorem
s < t & t <= v implies s < v
by Th21,Th25;
definition
let A;
let s be set;
func s@A -> QC-symbol of A equals :Def39:
s if s is QC-symbol of A
otherwise 0;
correctness by Th3;
end;
definition
let A,t,n;
func t + n -> QC-symbol of A means :Def40:
ex f being sequence of QC-symbols(A) st
it = f.n & f.0 = t & for k holds f.(k+1) = (f.k)++;
existence
proof
deffunc F(set,set) = ($2@A)++;
consider f being sequence of QC-symbols(A) such that
A1: f.0 = t & for k being Nat holds f.(k+1) = F(k,f.k) from NAT_1:sch 12;
take f.n;
for k holds f.(k+1) = (f.k)++
proof
let k;
(f.k)++ = F(k,f.k) & F(k,f.k) = f.(k+1) by A1,Def39;
hence thesis;
end;
hence thesis by A1;
end;
uniqueness
proof
let u,v such that
A2: (ex f being sequence of QC-symbols(A) st f.n = u & f.0 = t &
for k holds f.(k+1) = (f.k)++) & (ex g being sequence of QC-symbols(A)
st g.n = v & g.0 = t & for k holds g.(k+1) = (g.k)++);
consider f being sequence of QC-symbols(A) such that
A3: f.n = u & f.0 = t & for k holds f.(k+1) = (f.k)++ by A2;
consider g being sequence of QC-symbols(A) such that
A4: g.n = v & g.0 = t & for k holds g.(k+1) = (g.k)++ by A2;
defpred P[Nat] means f.($1) = g.($1);
A5: P[0] by A3,A4;
A6: for k st P[k] holds P[k+1]
proof
let k;
assume
A7: P[k];
thus f.(k+1) = (f.k)++ by A3
.= g.(k+1) by A4,A7;
end;
for k holds P[k] from NAT_1:sch 2(A5,A6);
hence thesis by A3,A4;
end;
end;
theorem
t <= t+n
proof
defpred P[Nat] means t <= t + $1;
A1: P[0]
proof
consider f being sequence of QC-symbols(A) such that
A2: t + 0 = f.0 & f.0 = t & for k holds f.(k+1) = (f.k)++ by Def40;
thus thesis by A2,Th22;
end;
A3: for k st P[k] holds P[k+1]
proof
let k such that
A4: t <= t + k;
consider f being sequence of QC-symbols(A) such that
A5: t + (k+1) = f.(k+1) & f.0 = t & for k holds f.(k+1) = (f.k)++ by Def40;
f.k = t + k by A5,Def40;
then f.(k+1) = (t + k)++ by A5;
then t < t + (k+1) by A5,A4,Th27,Th29;
hence thesis;
end;
for n holds P[n] from NAT_1:sch 2(A1,A3);
hence thesis;
end;
definition
let A;
let Y be set;
func A-one_in Y -> QC-symbol of A equals
the Element of Y if Y is non empty Subset of QC-symbols(A)
otherwise 0(A);
coherence
proof
thus Y is non empty Subset of QC-symbols(A)
implies the Element of Y is QC-symbol of A
proof
assume
A1: Y is non empty Subset of QC-symbols(A);
consider a being set such that
A2: a = the Element of Y;
A3: a in Y by A1,A2;
a is QC-symbol of A by A1,A3;
hence thesis by A2;
end;
thus not Y is non empty Subset of QC-symbols(A)
implies 0(A) is QC-symbol of A;
end;
consistency;
end;