:: Similarity of Formulae
:: by Agata Darmochwa{\l} and Andrzej Trybulec
::
:: Received November 22, 1991
:: Copyright (c) 1991-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, FUNCT_1, RELAT_1, FUNCT_4, FUNCOP_1, TARSKI, XBOOLE_0,
SUBSET_1, CQC_LANG, QC_LANG1, ZF_LANG, REALSET1, XXREAL_0, FINSEQ_1,
XBOOLEAN, CLASSES2, BVFUNC_2, NAT_1, ARYTM_3, CARD_1, FUNCT_2, MARGREL1,
FINSUB_1, ZFMISC_1, FINSET_1, ZF_LANG1, RCOMP_1, PARTFUN1, SETWISEO,
SETFAM_1, MEMBER_1, CQC_SIM1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS,
DOMAIN_1, MCART_1, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1,
XCMPLX_0, PARTFUN1, XXREAL_0, FUNCOP_1, FINSEQ_1, FINSET_1, FINSUB_1,
NAT_1, SETWISEO, QC_LANG1, QC_LANG2, QC_LANG3, CQC_LANG, FUNCT_4,
RECDEF_1, SEQ_4;
constructors SETFAM_1, PARTFUN1, BINOP_1, DOMAIN_1, FUNCT_4, SETWISEO,
XXREAL_0, NAT_1, RECDEF_1, SEQ_4, QC_LANG3, CQC_LANG, XXREAL_2, RELSET_1,
XTUPLE_0, XXREAL_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, FUNCT_2, FINSUB_1,
XXREAL_0, FINSEQ_1, QC_LANG1, CQC_LANG, FINSET_1, FUNCOP_1, RELSET_1,
RELAT_1;
requirements NUMERALS, REAL, BOOLE, SUBSET;
definitions TARSKI, XBOOLE_0;
equalities BINOP_1, QC_LANG3, SUBSET_1, RELAT_1, FUNCOP_1;
expansions TARSKI, XBOOLE_0;
theorems ZFMISC_1, DOMAIN_1, FINSEQ_1, CQC_LANG, QC_LANG1, PARTFUN1, QC_LANG3,
FUNCT_1, FUNCT_2, NAT_1, TARSKI, FUNCOP_1, FUNCT_4, FINSEQ_2, SETFAM_1,
QC_LANG2, RELAT_1, RELSET_1, FINSEQ_3, XBOOLE_0, XBOOLE_1, XXREAL_0,
CARD_1, XTUPLE_0, ORDINAL1;
schemes CQC_LANG, CLASSES1, NAT_1, FRAENKEL, QC_LANG1, FUNCT_1, BINOP_1,
CARD_2, FUNCT_2;
begin
reserve A for QC-alphabet;
definition
let A;
let b be bound_QC-variable of A;
func x. b -> QC-symbol of A means :Def1:
x.it = b;
existence by QC_LANG3:30;
uniqueness by XTUPLE_0:1;
end;
theorem Th1:
for x,y being set, f being Function holds Im(f+*(x .--> y),x) = { y}
proof
let x,y be set, f be Function;
now
let u be object;
thus u in (f+*(x .--> y)).:{x} implies u = y
proof
assume u in (f+*(x .--> y)).:{x};
then consider z being object such that
z in dom(f+*(x .--> y)) and
A1: z in {x} and
A2: u = (f+*(x .--> y)).z by FUNCT_1:def 6;
z in dom(x .--> y) by A1;
then u = (x .--> y).z by A2,FUNCT_4:13;
hence thesis by A1,FUNCOP_1:7;
end;
A3: x in {x} by TARSKI:def 1;
then
A4: x in dom(x .--> y);
then
A5: x in dom(f+*(x .--> y)) by FUNCT_4:12;
(x .--> y).x = y by A3,FUNCOP_1:7;
then y = (f+*(x .--> y)).x by A4,FUNCT_4:13;
hence u = y implies u in (f+*(x .--> y)).:{x} by A3,A5,FUNCT_1:def 6;
end;
hence thesis by TARSKI:def 1;
end;
theorem Th2:
for K,L being set for x,y being set, f being Function holds (f+*(
L --> y)).:K c= f.:K \/ {y}
proof
let K,L be set, x,y be set, f be Function, z be object;
assume z in (f+*(L --> y)).:K;
then consider u being object such that
A1: u in dom(f+*(L --> y)) and
A2: u in K and
A3: z = (f+*(L --> y)).u by FUNCT_1:def 6;
A4: dom(L --> y) = L;
now
per cases;
case
A5: u in L;
then z = (L --> y).u by A3,A4,FUNCT_4:13;
then z = y by A5,FUNCOP_1:7;
hence z in {y} by TARSKI:def 1;
end;
case
A6: not u in L;
then
A7: z = f.u by A3,A4,FUNCT_4:11;
u in dom f by A1,A4,A6,FUNCT_4:12;
hence z in f.:K by A2,A7,FUNCT_1:def 6;
end;
end;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th3:
for x,y being set, g being Function, A being set holds (g +* (x
.--> y)).:(A \ {x}) = g.:(A \ {x})
proof
let x,y be set, g be Function, A be set;
thus (g +* (x .--> y)).:(A \ {x}) c= g.:(A \ {x})
proof
let u be object;
A1: dom(x .--> y) = {x};
assume u in (g +* (x .--> y)).:(A \ {x});
then consider z being object such that
A2: z in dom(g +* (x .--> y)) and
A3: z in A \ {x} and
A4: u = (g +* (x .--> y)).z by FUNCT_1:def 6;
A5: not z in {x} by A3,XBOOLE_0:def 5;
then
A6: z in dom g by A2,A1,FUNCT_4:12;
u = g.z by A4,A5,A1,FUNCT_4:11;
hence thesis by A3,A6,FUNCT_1:def 6;
end;
let u be object;
assume u in g.:(A \ {x});
then consider z being object such that
A7: z in dom g and
A8: z in A \ {x} and
A9: u = g.z by FUNCT_1:def 6;
not z in {x} by A8,XBOOLE_0:def 5;
then not z in dom(x .--> y);
then
A10: u = (g +* (x .--> y)).z by A9,FUNCT_4:11;
z in dom(g +* (x .--> y)) by A7,FUNCT_4:12;
hence thesis by A8,A10,FUNCT_1:def 6;
end;
theorem Th4:
for x,y being set for g being Function for A being set st not y
in g.:(A \ {x}) holds (g +* (x .--> y)).:(A \ {x}) = (g +* (x .--> y)).:A \ {y}
proof
let x,y be set, g be Function, A be set;
assume
A1: not y in g.:(A \ {x});
thus (g +* (x .--> y)).:(A \ {x}) c= (g +* (x .--> y)).:A \ {y}
proof
let u be object;
A2: dom(x .--> y) = {x};
assume
A3: u in (g +* (x .--> y)).:(A \ {x});
then consider z being object such that
A4: z in dom(g +* (x .--> y)) and
A5: z in A \ {x} and
A6: u = (g +* (x .--> y)).z by FUNCT_1:def 6;
A7: not z in {x} by A5,XBOOLE_0:def 5;
then
A8: z in dom g by A4,A2,FUNCT_4:12;
u = g.z by A6,A7,A2,FUNCT_4:11;
then u <> y by A1,A5,A8,FUNCT_1:def 6;
then
A9: not u in {y} by TARSKI:def 1;
(g +* (x .--> y)).:(A \ {x}) c= (g +* (x .--> y)).: A by RELAT_1:123;
hence thesis by A3,A9,XBOOLE_0:def 5;
end;
let u be object;
assume
A10: u in (g +* (x .--> y)).:A \ {y};
then consider z being object such that
A11: z in dom(g +* (x .--> y)) and
A12: z in A and
A13: u = (g +* (x .--> y)).z by FUNCT_1:def 6;
now
assume
A14: z in {x};
then z in dom(x .--> y);
then u = (x .--> y).z by A13,FUNCT_4:13;
then u = y by A14,FUNCOP_1:7;
then u in {y} by TARSKI:def 1;
hence contradiction by A10,XBOOLE_0:def 5;
end;
then z in A \ {x} by A12,XBOOLE_0:def 5;
hence thesis by A11,A13,FUNCT_1:def 6;
end;
reserve i,j,k,l,m,n for Nat;
reserve a,b,e for set;
reserve t,u,v,w,z for QC-symbol of A;
reserve p,q,r,s for Element of CQC-WFF(A);
reserve x for Element of bound_QC-variables(A);
reserve ll for CQC-variable_list of k,A;
reserve P for QC-pred_symbol of k,A;
theorem Th5:
p is atomic implies ex k,P,ll st p = P!ll
proof
assume p 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: p = P!ll by QC_LANG1:def 18;
reconsider k as Element of NAT by ORDINAL1:def 12;
reconsider ll as QC-variable_list of k,A;
A2: { ll.m where m is Nat
: 1 <= m & m <= len ll & ll.m in fixed_QC-variables(A) } = {} by A1,
CQC_LANG:7;
{ ll.i where i is Nat:
1 <= i & i <= len ll & ll.i in free_QC-variables(A) } = {} by A1,
CQC_LANG:7;
then ll is CQC-variable_list of k,A by A2,CQC_LANG:5;
hence thesis by A1;
end;
theorem
p is negative implies ex q st p = 'not' q
proof
assume p is negative;
then consider r being Element of QC-WFF(A) such that
A1: p = 'not' r by QC_LANG1:def 19;
r is Element of CQC-WFF(A) by A1,CQC_LANG:8;
hence thesis by A1;
end;
theorem
p is conjunctive implies ex q,r st p = q '&' r
proof
assume p is conjunctive;
then consider q, r being Element of QC-WFF(A) such that
A1: p = q '&' r by QC_LANG1:def 20;
A2: r is Element of CQC-WFF(A) by A1,CQC_LANG:9;
q is Element of CQC-WFF(A) by A1,CQC_LANG:9;
hence thesis by A1,A2;
end;
theorem
p is universal implies ex x,q st p = All(x,q)
proof
assume p is universal;
then consider x being bound_QC-variable of A,
q being Element of QC-WFF(A) such that
A1: p = All(x,q) by QC_LANG1:def 21;
q is Element of CQC-WFF(A) by A1,CQC_LANG:13;
hence thesis by A1;
end;
theorem Th9:
for l being FinSequence holds rng l = { l.i : 1 <= i & i <= len l }
proof
let l be FinSequence;
thus rng l c= { l.i : 1 <= i & i <= len l }
proof
let a be object;
assume a in rng l;
then consider x being object such that
A1: x in dom l and
A2: a = l.x by FUNCT_1:def 3;
reconsider k = x as Element of NAT by A1;
A3: k <= len l by A1,FINSEQ_3:25;
1 <= k by A1,FINSEQ_3:25;
hence thesis by A2,A3;
end;
thus { l.i : 1 <= i & i <= len l } c= rng l
proof
let a be object;
assume a in { l.i : 1 <= i & i <= len l };
then consider k being Nat such that
A4: a = l.k and
A5: 1 <= k and
A6: k <= len l;
k in dom l by A5,A6,FINSEQ_3:25;
hence thesis by A4,FUNCT_1:def 3;
end;
end;
scheme
QCFuncExN { Al() -> QC-alphabet, D() -> non empty set,
V() -> Element of D(), A(object) -> Element of D(),
N(object,object) -> Element of D(),
C(object,object,object) -> Element of D(), Q(object,object) -> 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)) &
(p is conjunctive implies F.p = C(F.the_left_argument_of p,
F.the_right_argument_of p, p)) & (p is universal implies F.p =
Q(F.the_scope_of p, p))
proof
defpred Pfn[Function of QC-WFF(Al()), D(), Nat]
means for p being Element of
QC-WFF(Al()) st len @p <= $2 holds (p = VERUM(Al()) implies $1.p = V()) &
(p is atomic implies $1.p = A(p)) & (p is negative implies $1.p =
N($1.the_argument_of p, p)) & (p is conjunctive implies $1.p =
C($1.the_left_argument_of p, $1.the_right_argument_of p, p)) &
(p is universal implies $1.p = Q($1.the_scope_of p, 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)) & ($3 is conjunctive implies $1 =
C($2.the_left_argument_of $3, $2.the_right_argument_of $3, $3)) &
($3 is universal implies $1 = Q($2.the_scope_of $3,$3));
defpred S[Nat] means ex F being Function of QC-WFF(Al()), D()
st Pfn[F,$1];
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 P[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 x being Element of QC-WFF(Al()) ex y being Element of D() st P[x,y]
proof
let p be Element of QC-WFF(Al());
now
per cases by QC_LANG1:9;
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,QC_LANG1:20;
end;
case
A5: len @p = n+1 & p is atomic;
take y = A(p);
thus Pfgp[y, F, p] by A5,QC_LANG1:20;
end;
case
A6: len @p = n+1 & p is negative;
take y = N(F.the_argument_of p, p);
thus Pfgp[y, F, p] by A6,QC_LANG1:20;
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, p);
thus Pfgp[y, F, p] by A7,QC_LANG1:20;
end;
case
A8: len @p = n+1 & p is universal;
take y = Q(F.the_scope_of p, p);
thus Pfgp[y, F, p] by A8,QC_LANG1:20;
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 P[p,G.p] from FUNCT_2:sch 3 (
A3);
take H = G;
thus Pfn[H, n+1]
proof
let p be Element of QC-WFF(Al()) such that
A10: len @p <= n+1;
thus p = VERUM(Al()) implies H.p = V()
proof
now
per cases;
suppose
A11: len @p <> n+1;
then
A12: H.p = F.p by A9;
len @p <= n by A10,A11,NAT_1:8;
hence thesis by A2,A12;
end;
suppose
len @p = n+1;
hence thesis by A9;
end;
end;
hence thesis;
end;
thus p is atomic implies H.p = A(p)
proof
now
per cases;
suppose
A13: len @p <> n+1;
then
A14: H.p = F.p by A9;
len @p <= n by A10,A13,NAT_1:8;
hence thesis by A2,A14;
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,p)
proof
assume
A15: p is negative;
then len @the_argument_of p <> n+1 by A10,QC_LANG1:14;
then
A16: H.the_argument_of p = F.the_argument_of p by A9;
now
per cases;
suppose
A17: len @p <> n+1;
then
A18: H.p = F.p by A9;
len @p <= n by A10,A17,NAT_1:8;
hence thesis by A2,A15,A16,A18;
end;
suppose
len @p = n+1;
hence thesis by A9,A15,A16;
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, p)
proof
assume
A19: p is conjunctive;
then len @the_right_argument_of p <> n+1 by A10,QC_LANG1:15;
then
A20: H.the_right_argument_of p = F.the_right_argument_of p by A9;
len @the_left_argument_of p <> n+1 by A10,A19,QC_LANG1:15;
then
A21: H.the_left_argument_of p = F.the_left_argument_of p by A9;
now
per cases;
suppose
A22: len @p <> n+1;
then
A23: H.p = F.p by A9;
len @p <= n by A10,A22,NAT_1:8;
hence thesis by A2,A19,A21,A20,A23;
end;
suppose
len @p = n+1;
hence thesis by A9,A19,A21,A20;
end;
end;
hence thesis;
end;
thus p is universal implies H.p = Q(H.the_scope_of p, p)
proof
assume
A24: p is universal;
then len @the_scope_of p <> n+1 by A10,QC_LANG1:16;
then
A25: H.the_scope_of p = F.the_scope_of p by A9;
now
per cases;
suppose
A26: len @p <> n+1;
then
A27: H.p = F.p by A9;
len @p <= n by A10,A26,NAT_1:8;
hence thesis by A2,A24,A25,A27;
end;
suppose
len @p = n+1;
hence thesis by A9,A24,A25;
end;
end;
hence thesis;
end;
end;
end;
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] holds $2 = g.p;
A28: S[0]
proof
set F =the Function of QC-WFF(Al()), D();
take F;
thus thesis by QC_LANG1:10;
end;
A29: for n being Nat holds S[n] from NAT_1:sch 2(A28, A1);
A30: 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
A31: Pfn[F, len @x9] by A29;
take F.x, x9;
thus x = x9;
let G be Function of QC-WFF(Al()), D() such that
A32: Pfn[G, len @x9];
defpred Prop[Element of QC-WFF(Al())] means
len @$1 <= len@x9 implies F.$1 = G.
$1;
A33: now
let p be Element of QC-WFF(Al());
thus p is atomic implies Prop[p]
proof
assume that
A34: p is atomic and
A35: len @p <= len@x9;
thus F.p = A(p) by A31,A34,A35
.= G.p by A32,A34,A35;
end;
thus Prop[VERUM(Al())]
proof
assume
A36: len @VERUM(Al()) <= len @x9;
hence F.VERUM(Al()) = V() by A31
.= G.VERUM(Al()) by A32,A36;
end;
thus p is negative & Prop[the_argument_of p] implies Prop[p]
proof
assume that
A37: p is negative and
A38: Prop[the_argument_of p] and
A39: len @p <= len @x9;
len @the_argument_of p < len @p by A37,QC_LANG1:14;
hence F.p = N(G.the_argument_of p, p) by A31,A37,A38,A39,XXREAL_0:2
.= G.p by A32,A37,A39;
end;
thus p is conjunctive & Prop[the_left_argument_of p] & Prop[
the_right_argument_of p] implies Prop[p]
proof
assume that
A40: p is conjunctive and
A41: Prop[the_left_argument_of p] and
A42: Prop[the_right_argument_of p] and
A43: len @p <= len @x9;
A44: len @the_right_argument_of p < len @p by A40,QC_LANG1:15;
len @the_left_argument_of p < len @p by A40,QC_LANG1:15;
hence F.p = C(G.the_left_argument_of p, G.the_right_argument_of p, p)
by A31,A40,A41,A42,A43,A44,XXREAL_0:2
.= G.p by A32,A40,A43;
end;
thus p is universal & Prop[the_scope_of p] implies Prop[p]
proof
assume that
A45: p is universal and
A46: Prop[the_scope_of p] and
A47: len @p <= len @x9;
len @the_scope_of p < len @p by A45,QC_LANG1:16;
hence F.p = Q(G.the_scope_of p, p) by A31,A45,A46,A47,XXREAL_0:2
.= G.p by A32,A45,A47;
end;
end;
for p being Element of QC-WFF(Al()) holds Prop[p] from QC_LANG1:sch 2 (A33
);
hence thesis;
end;
consider F being Function such that
A48: dom F = QC-WFF(Al()) and
A49: for x being object st x in QC-WFF(Al()) holds Qfn[x, F.x]
from CLASSES1:sch
1 (A30);
rng F c= D()
proof
let y be object;
assume y in rng F;
then consider x being object such that
A50: x in QC-WFF(Al()) and
A51: y = F.x by A48,FUNCT_1:def 3;
consider p being Element of QC-WFF(Al()) such that
p = x and
A52: for g being Function of QC-WFF(Al()), D() st Pfn[g, len @p] holds y =
g.p by A49,A50,A51;
consider G being Function of QC-WFF(Al()), D() such that
A53: Pfn[G, len @p] by A29;
y = G.p by A52,A53;
hence thesis;
end;
then reconsider F as Function of QC-WFF(Al()),
D() by A48,FUNCT_2:def 1,RELSET_1:4;
consider p1 being Element of QC-WFF(Al()) such that
A54: p1 = VERUM(Al()) and
A55: for g being Function of QC-WFF(Al()), D() st Pfn[g, len @p1] holds F.
VERUM(Al()) = g.p1 by A49;
take F;
consider G being Function of QC-WFF(Al()), D() such that
A56: Pfn[G, len @p1] by A29;
F.VERUM(Al()) = G.VERUM(Al()) by A54,A55,A56;
hence F.VERUM(Al()) = V() by A54,A56;
let p be Element of QC-WFF(Al());
consider p1 being Element of QC-WFF(Al()) such that
A57: p1 = p and
A58: for g being Function of QC-WFF(Al()), D() st Pfn[g, len @p1] holds F.p =
g.p1 by A49;
consider G being Function of QC-WFF(Al()), D() such that
A59: Pfn[G, len @p1] by A29;
set p9 = the_scope_of p;
A60: 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] holds F.p9 = g.p1 by A49;
A61: F.p = G.p by A57,A58,A59;
hence p is atomic implies F.p = A(p) by A57,A59;
A62: for k being Element of NAT st k < len @p holds Pfn[G, k]
proof
let k be Element of NAT;
assume
A63: k < len @p;
let p9 be Element of QC-WFF(Al());
assume len @p9 <= k;
then len @p9 <= len@p by A63,XXREAL_0:2;
hence thesis by A57,A59;
end;
thus p is negative implies F.p = N(F.the_argument_of p, p)
proof
set p9 = the_argument_of p;
set k = len @p9;
A64: 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] holds F.p9 = g.p1 by A49;
assume
A65: p is negative;
then k < len @p by QC_LANG1:14;
then Pfn[G, k] by A62;
then F.p9 = G.p9 by A64;
hence thesis by A57,A59,A61,A65;
end;
thus p is conjunctive implies F.p = C(F.the_left_argument_of p, F.
the_right_argument_of p, p)
proof
set p99 = the_right_argument_of p;
set p9 = the_left_argument_of p;
set k9 = len @p9;
set k99 = len @p99;
A66: 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] holds F.p99 = g.p2 by A49;
assume
A67: p is conjunctive;
then k9 < len @p by QC_LANG1:15;
then
A68: Pfn[G, k9] by A62;
k99 < len @p by A67,QC_LANG1:15;
then Pfn[G, k99] by A62;
then
A69: F.p99 = G.p99 by A66;
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] holds F.p9 = g.p1 by A49;
then F.p9 = G.p9 by A68;
hence thesis by A57,A59,A61,A67,A69;
end;
set k = len @p9;
assume
A70: p is universal;
then k < len @p by QC_LANG1:16;
then Pfn[G, k] by A62;
then F.p9 = G.p9 by A60;
hence thesis by A57,A59,A61,A70;
end;
scheme
CQCF2FuncEx { Al() -> QC-alphabet, D, E() -> non empty set,
V() -> Element of Funcs(D(),E()),
A(object,object,object) -> Element of Funcs(D(),E()),
N(object,object) -> Element of Funcs(D(),E()),
C(object,object,object,object) -> Element of Funcs(D(),E()),
Q(object,object,object) -> Element of Funcs(D(),E()) }
:
ex F being Function of CQC-WFF(Al()), Funcs(D(),E()) st
F.VERUM(Al()) = V() & (for k for l being CQC-variable_list of k,Al()
for P being QC-pred_symbol of k,Al() holds F.(P!l) = A(k,P,l)) &
for r,s being Element of CQC-WFF(Al())
for x being Element of bound_QC-variables(Al())
holds F.('not' r) = N(F.r,r) & F.(r '&' s) = C(F.r,F.s,r,s) &
F.All(x,r) = Q(x,F.r,r)
proof
deffunc q(set,Element of QC-WFF(Al())) = Q(bound_in $2,$1,the_scope_of $2);
deffunc c(set,set,Element of QC-WFF(Al())) =
C($1,$2, the_left_argument_of $3,the_right_argument_of $3);
deffunc n(set,Element of QC-WFF(Al())) = N($1,the_argument_of $2);
deffunc a(Element of QC-WFF(Al())) = A(the_arity_of the_pred_symbol_of $1,
the_pred_symbol_of $1,the_arguments_of $1);
consider F being Function of QC-WFF(Al()), Funcs(D(),E()) such that
A1: 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)) &
(p is conjunctive implies F.p = c(F.the_left_argument_of p,F.
the_right_argument_of p,p)) & (p is universal implies F.p = q(F.the_scope_of p,
p)) from QCFuncExN;
reconsider G = F|CQC-WFF(Al()) as Function of CQC-WFF(Al()),Funcs(D(),E())
by FUNCT_2:32;
take G;
thus G.VERUM(Al()) = V() by A1,FUNCT_1:49;
thus for k for l being CQC-variable_list of k,Al()
for P being QC-pred_symbol of
k,Al() holds G.(P!l) = A(k,P,l)
proof
let k;
let l be CQC-variable_list of k,Al();
let P be QC-pred_symbol of k,Al();
A2: the_arity_of P = k by QC_LANG1:11;
A3: P!l is atomic by QC_LANG1:def 18;
then
A4: the_arguments_of (P!l) = l by QC_LANG1:def 23;
A5: the_pred_symbol_of (P!l) = P by A3,QC_LANG1:def 22;
thus G.(P!l) = F.(P!l) by FUNCT_1:49
.= A(k,P,l) by A1,A3,A4,A5,A2;
end;
let r,s be Element of CQC-WFF(Al()),x be Element of bound_QC-variables(Al());
set r9 = G.r, s9 = G.s;
A6: r9 = F.r by FUNCT_1:49;
A7: 'not' r is negative by QC_LANG1:def 19;
then
A8: the_argument_of 'not' r = r by QC_LANG1:def 24;
thus G.('not' r) = F.('not' r) by FUNCT_1:49
.= N(r9,r) by A1,A6,A7,A8;
A9: s9 = F.s by FUNCT_1:49;
A10: r '&' s is conjunctive by QC_LANG1:def 20;
then
A11: the_left_argument_of(r '&' s) = r by QC_LANG1:def 25;
A12: the_right_argument_of(r '&' s) = s by A10,QC_LANG1:def 26;
thus G.(r '&' s) = F.(r '&' s) by FUNCT_1:49
.= C(r9,s9,r,s) by A1,A6,A9,A10,A11,A12;
A13: All(x,r) is universal by QC_LANG1:def 21;
then
A14: bound_in All(x,r) = x by QC_LANG1:def 27;
A15: the_scope_of All(x,r) = r by A13,QC_LANG1:def 28;
thus G.All(x,r) = F.All(x,r) by FUNCT_1:49
.= Q(x,r9,r) by A1,A6,A13,A14,A15;
end;
scheme
CQCF2FUniq { Al() -> QC-alphabet, D, E() -> non empty set, F1,
F2() -> Function of CQC-WFF(Al()),Funcs(D(),E()),
V() -> Function of D(),E(),
A(object,object,object) -> Function of D(),E(),
N(object,object) -> Function of D(),E(),
C(object,object,object,object) -> Function of D(),E(),
Q(object,object,object) -> Function of D(),E() }
:
F1() = F2()
provided
A1: F1().VERUM(Al()) = V() and
A2: for k for ll be CQC-variable_list of k,Al()
for P be QC-pred_symbol of k,Al()
holds F1().(P!ll) = A(k,P,ll) and
A3: for r,s be Element of CQC-WFF(Al())
for x be Element of bound_QC-variables(Al())
holds F1().('not' r) = N(F1().r,r) &
F1().(r '&' s) = C(F1().r,F1().s,r,s) & F1().All(x,r) = Q(x,F1().r,r) and
A4: F2().VERUM(Al()) = V() and
A5: for k for ll be CQC-variable_list of k,Al()
for P be QC-pred_symbol of k,Al()
holds F2().(P!ll) = A(k,P,ll) and
A6: for r,s be Element of CQC-WFF(Al())
for x be Element of bound_QC-variables(Al())
holds F2().('not' r) = N(F2().r,r) &
F2().(r '&' s) = C(F2().r,F2().s,r,s) & F2().All(x,r) = Q(x,F2().r,r)
proof
defpred P[set] means F1().$1 = F2().$1;
A7: for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k being Nat
for ll being CQC-variable_list of k,Al()
for P being QC-pred_symbol of k,Al()
holds P[VERUM(Al())] & P[P!ll] &
(P[r] implies P['not' r]) &
(P[r] & P[s] implies P[r '&' s]) & (P[r] implies P[All(x, r)])
proof
let r,s be Element of CQC-WFF(Al());
let x be Element of bound_QC-variables(Al());
let k be Nat;
let ll be CQC-variable_list of k,Al();
let P be QC-pred_symbol of k,Al();
thus F1().VERUM(Al()) = F2().VERUM(Al()) by A1,A4;
reconsider k as Element of NAT by ORDINAL1:def 12;
reconsider l1=ll as CQC-variable_list of k,Al();
F1().(P!l1) = A(k,P,l1) by A2;
hence F1().(P!ll) = F2().(P!ll) by A5;
F1().('not' r) = N(F1().r,r) by A3;
hence F1().r = F2().r implies F1().('not' r) = F2().('not' r) by A6;
F1().(r '&' s) = C(F1().r,F1().s,r,s) by A3;
hence F1().r = F2().r & F1().s = F2().s implies F1().(r '&' s) = F2().(r
'&' s) by A6;
F1().All(x,r) = Q(x,F1().r,r) by A3;
hence thesis by A6;
end;
for r being Element of CQC-WFF(Al()) holds P[r] from CQC_LANG:sch 1(A7);
hence thesis by FUNCT_2:63;
end;
theorem Th10:
p is_subformula_of 'not' p
proof
p is_proper_subformula_of 'not' p by QC_LANG2:66;
hence thesis by QC_LANG2:def 21;
end;
theorem Th11:
p is_subformula_of p '&' q & q is_subformula_of p '&' q
proof
A1: q is_proper_subformula_of p '&' q by QC_LANG2:69;
p is_proper_subformula_of p '&' q by QC_LANG2:69;
hence thesis by A1,QC_LANG2:def 21;
end;
theorem Th12:
p is_subformula_of All(x,p)
proof
p is_proper_subformula_of All(x,p) by QC_LANG2:71;
hence thesis by QC_LANG2:def 21;
end;
theorem Th13:
for l being CQC-variable_list of k,A, i st 1<=i & i<=len l holds l
.i in bound_QC-variables(A)
proof
let l be CQC-variable_list of k,A, i;
assume that
A1: 1<=i and
A2: i<=len l;
i in dom l by A1,A2,FINSEQ_3:25;
then
A3: l.i in rng l by FUNCT_1:def 3;
rng l c= bound_QC-variables(A) by RELAT_1:def 19;
hence thesis by A3;
end;
definition
let A;
let D be non empty set, f be Function of D, CQC-WFF(A);
func NEGATIVE f -> Element of Funcs(D, CQC-WFF(A)) means
:Def2:
for a being
Element of D for p being Element of CQC-WFF(A) st p=f.a holds it.a = 'not' p;
existence
proof
defpred P[set,set] means for p being Element of CQC-WFF(A) st p=f.$1 holds
$2 = 'not' p;
A1: for e being Element of D ex u being Element of CQC-WFF(A) st P[e,u]
proof
let e be Element of D;
reconsider p = f.e as Element of CQC-WFF(A);
take 'not' p;
thus thesis;
end;
consider F being Function of D,CQC-WFF(A) such that
A2: for e being Element of D holds P[e,F.e] from FUNCT_2:sch 3(A1);
F is Element of Funcs(D,CQC-WFF(A)) by FUNCT_2:8;
hence thesis by A2;
end;
uniqueness
proof
let F,G be Element of Funcs(D,CQC-WFF(A));
assume
A3: for a being Element of D holds for p being Element of CQC-WFF(A) st p
=f.a holds F.a = 'not' p;
assume
A4: for a being Element of D holds for p being Element of CQC-WFF(A) st p
=f.a holds G.a = 'not' p;
for a being Element of D holds F.a = G.a
proof
let a be Element of D;
consider p such that
A5: p=f.a;
thus F.a = 'not' p by A3,A5
.=G.a by A4,A5;
end;
hence F=G by FUNCT_2:63;
end;
end;
reserve f,h for Element of Funcs(bound_QC-variables(A),bound_QC-variables(A)),
K,L for Element of Fin bound_QC-variables(A);
definition
let A;
let f,g be Function of [:QC-symbols(A),Funcs(bound_QC-variables(A),
bound_QC-variables(A)):],
CQC-WFF(A), n be Nat;
func CON(f,g,n) -> Element of Funcs([:QC-symbols(A),
Funcs(bound_QC-variables(A), bound_QC-variables(A)):], CQC-WFF(A)) means
:Def3:
for t,h,p,q st p = f.(t,h) & q = g .(t+n,h) holds it.(t,h) = p '&' q;
existence
proof
defpred P[Element of QC-symbols(A),set,set] means
for p,q st p = f.[$1,$2] & q = g.[$1+n,$2] holds $3 = p '&' q;
A1: for t,h ex u being Element of CQC-WFF(A) st P[t,h,u]
proof
let t,h;
reconsider p=f.([t,h]) as Element of CQC-WFF(A);
reconsider q=g.([t+n,h]) as Element of CQC-WFF(A);
take p '&' q;
let p1,q1 be Element of CQC-WFF(A);
assume that
A2: p1=f.[t,h] and
A3: q1=g.[t+n,h];
thus thesis by A2,A3;
end;
consider F being Function of [:QC-symbols(A),Funcs(bound_QC-variables(A),
bound_QC-variables(A)):],CQC-WFF(A) such that
A4: for t,h holds P[t,h,F.(t,h)] from BINOP_1:sch 3(A1);
reconsider F as Element of Funcs([:QC-symbols(A),
Funcs(bound_QC-variables(A), bound_QC-variables(A)):],CQC-WFF(A))
by FUNCT_2:8;
take F;
let t,h,p,q;
assume that
A5: p = f.(t,h) and
A6: q = g.(t+n,h);
thus thesis by A4,A5,A6;
end;
uniqueness
proof
let F,G be Element of Funcs([:QC-symbols(A),Funcs(bound_QC-variables(A),
bound_QC-variables(A)):],CQC-WFF(A));
assume
A7: for t,h,p,q holds p = f.(t,h) & q = g.(t+n,h) implies F.(t,h) = p '&' q;
assume
A8: for t,h,p,q holds p = f.(t,h) & q = g.(t+n,h) implies G.(t,h) = p '&' q;
for a being Element of [:QC-symbols(A),Funcs(bound_QC-variables(A),
bound_QC-variables(A)):] holds F.a = G.a
proof
let a be Element of [:QC-symbols(A),Funcs(bound_QC-variables(A),
bound_QC-variables(A)):];
consider k being Element of QC-symbols(A), h being Element of Funcs(
bound_QC-variables(A),bound_QC-variables(A)) such that
A9: a=[k,h] by DOMAIN_1:1;
reconsider q=g.(k+n,h) as Element of CQC-WFF(A);
reconsider p=f.(k,h) as Element of CQC-WFF(A);
F.(k,h) = p '&' q by A7
.=G.(k,h) by A8;
hence thesis by A9;
end;
hence F=G by FUNCT_2:63;
end;
end;
Lm1: h+*(x .--> x.t) is Function of bound_QC-variables(A),
bound_QC-variables(A)
proof
A1: rng (h+*(x .--> x.t)) c= rng h \/ rng(x .--> x.t) by FUNCT_4:17;
A2: rng(x .--> x.t) c= bound_QC-variables(A) by RELAT_1:def 19;
rng h c= bound_QC-variables(A) by RELAT_1:def 19;
then
A3: rng h \/ rng(x .--> x.t) c= bound_QC-variables(A) by A2,XBOOLE_1:8;
dom (h+*(x .--> x.t)) = dom h \/ dom({x}-->x.t) by FUNCT_4:def 1
.= dom h \/ {x}
.= bound_QC-variables(A) \/ {x} by FUNCT_2:52
.= bound_QC-variables(A) by ZFMISC_1:40;
hence thesis by A1,A3,FUNCT_2:2,XBOOLE_1:1;
end;
definition
let A;
let f be Function of
[:QC-symbols(A),Funcs(bound_QC-variables(A),bound_QC-variables(A)):],
CQC-WFF(A),x be bound_QC-variable of A;
func UNIVERSAL(x,f) -> Element of Funcs([:QC-symbols(A),
Funcs(bound_QC-variables(A), bound_QC-variables(A)):],CQC-WFF(A)) means
:Def4:
for t,h,p st p = f.(t++,h +* (x .--> x.t)) holds it.(t,h)=All(x.t,p);
existence
proof
defpred P[Element of QC-symbols(A), Element of Funcs(bound_QC-variables(A),
bound_QC-variables(A)),set] means for p st
p=f.[$1++,$2+*({x} --> x.$1)] holds $3 = All(x.$1,p);
A1: for t,h ex u being Element of CQC-WFF(A) st P[t,h,u]
proof
let t,h;
reconsider h2=h+*(x .--> x.t) as Function of bound_QC-variables(A),
bound_QC-variables(A) by Lm1;
reconsider h2 as Element of Funcs(bound_QC-variables(A),
bound_QC-variables(A)) by FUNCT_2:8;
reconsider q=f.([t++,h2]) as Element of CQC-WFF(A);
take All(x.t,q);
thus thesis;
end;
consider F being Function of [:QC-symbols(A),Funcs(bound_QC-variables(A),
bound_QC-variables(A)):],CQC-WFF(A) such that
A2: for t,h holds P[t,h,F.(t,h)] from BINOP_1:sch 3(A1);
reconsider F as Element of Funcs([:QC-symbols(A),
Funcs(bound_QC-variables(A), bound_QC-variables(A)):],CQC-WFF(A))
by FUNCT_2:8;
take F;
let t,h,p;
assume p=f.(t++,h+*(x .--> x.t));
hence thesis by A2;
end;
uniqueness
proof
let F,G be Element of Funcs([:QC-symbols(A),Funcs(bound_QC-variables(A),
bound_QC-variables(A)):],CQC-WFF(A));
assume
A3: for t,h,p st p=f.(t++,h +* (x .--> x.t)) holds F.(t,h)=All(x.t ,p);
assume
A4: for t,h,p st p=f.(t++,h +* (x .--> x.t)) holds G.(t,h)=All(x.t ,p);
for a being Element of [:QC-symbols(A),Funcs(bound_QC-variables(A),
bound_QC-variables(A)):] holds F.a = G.a
proof
let a be Element of [:QC-symbols(A),Funcs(bound_QC-variables(A),
bound_QC-variables(A)):];
consider k being Element of QC-symbols(A), h being Element of Funcs(
bound_QC-variables(A),bound_QC-variables(A)) such that
A5: a=[k,h] by DOMAIN_1:1;
reconsider h2=h+*(x .--> x.k) as Function of bound_QC-variables(A),
bound_QC-variables(A) by Lm1;
reconsider h2 as Element of Funcs(bound_QC-variables(A),
bound_QC-variables(A)) by FUNCT_2:8;
reconsider p=f.(k++,h2) as Element of CQC-WFF(A);
F.(k,h) = All(x.k,p) by A3
.= G.(k,h) by A4;
hence thesis by A5;
end;
hence F=G by FUNCT_2:63;
end;
end;
Lm2: for f being CQC-variable_list of k,A holds f is FinSequence of
bound_QC-variables(A)
proof
let f be CQC-variable_list of k,A;
rng f c= bound_QC-variables(A) by RELAT_1:def 19;
hence thesis by FINSEQ_1:def 4;
end;
definition
let A;
let k;
let l be CQC-variable_list of k,A;
let f be Element of Funcs(bound_QC-variables(A),bound_QC-variables(A));
redefine func f*l -> CQC-variable_list of k,A; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
coherence
proof
reconsider l9=l as FinSequence of bound_QC-variables(A) by Lm2;
reconsider h=f*l9 as FinSequence of bound_QC-variables(A) by FINSEQ_2:32;
len h = len l9 by FINSEQ_2:33
.= k by CARD_1:def 7;
hence thesis by CARD_1:def 7,FINSEQ_2:24;
end;
end;
definition
let A;
let k;
let P be QC-pred_symbol of k,A, l be CQC-variable_list of k,A;
func ATOMIC(P,l) -> Element of Funcs([:QC-symbols(A),
Funcs(bound_QC-variables(A), bound_QC-variables(A)):], CQC-WFF(A)) means
:Def5:
for t,h holds it.(t,h) = P!(h*l);
existence
proof
deffunc f(set,Element of Funcs(bound_QC-variables(A),
bound_QC-variables(A))) = P!($2*l);
consider f being Function of [:QC-symbols(A),Funcs(bound_QC-variables(A),
bound_QC-variables(A)):], CQC-WFF(A) such that
A1: for t,h holds f.(t,h) = f(t,h) from BINOP_1:sch 4;
f is Element of Funcs([:QC-symbols(A),Funcs(bound_QC-variables(A),
bound_QC-variables(A)):], CQC-WFF(A)) by FUNCT_2:8;
hence thesis by A1;
end;
uniqueness
proof
let F,G be Element of Funcs([:QC-symbols(A),Funcs(bound_QC-variables(A),
bound_QC-variables(A)):],CQC-WFF(A));
assume
A2: for t,h holds F.(t,h) = P!(h*l);
assume
A3: for t,h holds G.(t,h) = P!(h*l);
for a being Element of [:QC-symbols(A),Funcs(bound_QC-variables(A),
bound_QC-variables(A)):] holds F.a = G.a
proof
let a be Element of [:QC-symbols(A),Funcs(bound_QC-variables(A),
bound_QC-variables(A)):];
consider k being Element of QC-symbols(A), f being Element of Funcs(
bound_QC-variables(A),bound_QC-variables(A)) such that
A4: a=[k,f] by DOMAIN_1:1;
F.(k,f) = P!(f*l) by A2
.=G.(k,f) by A3;
hence thesis by A4;
end;
hence F=G by FUNCT_2:63;
end;
end;
deffunc A(set,set,set) = 0;
deffunc N(Element of NAT) = $1;
deffunc C(Element of NAT,Element of NAT) = $1 + $2;
deffunc Q(set,Element of NAT) = $2 + 1;
definition
let A;
let p;
func QuantNbr(p) -> Element of NAT means
:Def6:
ex F being Function of
CQC-WFF(A), NAT st it = F.p & F.VERUM(A) = 0 & for r,s,x,k for l being
CQC-variable_list of k,A for P being QC-pred_symbol of k,A holds F.(P!l) = 0 &
F.('not' r) = F.r & F.(r '&' s) = F.r + F.s & F.All(x,r) = F.r + 1;
correctness
proof
thus (ex d being Element of NAT st ex F being Function of CQC-WFF A,
NAT st d = F.p & F.VERUM(A) = 0 &
for r,s being Element of CQC-WFF(A)
for x being bound_QC-variable of A
for k
for l being CQC-variable_list of k, A for P being
QC-pred_symbol of k,A holds F.(P!l) = A(k,P,l) & F.('not' r) = N(F.r) &
F.(r '&' s) = C(F.r,F.s) & F.All(x,r) = Q(x,F.r) ) &
for d1,d2 being Element of NAT st (ex F being Function of CQC-WFF(A),
NAT st d1 = F.p & F.VERUM(A) = 0 &
for r,s being Element of CQC-WFF(A)
for x being bound_QC-variable of A
for k
for l being CQC-variable_list of k, A
for P being QC-pred_symbol of k,A
holds F.(P!l) = A(k,P,l) & F.('not' r) = N(F.r) &
F.(r '&' s) = C(F.r,F.s) & F.All(x,r) = Q(x,F.r) ) &
(ex F being Function of CQC-WFF(A), NAT st d2 = F.p &
F.VERUM(A) = 0 &
for r,s being Element of CQC-WFF(A)
for x being bound_QC-variable of A
for k
for l being CQC-variable_list of k, A
for P being QC-pred_symbol of k,A holds F.(P!l) = A(k,P,l) &
F.('not' r) = N(F.r) & F.(r '&' s) = C(F.r,F.s) &
F.All(x,r) = Q(x,F.r) ) holds d1 = d2 from CQC_LANG:sch 4;
end;
end;
definition
let A;
let f be Function of CQC-WFF(A), Funcs([:QC-symbols(A),
Funcs(bound_QC-variables(A), bound_QC-variables(A)):],CQC-WFF(A)),
x be Element of CQC-WFF(A);
redefine func f.x -> Element of Funcs([:QC-symbols(A), :: redefines . (FUNCT_1, definition)
Funcs(bound_QC-variables(A), bound_QC-variables(A)):],CQC-WFF(A));
coherence
proof
thus f.x is Element of Funcs([:QC-symbols(A),Funcs(bound_QC-variables(A),
bound_QC-variables(A)):],CQC-WFF(A));
end;
end;
definition
let A;
func SepFunc(A) -> Function of CQC-WFF(A),
Funcs([:QC-symbols(A),Funcs(bound_QC-variables(A), bound_QC-variables(A)):],
CQC-WFF(A)) means
:Def7:
it.VERUM(A) = [:QC-symbols(A),Funcs(
bound_QC-variables(A),bound_QC-variables(A)):] --> VERUM(A) &
(for k for l being CQC-variable_list of k,A for P being QC-pred_symbol of k,A
holds it.(P!l)=ATOMIC(P,l)) & for r,s,x holds it.('not' r) = NEGATIVE(it.r)
& it.(r '&' s) = CON(it.r,it.s,QuantNbr(r)) & it.All(x,r) =UNIVERSAL(x,it.r);
existence
proof
deffunc A(Nat,QC-pred_symbol of $1,A,
CQC-variable_list of $1,A) = ATOMIC($2,$3);
set D=[:QC-symbols(A),Funcs(bound_QC-variables(A),bound_QC-variables(A)):];
deffunc N(Function of D, CQC-WFF(A), set) = NEGATIVE $1;
deffunc C(Function of D,CQC-WFF(A), Function of D,CQC-WFF(A),
Element of CQC-WFF(A),set) = CON($1,$2,QuantNbr($3));
deffunc Q(Element of bound_QC-variables(A), Function of D,CQC-WFF(A),set) =
UNIVERSAL($1,$2);
reconsider V = D --> VERUM(A) as Function of D,CQC-WFF(A);
reconsider V as Element of Funcs(D,CQC-WFF(A)) by FUNCT_2:8;
consider F being Function of CQC-WFF(A),Funcs(D,CQC-WFF(A)) such that
A1: F.VERUM(A) = V and
A2: for k for l being CQC-variable_list of k,A for P being
QC-pred_symbol of k,A holds F.(P!l) = A(k,P,l) and
A3: for r,s,x holds F.('not' r) = N(F.r,r) & F.(r '&' s) = C(F.r,F.s,r
,s) & F.All(x,r) = Q(x,F.r,r) from CQCF2FuncEx;
take F;
thus thesis by A1,A2,A3;
end;
uniqueness
proof
deffunc A(Nat,QC-pred_symbol of $1,A,
CQC-variable_list of $1,A)= ATOMIC($2,$3);
set D=[:QC-symbols(A),Funcs(bound_QC-variables(A),bound_QC-variables(A)):];
deffunc N(Function of D, CQC-WFF(A), set) = NEGATIVE $1;
deffunc C(Function of D,CQC-WFF(A), Function of D,CQC-WFF(A),
Element of CQC-WFF(A),set) = CON($1,$2,QuantNbr($3));
deffunc Q(Element of bound_QC-variables(A),Function of D,CQC-WFF(A), set) =
UNIVERSAL($1,$2);
reconsider V = D --> VERUM(A) as Function of D,CQC-WFF(A);
let F,G be Function of CQC-WFF(A),Funcs(D,CQC-WFF(A)) such that
A4: F.VERUM(A) = D --> VERUM(A) and
A5: for k,ll,P holds F.(P!ll) = A(k,P,ll) and
A6: for r,s,x holds F.('not' r) = N(F.r,r) & F.(r '&' s) = C(F.r,F.s,r
,s) & F.All(x,r) = Q(x,F.r,r) and
A7: G.VERUM(A) = D --> VERUM(A) and
A8: for k,ll,P holds G.(P!ll) = A(k,P,ll) and
A9: for r,s,x holds G.('not' r) = N(G.r,r) & G.(r '&' s) = C(G.r,G.s,
r,s) & G.All(x,r) = Q(x,G.r,r);
A10: G.VERUM(A) = V by A7;
A11: F.VERUM(A) = V by A4;
thus F = G from CQCF2FUniq(A11,A5,A6,A10,A8,A9);
end;
end;
definition
let A;
let p,t,f;
func SepFunc(p,t,f) -> Element of CQC-WFF(A) equals
((SepFunc(A)).p).[t,f];
correctness;
end;
theorem
QuantNbr(VERUM(A)) = 0
proof
deffunc F(Element of CQC-WFF(A)) = QuantNbr($1);
A1: for d being Element of NAT holds d = F(p) iff ex F being Function of
CQC-WFF(A), NAT st d = F.p & F.VERUM(A) = 0 & for r,s,x,k for l being
CQC-variable_list of k,A for P being QC-pred_symbol of k,A
holds F.(P!l) = A(k,P,l)
& F.('not' r) = N(F.r) & F.(r '&' s) = C(F.r,F.s) & F.All(x,r) = Q(x,F.r) by
Def6;
thus F(VERUM(A)) = 0 from CQC_LANG:sch 5(A1);
end;
theorem
QuantNbr(P!ll) = 0
proof
deffunc F(Element of CQC-WFF(A)) = QuantNbr($1);
A1: for d being Element of NAT holds d = F(p) iff ex F being Function of
CQC-WFF(A), NAT st d = F.p & F.VERUM(A) = 0 & for r,s,x,k for l being
CQC-variable_list of k,A for P being QC-pred_symbol of k,A
holds F.(P!l) = A(k,P,l)
& F.('not' r) = N(F.r) & F.(r '&' s) = C(F.r,F.s) & F.All(x,r) = Q(x,F.r) by
Def6;
thus F(P!ll) = A(k,P,ll) from CQC_LANG:sch 6(A1);
end;
theorem
QuantNbr('not' p) = QuantNbr(p)
proof
deffunc F(Element of CQC-WFF(A)) = QuantNbr($1);
A1: for p being Element of CQC-WFF(A),
d being Element of NAT holds d = F(p)
iff ex F being Function of CQC-WFF(A), NAT st d = F.p & F.VERUM(A) = 0 &
for r,s,x,k
for l being CQC-variable_list of k,A for P being QC-pred_symbol of k,A holds
F.(P!l) = A(k,P,l) & F.('not' r) = N(F.r) & F.(r '&' s) = C(F.r,F.s) &
F.All(x,r) = Q(x,F.r) by Def6;
thus F('not' p) = N(F(p)) from CQC_LANG:sch 7(A1);
end;
theorem
QuantNbr(p '&' q) = QuantNbr(p) + QuantNbr(q)
proof
deffunc F(Element of CQC-WFF(A)) = QuantNbr($1);
A1: for p being Element of CQC-WFF(A), d being Element of NAT
holds d = F(p)
iff ex F being Function of CQC-WFF(A), NAT st d = F.p & F.VERUM(A) = 0 &
for r,s,x,k
for l being CQC-variable_list of k,A for P being QC-pred_symbol of k,A holds
F.(P!l) = A(k,P,l) & F.('not' r) = N(F.r) & F.(r '&' s) = C(F.r,F.s) &
F.All(x,r) = Q(x,F.r) by Def6;
thus F(p '&' q) = C(F(p), F(q)) from CQC_LANG:sch 8(A1);
end;
theorem
QuantNbr(All(x,p)) = QuantNbr(p) + 1
proof
deffunc F(Element of CQC-WFF(A)) = QuantNbr($1);
A1: for p being Element of CQC-WFF(A), d being Element of NAT holds d = F(p)
iff ex F being Function of CQC-WFF(A), NAT st d = F.p & F.VERUM(A) = 0 &
for r,s,x,k
for l being CQC-variable_list of k,A for P being QC-pred_symbol of k,A holds
F.(P!l) = A(k,P,l) & F.('not' r) = N(F.r) & F.(r '&' s) = C(F.r,F.s) &
F.All(x,r) = Q(x,F.r) by Def6;
thus F(All(x,p)) = Q(x,F(p)) from CQC_LANG:sch 9(A1);
end;
theorem Th19:
for p being Element of QC-WFF(A) holds still_not-bound_in p is finite
proof
defpred P[Element of QC-WFF(A)] means still_not-bound_in $1 is finite;
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
let p be Element of QC-WFF(A);
thus p is atomic implies still_not-bound_in p is finite
proof
deffunc F(set) = (the_arguments_of p).$1;
defpred B[Nat] means 1 <= $1 & $1 <= len the_arguments_of p;
defpred A[Nat] means 1 <= $1 & $1 <= len the_arguments_of p &
(the_arguments_of p).$1 in bound_QC-variables(A);
A2: { F(k) : A[k] } c= { F(n) : B[n]}
proof let e be object;
assume e in { F(k) : A[k] };
then ex k st e=F(k) & A[k];
hence thesis;
end;
assume p is atomic;
then still_not-bound_in p = still_not-bound_in the_arguments_of p by
QC_LANG3:4
.= variables_in(the_arguments_of p,bound_QC-variables(A)) by QC_LANG3:2
.= { (the_arguments_of p).k :
1 <= k & k <= len the_arguments_of p &
(the_arguments_of p).k in bound_QC-variables(A) };
then still_not-bound_in p c= rng (the_arguments_of p) by A2,Th9;
hence thesis;
end;
thus still_not-bound_in VERUM(A) is finite by QC_LANG3:3;
thus p is negative & still_not-bound_in the_argument_of p is finite
implies still_not-bound_in p is finite by QC_LANG3:6;
thus p is conjunctive & still_not-bound_in the_left_argument_of p is
finite & still_not-bound_in the_right_argument_of p is finite implies
still_not-bound_in p is finite
proof
assume that
A3: p is conjunctive and
A4: still_not-bound_in the_left_argument_of p is finite and
A5: still_not-bound_in the_right_argument_of p is finite;
still_not-bound_in p = (still_not-bound_in the_left_argument_of p)
\/ (still_not-bound_in the_right_argument_of p) by A3,QC_LANG3:9;
hence thesis by A4,A5;
end;
assume that
A6: p is universal and
A7: still_not-bound_in the_scope_of p is finite;
still_not-bound_in p = (still_not-bound_in the_scope_of p) \ {
bound_in p} by A6,QC_LANG3:11;
hence thesis by A7;
end;
thus for p being Element of QC-WFF(A) holds P[p] from QC_LANG1:sch 2(A1 );
end;
scheme
MaxFinDomElem {D()->non empty set, X()->set, P[object,object] }:
ex x being
Element of D() st x in X() & for y being Element of D() st y in X() holds P[x,y
]
provided
A1: X() is finite & X() <> {} & X() c= D() and
A2: for x,y being Element of D() holds P[x,y] or P[y,x] and
A3: for x,y,z being Element of D() st P[x,y] & P[y,z] holds P[x,z]
proof
reconsider X = X() as finite set by A1;
A4: X <> {} by A1;
defpred R[object,object] means not $1 in X or ($2 in X & P[$1,$2]);
A5: for x,y,z being object st R[x,y] & R[y,z] holds R[x,z] by A1,A3;
A6: for x,y being object holds R[x,y] or R[y,x] by A1,A2;
consider x being object such that
A7: x in X and
A8: for y being object st y in X holds R[x,y] from CARD_2:sch 2(A4,A6,A5);
reconsider x as Element of D() by A1,A7;
take x;
thus x in X() by A7;
let y be Element of D();
assume y in X();
hence thesis by A7,A8;
end;
definition
let X be set;
redefine func id X -> Element of Funcs(X,X); :: redefines id (RELAT_1, definition)
coherence
proof
id X is Function of X,X;
hence thesis by FUNCT_2:9;
end;
end;
definition
let A;
let p;
func NBI p -> Subset of QC-symbols(A) equals
{t: for u st t<=u holds not x.u in still_not-bound_in p};
coherence
proof
defpred P[QC-symbol of A] means for u st $1<=u holds not x.u in
still_not-bound_in p;
{t: P[t]} c= QC-symbols(A) from FRAENKEL:sch 10;
hence thesis;
end;
end;
registration
let A;
let p;
cluster NBI p -> non empty;
coherence
proof
set A2 = {t: for u st t<=u holds not x.u in still_not-bound_in p};
ex t st t in A2
proof
now
per cases;
suppose
still_not-bound_in p = {};
then 0(A)<=u implies not x.u in still_not-bound_in p;
then
0(A) in {t: for u st t<=u holds not x.u in still_not-bound_in p};
hence thesis;
end;
suppose
A1: still_not-bound_in p <> {};
defpred P[QC-symbol of A] means x.$1 in still_not-bound_in p;
defpred R[object,object] means for t st t=$2 holds x.t = $1;
A2: {t: P[t]} c= QC-symbols(A) from FRAENKEL:sch 10;
A3: for e being object st e in still_not-bound_in p
ex b being object st b in QC-symbols(A) &R[e,b]
proof
let e be object;
assume e in still_not-bound_in p;
then reconsider e as bound_QC-variable of A;
consider t such that
A4: x.t = e by QC_LANG3:30;
reconsider t as set;
take t;
thus thesis by A4;
end;
consider f being Function such that
A5: dom f = still_not-bound_in p & rng f c= QC-symbols(A) and
for e being object st e in still_not-bound_in p holds R[e,f.e] from
FUNCT_1:sch 6(A3);
reconsider f as Function of still_not-bound_in p, QC-symbols(A)
by A5,FUNCT_2:def 1,RELSET_1:4;
set x =the Element of still_not-bound_in p;
reconsider x as bound_QC-variable of A by A1,TARSKI:def 3;
consider t such that
A6: x.t = x by QC_LANG3:30;
A7: ex a st a in {z: x.z in still_not-bound_in p}
proof
take t;
thus thesis by A1,A6;
end;
defpred R[QC-symbol of A, QC-symbol of A] means $2 <= $1;
A8: for t,u holds R[t,u] or R[u,t] by QC_LANG1:24;
A9: for t,u,v st R[t,u] & R[u,v] holds R[t,v] by QC_LANG1:21;
A10: still_not-bound_in p is finite by Th19;
deffunc Z(bound_QC-variable of A) = x.$1;
A11: {Z(b) where b is Element of bound_QC-variables(A) : b in
still_not-bound_in p} is finite from FRAENKEL:sch 21(A10);
{x.b where b is Element of bound_QC-variables(A) : b in
still_not-bound_in p} = { w : x.w in still_not-bound_in p }
proof
set S1 = {x.b where b is Element of bound_QC-variables(A) : b in
still_not-bound_in p};
set S2 = { w : x.w in still_not-bound_in p };
for s being object holds s in S1 implies s in S2
proof
let s be object;
assume s in S1;
then consider b being Element of bound_QC-variables(A) such that
A12: s = x.b & b in still_not-bound_in p;
reconsider s1=s as QC-symbol of A by A12;
x.s1 = b by A12,Def1;
hence thesis by A12;
end;
hence S1 c= S2;
for s being object holds s in S2 implies s in S1
proof
let s be object;
assume s in S2;
then consider w such that
A13: s = w & x.w in still_not-bound_in p;
x.(x.w) = w by Def1;
hence thesis by A13;
end;
hence S2 c= S1;
end;
then
A14: {w : x.w in still_not-bound_in p} is finite & {z: x.z in
still_not-bound_in p} <> {} & {v: x.v in still_not-bound_in p}
c= QC-symbols(A) by A11,A2,A7;
consider v such that
v in {w: x.w in still_not-bound_in p} and
A15: for t st t in {z: x.z in still_not-bound_in p} holds R[v,t]
from MaxFinDomElem(A14,A8,A9);
now
take n=v++;
thus n=v++;
let z;
assume that
A16: v++ <= z and
A17: x.z in still_not-bound_in p;
z in {w: x.w in still_not-bound_in p} by A17;
then z <= v by A15;
then v++ <= v by A16,QC_LANG1:21;
then not v < v++ by QC_LANG1:25;
hence contradiction by QC_LANG1:27;
end;
then v++ in A2;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
end;
definition
let A;
let p;
func index p -> QC-symbol of A equals
min NBI p;
coherence;
end;
theorem Th20:
index p = 0(A) iff p is closed
proof
thus index p = 0(A) implies p is closed
proof
assume index p = 0(A);
then 0(A) in NBI p by QC_LANG1:def 35;
then
consider t such that
A1: t=0(A) & for u st t<=u holds not x.u in still_not-bound_in p;
now
set a =the Element of still_not-bound_in p;
assume
A2: still_not-bound_in p <> {};
then reconsider a as bound_QC-variable of A by TARSKI:def 3;
consider u such that
A3: x.u = a by QC_LANG3:30;
not t <= u by A1,A2,A3;
hence contradiction by A1,QC_LANG1:def 36;
end;
hence thesis by QC_LANG1:def 31;
end;
assume p is closed;
then 0(A)<=t implies not x.t in still_not-bound_in p by QC_LANG1:def 31;
then
A4: 0(A) in NBI p;
0(A) = min NBI p
proof
assume min NBI p <> 0(A);
then consider t such that
A5: 0(A) <> t & t = min NBI p;
t <= 0(A) by A4,A5,QC_LANG1:def 35;
then t < 0(A) by A5,QC_LANG1:def 34;
then not 0(A) <= t by QC_LANG1:25;
hence contradiction by QC_LANG1:def 36;
end;
hence thesis;
end;
theorem Th21:
x.t in still_not-bound_in p implies t < index p
proof
assume
A1: x.t in still_not-bound_in p;
now
min NBI p in NBI p by QC_LANG1:def 35;
then
A2: ex u st u = min NBI p & for t st u<=t holds not x.t in
still_not-bound_in p;
assume min (NBI p) <= t;
hence contradiction by A1,A2;
end;
hence thesis by QC_LANG1:25;
end;
theorem Th22:
index VERUM(A) = 0(A)
proof
VERUM(A) is closed by QC_LANG3:20;
hence thesis by Th20;
end;
theorem Th23:
index ('not' p) = index p
proof
still_not-bound_in p = still_not-bound_in 'not' p by QC_LANG3:7;
hence thesis;
end;
theorem
index p <= index(p '&' q) & index q <= index(p '&' q)
proof
A1: still_not-bound_in(p '&' q) = (still_not-bound_in p) \/ (
still_not-bound_in q) by QC_LANG3:10;
A2: NBI(p '&' q) c= NBI q
proof
let e be object;
assume e in NBI(p '&' q);
then consider t such that
A3: t = e and
A4: for u st t<=u holds not x.u in still_not-bound_in p '&' q;
now
let u;
assume
A5: t<=u;
still_not-bound_in q c= still_not-bound_in p '&' q by A1,XBOOLE_1:7;
hence not x.u in still_not-bound_in q by A4,A5;
end;
hence thesis by A3;
end;
NBI(p '&' q) c= NBI p
proof
let e be object;
assume e in NBI(p '&' q);
then consider t such that
A6: t = e and
A7: for u st t<=u holds not x.u in still_not-bound_in p '&' q;
now
let u;
assume
A8: t<=u;
still_not-bound_in p c= still_not-bound_in p '&' q by A1,XBOOLE_1:7;
hence not x.u in still_not-bound_in p by A7,A8;
end;
hence thesis by A6;
end;
hence thesis by A2,QC_LANG1:28;
end;
definition
let A;
let p;
func SepVar(p) -> Element of CQC-WFF(A) equals
SepFunc(p, index p, id(bound_QC-variables(A)));
coherence;
end;
theorem
SepVar VERUM(A) = VERUM(A)
proof
index VERUM(A) = 0(A) by Th22;
hence SepVar VERUM(A) =
([:QC-symbols(A),Funcs(bound_QC-variables(A),bound_QC-variables(A)):]
--> VERUM(A)).[0(A),id bound_QC-variables(A)] by Def7 .= VERUM(A);
end;
scheme
CQCInd{ A() -> QC-alphabet, P[object] }: for r being Element of CQC-WFF(A())
holds P[r]
provided
A1: P[VERUM(A())] and
A2: for k for l being CQC-variable_list of k,A() for P being QC-pred_symbol
of k,A() holds P[P!l] and
A3: for r being Element of CQC-WFF(A()) st P[r] holds P['not' r] and
A4: for r,s being Element of CQC-WFF(A()) st P[r] & P[s] holds P[r '&' s] and
A5: for r being Element of CQC-WFF(A()), x being bound_QC-variable of A()
st P[r] holds P[All(x, r)]
proof
A6: for r,s being Element of CQC-WFF(A()),x being bound_QC-variable of A(),
k being Nat for l being CQC-variable_list of k,A() for P being
QC-pred_symbol of k,A() holds P[VERUM(A())] & P[P!l] & (P[r] implies
P['not' r]) & (P[r] & P[s] implies P[r '&' s]) & (P[r] implies P[All(x, r)])
by A1,A2,A3,A4,A5;
thus for r being Element of CQC-WFF(A()) holds P[r] from CQC_LANG:sch 1(A6);
end;
theorem Th26:
SepVar(P!ll) = P!ll
proof
A1: dom ll = dom ll;
rng ll c= bound_QC-variables(A) by RELAT_1:def 19;
then reconsider lf = ll as PartFunc of NAT,bound_QC-variables(A) by A1,
RELSET_1:4;
A2: id bound_QC-variables(A)*lf = ll by PARTFUN1:7;
thus SepVar (P!ll) =ATOMIC(P,ll).(index (P!ll),(id bound_QC-variables(A)))
by Def7
.= P!ll by A2,Def5;
end;
theorem
p is atomic implies SepVar p = p
proof
assume p is atomic;
then ex k, P, ll st p = P!ll by Th5;
hence thesis by Th26;
end;
theorem Th28:
SepVar 'not' p = 'not' SepVar p
proof
reconsider FP = (SepFunc(A)).p as Function of
[:QC-symbols(A),Funcs(bound_QC-variables(A), bound_QC-variables(A)):],
CQC-WFF(A);
thus SepVar 'not' p =(NEGATIVE FP).[index ('not' p),id bound_QC-variables(A)]
by Def7
.= (NEGATIVE FP).[index p,(id bound_QC-variables(A))] by Th23
.= 'not' SepVar p by Def2;
end;
theorem
p is negative & q = the_argument_of p implies SepVar p = 'not' SepVar q
proof
assume that
A1: p is negative and
A2: q = the_argument_of p;
p = 'not' q by A1,A2,QC_LANG1:def 24;
hence thesis by Th28;
end;
definition
let A;
let p;
let X be Subset of [:CQC-WFF(A),QC-symbols(A),Fin bound_QC-variables(A),
Funcs(bound_QC-variables(A),bound_QC-variables(A)):];
pred X is_Sep-closed_on p means
[p,index p, {}.bound_QC-variables(A),id
(bound_QC-variables(A))] in X & (for q,t,K,f holds ['not' q,t,K,f] in X
implies [q,t,K,f] in X) & (for q,r,t,K,f holds [q '&' r,t,K,f] in X implies
[q,t,K,f] in X & [r,t+QuantNbr(q),K,f] in X) & for q,x,t,K,f st
[All(x,q),t,K,f] in X holds [q,t++,K \/ {x}, f+*(x .--> x.t)] in X;
end;
definition
let A;
let p;
func SepQuadruples p -> Subset of [:CQC-WFF(A),QC-symbols(A),Fin
bound_QC-variables(A), Funcs(bound_QC-variables(A),bound_QC-variables(A)):]
means :Def13:
it is_Sep-closed_on p & for D being Subset of [:CQC-WFF(A), QC-symbols(A),
Fin bound_QC-variables(A),Funcs(bound_QC-variables(A),
bound_QC-variables(A)):] st D is_Sep-closed_on p holds it c= D;
existence
proof
set S = [:CQC-WFF(A),QC-symbols(A),Fin bound_QC-variables(A),
Funcs(bound_QC-variables(A),bound_QC-variables(A)):];
set A2 = { X where X is Subset of S : X is_Sep-closed_on p };
A2 c= bool S
proof
let a be object;
assume a in A2;
then ex X being Subset of S st X = a & X is_Sep-closed_on p;
hence thesis;
end;
then reconsider A2 as Subset-Family of S;
take X = meet A2;
set B=[#](S);
B is_Sep-closed_on p
proof
thus [p,index p,{}.bound_QC-variables(A),id(bound_QC-variables(A))] in B;
thus for q,t,K,f holds ['not' q,t,K,f] in B implies [q,t,K,f] in B;
thus for q,r,t,K,f holds [q '&' r,t,K,f] in B implies [q,t,K,f] in B & [
r,t+QuantNbr(q),K,f] in B;
let q,x,t,K,f such that
[All(x,q),t,K,f] in B;
A1: rng (f+*(x .--> x.t)) c= rng f \/ rng (x .--> x.t) by FUNCT_4:17;
A2: rng (x .--> x.t) = {x.t} by FUNCOP_1:8;
A3: bound_QC-variables(A) \/ {x.t} =bound_QC-variables(A) by ZFMISC_1:40;
rng f c= bound_QC-variables(A) by RELAT_1:def 19;
then rng f \/ rng(x .--> x.t) c= bound_QC-variables(A)
by A2,A3,XBOOLE_1:9;
then
A4: rng (f+*(x .--> x.t)) c= bound_QC-variables(A) by A1;
dom(f+*(x .--> x.t)) = dom f \/ dom (x .--> x.t) by FUNCT_4:def 1
.= bound_QC-variables(A) \/ dom(x .--> x.t) by FUNCT_2:def 1
.= bound_QC-variables(A) \/ {x}
.= bound_QC-variables(A) by ZFMISC_1:40;
then f+*(x .--> x.t) is Function of bound_QC-variables(A),
bound_QC-variables(A) by A4,FUNCT_2:def 1,RELSET_1:4;
then reconsider
ff = f+*(x .--> x.t) as Element of Funcs(bound_QC-variables(A),
bound_QC-variables(A)) by FUNCT_2:8;
[q,t++,K \/ {.x .}, ff] in B;
hence thesis;
end;
then
A5: B in A2;
for Y being set st Y in A2 holds [p,index p,{}.bound_QC-variables(A),id(
bound_QC-variables(A))] in Y
proof
let Y be set;
assume Y in A2;
then ex X being Subset of S st X = Y & X is_Sep-closed_on p;
hence thesis;
end;
hence
[p,index p, {}.bound_QC-variables(A),id(bound_QC-variables(A))] in X by A5,
SETFAM_1:def 1;
thus for q,t,K,f holds ['not' q,t,K,f] in X implies [q,t,K,f] in X
proof
let q,t,K,f such that
A6: ['not' q,t,K,f] in X;
for Y being set st Y in A2 holds [q,t,K,f] in Y
proof
let Y be set;
assume
A7: Y in A2;
then
A8: ex X being Subset of S st X = Y & X is_Sep-closed_on p;
['not' q,t,K,f] in Y by A6,A7,SETFAM_1:def 1;
hence thesis by A8;
end;
hence thesis by A5,SETFAM_1:def 1;
end;
thus for q,r,t,K,f holds [q '&' r,t,K,f] in X implies [q,t,K,f] in X & [r,
t+QuantNbr(q),K,f] in X
proof
let q,r,t,K,f such that
A9: [q '&' r,t,K,f] in X;
for Y being set st Y in A2 holds [q,t,K,f] in Y
proof
let Y be set;
assume
A10: Y in A2;
then
A11: ex X being Subset of S st X = Y & X is_Sep-closed_on p;
[q '&' r,t,K,f] in Y by A9,A10,SETFAM_1:def 1;
hence thesis by A11;
end;
hence [q,t,K,f] in X by A5,SETFAM_1:def 1;
for Y being set st Y in A2 holds [r,t+QuantNbr(q),K,f] in Y
proof
let Y be set;
assume
A12: Y in A2;
then
A13: ex X being Subset of S st X = Y & X is_Sep-closed_on p;
[q '&' r,t,K,f] in Y by A9,A12,SETFAM_1:def 1;
hence thesis by A13;
end;
hence thesis by A5,SETFAM_1:def 1;
end;
thus for q,x,t,K,f st [All(x,q),t,K,f] in X holds [q,t++,K \/ {x}, f+*(x
.--> x.t)] in X
proof
let q,x,t,K,f such that
A14: [All(x,q),t,K,f] in X;
for Y being set st Y in A2 holds [q,t++,K \/{x},f+*(x .--> x.t)] in Y
proof
let Y be set;
assume
A15: Y in A2;
then
A16: ex X being Subset of S st X = Y & X is_Sep-closed_on p;
[All(x,q),t,K,f] in Y by A14,A15,SETFAM_1:def 1;
hence thesis by A16;
end;
hence thesis by A5,SETFAM_1:def 1;
end;
let D be Subset of S;
assume D is_Sep-closed_on p;
then D in A2;
hence thesis by SETFAM_1:3;
end;
uniqueness;
end;
theorem Th30:
[p,index p,{}.bound_QC-variables(A),id(bound_QC-variables(A))] in
SepQuadruples(p)
proof
SepQuadruples(p) is_Sep-closed_on p by Def13;
hence thesis;
end;
theorem Th31:
for q,t,K,f st ['not' q,t,K,f] in SepQuadruples p holds [q,t,K,f
] in SepQuadruples p
proof
SepQuadruples(p) is_Sep-closed_on p by Def13;
hence thesis;
end;
theorem Th32:
for q,r,t,K,f st [q '&' r,t,K,f] in SepQuadruples p holds [q,t,K
,f] in SepQuadruples p & [r,t+QuantNbr(q),K,f] in SepQuadruples p
proof
SepQuadruples(p) is_Sep-closed_on p by Def13;
hence thesis;
end;
theorem Th33:
for q,x,t,K,f st [All(x,q),t,K,f] in SepQuadruples p holds [q,t++,K \/ {x},
f+*(x .--> x.t)] in SepQuadruples p
proof
SepQuadruples(p) is_Sep-closed_on p by Def13;
hence thesis;
end;
theorem Th34:
[q,t,K,f] in SepQuadruples p implies [q,t,K,f] = [p,index p,{}.
bound_QC-variables(A),id bound_QC-variables(A)] or ['not' q,t,K,f]
in SepQuadruples p or (ex r st [q '&' r, t, K,f] in SepQuadruples p) or
(ex r,u st t = u+QuantNbr r & [r '&' q,u,K,f] in SepQuadruples p) or
ex x,u,h st u++ = t & h +*({x} --> x.u) = f & ([All(x,q),u,K,h]
in SepQuadruples p or [All(x,q),u,K\{x},h] in SepQuadruples p)
proof
assume that
A1: [q,t,K,f] in SepQuadruples p and
A2: [q,t,K,f] <> [p,index p,{}.bound_QC-variables(A),id bound_QC-variables(A)]
and
A3: not ['not' q,t,K,f] in SepQuadruples p and
A4: not ex r st [q '&' r, t, K,f] in SepQuadruples p and
A5: not ex r,u st t = u+QuantNbr r & [r '&' q,u,K,f] in SepQuadruples p and
A6: not ex x,u,h st u++ = t & h +*({x} --> x.u) = f & ([All(x,q),u,K,h]
in SepQuadruples p or [All(x,q),u,K\{x},h] in SepQuadruples p);
reconsider Y = SepQuadruples p \ {[q,t,K,f]} as Subset of [:CQC-WFF(A),
QC-symbols(A), Fin bound_QC-variables(A), Funcs(bound_QC-variables(A),
bound_QC-variables(A)):];
A7: SepQuadruples(p) is_Sep-closed_on p by Def13;
A8: for q,t,K,f holds ['not' q,t,K,f] in Y implies [q,t,K,f] in Y
proof
let s,u,L,h;
assume
A9: ['not' s,u,L,h] in Y;
then s <> q or u <> t or L <> K or f <> h by A3,XBOOLE_0:def 5;
then
A10: [s,u,L,h] <> [q,t,K,f] by XTUPLE_0:5;
['not' s,u,L,h] in SepQuadruples p by A9,XBOOLE_0:def 5;
then [s,u,L,h] in SepQuadruples p by A7;
hence thesis by A10,ZFMISC_1:56;
end;
A11: for q,r,t,K,f holds [q '&' r,t,K,f] in Y implies [q,t,K,f] in Y & [r,t+
QuantNbr(q),K,f] in Y
proof
let s,r,u,L,h;
assume [s '&' r,u,L,h] in Y;
then
A12: [s '&' r,u,L,h] in SepQuadruples p by XBOOLE_0:def 5;
then s <> q or u <> t or L <> K or f <> h by A4;
then
A13: [s,u,L,h] <> [q,t,K,f] by XTUPLE_0:5;
[s,u,L,h] in SepQuadruples p by A7,A12;
hence [s,u,L,h] in Y by A13,ZFMISC_1:56;
r <> q or L <> K or f <> h or u+QuantNbr(s) <> t by A5,A12;
then
A14: [r,u+QuantNbr(s),L,h] <> [q,t,K,f] by XTUPLE_0:5;
[r,u+QuantNbr(s),L,h] in SepQuadruples p by A7,A12;
hence thesis by A14,ZFMISC_1:56;
end;
A15: Y c= SepQuadruples p by XBOOLE_1:36;
A16: for q,x,t,K,f st [All(x,q),t,K,f] in Y holds [q,t++,K \/ {x}, f+*(x
.--> x.t)] in Y
proof
let s,x,u,L,h;
assume
A17: [All(x,s),u,L,h] in Y;
now
assume that
A18: not [All(x,q),u,K,h] in SepQuadruples p and
A19: not [All(x,q),u,K\{x},h] in SepQuadruples p;
A20: s <> q or L <> K & L <> K \ {x} by A17,A18,A19,XBOOLE_0:def 5;
assume
A21: s = q;
assume
A22: L \/ {x} = K;
then K \ {x} = L \ {x} by XBOOLE_1:40;
hence contradiction by A20,A21,A22,ZFMISC_1:40,57;
end;
then s<>q or u++<>t or L \/ {x} <> K or f <> h+*({x} --> x.u) by A6;
then
A23: [s,u++,L \/ {x}, h+*(x .--> x.u)] <> [q,t,K,f] by XTUPLE_0:5;
[All(x,s),u,L,h] in SepQuadruples p by A17,XBOOLE_0:def 5;
then [s,u++,L \/ {x}, h+*(x .--> x.u)] in SepQuadruples p by A7;
hence thesis by A23,ZFMISC_1:56;
end;
[p,index p, {}.bound_QC-variables(A),id(bound_QC-variables(A))] in
SepQuadruples p by A7;
then [p,index p, {}.bound_QC-variables(A),id(bound_QC-variables(A))] in Y
by A2,ZFMISC_1:56;
then Y is_Sep-closed_on p by A8,A11,A16;
then SepQuadruples p c= Y by Def13;
then Y = SepQuadruples p by A15;
hence contradiction by A1,ZFMISC_1:57;
end;
scheme
Sepregression{A() -> QC-alphabet, p()-> Element of CQC-WFF(A()),
P[object,object,object,object] }:
for q being Element of CQC-WFF(A()), t being QC-symbol of A(),
K being Element of Fin bound_QC-variables(A()), f being Element of
Funcs(bound_QC-variables(A()),bound_QC-variables(A())) st
[q,t,K,f] in SepQuadruples p() holds P[q,t,K,f]
provided
A1: P[p(),index p(),{}.bound_QC-variables(A()),id bound_QC-variables(A())] and
A2: for q being Element of CQC-WFF(A()), t being QC-symbol of A(),
K being Element of Fin bound_QC-variables(A()), f being Element of
Funcs(bound_QC-variables(A()),bound_QC-variables(A())) st
['not' q,t,K,f] in SepQuadruples p() & P['not' q,t,K,
f] holds P[q,t,K,f] and
A3: for q,r being Element of CQC-WFF(A()), t being QC-symbol of A(),
K being Element of Fin bound_QC-variables(A()), f being Element of
Funcs(bound_QC-variables(A()),bound_QC-variables(A())) st
[q '&' r, t, K,f] in SepQuadruples p() & P[q '&' r,
t, K,f] holds P[q,t,K,f] & P[r,t+QuantNbr(q),K,f] and
A4: for q being Element of CQC-WFF(A()), x being bound_QC-variable of A(),
t being QC-symbol of A(), K being Element of Fin bound_QC-variables(A()),
f being Element of Funcs(bound_QC-variables(A()),bound_QC-variables(A()))
st [All(x,q),t,K,f] in SepQuadruples p() & P[All(x,q),t,K,f] holds
P[q,t++,K \/ {x},f+*(x .--> x.t)]
proof
set Y = { [s,v,M,g] where s is Element of CQC-WFF(A()),
M is Element of Fin bound_QC-variables(A()),v is QC-symbol of A(),
g is Element of Funcs(bound_QC-variables(A()),bound_QC-variables(A())) :
P[s,v,M,g] };
reconsider X = SepQuadruples p() /\ Y as Subset of [:CQC-WFF(A()),
QC-symbols(A()),Fin bound_QC-variables(A()), Funcs(bound_QC-variables(A()),
bound_QC-variables(A())):];
A5: SepQuadruples p() is_Sep-closed_on p() by Def13;
X is_Sep-closed_on p()
proof
A6: [p(),index p(),{}.bound_QC-variables(A()),id bound_QC-variables(A())] in Y
by A1;
[p(),index p(),{}.bound_QC-variables(A()),id(bound_QC-variables(A()))] in
SepQuadruples p() by Th30;
hence [p(),index p(), {}.bound_QC-variables(A()),
id(bound_QC-variables(A()))] in X by A6,XBOOLE_0:def 4;
thus for q being Element of CQC-WFF(A()), t being QC-symbol of A(),
K being Element of Fin bound_QC-variables(A()), f being Element of
Funcs(bound_QC-variables(A()),bound_QC-variables(A())) holds
['not' q,t,K,f] in X implies [q,t,K,f] in X
proof
let q be Element of CQC-WFF(A()), t be QC-symbol of A(),
K be Element of Fin bound_QC-variables(A()), f be Element of
Funcs(bound_QC-variables(A()),bound_QC-variables(A()));
assume
A7: ['not' q,t,K,f] in X;
then
A8: ['not' q,t,K,f] in SepQuadruples p() by XBOOLE_0:def 4;
['not' q,t,K,f] in Y by A7,XBOOLE_0:def 4;
then consider p being Element of CQC-WFF(A()), L being Element of Fin
bound_QC-variables(A()),u being QC-symbol of A(), h being Element of
Funcs(bound_QC-variables(A()),bound_QC-variables(A())) such that
A9: ['not' q,t,K,f] = [p,u,L,h] and
A10: P[p,u,L,h];
A11: t = u by A9,XTUPLE_0:5;
A12: f = h by A9,XTUPLE_0:5;
A13: K = L by A9,XTUPLE_0:5;
'not' q = p by A9,XTUPLE_0:5;
then P[q,t,K,f] by A2,A8,A10,A11,A13,A12;
then
A14: [q,t,K,f] in Y;
[q,t,K,f] in SepQuadruples p() by A5,A8;
hence thesis by A14,XBOOLE_0:def 4;
end;
thus for q,r being Element of CQC-WFF(A()), t being QC-symbol of A(),
K being Element of Fin bound_QC-variables(A()), f being Element of
Funcs(bound_QC-variables(A()),bound_QC-variables(A())) holds
[q '&' r,t,K,f] in X implies [q,t,K,f] in X & [r,t+QuantNbr(q),K,f] in X
proof
let q,r be Element of CQC-WFF(A()),
t be QC-symbol of A(), K be Element of Fin bound_QC-variables(A()),
f be Element of Funcs(bound_QC-variables(A()),bound_QC-variables(A()));
assume
A15: [q '&' r,t,K,f] in X;
then
A16: [q '&' r,t,K,f] in SepQuadruples p() by XBOOLE_0:def 4;
then
A17: [r,t+QuantNbr(q),K,f] in SepQuadruples p() by A5;
[q '&' r,t,K,f] in Y by A15,XBOOLE_0:def 4;
then consider p being Element of CQC-WFF(A()), L being Element of Fin
bound_QC-variables(A()),u being QC-symbol of A(), h being Element of
Funcs(bound_QC-variables(A()),bound_QC-variables(A())) such that
A18: [q '&' r,t,K,f] = [p,u,L,h] and
A19: P[p,u,L,h];
A20: t = u by A18,XTUPLE_0:5;
A21: f = h by A18,XTUPLE_0:5;
A22: K = L by A18,XTUPLE_0:5;
A23: q '&' r = p by A18,XTUPLE_0:5;
then P[q,t,K,f] by A3,A16,A19,A20,A22,A21;
then
A24: [q,t,K,f] in Y;
P[r,t+QuantNbr(q),K,f] by A3,A16,A19,A23,A20,A22,A21;
then
A25: [r,t+QuantNbr(q),K,f] in Y;
[q,t,K,f] in SepQuadruples p() by A5,A16;
hence thesis by A24,A25,A17,XBOOLE_0:def 4;
end;
let q be Element of CQC-WFF(A()), x be bound_QC-variable of A(),
t be QC-symbol of A(), K be Element of Fin bound_QC-variables(A()),
f be Element of Funcs(bound_QC-variables(A()),bound_QC-variables(A()));
assume
A26: [All(x,q),t,K,f] in X;
then
A27: [All(x,q),t,K,f] in SepQuadruples p() by XBOOLE_0:def 4;
f+*(x .--> x.t) is Function of bound_QC-variables(A()),
bound_QC-variables(A()) by Lm1;
then reconsider
g = f+*(x .--> x.t) as Element of Funcs(bound_QC-variables(A()),
bound_QC-variables(A())) by FUNCT_2:8;
[All(x,q),t,K,f] in Y by A26,XBOOLE_0:def 4;
then consider p being Element of CQC-WFF(A()), L being Element of Fin
bound_QC-variables(A()),u being QC-symbol of A(), h being Element of
Funcs(bound_QC-variables(A()),bound_QC-variables(A())) such that
A28: [All(x,q),t,K,f] = [p,u,L,h] and
A29: P[p,u,L,h];
A30: t = u by A28,XTUPLE_0:5;
A31: f = h by A28,XTUPLE_0:5;
A32: K = L by A28,XTUPLE_0:5;
All(x,q) = p by A28,XTUPLE_0:5;
then P[q,t++,K \/ {x},g] by A4,A27,A29,A30,A32,A31;
then
A33: [q,t++,K \/ {.x .},f+*(x .--> x.t)] in Y;
[q,t++,K \/{x},f+*(x .--> x.t)] in SepQuadruples p() by A5,A27;
hence thesis by A33,XBOOLE_0:def 4;
end;
then
A34: SepQuadruples p() c= X by Def13;
let q be Element of CQC-WFF(A()),
t be QC-symbol of A(), K be Element of Fin bound_QC-variables(A()),
f be Element of Funcs(bound_QC-variables(A()),bound_QC-variables(A()));
assume [q,t,K,f] in SepQuadruples p();
then [q,t,K,f] in Y by A34,XBOOLE_0:def 4;
then consider p being Element of CQC-WFF(A()), L being Element of Fin
bound_QC-variables(A()),u being QC-symbol of A(), h being Element of
Funcs(bound_QC-variables(A()),bound_QC-variables(A())) such that
A35: [q,t,K,f] = [p,u,L,h] and
A36: P[p,u,L,h];
A37: t = u by A35,XTUPLE_0:5;
A38: K = L by A35,XTUPLE_0:5;
q = p by A35,XTUPLE_0:5;
hence thesis by A35,A36,A37,A38,XTUPLE_0:5;
end;
theorem Th35:
for q,t,K,f holds [q,t,K,f] in SepQuadruples p implies q is_subformula_of p
proof
defpred P[Element of CQC-WFF(A),set,set,set] means $1 is_subformula_of p;
A1: now
let q,t,K,f such that
['not' q,t,K,f] in SepQuadruples p;
q is_subformula_of 'not' q by Th10;
hence P['not' q,t,K,f] implies P[q,t,K,f] by QC_LANG2:57;
end;
A2: now
let q,x,t,K,f such that
[All(x,q),t,K,f] in SepQuadruples p;
q is_subformula_of All(x,q) by Th12;
hence P[All(x,q),t,K,f] implies P[q,t++,K \/ {x},f+*(x .--> x.t)] by
QC_LANG2:57;
end;
A3: now
let q,r,t,K,f such that
[q '&' r, t, K,f] in SepQuadruples p;
A4: r is_subformula_of q '&'r by Th11;
q is_subformula_of q '&'r by Th11;
hence P[q '&' r,t,K,f] implies P[q,t,K,f] & P[r,t+QuantNbr(q),K,f] by A4,
QC_LANG2:57;
end;
A5: P[p,index p,{}.bound_QC-variables(A),id bound_QC-variables(A)];
thus for q,t,K,f st [q,t,K,f] in SepQuadruples p holds P[q,t,K,f] from
Sepregression(A5,A1,A3,A2);
end;
theorem
SepQuadruples VERUM(A) = { [VERUM(A),0(A),{}.bound_QC-variables(A),id
bound_QC-variables(A)] }
proof
now
let x be object;
thus x in SepQuadruples VERUM(A) implies x =
[VERUM(A),0(A),{}.bound_QC-variables(A),id bound_QC-variables(A)]
proof
assume
A1: x in SepQuadruples VERUM(A);
then consider q,t,K,f such that
A2: x = [q,t,K,f] by DOMAIN_1:10;
A3: now
given x,v,h such that
v++ = t and
h +*({x} --> x.v) = f and
A4: [All(x,q),v,K,h] in SepQuadruples VERUM(A) or [All(x,q),v,K\{.x
.},h] in SepQuadruples VERUM(A);
All(x,q) is_subformula_of VERUM(A) by A4,Th35;
then All(x,q) = VERUM(A) by QC_LANG2:79;
then VERUM(A) is universal by QC_LANG1:def 21;
hence contradiction by QC_LANG1:20;
end;
A5: now
given r,v such that
t = v+QuantNbr r and
A6: [r '&' q,v,K,f] in SepQuadruples VERUM(A);
r '&' q is_subformula_of VERUM(A) by A6,Th35;
then r '&' q = VERUM(A) by QC_LANG2:79;
then VERUM(A) is conjunctive by QC_LANG1:def 20;
hence contradiction by QC_LANG1:20;
end;
A7: now
given r such that
A8: [q '&' r, t, K,f] in SepQuadruples VERUM(A);
q '&' r is_subformula_of VERUM(A) by A8,Th35;
then q '&' r = VERUM(A) by QC_LANG2:79;
then VERUM(A) is conjunctive by QC_LANG1:def 20;
hence contradiction by QC_LANG1:20;
end;
A9: now
assume ['not' q,t,K,f] in SepQuadruples VERUM(A);
then 'not' q is_subformula_of VERUM(A) by Th35;
then 'not' q = VERUM(A) by QC_LANG2:79;
then VERUM(A) is negative by QC_LANG1:def 19;
hence contradiction by QC_LANG1:20;
end;
A10: index VERUM(A) = 0(A) by Th22;
set p = VERUM(A);
[q,t,K,f] = [p,index p,{}.
bound_QC-variables(A),id bound_QC-variables(A)] or
['not' q,t,K,f]
in SepQuadruples p or
(ex r st [q '&' r, t, K,f] in SepQuadruples p) or
(ex r,u st t = u+QuantNbr r & [r '&' q,u,K,f] in SepQuadruples p) or
ex x,u,h st u++ = t & h +*({x} --> x.u) = f & ([All(x,q),u,K,h]
in SepQuadruples p or
[All(x,q),u,K\{x},h] in SepQuadruples p) by A1,A2,Th34;
hence x =
[VERUM(A),0(A),{}.bound_QC-variables(A),id bound_QC-variables(A)]
by A2,A7,A5,A3,A9,A10;
end;
index VERUM(A) = 0(A) by Th22;
hence x = [VERUM(A),0(A),{}.bound_QC-variables(A),id bound_QC-variables(A)]
implies x in SepQuadruples VERUM(A) by Th30;
end;
hence thesis by TARSKI:def 1;
end;
theorem
for k for l being CQC-variable_list of k,A for P being QC-pred_symbol of
k,A holds SepQuadruples(P!l) = { [P!l,index(P!l),{}.bound_QC-variables(A),
id bound_QC-variables(A)] }
proof
let k;
let l be CQC-variable_list of k,A;
let P be QC-pred_symbol of k,A;
A1: P!l is atomic by QC_LANG1:def 18;
now
let x be object;
thus x in SepQuadruples(P!l) implies x = [P!l,index(P!l),{}.
bound_QC-variables(A),id bound_QC-variables(A)]
proof
assume
A2: x in SepQuadruples(P!l);
then consider q,t,K,f such that
A3: x = [q,t,K,f] by DOMAIN_1:10;
A4: now
given x,u,h such that
u++ = t and
h +*({x} --> x.u) = f and
A5: [All(x,q),u,K,h] in SepQuadruples(P!l) or [All(x,q),u,K\{.x
.},h] in SepQuadruples(P!l);
All(x,q) is_subformula_of P!l by A5,Th35;
then All(x,q) = P!l by QC_LANG2:80;
then P!l is universal by QC_LANG1:def 21;
hence contradiction by A1,QC_LANG1:20;
end;
A6: now
given r,u such that
t = u+QuantNbr r and
A7: [r '&' q,u,K,f] in SepQuadruples(P!l);
r '&' q is_subformula_of P!l by A7,Th35;
then r '&' q = P!l by QC_LANG2:80;
then P!l is conjunctive by QC_LANG1:def 20;
hence contradiction by A1,QC_LANG1:20;
end;
A8: now
given r such that
A9: [q '&' r, t, K,f] in SepQuadruples(P!l);
q '&' r is_subformula_of P!l by A9,Th35;
then q '&' r = P!l by QC_LANG2:80;
then P!l is conjunctive by QC_LANG1:def 20;
hence contradiction by A1,QC_LANG1:20;
end;
A10: now
assume ['not' q,t,K,f] in SepQuadruples(P!l);
then 'not' q is_subformula_of P!l by Th35;
then 'not' q = P!l by QC_LANG2:80;
then P!l is negative by QC_LANG1:def 19;
hence contradiction by A1,QC_LANG1:20;
end;
set p = P!l;
[q,t,K,f] = [p,index p,{}.
bound_QC-variables(A),id bound_QC-variables(A)] or
['not' q,t,K,f]
in SepQuadruples p or
(ex r st [q '&' r, t, K,f] in SepQuadruples p) or
(ex r,u st t = u+QuantNbr r & [r '&' q,u,K,f] in SepQuadruples p) or
ex x,u,h st u++ = t & h +*({x} --> x.u) = f & ([All(x,q),u,K,h]
in SepQuadruples p or
[All(x,q),u,K\{x},h] in SepQuadruples p) by A2,Th34,A3;
hence thesis by A3,A8,A6,A4,A10;
end;
thus x = [P!l,index(P!l),{}.bound_QC-variables(A),id bound_QC-variables(A)]
implies x in SepQuadruples(P!l) by Th30;
end;
hence thesis by TARSKI:def 1;
end;
theorem Th38:
for q,t,K,f st [q,t,K,f] in SepQuadruples p holds
still_not-bound_in q c= still_not-bound_in p \/ K
proof
deffunc f(QC-formula of A) = still_not-bound_in $1;
defpred P[QC-formula of A,set, set, set] means f($1) c= f(p) \/ $3;
A1: for q,t,K,f st ['not' q,t,K,f] in SepQuadruples p & P['not' q,t,K,f]
holds P[q,t,K,f] by QC_LANG3:7;
A2: now
let q,r,t,K,f such that
[q '&' r, t, K,f] in SepQuadruples p and
A3: P[q '&' r,t,K,f];
A4: still_not-bound_in q '&' r = still_not-bound_in q \/
still_not-bound_in r by QC_LANG3:10;
then
A5: still_not-bound_in r c= still_not-bound_in q '&' r by XBOOLE_1:7;
still_not-bound_in q c= still_not-bound_in q '&' r by A4,XBOOLE_1:7;
hence P[q,t,K,f] & P[r,t+QuantNbr(q),K,f] by A3,A5,XBOOLE_1:1;
end;
A6: now
let q,x,t,K,f such that
[All(x,q),t,K,f] in SepQuadruples p and
A7: P[All(x,q),t,K,f];
still_not-bound_in All(x,q) = still_not-bound_in q \ {x} by QC_LANG3:12;
then still_not-bound_in q c= still_not-bound_in p \/ K \/ {x} by A7,
XBOOLE_1:44;
hence P[q,t++,K \/ {x},f+*(x .--> x.t)] by XBOOLE_1:4;
end;
A8: P[p,index p,{}.bound_QC-variables(A),id bound_QC-variables(A)];
thus for q,t,K,f st [q,t,K,f] in SepQuadruples p holds P[q,t,K,f] from
Sepregression(A8,A1,A2,A6);
end;
theorem Th39:
[q,t,K,f] in SepQuadruples p & x.u in f.:K implies u < t
proof
defpred P[Element of CQC-WFF(A),QC-symbol of A, Element of Fin
bound_QC-variables(A),Function] means for u holds x.u in $4.:$3 implies
u < $2;
A1: for q,v,K,f st ['not' q,v,K,f] in SepQuadruples p & P['not' q,v,K,f]
holds P[q,v,K,f];
A2: now
let q,r,v,K,f;
assume [q '&' r, v, K,f] in SepQuadruples p;
assume
A3: P[q '&' r, v, K,f];
hence P[q,v,K,f];
thus P[r,v+QuantNbr(q),K,f]
proof
let u;
A4: v <= v + QuantNbr(q) by QC_LANG1:31;
assume
x.u in f.:K;
hence thesis by A3,A4,QC_LANG1:30;
end;
end;
A5: now
let q,x,v,K,f such that
[All(x,q),v,K,f] in SepQuadruples p;
assume
A6: P[All(x,q),v,K,f];
thus P[q,v++,K \/ {.x .},f+*(x .--> x.v)]
proof
let u;
assume x.u in (f+*(x .--> x.v)).:(K \/ {x});
then x.u in (f+*(x .--> x.v)).:K \/ (f+*(x .--> x.v)).: {x}
by RELAT_1:120;
then
A7: x.u in (f+*(x .--> x.v)).:K or x.u
in Im(f+*(x .--> x.v),x) by XBOOLE_0:def 3;
(f+*(x .--> x.v)).:K c= f.:K \/ {x.v} by Th2;
then x.u in f.:K or x.u in {x.v} by A7,Th1,XBOOLE_0:def 3;
then u < v or x.u = x.v by A6,TARSKI:def 1;
then u < v or u = v by XTUPLE_0:1;
then u <= v & v < v++ by QC_LANG1:22,27,def 34;
hence thesis by QC_LANG1:29;
end;
end;
A8: P[p, index p,{}.bound_QC-variables(A),id bound_QC-variables(A)];
for q,v,K,f st [q,v,K,f] in SepQuadruples p holds P[q,v,K,f] from
Sepregression(A8,A1,A2,A5);
hence thesis;
end;
theorem
[q,t,K,f] in SepQuadruples p implies not x.t in f.:K
proof
assume
A1: [q,t,K,f] in SepQuadruples p;
assume x.t in f.:K;
then t < t & t <= t by A1,Th39,QC_LANG1:22;
hence contradiction by QC_LANG1:25;
end;
theorem Th41:
[q,t,K,f] in SepQuadruples p & x.u in f.:still_not-bound_in p implies u<t
proof
defpred P[Element of CQC-WFF(A),QC-symbol of A, Element of Fin
bound_QC-variables(A),Function] means for u holds x.u in
$4.:still_not-bound_in p implies u < $2;
A1: now
let q,r,v,K,f;
assume [q '&' r, v, K,f] in SepQuadruples p;
assume
A2: P[q '&' r, v, K,f];
hence P[q,v,K,f];
thus P[r,v+QuantNbr(q),K,f]
proof
let u;
A3: v <= v + QuantNbr(q) by QC_LANG1:31;
assume x.u in f.:still_not-bound_in p;
hence thesis by A2,A3,QC_LANG1:30;
end;
end;
A4: P[p,index p,{}.bound_QC-variables(A),id bound_QC-variables(A)]
proof
let u;
assume
A5: x.u in (id bound_QC-variables(A)).:still_not-bound_in p;
(id bound_QC-variables(A)).:still_not-bound_in p = still_not-bound_in p
by FUNCT_1:92;
hence thesis by A5,Th21;
end;
A6: now
let q,x,v,K,f such that
[All(x,q),v,K,f] in SepQuadruples p;
assume
A7: P[All(x,q),v,K,f];
thus P[q,v++,K \/ {.x .},f+*(x .--> x.v)]
proof
let u;
assume
A8: x.u in (f+*(x .--> x.v)).:still_not-bound_in p;
(f+*(x .--> x.v)).:still_not-bound_in p c= f.:(still_not-bound_in p
) \/ {x.v} by Th2;
then x.u in f.:still_not-bound_in p or x.u in {x.v}
by A8,XBOOLE_0:def 3;
then u < v or x.u = x.v by A7,TARSKI:def 1;
then u < v or u = v by XTUPLE_0:1;
then u <= v & v < v++ by QC_LANG1:22,27,def 34;
hence thesis by QC_LANG1:29;
end;
end;
A9: for q,v,K,f st ['not' q,v,K,f] in SepQuadruples p & P['not' q,v,K,f]
holds P[q,v,K,f];
for q,v,K,f st [q,v,K,f] in SepQuadruples p holds P[q,v,K,f] from
Sepregression(A4,A9,A1,A6);
hence thesis;
end;
theorem Th42:
[q,t,K,f] in SepQuadruples p & x.u in f.:still_not-bound_in q implies u<t
proof
assume that
A1: [q,t,K,f] in SepQuadruples p and
A2: x.u in f.:still_not-bound_in q;
f.:still_not-bound_in q c= f.: (still_not-bound_in p \/ K) by A1,Th38,
RELAT_1:123;
then x.u in f.:(still_not-bound_in p \/ K) by A2;
then x.u in f.:still_not-bound_in p \/ f.:K by RELAT_1:120;
then x.u in f.:still_not-bound_in p or x.u in f.:K by XBOOLE_0:def 3;
hence thesis by A1,Th39,Th41;
end;
theorem Th43:
[q,t,K,f] in SepQuadruples p implies not x.t in f.:(still_not-bound_in
q)
proof
assume
A1: [q,t,K,f] in SepQuadruples p;
assume x.t in f.:(still_not-bound_in q);
then t < t & t <= t by A1,Th42,QC_LANG1:22;
hence contradiction by QC_LANG1:25;
end;
theorem Th44:
still_not-bound_in p = still_not-bound_in SepVar p
proof
defpred P[Element of CQC-WFF(A)] means for t,K,f st [$1,t,K,f]
in SepQuadruples p holds f.:(still_not-bound_in $1) = still_not-bound_in
(((SepFunc(A)).$1 qua Element of Funcs([:QC-symbols(A),
Funcs(bound_QC-variables(A), bound_QC-variables(A)):],
CQC-WFF(A))).([t,f] qua Element of [:QC-symbols(A),
Funcs(bound_QC-variables(A),bound_QC-variables(A)):]) qua Element of
CQC-WFF(A));
A1: [p,index p,{}.bound_QC-variables(A),id bound_QC-variables(A)] in
SepQuadruples p by Th30;
A2: now
let r;
reconsider g = (SepFunc(A)).r as Function of [:QC-symbols(A),
Funcs(bound_QC-variables(A), bound_QC-variables(A)):], CQC-WFF(A);
assume
A3: P[r];
A4: (SepFunc(A)).('not' r) = NEGATIVE(g) by Def7;
thus P['not' r]
proof
let u,K,f;
assume ['not' r,u,K,f] in SepQuadruples p;
then
A5: [r,u,K,f] in SepQuadruples p by Th31;
set uf = [u,f];
reconsider r9 = g.uf as Element of CQC-WFF(A);
A6: still_not-bound_in r9 = still_not-bound_in 'not' r9 by QC_LANG3:7;
A7: still_not-bound_in r = still_not-bound_in 'not' r by QC_LANG3:7;
(NEGATIVE g).uf = 'not' r9 by Def2;
hence thesis by A4,A3,A7,A6,A5;
end;
end;
A8: now
let k;
let l be CQC-variable_list of k,A;
let P be QC-pred_symbol of k,A;
thus P[P!l]
proof
let u,K,f such that
[P!l,u,K,f] in SepQuadruples p;
set fl = f*l;
A9: f.:{ l.i : 1 <= i & i <= len l & l.i in bound_QC-variables(A) } = { (
fl).j : 1 <= j & j <= len fl & fl.j in bound_QC-variables(A) }
proof
A10: len fl = k by CARD_1:def 7
.= len l by CARD_1:def 7;
thus f.:{ l.i : 1 <= i & i <= len l & l.i in bound_QC-variables(A) } c=
{fl.j : 1 <= j & j <= len fl & fl.j in bound_QC-variables(A) }
proof
let x be object;
assume
x in f.: { l.i : 1 <= i & i <= len l & l.i in bound_QC-variables(A)};
then consider y being object such that
A11: y in dom f & y in { l.i : 1 <= i & i <= len l & l.i in
bound_QC-variables(A) } & x = f.y by FUNCT_1:def 6;
consider i such that
A12: y = l.i and
A13: 1 <= i and
A14: i <= len l and
l.i in bound_QC-variables(A) by A11;
i in dom l by A13,A14,FINSEQ_3:25;
then
A15: f.(l.i) = fl.i by FUNCT_1:13;
fl.i in bound_QC-variables(A) by A10,A13,A14,Th13;
hence thesis by A10,A11,A12,A13,A14,A15;
end;
let x be object;
assume x in {fl.i: 1<=i & i<=len fl & fl.i in bound_QC-variables(A) };
then consider i such that
A16: x = fl.i and
A17: 1 <= i and
A18: i <= len fl and
fl.i in bound_QC-variables(A);
i in dom l by A10,A17,A18,FINSEQ_3:25;
then
A19: fl.i = f.(l.i) by FUNCT_1:13;
A20: l.i in bound_QC-variables(A) by A10,A17,A18,Th13;
then
A21: l.i in dom f by FUNCT_2:def 1;
l.i in { l.j : 1 <= j & j <= len l & l.j in bound_QC-variables(A) }
by A10,A17,A18,A20;
hence thesis by A16,A21,A19,FUNCT_1:def 6;
end;
A22: f.:still_not-bound_in (P!l) = f.:still_not-bound_in l by QC_LANG3:5
.= f.:variables_in(l,bound_QC-variables(A)) by QC_LANG3:2
.= variables_in(fl,bound_QC-variables(A)) by A9
.= still_not-bound_in fl by QC_LANG3:2
.= still_not-bound_in (P!fl) by QC_LANG3:5;
ATOMIC(P,l).(u,f) = P!(f*l) by Def5;
hence thesis by A22,Def7;
end;
end;
A23: now
let r,x such that
A24: P[r];
thus P[All(x, r)]
proof
reconsider g = (SepFunc(A)).r as Function of
[:QC-symbols(A),Funcs(bound_QC-variables(A),bound_QC-variables(A)):],
CQC-WFF(A);
let u,K,f such that
A25: [All(x,r),u,K,f] in SepQuadruples p;
A26: [r,u++,K \/ {.x .}, f+*(x .--> x.u)] in SepQuadruples p by A25,Th33;
f+*(x .--> x.u) is Function of bound_QC-variables(A),
bound_QC-variables(A) by Lm1;
then reconsider
fu = f +* (x .--> x.u) as Element of Funcs(bound_QC-variables(A)
,bound_QC-variables(A)) by FUNCT_2:8;
reconsider r99 = g.(u++,fu) as Element of CQC-WFF(A);
A27: UNIVERSAL(x,g).(u,f) = All(x.u,r99) by Def4;
A28: still_not-bound_in All(x, r) = still_not-bound_in r \ {x} by QC_LANG3:12;
then
A29: not x.u in f.:(still_not-bound_in r \ {x}) by A25,Th43;
thus f.:(still_not-bound_in All(x, r)) = fu.:(still_not-bound_in r \ {x}
) by A28,Th3
.= fu.:(still_not-bound_in r) \ {x.u} by A29,Th4
.= still_not-bound_in r99 \ {x.u} by A24,A26
.= still_not-bound_in All(x.u,r99) by QC_LANG3:12
.= still_not-bound_in (((SepFunc(A)).(All(x, r)) qua Element of Funcs([:
QC-symbols(A),Funcs(bound_QC-variables(A),bound_QC-variables(A)):],
CQC-WFF(A))).([u,f] qua Element of [:QC-symbols(A),
Funcs(bound_QC-variables(A), bound_QC-variables(A)):])
qua Element of CQC-WFF(A)) by A27,Def7;
end;
end;
A30: now
let r,s such that
A31: P[r] and
A32: P[s];
thus P[r '&' s]
proof
reconsider g = (SepFunc(A)).r, h = (SepFunc(A)).s as Function of
[:QC-symbols(A),Funcs(bound_QC-variables(A),bound_QC-variables(A)):],
CQC-WFF(A);
let u,K,f such that
A33: [r '&' s, u, K, f] in SepQuadruples p;
reconsider r9=g.(u,f), s9 = h.(u+QuantNbr(r),f) as Element of CQC-WFF(A);
A34: CON(g,h,QuantNbr(r)).(u,f) = r9 '&' s9 by Def3;
[r,u,K,f] in SepQuadruples p by A33,Th32;
then
A35: f.:(still_not-bound_in r) = still_not-bound_in r9 by A31;
[s,u+QuantNbr(r),K,f] in SepQuadruples p by A33,Th32;
then
A36: f.:(still_not-bound_in s) = still_not-bound_in s9 by A32;
thus f.:(still_not-bound_in r '&' s) = f.:(still_not-bound_in r \/
still_not-bound_in s) by QC_LANG3:10
.= still_not-bound_in r9 \/ still_not-bound_in s9 by A35,A36,RELAT_1:120
.= still_not-bound_in(r9 '&' s9) by QC_LANG3:10
.= still_not-bound_in (((SepFunc(A)).(r '&' s) qua Element of
Funcs([:QC-symbols(A),Funcs(bound_QC-variables(A),bound_QC-variables(A)):],
CQC-WFF(A))).([u,f] qua Element of [:QC-symbols(A),
Funcs(bound_QC-variables(A),bound_QC-variables(A)):]) qua Element of
CQC-WFF(A)) by A34,Def7;
end;
end;
A37: (SepFunc(A)).VERUM(A) = [:QC-symbols(A),Funcs(bound_QC-variables(A),
bound_QC-variables(A)):] --> VERUM(A) by Def7;
A38: P[VERUM(A)]
proof
let v,K,f such that
[VERUM(A),v,K,f] in SepQuadruples p;
A39: still_not-bound_in VERUM(A) = {} by QC_LANG3:3;
thus thesis by A39,A37;
end;
A40: for q holds P[q] from CQCInd(A38,A8,A2,A30,A23);
thus still_not-bound_in p =
(id bound_QC-variables(A)).:(still_not-bound_in p)
by FUNCT_1:92
.= still_not-bound_in SepVar p by A40,A1;
end;
theorem
index p = index(SepVar p)
proof
still_not-bound_in p = still_not-bound_in (SepVar p) by Th44;
hence thesis;
end;
definition
let A;
let p,q;
pred p,q are_similar means
SepVar(p) = SepVar(q);
reflexivity;
symmetry;
end;
theorem
p,q are_similar & q,r are_similar implies p,r are_similar;