:: Substitution in First-Order Formulas: Elementary Properties
:: by Patrick Braselmann and Peter Koepke
::
:: Received September 25, 2004
:: Copyright (c) 2004-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, SUBSET_1, QC_LANG1, CQC_LANG, FINSEQ_1, PARTFUN1,
XBOOLE_0, FUNCT_1, RELAT_1, XXREAL_0, NAT_1, TARSKI, FINSET_1, ZFMISC_1,
ZF_LANG, CLASSES2, CARD_1, BVFUNC_2, ORDINAL4, REALSET1, XBOOLEAN,
MARGREL1, MCART_1, ARYTM_3, SUBSTUT1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, FUNCT_1,
CARD_1, ORDINAL1, NUMBERS, FINSEQ_1, NAT_1, QC_LANG1, QC_LANG3, PARTFUN1,
SEQ_4, CQC_LANG, FINSET_1, RELSET_1, FUNCT_2, DOMAIN_1, MCART_1,
XXREAL_0, CARD_3;
constructors PARTFUN1, DOMAIN_1, XXREAL_0, NAT_1, SEQ_4, QC_LANG3, CQC_SIM1,
RELSET_1, ORDINAL1, CARD_3, ORDERS_1, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1,
FINSET_1, FINSEQ_1, QC_LANG1, CQC_LANG, XXREAL_0, XTUPLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE;
definitions TARSKI, FUNCT_1;
equalities QC_LANG1, QC_LANG3;
expansions TARSKI, QC_LANG1;
theorems TARSKI, FINSEQ_1, FUNCT_1, MCART_1, CQC_SIM1, XBOOLE_0, CQC_LANG,
QC_LANG1, ZFMISC_1, RELAT_1, XBOOLE_1, CARD_3, FUNCT_2, PARTFUN1,
RELSET_1, NAT_1, QC_LANG2, FINSEQ_3, CARD_1, XXREAL_0, ORDINAL1,
XTUPLE_0;
schemes FUNCT_1, FUNCT_2, QC_LANG1, QC_LANG3, NAT_1, XBOOLE_0, FINSEQ_1,
CLASSES1;
begin :: Preliminaries
reserve A for QC-alphabet;
reserve a,b,b1,b2,c,d for object,
i,j,k,n for Nat,
x,y,x1,x2 for bound_QC-variable of A,
P for QC-pred_symbol of k,A,
ll for CQC-variable_list of k,A,
l1 ,l2 for FinSequence of QC-variables(A),
p for QC-formula of A,
s,t for QC-symbol of A;
definition
let A;
func vSUB(A) -> set equals
PFuncs(bound_QC-variables(A),bound_QC-variables(A));
coherence;
end;
registration
let A;
cluster vSUB(A) -> non empty;
coherence;
end;
definition
let A;
mode CQC_Substitution of A is Element of vSUB(A);
end;
registration
let A;
cluster vSUB(A) -> functional;
coherence;
end;
reserve Sub for CQC_Substitution of A;
definition
let A;
let Sub;
func @Sub -> PartFunc of bound_QC-variables(A),bound_QC-variables(A) equals
Sub;
coherence by PARTFUN1:47;
end;
theorem Th1:
a in dom Sub implies Sub.a in bound_QC-variables(A)
proof
assume a in dom Sub;
then a in dom @Sub;
hence thesis by PARTFUN1:4;
end;
definition
let A;
let l be FinSequence of QC-variables(A);
let Sub;
func CQC_Subst(l,Sub) -> FinSequence of QC-variables(A) means
:Def3:
len it =
len l & for k st 1 <= k & k <= len l holds (l.k in dom Sub implies it.k = Sub.(
l.k)) & (not l.k in dom Sub implies it.k = l.k);
existence
proof
defpred P[set,object] means
(l.$1 in dom Sub implies $2 = Sub.(l.$1)) & (not
l.$1 in dom Sub implies $2 = l.$1);
A1: for k be Nat st k in Seg len l ex y being object st P[k,y]
proof
let k be Nat;
assume k in Seg len l;
l.k in dom Sub implies thesis;
hence thesis;
end;
consider s being FinSequence such that
A2: dom s = Seg len l and
A3: for k be Nat st k in Seg len l holds P[k,s.k] from FINSEQ_1:sch 1(
A1);
rng s c= QC-variables(A)
proof
let y be object;
assume y in rng s;
then consider x being object such that
A4: x in dom s and
A5: s.x = y by FUNCT_1:def 3;
reconsider x as Nat by A4;
now
per cases;
case
A6: l.x in dom Sub;
then s.x = Sub.(l.x) by A2,A3,A4;
hence s.x in bound_QC-variables(A) by A6,Th1;
end;
case
A7: not l.x in dom Sub;
x in dom l by A2,A4,FINSEQ_1:def 3;
then
A8: l.x in rng l by FUNCT_1:3;
s.x = l.x by A2,A3,A4,A7;
hence s.x in QC-variables(A) by A8;
end;
end;
hence thesis by A5;
end;
then reconsider s as FinSequence of QC-variables(A) by FINSEQ_1:def 4;
take s;
thus len s = len l by A2,FINSEQ_1:def 3;
thus for k st 1 <= k & k <= len l holds (l.k in dom Sub implies s.k = Sub.
(l.k)) & (not l.k in dom Sub implies s.k = l.k)
proof
let k;
assume 1 <= k & k <= len l;
then k in dom l by FINSEQ_3:25;
then k in Seg len l by FINSEQ_1:def 3;
hence thesis by A3;
end;
end;
uniqueness
proof
let l1,l2 such that
A9: len l1 = len l and
A10: for k st 1 <= k & k <= len l holds (l.k in dom Sub implies l1.k =
Sub.(l.k)) & (not l.k in dom Sub implies l1.k = l.k) and
A11: len l2 = len l and
A12: for k st 1 <= k & k <= len l holds (l.k in dom Sub implies l2.k =
Sub.(l.k)) & (not l.k in dom Sub implies l2.k = l.k);
now
let k be Nat;
assume
A13: 1 <= k & k <= len l;
A14: not l.k in dom Sub implies l1.k = l.k by A10,A13;
l.k in dom Sub implies l1.k = Sub.(l.k) by A10,A13;
hence l1.k = l2.k by A12,A13,A14;
end;
hence thesis by A9,A11,FINSEQ_1:14;
end;
end;
definition
let A;
let l be FinSequence of bound_QC-variables(A);
func @l -> FinSequence of QC-variables(A) equals
l;
coherence
proof
rng l c= QC-variables(A) by XBOOLE_1:1;
hence thesis by FINSEQ_1:def 4;
end;
end;
definition
let A;
let l be FinSequence of bound_QC-variables(A);
let Sub;
func CQC_Subst(l,Sub) -> FinSequence of bound_QC-variables(A) equals
CQC_Subst(
@l,Sub);
coherence
proof
len CQC_Subst(@l,Sub) = len @l by Def3;
then
A1: dom CQC_Subst(@l,Sub) = Seg len @l by FINSEQ_1:def 3;
A2: for k st k in Seg len @l holds (@l.k in dom Sub implies CQC_Subst(@l,
Sub).k = Sub.(@l.k)) & (not @l.k in dom Sub implies CQC_Subst(@l,Sub).k = @l.k)
proof
let k;
assume k in Seg len @l;
then 1 <= k & k <= len @l by FINSEQ_1:1;
hence thesis by Def3;
end;
rng CQC_Subst(@l,Sub) c= bound_QC-variables(A)
proof
let y be object;
assume y in rng CQC_Subst(@l,Sub);
then consider x being object such that
A3: x in dom CQC_Subst(@l,Sub) and
A4: CQC_Subst(@l,Sub).x = y by FUNCT_1:def 3;
reconsider x as Nat by A3;
now
per cases;
case
A5: @l.x in dom Sub;
then CQC_Subst(@l,Sub).x = Sub.(@l.x) by A1,A2,A3;
hence CQC_Subst(@l,Sub).x in bound_QC-variables(A) by A5,Th1;
end;
case
A6: not @l.x in dom Sub;
A7: rng l c= bound_QC-variables(A);
x in dom @l by A1,A3,FINSEQ_1:def 3;
then
A8: @l.x in rng @l by FUNCT_1:3;
CQC_Subst(@l,Sub).x = @l.x by A1,A2,A3,A6;
hence CQC_Subst(@l,Sub).x in bound_QC-variables(A) by A8,A7;
end;
end;
hence thesis by A4;
end;
hence thesis by FINSEQ_1:def 4;
end;
end;
definition
let A;
let Sub;
let X be set;
redefine func Sub|X -> CQC_Substitution of A; :: redefines | (RELAT_1, definition)
coherence
proof
Sub|X = @Sub|X;
hence thesis by PARTFUN1:45;
end;
end;
registration
let A;
cluster finite for CQC_Substitution of A;
existence
proof
take L = {};
L is PartFunc of bound_QC-variables(A),bound_QC-variables(A)
by RELSET_1:12;
hence L is CQC_Substitution of A by PARTFUN1:45;
thus thesis;
end;
end;
definition
let A;
let x, p, Sub;
func RestrictSub(x,p,Sub) -> finite CQC_Substitution of A equals
Sub|{y : y in
still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub.y};
coherence
proof
set Y = {y : y is Element of dom Sub & y <> x & y <> Sub.y};
set X = {y : y in still_not-bound_in p & y is Element of dom Sub & y <> x
& y <> Sub.y};
reconsider Z = still_not-bound_in p as finite set by CQC_SIM1:19;
for a being object holds (a in X iff a in Z /\ Y)
proof
let a be object;
thus a in X implies a in Z /\ Y
proof
assume a in X;
then consider y such that
A1: a = y & y in still_not-bound_in p and
A2: y is Element of dom Sub & y <> x & y <> Sub.y;
y in Y by A2;
hence thesis by A1,XBOOLE_0:def 4;
end;
thus a in Z /\ Y implies a in X
proof
assume
A3: a in Z /\ Y;
then a in Y by XBOOLE_0:def 4;
then
A4: ex y st a = y & y is Element of dom Sub & y <> x & y <> Sub.y;
a in Z by A3,XBOOLE_0:def 4;
hence thesis by A4;
end;
end;
then reconsider X as finite set by TARSKI:2;
Sub|X is finite;
hence thesis;
end;
end;
definition
let A;
let l1;
func Bound_Vars(l1) -> Subset of bound_QC-variables(A) equals
{ l1.k : 1 <= k &
k <= len l1 & l1.k in bound_QC-variables(A)};
coherence
proof
set A2 = { l1.k : 1 <= k & k <= len l1 & l1.k in bound_QC-variables(A)};
A2 c= bound_QC-variables(A)
proof
let x be object;
assume x in A2;
then
ex k st l1.k = x & 1 <= k & k <= len l1 & l1.k in bound_QC-variables(A);
hence thesis;
end;
hence thesis;
end;
end;
definition
let A;
let p;
func Bound_Vars(p) -> Subset of bound_QC-variables(A) means
:Def8:
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) for d1,d2 being Subset of bound_QC-variables(A)
holds (p = VERUM(A) implies
F.p = {}(bound_QC-variables(A))) & (p is atomic implies F.p = Bound_Vars(
the_arguments_of p)) & (p is negative & d1 = F.the_argument_of p implies F.p =
d1) & (p is conjunctive & d1 = F.the_left_argument_of p & d2 = F.
the_right_argument_of p implies F.p = d1 \/ d2) & (p is universal & d1 = F.
the_scope_of p implies F.p = (d1 \/ {bound_in p}));
correctness
proof
deffunc A(Element of QC-WFF(A)) = Bound_Vars(the_arguments_of $1);
set V = bound_QC-variables(A);
deffunc N(Subset of V) = $1;
deffunc C(Subset of V,Subset of V) = $1 \/ $2;
deffunc Q(Element of QC-WFF(A),Subset of V) = $2 \/ {bound_in $1};
thus (ex d being (Subset of V), F being Function of QC-WFF(A),
bool V st d =
F.p & for p being Element of QC-WFF(A) for d1,d2 being Subset of V
holds (p = VERUM(A) implies F.p = {}V) &
(p is atomic implies F.p = A(p)) & (p is negative &
d1 = F.the_argument_of p implies F.p = N(d1)) & (p is conjunctive & d1 = F.
the_left_argument_of p & d2 = F.the_right_argument_of p implies F.p = C(d1, d2)
) & (p is universal & d1 = F.the_scope_of p implies F.p = Q(p, d1)) ) & for x1,
x2 being Subset of V st (ex F being Function of QC-WFF(A), bool V st x1 = F.p &
for p being Element of QC-WFF(A) for d1,d2 being Subset of V holds
(p = VERUM(A)
implies F.p = {}V) & (p is atomic implies F.p = A(p)) & (p is negative & d1 = F
.the_argument_of p implies F.p = N(d1)) & (p is conjunctive & d1 = F.
the_left_argument_of p & d2 = F.the_right_argument_of p implies F.p = C(d1, d2)
) & (p is universal & d1 = F.the_scope_of p implies F.p = Q(p, d1)) ) & (ex F
being Function of QC-WFF(A), bool V st x2 = F.p &
for p being Element of QC-WFF(A)
for d1,d2 being Subset of V holds (p = VERUM(A) implies F.p = {}V) &
(p is atomic implies F.p = A(p)) & (p is negative
& d1 = F.the_argument_of p implies F.p = N
(d1)) & (p is conjunctive & d1 = F.the_left_argument_of p & d2 = F.
the_right_argument_of p implies F.p = C(d1, d2)) & (p is universal & d1 = F.
the_scope_of p implies F.p = Q(p, d1)) ) holds x1 = x2 from QC_LANG3:sch 2;
end;
end;
Lm1: Bound_Vars(VERUM(A)) = {}(bound_QC-variables(A)) & (p is atomic implies
Bound_Vars(p) = Bound_Vars(the_arguments_of p)) & (p is negative implies
Bound_Vars(p) = Bound_Vars(the_argument_of p)) & (p is conjunctive implies
Bound_Vars(p) = Bound_Vars(the_left_argument_of p) \/ Bound_Vars(
the_right_argument_of p)) & (p is universal implies Bound_Vars(p) = Bound_Vars(
the_scope_of p) \/ {bound_in p})
proof
deffunc A(Element of QC-WFF(A)) = Bound_Vars(the_arguments_of $1);
deffunc F1(Element of QC-WFF(A)) = Bound_Vars($1);
set V = bound_QC-variables(A);
deffunc N(Subset of V) = $1;
deffunc C(Subset of V,Subset of V) = $1 \/ $2;
deffunc Q(Element of QC-WFF(A),Subset of V) = $2 \/ {bound_in $1};
A1: for p being QC-formula of A, X being Subset of V holds X = F1(p) iff ex F
being Function of QC-WFF(A), bool V st X = F.p &
for p being Element of QC-WFF(A) for
d1,d2 being Subset of bound_QC-variables(A) holds
(p = VERUM(A) implies F.p = {}(V))
& (p is atomic implies F.p = A(p)) & (p is negative & d1 = F.the_argument_of p
implies F.p = N(d1)) & (p is conjunctive & d1 = F.the_left_argument_of p & d2 =
F.the_right_argument_of p implies F.p = C(d1,d2)) & (p is universal & d1 = F.
the_scope_of p implies F.p = Q(p,d1)) by Def8;
F1(VERUM(A)) = {}(V) from QC_LANG3:sch 3(A1)
.= {};
hence Bound_Vars(VERUM(A)) = {}(bound_QC-variables(A));
thus p is atomic implies Bound_Vars(p) = Bound_Vars(the_arguments_of p)
proof
assume
A2: p is atomic;
thus F1(p) = A(p) from QC_LANG3:sch 4(A1,A2);
end;
thus p is negative implies Bound_Vars(p) = Bound_Vars(the_argument_of p)
proof
assume
A3: p is negative;
thus F1(p) = N(F1(the_argument_of p)) from QC_LANG3:sch 5(A1,A3);
end;
thus p is conjunctive implies Bound_Vars(p) = Bound_Vars(
the_left_argument_of p) \/ Bound_Vars(the_right_argument_of p)
proof
assume
A4: p is conjunctive;
for d1,d2 being Subset of V st d1 = F1(the_left_argument_of p) & d2 =
F1(the_right_argument_of p) holds F1(p) = C(d1,d2) from QC_LANG3: sch 6(A1,A4);
hence thesis;
end;
thus p is universal implies Bound_Vars(p) = Bound_Vars(the_scope_of p) \/ {
bound_in p}
proof
assume
A5: p is universal;
thus F1(p) = Q(p,F1(the_scope_of p)) from QC_LANG3:sch 7(A1,A5);
end;
end;
theorem Th2:
Bound_Vars(VERUM(A)) = {}
proof
Bound_Vars(VERUM(A)) = {}(bound_QC-variables(A)) by Lm1;
hence Bound_Vars(VERUM(A)) = {};
end;
theorem
for p being QC-formula of A st p is atomic holds Bound_Vars(p) = Bound_Vars
(the_arguments_of p) by Lm1;
theorem
for p being QC-formula of A st p is negative holds Bound_Vars(p) =
Bound_Vars(the_argument_of p) by Lm1;
theorem
for p being QC-formula of A st p is conjunctive holds Bound_Vars(p) = (
Bound_Vars(the_left_argument_of p)) \/ ( Bound_Vars(the_right_argument_of p))
by Lm1;
theorem
for p being QC-formula of A st p is universal holds Bound_Vars(p) =
Bound_Vars(the_scope_of p) \/ {bound_in p} by Lm1;
registration
let A;
let p;
cluster Bound_Vars(p) -> finite;
coherence
proof
defpred P[Element of QC-WFF(A)] means Bound_Vars($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 Bound_Vars(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 Bound_Vars(p) = Bound_Vars(the_arguments_of p) by Lm1
.= { (the_arguments_of p).k:
1 <= k & k <= len (the_arguments_of
p) & (the_arguments_of p).k in bound_QC-variables(A) };
then Bound_Vars(p) c= rng (the_arguments_of p) by A2,CQC_SIM1:9;
hence thesis;
end;
thus Bound_Vars(VERUM(A)) is finite by Th2;
thus p is negative & Bound_Vars(the_argument_of p) is finite implies
Bound_Vars(p) is finite by Lm1;
thus p is conjunctive & Bound_Vars(the_left_argument_of p) is finite &
Bound_Vars(the_right_argument_of p) is finite implies Bound_Vars(p) is finite
proof
assume that
A3: p is conjunctive and
A4: Bound_Vars(the_left_argument_of p) is finite & Bound_Vars(
the_right_argument_of p) is finite;
Bound_Vars(p) = (Bound_Vars(the_left_argument_of p)) \/ (
Bound_Vars(the_right_argument_of p)) by A3,Lm1;
hence thesis by A4;
end;
assume that
A5: p is universal and
A6: Bound_Vars(the_scope_of p) is finite;
Bound_Vars(p) = (Bound_Vars(the_scope_of p)) \/ {bound_in p} by A5,Lm1;
hence thesis by A6;
end;
for p being Element of QC-WFF(A) holds P[p] from QC_LANG1:sch 2(A1);
hence thesis;
end;
end;
definition
let A;
let p;
func Dom_Bound_Vars(p) -> finite Subset of QC-symbols(A) equals
{s : x.s in Bound_Vars p};
coherence
proof
defpred P[object,object] means ex s st s = $1 & $2 = x.s;
set X = {s : x.s in Bound_Vars(p)};
A1: X c= QC-symbols(A)
proof
let a be object;
assume a in X;
then ex s st a = s & x.s in Bound_Vars(p);
hence thesis;
end;
A2: for a being object st a in QC-symbols(A) ex b being object st P[a,b]
proof
let a be object;
assume a in QC-symbols(A);
then reconsider s = a as QC-symbol of A;
take x.s;
take s;
thus thesis;
end;
consider f being Function such that
A3: dom f = QC-symbols(A) &
for a being object st a in QC-symbols(A) holds P[a,f.a]
from CLASSES1:sch 1(A2);
A4: rng(f|X) c= Bound_Vars(p)
proof
let b be object;
assume b in rng(f|X);
then consider a being object such that
A5: a in dom(f|X) and
A6: b = (f|X).a by FUNCT_1:def 3;
a in X by A5,RELAT_1:57;
then
A7: ex s st a = s & x.s in Bound_Vars(p);
b = f.a & a in dom f by A5,A6,FUNCT_1:47,RELAT_1:57;
then ex s st s = a & b = x.s by A3;
hence thesis by A7;
end;
f is one-to-one
proof
let a1,a2 be object such that
A8: a1 in dom f & a2 in dom f and
A9: f.a1 = f.a2;
(ex s st s = a1 & f.a1 = x.s )& ex t st t = a2 & f.a2 = x.t by A3,A8;
hence thesis by A9,XTUPLE_0:1;
end;
then f|X is one-to-one by FUNCT_1:52;
then
A10: dom(f|X) is finite by A4,CARD_1:59;
reconsider X as Subset of QC-symbols(A) by A1;
for a being object holds a in dom(f|X) iff a in X & a in dom f
by RELAT_1:57;
then dom(f|X) = X /\ QC-symbols(A) by A3,XBOOLE_0:def 4;
hence thesis by A10,XBOOLE_1:28;
end;
end;
reserve finSub for finite CQC_Substitution of A;
definition
let A;
let finSub;
func Sub_Var(finSub) -> finite Subset of QC-symbols(A) equals
{s : x.s in rng finSub};
coherence
proof
defpred P[object,object] means ex s st s = $1 & $2 = x.s;
set X = {s : x.s in rng finSub};
A1: X c= QC-symbols(A)
proof
let a be object;
assume a in X;
then ex s st a = s & x.s in rng finSub;
hence thesis;
end;
A2: for a being object st a in QC-symbols(A) ex b being object st P[a,b]
proof
let a be object;
assume a in QC-symbols(A);
then reconsider s = a as QC-symbol of A;
take x.s;
take s;
thus thesis;
end;
consider f being Function such that
A3: dom f = QC-symbols(A) &
for a being object st a in QC-symbols(A) holds P[a,f.a]
from CLASSES1:sch 1(A2);
A4: rng(f|X) c= rng finSub
proof
let b be object;
assume b in rng(f|X);
then consider a being object such that
A5: a in dom(f|X) and
A6: b = (f|X).a by FUNCT_1:def 3;
a in X by A5,RELAT_1:57;
then
A7: ex s st a = s & x.s in rng finSub;
b = f.a & a in dom f by A5,A6,FUNCT_1:47,RELAT_1:57;
then ex s st s = a & b = x.s by A3;
hence thesis by A7;
end;
f is one-to-one
proof
let a1,a2 be object such that
A8: a1 in dom f & a2 in dom f and
A9: f.a1 = f.a2;
(ex s st s = a1 & f.a1 = x.s )& ex t st t = a2 & f.a2 = x.t by A3,A8;
hence thesis by A9,XTUPLE_0:1;
end;
then f|X is one-to-one by FUNCT_1:52;
then
A10: dom(f|X) is finite by A4,CARD_1:59;
reconsider X as Subset of QC-symbols(A) by A1;
for a being object holds a in dom(f|X) iff a in X & a in dom f
by RELAT_1:57;
then dom(f|X) = X /\ QC-symbols(A) by A3,XBOOLE_0:def 4;
hence thesis by A10,XBOOLE_1:28;
end;
end;
Lm2: for X, Y being set st card X in card Y holds Y \ X <> {}
proof
let X, Y be set;
assume that
A1: card X in card Y and
A2: Y \ X = {};
Y c= X by A2,XBOOLE_1:37;
then card Y c= card X by CARD_1:11;
hence contradiction by A1,CARD_1:4;
end;
definition
let A;
let p, finSub;
func NSub(p,finSub) -> non empty Subset of QC-symbols(A) equals
NAT\(Dom_Bound_Vars(p)\/ Sub_Var(finSub));
coherence
proof
set X = (Dom_Bound_Vars p) \/ (Sub_Var finSub);
card ((Dom_Bound_Vars p) \/ (Sub_Var finSub)) in card NAT by CARD_3:42;
hence NAT \ ((Dom_Bound_Vars p) \/ (Sub_Var finSub)) is non empty Subset of
QC-symbols(A) by Lm2,QC_LANG1:3,XBOOLE_1:109;
end;
end;
definition
let A;
let finSub, p;
func upVar(finSub,p) -> QC-symbol of A equals
the Element of NSub(p,finSub);
coherence;
end;
definition
let A;
let x, p, finSub;
assume
A1: ex Sub st finSub = RestrictSub(x,All(x,p),Sub);
func ExpandSub(x,p,finSub) -> CQC_Substitution of A equals
finSub \/ {[x,x.upVar(finSub,p)]}
if x in rng finSub otherwise finSub \/ {[x,x]};
coherence
proof
A2: now
reconsider Z = {[x,x]} as Relation-like set;
assume not x in rng finSub;
A3: now
consider Sub such that
A4: finSub = RestrictSub(x,All(x,p),Sub) by A1;
set X = {y : y in still_not-bound_in All(x,p) & y is Element of dom
Sub & y <> x & y <> Sub.y};
A5: dom finSub c= X by A4,RELAT_1:58;
given a such that
A6: a in dom finSub /\ dom Z;
a in dom finSub by A6,XBOOLE_0:def 4;
then a in X by A5;
then
A7: dom Z = {x} & ex y st a = y & y in still_not-bound_in All(x,p) &
y is Element of dom Sub & y <> x & y <> Sub.y by RELAT_1:9;
a in dom Z by A6,XBOOLE_0:def 4;
hence contradiction by A7,TARSKI:def 1;
end;
reconsider Z as Function;
for a being object st a in dom (@finSub) /\ dom Z
holds (@finSub).a = Z.a by A3;
then reconsider h = (@finSub) \/ Z as Function by PARTFUN1:1;
reconsider Z as Relation of bound_QC-variables(A),bound_QC-variables(A);
@finSub \/ Z = h;
hence finSub \/ {[x,x]} is CQC_Substitution of A by PARTFUN1:45;
end;
now
reconsider Z = {[x,x.upVar(finSub,p)]} as Relation-like set;
assume x in rng finSub;
A9: now
consider Sub such that
A10: finSub = RestrictSub(x,All(x,p),Sub) by A1;
set X = {y : y in still_not-bound_in All(x,p) & y is Element of dom
Sub & y <> x & y <> Sub.y};
A11: dom finSub c= X by A10,RELAT_1:58;
given a such that
A12: a in dom finSub /\ dom Z;
a in dom finSub by A12,XBOOLE_0:def 4;
then a in X by A11;
then
A13: dom Z = {x} & ex y st a = y & y in still_not-bound_in All(x,p) &
y is Element of dom Sub & y <> x & y <> Sub.y by RELAT_1:9;
a in dom Z by A12,XBOOLE_0:def 4;
hence contradiction by A13,TARSKI:def 1;
end;
reconsider Z as Function;
for a being object st a in dom (@finSub) /\ dom Z
holds (@finSub).a = Z.a by A9;
then reconsider h = (@finSub) \/ Z as Function by PARTFUN1:1;
reconsider Z as Relation of bound_QC-variables(A),bound_QC-variables(A);
@finSub \/ Z = h;
hence finSub \/ {[x,x.upVar(finSub,p)]} is CQC_Substitution of A by
PARTFUN1:45;
end;
hence thesis by A2;
end;
consistency;
end;
definition
let A;
let p, Sub; let b be object;
pred p,Sub PQSub b means
(p is universal implies b = ExpandSub(
bound_in p,the_scope_of p, RestrictSub(bound_in p,p,Sub))) & (not p is
universal implies b = {});
end;
definition
let A;
func QSub(A) -> Function means
a in it iff ex p,Sub,b st a = [[p,Sub],b] & p, Sub PQSub b;
existence
proof
defpred P[object,object] means
ex p,Sub st $1 = [p,Sub] & p,Sub PQSub $2;
A1: for a,b1,b2 being object st P[a,b1] & P[a,b2] holds b1 = b2
proof
let a,b1,b2 be object such that
A2: ex p,Sub st a = [p,Sub] & p,Sub PQSub b1 and
A3: ex p,Sub st a = [p,Sub] & p,Sub PQSub b2;
consider p1 being QC-formula of A, Sub1 being CQC_Substitution of A
such that
A4: a = [p1,Sub1] and
A5: p1,Sub1 PQSub b1 by A2;
consider p2 being QC-formula of A, Sub2 being CQC_Substitution of A
such that
A6: a = [p2,Sub2] and
A7: p2,Sub2 PQSub b2 by A3;
A8: p1 = p2 by A4,A6,XTUPLE_0:1;
A9: Sub1 = Sub2 by A4,A6,XTUPLE_0:1;
per cases;
suppose
A10: p1 is universal;
then b1 = ExpandSub(bound_in p1,the_scope_of p1, RestrictSub(bound_in
p1,p1, Sub1)) by A5;
hence thesis by A7,A8,A9,A10;
end;
suppose
A11: not p1 is universal;
then b1 = {} by A5;
hence thesis by A7,A8,A11;
end;
end;
consider f being Function such that
A12: for a,b being object
holds [a,b] in f iff a in [:QC-WFF(A),vSUB(A):] & P[a,b]
from FUNCT_1:sch 1(A1);
take f;
c in f iff ex p,Sub,b st c = [[p,Sub],b] & p,Sub PQSub b
proof
thus c in f implies ex p,Sub,b st c = [[p,Sub],b] & p,Sub PQSub b
proof
assume
A13: c in f;
then consider a,b being object such that
A14: c = [a,b] by RELAT_1:def 1;
ex p,Sub st a = [p,Sub] & p,Sub PQSub b by A12,A13,A14;
hence thesis by A14;
end;
thus thesis by A12;
end;
hence thesis;
end;
uniqueness
proof
let F1, F2 be Function;
assume that
A15: for a holds a in F1 iff ex p,Sub,b st a = [[p,Sub],b] & p,Sub PQSub b and
A16: for a holds a in F2 iff ex p,Sub,b st a = [[p,Sub],b] & p,Sub PQSub b;
now
let a be object;
a in F1 iff ex p,Sub,b st a = [[p,Sub],b] & p,Sub PQSub b by A15;
hence a in F1 iff a in F2 by A16;
end;
hence thesis by TARSKI:2;
end;
end;
begin :: Definition and Properties of the
:: Formula - Substitution - Construction
reserve e for Element of vSUB(A);
theorem Th7:
[:QC-WFF(A),vSUB(A):] is Subset of [:[:NAT, QC-symbols(A):]*,vSUB(A):] &
(for k being Nat, p being (QC-pred_symbol of k,A),
ll being QC-variable_list
of k,A , e being Element of vSUB(A) holds [<*p*>^ll,e]
in [:QC-WFF(A),vSUB(A):]) & (for e
being Element of vSUB(A) holds [<*[0, 0]*>,e] in
[:QC-WFF(A),vSUB(A):]) & (for p being
FinSequence of [:NAT,QC-symbols(A):], e being Element of vSUB(A)
st [p,e] in [:QC-WFF(A),vSUB(A):]
holds [<*[1, 0]*>^p,e] in [:QC-WFF(A),vSUB(A):]) &
(for p, q being FinSequence of [:
NAT, QC-symbols(A):], e being Element of vSUB(A) st
[p,e] in [:QC-WFF(A),vSUB(A):] & [q,e] in [:
QC-WFF(A),vSUB(A):] holds [<*[2, 0]*>^p^q,e]
in [:QC-WFF(A),vSUB(A):]) & (for x being
bound_QC-variable of A, p being FinSequence of [:NAT, QC-symbols(A):],
e being Element of vSUB(A)
st [p,(QSub(A)).[<*[3, 0]*>^<*x*>^p,e]] in [:QC-WFF(A),vSUB(A):]
holds [<*[3, 0]*>^<*x*>^p,e] in [:QC-WFF(A),vSUB(A):])
proof
QC-WFF(A) is A-closed by QC_LANG1:7;
then QC-WFF(A) is Subset of [:NAT, QC-symbols(A):]*;
hence [:QC-WFF(A),vSUB(A):] is Subset of [:[:NAT, QC-symbols(A):]*,vSUB(A):]
by ZFMISC_1:95;
thus (for k being Nat, p being (QC-pred_symbol of k,A), ll being
QC-variable_list of k,A, e being Element of vSUB(A)
holds [<*p*>^ll,e] in [:QC-WFF(A),
vSUB(A):])
proof
let k be Nat, p be (QC-pred_symbol of k,A), ll be
QC-variable_list of k,A, e be Element of vSUB(A);
p!ll = <*p*>^ll by QC_LANG1:8;
hence thesis by ZFMISC_1:def 2;
end;
VERUM(A) in QC-WFF(A);
hence for e being Element of vSUB(A) holds [<*[0, 0]*>,e] in
[:QC-WFF(A),vSUB(A):] by ZFMISC_1:def 2;
thus for p being FinSequence of [:NAT,QC-symbols(A):],
e being Element of vSUB(A) st
[p,e] in [:QC-WFF(A),vSUB(A):] holds [<*[1, 0]*>^p,e] in
[:QC-WFF(A),vSUB(A):]
proof
let p be FinSequence of [:NAT,QC-symbols(A):], e be Element of vSUB(A);
assume [p,e] in [:QC-WFF(A),vSUB(A):];
then ex a,b being object st a in QC-WFF(A) & b in vSUB(A) &
[p,e] = [a,b] by ZFMISC_1:def 2;
then reconsider p9 = p as Element of QC-WFF(A) by XTUPLE_0:1;
'not' p9 = <*[1, 0]*>^@p9;
hence thesis by ZFMISC_1:def 2;
end;
thus for p, q being FinSequence of [:NAT, QC-symbols(A):],
e being Element of vSUB(A) st [
p,e] in [:QC-WFF(A),vSUB(A):] & [q,e] in [:QC-WFF(A),vSUB(A):]
holds [<*[2, 0]*>^p^q,e] in
[:QC-WFF(A),vSUB(A):]
proof
let p, q be FinSequence of [:NAT, QC-symbols(A):], e be Element of vSUB(A);
assume that
A1: [p,e] in [:QC-WFF(A),vSUB(A):] and
A2: [q,e] in [:QC-WFF(A),vSUB(A):];
ex c,d being object st c in QC-WFF(A) & d in vSUB(A) &
[q,e] = [c,d] by A2,ZFMISC_1:def 2;
then reconsider q9 = q as Element of QC-WFF(A) by XTUPLE_0:1;
ex a,b being object st a in QC-WFF(A) & b in vSUB(A) &
[p,e] = [a,b] by A1,ZFMISC_1:def 2;
then reconsider p9 = p as Element of QC-WFF(A) by XTUPLE_0:1;
p9 '&' q9 = <*[2, 0]*>^@p9^@q9;
hence thesis by ZFMISC_1:def 2;
end;
thus for x being bound_QC-variable of A, p
being FinSequence of [:NAT, QC-symbols(A):], e
being Element of vSUB(A) st [p,(QSub(A)).[<*[3, 0]*>^<*x*>^p,e]] in
[:QC-WFF(A),vSUB(A):]
holds [<*[3, 0]*>^<*x*>^p,e] in [:QC-WFF(A),vSUB(A):]
proof
let x be bound_QC-variable of A,
p be FinSequence of [:NAT, QC-symbols(A):],
e be Element of vSUB(A);
assume [p,(QSub(A)).[<*[3, 0]*>^<*x*>^p,e]] in [:QC-WFF(A),vSUB(A):];
then
ex a,b being object st a in QC-WFF(A) & b in vSUB(A) &
[p,(QSub(A)).[<*[3, 0]*>^ <*x*>^p,e]] =
[a,b] by ZFMISC_1:def 2;
then reconsider p9 = p as Element of QC-WFF(A) by XTUPLE_0:1;
All(x,p9) = <*[3, 0]*>^<*x*>^@p9;
hence thesis by ZFMISC_1:def 2;
end;
end;
definition
let A;
let IT be set;
attr IT is A-Sub-closed means
:Def16:
IT is Subset of [:[:NAT, QC-symbols(A):]*,vSUB(A):] &
(for k being Nat, p being (QC-pred_symbol of k,A), ll being
QC-variable_list of k,A, e being Element of vSUB(A) holds
[<*p*>^ll,e] in IT) & (for
e being Element of vSUB(A) holds [<*[0, 0]*>,e] in IT) &
(for p being FinSequence of [:NAT,QC-symbols(A):],
e being Element of vSUB(A) st
[p,e] in IT holds [<*[1, 0]*>^p,e]
in IT) & (for p, q being FinSequence of [:NAT, QC-symbols(A):],
e being Element of vSUB(A)
st [p,e] in IT & [q,e] in IT holds [<*[2, 0]*>^p^q,e] in IT) & (for x being
bound_QC-variable of A, p being FinSequence of [:NAT, QC-symbols(A):],
e being Element of vSUB(A) st [p,(QSub(A)).[<*[3, 0]*>^<*x*>^p,e]] in IT holds
[<*[3, 0]*>^<*x*>^p,e] in IT);
end;
registration
let A;
cluster A-Sub-closed non empty for set;
existence
proof
take [:QC-WFF(A),vSUB(A):];
[:QC-WFF(A),vSUB(A):] is Subset of [:[:NAT, QC-symbols(A):]*,vSUB(A):] &
(for k being Nat, p being (QC-pred_symbol of k,A), ll being
QC-variable_list of k,A, e being Element of vSUB(A) holds
[<*p*>^ll,e] in [:QC-WFF(A),vSUB(A):]) & (for e being Element of vSUB(A)
holds [<*[0, 0]*>,e] in [:QC-WFF(A),vSUB(A):]) &
(for p being FinSequence of [:NAT,QC-symbols(A):],
e being Element of vSUB(A) st
[p,e] in [:QC-WFF(A),vSUB(A):] holds [<*[1, 0]*>^p,e]
in [:QC-WFF(A),vSUB(A):]) & (for p, q being FinSequence of
[:NAT, QC-symbols(A):], e being Element of vSUB(A) st [p,e]
in [:QC-WFF(A),vSUB(A):] & [q,e] in [:QC-WFF(A),vSUB(A):] holds
[<*[2, 0]*>^p^q,e] in [:QC-WFF(A),vSUB(A):]) &
(for x being bound_QC-variable of A, p being FinSequence of
[:NAT, QC-symbols(A):], e being Element of vSUB(A) st
[p,(QSub(A)).[<*[3, 0]*>^<*x*>^p,e]] in [:QC-WFF(A),vSUB(A):] holds
[<*[3, 0]*>^<*x*>^p,e] in [:QC-WFF(A),vSUB(A):])
by Th7;
hence thesis;
end;
end;
Lm3: 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
0 in QC-symbols(A) by QC_LANG1:3;
then [3,0] in [:NAT,QC-symbols(A):] by ZFMISC_1:87;
then rng <*[3, 0]*> = {[3, 0]} &
{[3, 0]} c= [:NAT, QC-symbols(A):] by FINSEQ_1:39,ZFMISC_1:31;
then reconsider y = <*[3, 0]*> as FinSequence of [:NAT, QC-symbols(A):]
by FINSEQ_1:def 4;
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 QC_LANG1:4;
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;
Lm4: for k being Nat, l being QC-symbol of A,
e being Element of vSUB(A) holds
[<*[k, l]*>,e] in [:[:NAT, QC-symbols(A):]*,vSUB(A):]
proof
let k be Nat;
A1: k in NAT by ORDINAL1:def 12;
let l be QC-symbol of A;
let e;
reconsider kl = [k, l] as Element of [:NAT,QC-symbols(A):]
by A1,ZFMISC_1:def 2;
<*kl*> in [:NAT,QC-symbols(A):]* by FINSEQ_1:def 11;
hence thesis by ZFMISC_1:def 2;
end;
Lm5: for k being Nat, p being (QC-pred_symbol of k,A), ll being (
QC-variable_list of k,A), e being Element of vSUB(A) holds [<*p*>^ll,e]
in [:[:NAT,QC-symbols(A):]*,vSUB(A):]
proof
let k be Nat, p be (QC-pred_symbol of k,A),
ll be QC-variable_list of k, A;
QC-pred_symbols(A) c= [:NAT,QC-symbols(A):] by QC_LANG1:6;
then k-ary_QC-pred_symbols(A) c= [:NAT,QC-symbols(A):];
then
A1: rng <*p*> c= [:NAT,QC-symbols(A):];
QC-variables(A) c= [:NAT,QC-symbols(A):] by QC_LANG1:4;
then rng ll 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;
then <*p*>^ll is FinSequence of [:NAT,QC-symbols(A):] by FINSEQ_1:def 4;
then <*p*>^ll in [:NAT,QC-symbols(A):]* by FINSEQ_1:def 11;
hence thesis by ZFMISC_1:def 2;
end;
definition
let A;
func QC-Sub-WFF(A) -> non empty set means
:Def17:
it is A-Sub-closed & for D
being non empty set st D is A-Sub-closed holds it c= D;
existence
proof
set e =the Element of vSUB(A);
defpred P[object] means
for D being non empty set st D is A-Sub-closed holds
$1 in D;
consider D0 being set such that
A1: for x being object holds x in D0 iff
x in [:[:NAT, QC-symbols(A):]*,vSUB(A):] & P[
x] from XBOOLE_0:sch 1;
0 in QC-symbols(A) by QC_LANG1:3;
then [<*[0, 0]*>,e] in [:[:NAT, QC-symbols(A):]*,vSUB(A):] &
for D being non empty set st D is A-Sub-closed
holds [<*[0, 0]*>,e] in D
by Lm4;
then reconsider D0 as non empty set by A1;
take D0;
D0 c= [:[:NAT, QC-symbols(A):]*,vSUB(A):]
by A1;
hence D0 is Subset of [:[:NAT, QC-symbols(A):]*,vSUB(A):];
thus for k being Nat, p being (QC-pred_symbol of k,A), ll being
QC-variable_list of k,A, e being Element of vSUB(A) holds
[<*p*>^ll,e] in D0
proof
let k be Nat, p be (QC-pred_symbol of k,A), ll be
QC-variable_list of k,A, e being Element of vSUB(A);
[<*p*>^ll,e] in [:[:NAT, QC-symbols(A):]*,vSUB(A):] &
for D being non empty set
st D is A-Sub-closed holds [<*p*>^ll,e] in D by Lm5;
hence thesis by A1;
end;
thus for e holds [<*[0, 0]*>,e] in D0
proof
let e;
0 in QC-symbols(A) by QC_LANG1:3;
then [<*[0, 0]*>,e] in [:[:NAT, QC-symbols(A):]*,vSUB(A):] &
for D being non empty set
st D is A-Sub-closed holds [<*[0, 0]*>,e] in D by Lm4;
hence thesis by A1;
end;
thus for p being FinSequence of [:NAT, QC-symbols(A):],
e being Element of vSUB(A) st [
p,e] in D0 holds [<*[1, 0]*>^p,e] in D0
proof
let p be FinSequence of [:NAT, QC-symbols(A):];
let e be Element of vSUB(A);
assume
A2: [p,e] in D0;
A3: for D being non empty set st D is A-Sub-closed holds [<*[1, 0]*>^p
,e] in D
proof
let D be non empty set;
assume
A4: D is A-Sub-closed;
then [p,e] in D by A1,A2;
hence thesis by A4;
end;
0 in QC-symbols(A) by QC_LANG1:3;
then [1,0] in [:NAT,QC-symbols(A):] by ZFMISC_1:87;
then rng <*[1, 0]*> = {[1, 0]} &
{[1, 0]} c= [:NAT, QC-symbols(A):] by FINSEQ_1:39,ZFMISC_1:31;
then reconsider y=<*[1, 0]*> as FinSequence of [:NAT, QC-symbols(A):]
by FINSEQ_1:def 4;
y^p is FinSequence of [:NAT, QC-symbols(A):];
then <*[1, 0]*>^p in [:NAT, QC-symbols(A):]* by FINSEQ_1:def 11;
then [<*[1, 0]*>^p,e] in [:[:NAT, QC-symbols(A):]*,vSUB(A):]
by ZFMISC_1:def 2;
hence thesis by A1,A3;
end;
thus for p, q being FinSequence of [:NAT, QC-symbols(A):],
e being Element of vSUB(A)
st [p,e] in D0 & [q,e] in D0 holds [<*[2, 0]*>^p^q,e] in D0
proof
let p, q be FinSequence of [:NAT, QC-symbols(A):],
e be Element of vSUB(A) such that
A5: [p,e] in D0 & [q,e] in D0;
A6: for D being non empty set st D is A-Sub-closed holds [<*[2, 0]*>^p
^q,e] in D
proof
let D be non empty set;
assume
A7: D is A-Sub-closed;
then [p,e] in D & [q,e] in D by A1,A5;
hence thesis by A7;
end;
0 in QC-symbols(A) by QC_LANG1:3;
then [2,0] in [:NAT,QC-symbols(A):] by ZFMISC_1:87;
then rng <*[2, 0]*> = {[2, 0]} &
{[2, 0]} c= [:NAT, QC-symbols(A):] by FINSEQ_1:39,ZFMISC_1:31;
then reconsider y=<*[2, 0]*> as FinSequence of [:NAT, QC-symbols(A):]
by FINSEQ_1:def 4;
y^p^q is FinSequence of [:NAT, QC-symbols(A):];
then <*[2, 0]*>^p^q in [:NAT, QC-symbols(A):]* by FINSEQ_1:def 11;
then [<*[2, 0]*>^p^q,e] in [:[:NAT, QC-symbols(A):]*,vSUB(A):]
by ZFMISC_1:def 2;
hence thesis by A1,A6;
end;
thus for x being bound_QC-variable of A, p being FinSequence of
[:NAT, QC-symbols(A):], e being Element of vSUB(A) st
[p,(QSub(A)).[<*[3, 0]*>^<*x*>^p,e]] in D0 holds [<*[3, 0]
*>^<*x*>^p,e] in D0
proof
let x be bound_QC-variable of A,
p be FinSequence of [:NAT, QC-symbols(A):], e be Element of vSUB(A);
assume
A8: [p,(QSub(A)).[<*[3, 0]*>^<*x*>^p,e]] in D0;
A9: for D being non empty set st D is A-Sub-closed holds [<*[3, 0]*>^
<*x*>^p,e] in D
proof
let D be non empty set;
assume
A10: D is A-Sub-closed;
then [p,(QSub(A)).[<*[3, 0]*>^<*x*>^p,e]] in D by A1,A8;
hence thesis by A10;
end;
<*[3, 0]*>^<*x*>^p is FinSequence of [:NAT, QC-symbols(A):] by Lm3;
then <*[3, 0]*>^<*x*>^p in [:NAT, QC-symbols(A):]* by FINSEQ_1:def 11;
then [<*[3, 0]*>^<*x*>^p,e] in [:[:NAT, QC-symbols(A):]*,vSUB(A):]
by ZFMISC_1:def 2;
hence thesis by A1,A9;
end;
let D be non empty set such that
A11: D is A-Sub-closed;
let x be object;
assume x in D0;
hence thesis by A1,A11;
end;
uniqueness
proof
let D1, D2 be non empty set;
assume D1 is A-Sub-closed & ( for D being non empty set st D is
A-Sub-closed holds D1 c= D)& D2 is A-Sub-closed & for D being non empty set
st D is A-Sub-closed holds D2 c= D;
then D1 c= D2 & D2 c= D1;
hence thesis by XBOOLE_0:def 10;
end;
end;
reserve S,S9,S1,S2,S19,S29,T1,T2 for Element of QC-Sub-WFF(A);
theorem Th8:
ex p,e st S = [p,e]
proof
[:QC-WFF(A),vSUB(A):] is Subset of [:[:NAT, QC-symbols(A):]*,vSUB(A):] &
(for k being Nat, p being (QC-pred_symbol of k,A),
ll being QC-variable_list
of k,A , e being Element of vSUB(A) holds [<*p*>^ll,e]
in [:QC-WFF(A),vSUB(A):]) & (for e
being Element of vSUB(A) holds [<*[0, 0]*>,e] in
[:QC-WFF(A),vSUB(A):]) & (for p being
FinSequence of [:NAT,QC-symbols(A):], e being Element of vSUB(A)
st [p,e] in [:QC-WFF(A),vSUB(A):]
holds [<*[1, 0]*>^p,e] in [:QC-WFF(A),vSUB(A):]) &
(for p, q being FinSequence of [:
NAT, QC-symbols(A):], e being Element of vSUB(A) st
[p,e] in [:QC-WFF(A),vSUB(A):] & [q,e] in [:
QC-WFF(A),vSUB(A):] holds [<*[2, 0]*>^p^q,e]
in [:QC-WFF(A),vSUB(A):]) & (for x being
bound_QC-variable of A, p being FinSequence of [:NAT, QC-symbols(A):],
e being Element of vSUB(A)
st [p,(QSub(A)).[<*[3, 0]*>^<*x*>^p,e]] in [:QC-WFF(A),vSUB(A):]
holds [<*[3, 0]*>^<*x*>^p,e] in [:QC-WFF(A),vSUB(A):]) by Th7;
then [:QC-WFF(A),vSUB(A):] is A-Sub-closed;
then QC-Sub-WFF(A) c= [:QC-WFF(A),vSUB(A):] by Def17;
then S in [:QC-WFF(A),vSUB(A):];
then consider a,b being object such that
A1: a in QC-WFF(A) and
A2: b in vSUB(A) and
A3: S = [a,b] by ZFMISC_1:def 2;
reconsider e = b as Element of vSUB(A) by A2;
reconsider p = a as Element of QC-WFF(A) by A1;
take p,e;
thus thesis by A3;
end;
registration
let A;
cluster QC-Sub-WFF(A) -> A-Sub-closed;
coherence by Def17;
end;
definition
let A;
let P be QC-pred_symbol of A;
let l be FinSequence of QC-variables(A);
let e;
assume
A1: the_arity_of P = len l;
func Sub_P(P,l,e) -> Element of QC-Sub-WFF(A) equals
:Def18:
[P!l,e];
coherence
proof
set k = len l;
set QCP = {QP where QP is QC-pred_symbol of A: the_arity_of QP = 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;
P!l = <*P*>^l by QC_LANG1:8;
hence thesis by Def16;
end;
end;
theorem Th9:
for k being Nat, P being QC-pred_symbol of k,A, ll being
QC-variable_list of k,A holds Sub_P(P,ll,e) = [P!ll,e]
proof
let k be Nat, P be QC-pred_symbol of k,A,
ll be QC-variable_list of k, A;
set QCP = {QP where QP is QC-pred_symbol of A: the_arity_of QP = 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,Def18;
end;
definition
let A;
let S;
attr S is A-Sub_VERUM means
ex e st S = [VERUM(A),e];
end;
definition
let A;
let S;
redefine func S`1 -> Element of QC-WFF(A); :: redefines `1 (XTUPLE_0, definition)
coherence
proof
ex p,e st S = [p,e] by Th8;
hence thesis;
end;
redefine func S`2 -> Element of vSUB(A); :: redefines `2 (XTUPLE_0, definition)
coherence
proof
ex p,e st S = [p,e] by Th8;
hence thesis;
end;
end;
theorem Th10:
S = [S`1,S`2]
proof
ex p,e st S = [p,e] by Th8;
hence thesis;
end;
definition
let A;
let S;
func Sub_not S -> Element of QC-Sub-WFF(A) equals
['not' S`1,S`2];
coherence
proof
[S`1,S`2] is Element of QC-Sub-WFF(A) by Th10;
hence thesis by Def16;
end;
end;
definition
let A;
let S, S9;
assume
A1: S`2 = (S9)`2;
func Sub_&(S,S9) -> Element of QC-Sub-WFF(A) equals
:Def21:
[(S`1) '&' ((S9)`1)
,S`2];
coherence
proof
[S`1,S`2] is Element of QC-Sub-WFF(A) & [(S9)`1,(S9)`2] is Element of
QC-Sub-WFF(A) by Th10;
hence thesis by A1,Def16;
end;
end;
reserve B for Element of [:QC-Sub-WFF(A),bound_QC-variables(A):];
definition
let A;
let B;
redefine func B`1 -> Element of QC-Sub-WFF(A); :: redefines `1 (XTUPLE_0, definition)
coherence by MCART_1:10;
redefine func B`2 -> Element of bound_QC-variables(A); :: redefines `2 (XTUPLE_0, definition)
coherence by MCART_1:10;
end;
definition
let A;
let B;
attr B is quantifiable means
ex e st (B`1)`2 = (QSub(A)).[All((B)`2,(B`1) `1),e];
end;
definition
let A;
let B;
assume
A1: B is quantifiable;
mode second_Q_comp of B -> Element of vSUB(A) means
:Def23:
(B`1)`2 = (QSub(A)).[All (B`2,(B`1)`1),it];
existence by A1;
end;
reserve SQ for second_Q_comp of B;
definition
let A;
let B, SQ;
assume
A1: B is quantifiable;
func Sub_All(B,SQ) -> Element of QC-Sub-WFF(A) equals
:Def24:
[All(B`2,(B`1)`1)
,SQ];
coherence
proof
(B`1)`2 = (QSub(A)).[All(B`2,(B`1)`1),SQ] by A1,Def23;
then B`1 = [(B`1)`1, (QSub(A)).[All(B`2,(B`1)`1),SQ]] by Th10;
hence thesis by Def16;
end;
end;
definition
let A;
let S, x;
redefine func [S,x] -> Element of [:QC-Sub-WFF(A),bound_QC-variables(A):]; :: redefines [ (TARSKI, definition)
coherence
proof
[S,x] in [:QC-Sub-WFF(A),bound_QC-variables(A):];
hence thesis;
end;
end;
scheme
SubQCInd { Al() -> QC-alphabet, Pro[Element of QC-Sub-WFF(Al())]}:
for S being Element of QC-Sub-WFF(Al())
holds Pro[S]
provided
A1: for k being Nat, P being (QC-pred_symbol of k,Al()), ll being
QC-variable_list of k,Al(), e being Element of vSUB(Al()) holds
Pro[Sub_P(P,ll,e)] and
A2: for S being Element of QC-Sub-WFF(Al()) st
S is Al()-Sub_VERUM holds Pro[S] and
A3: for S being Element of QC-Sub-WFF(Al()) st Pro[S] holds Pro[Sub_not S] and
A4: for S,S9 being Element of QC-Sub-WFF(Al())
st S`2 = (S9)`2 & Pro[S] & Pro[S9] holds Pro[Sub_&(S,S9)] and
A5: for x being bound_QC-variable of Al(),
S being Element of QC-Sub-WFF(Al()), SQ
being second_Q_comp of [S,x] st [S,x] is quantifiable & Pro[S] holds Pro[
Sub_All([S,x], SQ)]
proof
set X = { S where S is Element of QC-Sub-WFF(Al()) : Pro[S]};
X is non empty
proof
set e =the Element of vSUB(Al());
reconsider V = [VERUM(Al()),e] as Element of QC-Sub-WFF(Al()) by Def16;
V is Al()-Sub_VERUM;
then Pro[V] by A2;
then V in X;
hence thesis;
end;
then reconsider X as non empty set;
for e being Element of vSUB(Al()) holds [VERUM(Al()),e] in X
proof
let e be Element of vSUB(Al());
reconsider V = [VERUM(Al()),e] as Element of QC-Sub-WFF(Al()) by Def16;
V is Al()-Sub_VERUM;
then Pro[V] by A2;
hence thesis;
end;
then
A6: for e being Element of vSUB(Al()) holds [<*[0, 0]*>,e] in X;
A7: for p being FinSequence of [:NAT, QC-symbols(Al()):],
e being Element of vSUB(Al()) st [p,
e] in X holds [<*[1, 0]*>^p,e] in X
proof
let p be FinSequence of [:NAT, QC-symbols(Al()):],
e be Element of vSUB(Al());
assume [p,e] in X;
then consider S being Element of QC-Sub-WFF(Al()) such that
A8: S = [p,e] and
A9: Pro[S];
Pro[Sub_not S] by A3,A9;
then Sub_not S in X;
hence thesis by A8;
end;
A10: for x being bound_QC-variable of Al(),
p being FinSequence of [:NAT, QC-symbols(Al()):], e
being Element of vSUB(Al()) st [p,(QSub(Al())).[<*[3, 0]*>^<*x*>^p,e]]
in X holds
[<*[3, 0]*>^<*x*>^p,e] in X
proof
let x be bound_QC-variable of Al(),
p be FinSequence of [:NAT, QC-symbols(Al()):], e being
Element of vSUB(Al());
assume [p,(QSub(Al())).[<*[3, 0]*>^<*x*>^p,e]] in X;
then consider S being Element of QC-Sub-WFF(Al()) such that
A11: S = [p,(QSub(Al())).[<*[3,0]*>^<*x*>^p,e]] and
A12: Pro[S];
consider B being set such that
A13: B = [S,x];
reconsider B as Element of [:QC-Sub-WFF(Al()),bound_QC-variables(Al()):]
by A13;
A14: B`1 = S & B`2 = x by A13;
A15: S`2 = (QSub(Al())).[All(x,S`1),e] by A11;
then
A16: B is quantifiable by A14;
then reconsider e as second_Q_comp of B by A15,A14,Def23;
Pro[Sub_All(B,e)] by A5,A12,A13,A16;
then Sub_All(B,e) in X;
then [All(B`2,(B`1)`1),e] in X by A16,Def24;
hence thesis by A11,A14;
end;
let F be Element of QC-Sub-WFF(Al());
A17: X c= [:[:NAT, QC-symbols(Al()):]*,vSUB(Al()):]
proof
let x be object;
assume x in X;
then ex S being Element of QC-Sub-WFF(Al()) st x = S & Pro[S];
then consider p being Element of QC-WFF(Al()),
e being Element of vSUB(Al())
such that
A18: x = [p,e] by Th8;
p = @p;
then p in [:NAT,QC-symbols(Al()):]* by FINSEQ_1:def 11;
hence thesis by A18,ZFMISC_1:def 2;
end;
A19: for p, q being FinSequence of [:NAT, QC-symbols(Al()):],
e being Element of vSUB(Al()) st
[p,e] in X & [q,e] in X holds [<*[2, 0]*>^p^q,e] in X
proof
let p, q be FinSequence of [:NAT, QC-symbols(Al()):],
e be Element of vSUB(Al());
assume [p,e] in X;
then consider S1 being Element of QC-Sub-WFF(Al()) such that
A20: S1 = [p,e] and
A21: Pro[S1];
assume [q,e] in X;
then consider S2 being Element of QC-Sub-WFF(Al()) such that
A22: S2 = [q,e] and
A23: Pro[S2];
consider p9 being Element of QC-WFF(Al()),
e1 being Element of vSUB(Al()) such that
A24: [p,e] = [p9,e1] by A20,Th8;
A25: e = e1 by A24,XTUPLE_0:1;
then
A26: S1`2 = e1 by A20;
then
A27: S1`2 = S2`2 by A22,A25;
then Pro[Sub_&(S1,S2)] by A4,A21,A23;
then Sub_&(S1,S2) in X;
then
A28: [S1`1 '&' S2`1,S1`2] in X by A27,Def21;
A29: p = p9 by A24,XTUPLE_0:1;
then S1`1 = p9 by A20;
hence thesis by A22,A29,A25,A26,A28;
end;
for k being Nat, P being (QC-pred_symbol of k,Al()), ll being
QC-variable_list of k,Al(), e being Element of vSUB(Al()) holds
[<*P*>^ll,e] in X
proof
let k be Nat, P be (QC-pred_symbol of k,Al()), ll be
QC-variable_list of k,Al(), e being Element of vSUB(Al());
( Pro[Sub_P(P,ll,e)])& [P!ll,e] = Sub_P(P,ll,e) by A1,Th9;
then [P!ll,e] in X;
hence thesis by QC_LANG1:8;
end;
then X is Al()-Sub-closed by A17,A6,A7,A19,A10;
then QC-Sub-WFF(Al()) c= X by Def17;
then F in X;
then ex S being Element of QC-Sub-WFF(Al()) st S = F & Pro[S];
hence thesis;
end;
definition
let A;
let S;
attr S is Sub_atomic means
ex k being Nat, P being
QC-pred_symbol of k,A, ll being QC-variable_list of k,A,
e being Element of vSUB(A) st
S = Sub_P(P,ll,e);
end;
theorem Th11:
S is Sub_atomic implies S`1 is atomic
proof
assume S is Sub_atomic;
then consider
k being Nat, P being (QC-pred_symbol of k,A), ll being
QC-variable_list of k,A, e being Element of vSUB(A) such that
A1: S = Sub_P(P,ll,e);
S = [P!ll,e] by A1,Th9;
then S`1 = P!ll;
hence thesis;
end;
registration
let A;
let k be Nat;
let P be (QC-pred_symbol of k,A), ll be QC-variable_list of k,A;
let e be Element of vSUB(A);
cluster Sub_P(P,ll,e) -> Sub_atomic;
coherence;
end;
definition
let A;
let S;
attr S is Sub_negative means
:Def26:
ex S9 st S = Sub_not S9;
attr S is Sub_conjunctive means
:Def27:
ex S1,S2 st S = Sub_&(S1,S2) & S1`2 = S2`2;
end;
definition
let A;
let S;
attr S is Sub_universal means
:Def28:
ex B,SQ st S = Sub_All(B,SQ) & B is quantifiable;
end;
theorem Th12:
for S holds S is A-Sub_VERUM or S is Sub_atomic or S is
Sub_negative or S is Sub_conjunctive or S is Sub_universal
proof
defpred P[Element of QC-Sub-WFF(A)] means
$1 is A-Sub_VERUM or $1 is Sub_atomic
or $1 is Sub_negative or $1 is Sub_conjunctive or $1 is Sub_universal;
A1: for k being Nat, p being (QC-pred_symbol of k,A), ll being
QC-variable_list of k,A, e being Element of vSUB(A) holds P[Sub_P(p,ll,e)];
A2: for S being Element of QC-Sub-WFF(A) st S is A-Sub_VERUM holds P[S];
A3: for x being bound_QC-variable of A, S being Element of QC-Sub-WFF(A),
SQ being
second_Q_comp of [S,x] st [S,x] is quantifiable & P[S] holds P[Sub_All([S,x],
SQ)] by Def28;
A4: for S1, S2 being Element of QC-Sub-WFF(A) st S1`2 = S2`2 & P[S1] & P[S2]
holds P[Sub_&(S1,S2)] by Def27;
A5: for S being Element of QC-Sub-WFF(A) st P[S] holds P[Sub_not(S)] by Def26;
thus for S being Element of QC-Sub-WFF(A) holds
P[S] from SubQCInd (A1, A2, A5,
A4, A3);
end;
definition
let A;
let S such that
A1: S is Sub_atomic;
func Sub_the_arguments_of S -> FinSequence of QC-variables(A) means
:Def29:
ex k being Nat, P being (QC-pred_symbol of k,A), ll being
QC-variable_list of k,A, e being Element of vSUB(A)
st it = ll & S = Sub_P(P,ll,e);
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, e1 being Element of vSUB(A) such that
A2: ll1 = ll19 and
A3: S = Sub_P(P1,ll19,e1);
A4: S = [P1!ll19,e1] by A3,Th9;
given k2 being Nat, P2 being (QC-pred_symbol of k2,A),
ll29 being
QC-variable_list of k2,A, e2 being Element of vSUB(A) such that
A5: ll2 = ll29 and
A6: S = Sub_P(P2,ll29,e2);
A7: <*P2*>^ll29 = P2!ll29 & S`1 = <*P1*>^ll19 by A4,QC_LANG1:8;
A8: S`1 is atomic by A1,Th11;
A9: S = [P2!ll29,e2] by A6,Th9;
then
A10: S`1 = P2!ll29;
S`1 = P1!ll19 by A4;
then P1 = the_pred_symbol_of (S`1) by A8,QC_LANG1:def 22
.= P2 by A10,A8,QC_LANG1:def 22;
hence ll1 = ll2 by A2,A5,A9,A7,FINSEQ_1:33;
end;
end;
definition
let A;
let S such that
A1: S is Sub_negative;
func Sub_the_argument_of S -> Element of QC-Sub-WFF(A) means
:Def30:
S = Sub_not it;
existence by A1;
uniqueness
proof
let S1,S2;
A2: S1 = [S1`1,S1`2] & S2 = [S2`1,S2`2] by Th10;
assume
A3: S = Sub_not(S1) & S = Sub_not(S2);
then 'not' S1`1 = 'not' S2`1 by XTUPLE_0:1;
then S1`1 = S2`1 by FINSEQ_1:33;
hence thesis by A3,A2,XTUPLE_0:1;
end;
end;
definition
let A;
let S such that
A1: S is Sub_conjunctive;
func Sub_the_left_argument_of S -> Element of QC-Sub-WFF(A) means
:Def31:
ex S9 st S = Sub_&(it,S9) & it`2 = (S9)`2;
existence by A1;
uniqueness
proof
let S1,S2;
given T1 being Element of QC-Sub-WFF(A) such that
A2: S = Sub_&(S1,T1) & S1`2 = T1`2;
given T2 being Element of QC-Sub-WFF(A) such that
A3: S = Sub_&(S2,T2) & S2`2 = T2`2;
A4: len @(S1`1) <= len @(S2`1) or len @(S2`1) <= len @(S1`1);
A5: S = [(S2`1) '&' (T2`1),S2`2] by A3,Def21;
A6: S = [(S1`1) '&' (T1`1),S1`2] by A2,Def21;
then (S1`1) '&' (T1`1) = (S2`1) '&' (T2`1) by A5,XTUPLE_0:1;
then <*[2,0]*>^((@S1`1)^(@T1`1)) = (S2`1) '&' (T2`1) by FINSEQ_1:32
.= <*[2,0]*>^((@S2`1)^(@T2`1)) by FINSEQ_1:32;
then @S1`1^@T1`1 = @S2`1^@T2`1 by FINSEQ_1:33;
then consider a,b,c,d being FinSequence such that
A7: a = @S1`1 & b = @S2`1 or a = @S2`1 & b = @S1`1 and
A8: len a <= len b & a^c = b^d by A4;
A9: S1 = [S1`1,S1`2] & S2 = [S2`1,S2`2] by Th10;
ex t being FinSequence st a^t = b by A8,FINSEQ_1:47;
then S1`1 = S2`1 by A7,QC_LANG1:13;
hence thesis by A6,A5,A9,XTUPLE_0:1;
end;
end;
definition
let A;
let S such that
A1: S is Sub_conjunctive;
func Sub_the_right_argument_of S -> Element of QC-Sub-WFF(A) means
:Def32:
ex S9 st S = Sub_&(S9,it) & (S9)`2 = it`2;
existence
by A1;
uniqueness
proof
let T1,T2;
given S1 being Element of QC-Sub-WFF(A) such that
A2: S = Sub_&(S1,T1) & S1`2 = T1`2;
A3: T1 = [T1`1,T1`2] & T2 = [T2`1,T2`2] by Th10;
given S2 being Element of QC-Sub-WFF(A) such that
A4: S = Sub_&(S2,T2) & S2`2 = T2`2;
A5: S = [(S1`1) '&' (T1`1),T1`2] by A2,Def21;
A6: S = [(S2`1) '&' (T2`1),T2`2] by A4,Def21;
then (S1`1) '&' (T1`1) = (S2`1) '&' (T2`1) by A5,XTUPLE_0:1;
then <*[2,0]*>^((@S1`1)^(@T1`1)) = (S2`1) '&' (T2`1) by FINSEQ_1:32
.= <*[2,0]*>^((@S2`1)^(@T2`1)) by FINSEQ_1:32;
then
A7: @S1`1^@T1`1 = @S2`1^@T2`1 by FINSEQ_1:33;
S1 = Sub_the_left_argument_of S by A1,A2,Def31
.= S2 by A1,A4,Def31;
then @T1`1 = @T2`1 by A7,FINSEQ_1:33;
hence thesis by A5,A6,A3,XTUPLE_0:1;
end;
end;
definition
let A;
let S such that
A1: S is Sub_universal;
func Sub_the_bound_of S -> bound_QC-variable of A means
ex B,SQ st S = Sub_All(B, SQ) & B`2 = it & B is quantifiable;
existence
proof
consider B,SQ such that
A2: S = Sub_All(B,SQ) & B is quantifiable by A1;
take B`2;
thus thesis by A2;
end;
uniqueness
proof
let x1,x2;
assume that
A3: ex B,SQ st S = Sub_All(B,SQ) & B`2 = x1 & B is quantifiable and
A4: ex B,SQ st S = Sub_All(B,SQ) & B`2 = x2 & B is quantifiable;
consider B1 being Element of [:QC-Sub-WFF(A),bound_QC-variables(A):],
SQ1 being
second_Q_comp of B1 such that
A5: S = Sub_All(B1,SQ1) and
A6: B1`2 = x1 and
A7: B1 is quantifiable by A3;
consider B2 being Element of [:QC-Sub-WFF(A),bound_QC-variables(A):],
SQ2 being second_Q_comp of B2 such that
A8: S = Sub_All(B2,SQ2) and
A9: B2`2 = x2 and
A10: B2 is quantifiable by A4;
A11: [All(B2`2,(B2`1)`1),SQ2] = S by A8,A10,Def24;
[All(B1`2,(B1`1)`1),SQ1] = S by A5,A7,Def24;
then All(B1`2,(B1`1)`1) = All(B2`2,((B2`1))`1) by A11,XTUPLE_0:1;
hence thesis by A6,A9,QC_LANG2:5;
end;
end;
definition
let A;
let A2 be Element of QC-Sub-WFF(A) such that
A1: A2 is Sub_universal;
func Sub_the_scope_of A2 -> Element of QC-Sub-WFF(A) means
:Def34:
ex B,SQ st A2 = Sub_All(B,SQ) & B`1 = it & B is quantifiable;
existence
proof
consider B,SQ such that
A2: A2 = Sub_All(B,SQ) & B is quantifiable by A1;
take B`1;
thus thesis by A2;
end;
uniqueness
proof
let S1,S2;
given B1 being Element of [:QC-Sub-WFF(A),bound_QC-variables(A):],
SQ1 being second_Q_comp of B1 such that
A3: A2 = Sub_All(B1,SQ1) and
A4: B1`1 = S1 and
A5: B1 is quantifiable;
A6: A2 = [All(B1`2,(B1`1)`1),SQ1] by A3,A5,Def24;
A7: (B1`1)`2 = (QSub(A)).[All(B1`2,(B1`1)`1),SQ1] by A5,Def23;
given B2 being Element of [:QC-Sub-WFF(A),bound_QC-variables(A):],
SQ2 being second_Q_comp of B2 such that
A8: A2 = Sub_All(B2,SQ2) and
A9: B2`1 = S2 and
A10: B2 is quantifiable;
A11: B1`1 = [(B1`1)`1,(B1`1)`2] & B2`1 = [(B2`1)`1,(B2`1)`2] by Th10;
A12: A2 = [All(B2`2,(B2`1)`1),SQ2] by A8,A10,Def24;
then All(B1`2,(B1`1)`1)= All(B2`2,(B2`1)`1) by A6,XTUPLE_0:1;
then (B1`1)`1 = (B2`1)`1 by QC_LANG2:5;
hence thesis by A4,A9,A10,A6,A12,A7,A11,Def23;
end;
end;
registration
let A;
let S;
cluster Sub_not S -> Sub_negative;
coherence;
end;
theorem Th13:
S1`2 = S2`2 implies Sub_&(S1,S2) is Sub_conjunctive;
theorem Th14:
B is quantifiable implies Sub_All(B,SQ) is Sub_universal;
theorem
Sub_not(S) = Sub_not(S9) implies S = S9
proof
assume Sub_not(S) = Sub_not(S9);
then
A1: 'not' S`1 = 'not' (S9)`1 & S`2 = (S9)`2 by XTUPLE_0:1;
S = [S`1,S`2] & S9 = [(S9)`1,(S9)`2] by Th10;
hence thesis by A1,FINSEQ_1:33;
end;
theorem
Sub_the_argument_of(Sub_not(S)) = S by Def30;
theorem
S1`2 = S2`2 & (S19)`2 = (S29)`2 & Sub_&(S1,S2) = Sub_&(S19,S29)
implies S1 = S19 & S2 = S29
proof
assume that
A1: S1`2 = S2`2 and
A2: (S19)`2 = (S29)`2 and
A3: Sub_&(S1,S2) = Sub_&(S19,S29);
Sub_&(S1,S2) = [(S1`1) '&' (S2`1),S1`2] by A1,Def21;
then
[(S1`1) '&' (S2`1),S1`2] = [((S19)`1) '&' ((S29)`1),(S19)`2] by A2,A3,Def21;
then
A4: (S1`1) '&' (S2`1) = ((S19)`1) '&' ((S29)`1) & S1`2 = (S19)`2 by XTUPLE_0:1;
A5: S2 = [S2`1,S2`2] & S29 = [(S29)`1,(S29)`2] by Th10;
S1 = [S1`1,S1`2] & S19 = [(S19)`1,(S19)`2] by Th10;
hence thesis by A1,A2,A4,A5,QC_LANG2:2;
end;
theorem Th18:
S1`2 = S2`2 implies Sub_the_left_argument_of(Sub_&(S1,S2)) = S1
proof
assume
A1: S1`2 = S2`2;
then Sub_&(S1,S2) is Sub_conjunctive;
hence thesis by A1,Def31;
end;
theorem Th19:
S1`2 = S2`2 implies Sub_the_right_argument_of(Sub_&(S1,S2)) = S2
proof
assume
A1: S1`2 = S2`2;
then Sub_&(S1,S2) is Sub_conjunctive;
hence thesis by A1,Def32;
end;
theorem
for B1,B2 being Element of [:QC-Sub-WFF(A),bound_QC-variables(A):], SQ1
being second_Q_comp of B1, SQ2 being second_Q_comp of B2 st B1 is quantifiable
& B2 is quantifiable & Sub_All(B1,SQ1) = Sub_All(B2,SQ2) holds B1 = B2
proof
let B1,B2 be Element of [:QC-Sub-WFF(A),bound_QC-variables(A):], SQ1 being
second_Q_comp of B1, SQ2 being second_Q_comp of B2 such that
A1: B1 is quantifiable and
A2: B2 is quantifiable and
A3: Sub_All(B1,SQ1) = Sub_All(B2,SQ2);
A4: Sub_All(B1,SQ1) = [All(B1`2,(B1`1)`1),SQ1] & Sub_All(B2,SQ2) = [All(B2`2
,(B2 `1)`1),SQ2] by A1,A2,Def24;
then All(B1`2,(B1`1)`1) = All(B2`2,(B2`1)`1) by A3,XTUPLE_0:1;
then
A5: B1`2 = B2`2 & (B1`1)`1 = (B2`1)`1 by QC_LANG2:5;
ex a,b being object
st a in QC-Sub-WFF(A) & b in bound_QC-variables(A) & B2 = [a,b] by
ZFMISC_1:def 2;
then
A6: B2 = [B2`1,B2`2];
ex a,b being object
st a in QC-Sub-WFF(A) & b in bound_QC-variables(A) & B1 = [a,b] by
ZFMISC_1:def 2;
then
A7: B1 = [B1`1,B1`2];
A8: B1`1 = [(B1`1)`1,(B1`1)`2] & B2`1 = [(B2`1)`1,(B2`1)`2] by Th10;
(B1`1)`2 = (QSub(A)).[All(B1`2,(B1`1)`1),SQ1] by A1,Def23;
hence thesis by A2,A3,A4,A5,A8,A7,A6,Def23;
end;
theorem Th21:
B is quantifiable implies Sub_the_scope_of(Sub_All(B,SQ)) = B`1
proof
assume
A1: B is quantifiable;
then Sub_All(B,SQ) is Sub_universal;
hence thesis by A1,Def34;
end;
scheme
SubQCInd2 {Al() -> QC-alphabet, Pro[Element of QC-Sub-WFF(Al())]}:
for S being Element of QC-Sub-WFF(Al())
holds Pro[S]
provided
A1: for S being Element of QC-Sub-WFF(Al()) holds (S is Sub_atomic implies Pro
[S]) & (S is Al()-Sub_VERUM implies Pro[S]) & (S is Sub_negative & Pro[
Sub_the_argument_of S] implies Pro[S]) & (S is Sub_conjunctive & Pro[
Sub_the_left_argument_of S] & Pro[Sub_the_right_argument_of S] implies Pro[S])
& (S is Sub_universal & Pro[Sub_the_scope_of S] implies Pro[S])
proof
A2: now
let x be bound_QC-variable of Al(), S be Element of QC-Sub-WFF(Al()),
SQ being second_Q_comp of [S,x] such that
A3: [S,x] is quantifiable and
A4: Pro[S];
[S,x]`1 = Sub_the_scope_of(Sub_All([S,x], SQ)) by A3,Th21;
then
A5: S = Sub_the_scope_of(Sub_All([S,x], SQ));
Sub_All([S,x],SQ) is Sub_universal by A3;
hence Pro[Sub_All([S,x], SQ)] by A1,A4,A5;
end;
A6: now
let S1, S2 be Element of QC-Sub-WFF(Al()) such that
A7: S1`2 = S2`2 and
A8: ( Pro[S1])& Pro[S2];
A9: S2 = Sub_the_right_argument_of (Sub_&(S1,S2)) by A7,Th19;
Sub_&(S1,S2) is Sub_conjunctive & S1 = Sub_the_left_argument_of (
Sub_&(S1,S2 )) by A7,Th18;
hence Pro[Sub_&(S1,S2)] by A1,A8,A9;
end;
A10: now
let S be Element of QC-Sub-WFF(Al()) such that
A11: Pro[S];
S = Sub_the_argument_of(Sub_not(S)) by Def30;
hence Pro[Sub_not(S)] by A1,A11;
end;
A12: for S be Element of QC-Sub-WFF(Al())
st S is Al()-Sub_VERUM holds Pro[S] by A1;
A13: for k be Nat, P be (QC-pred_symbol of k,Al()), ll be
QC-variable_list of k,Al(), e be Element of vSUB(Al()) holds
Pro[Sub_P(P,ll,e)] by A1;
thus thesis from SubQCInd (A13, A12, A10, A6, A2);
end;
theorem Th22:
S is Sub_negative implies len @((Sub_the_argument_of(S))`1) < len @(S`1)
proof
assume S is Sub_negative;
then consider S9 such that
A1: S = Sub_not S9;
A2: 'not' (S9)`1 is negative;
S`1 = 'not' (S9)`1 by A1;
then
A3: len @the_argument_of ('not' (S9)`1) < len @(S`1) by A2,QC_LANG1:14;
(Sub_the_argument_of(S))`1 = (S9)`1 by A1,Def30;
hence thesis by A3,QC_LANG2:1;
end;
theorem Th23:
S is Sub_conjunctive implies len @((Sub_the_left_argument_of(S))
`1) < len @(S`1) & len @((Sub_the_right_argument_of(S))`1) < len @(S`1)
proof
assume S is Sub_conjunctive;
then consider S1,S2 such that
A1: S = Sub_&(S1,S2) & S1`2 = S2`2;
S = [(S1`1) '&' (S2`1),S1`2] by A1,Def21;
then
A2: S`1 = (S1`1) '&' (S2`1);
(S1`1) '&' (S2`1) is conjunctive;
then
A3: len @the_left_argument_of (S1`1) '&' (S2`1) < len @(S`1) & len @
the_right_argument_of (S1`1) '&' (S2`1) < len @(S`1) by A2,QC_LANG1:15;
(Sub_the_right_argument_of(S))`1 = S2`1 & (Sub_the_left_argument_of(S))
`1 = S1`1 by A1,Th18,Th19;
hence thesis by A3,QC_LANG2:4;
end;
theorem Th24:
S is Sub_universal implies len@((Sub_the_scope_of(S))`1) < len @ (S`1)
proof
assume S is Sub_universal;
then consider B,SQ such that
A1: S = Sub_All(B,SQ) & B is quantifiable;
S = [All(B`2,(B`1)`1),SQ] by A1,Def24;
then
A2: S`1 = All(B`2,(B`1)`1);
All(B`2,(B`1)`1) is universal;
then
A3: len @the_scope_of All(B`2,(B`1)`1) < len @(S`1) by A2,QC_LANG1:16;
(Sub_the_scope_of(S))`1 = (B`1)`1 by A1,Th21;
hence thesis by A3,QC_LANG2:7;
end;
theorem Th25:
(S is A-Sub_VERUM implies ((@S`1).1)`1 = 0) & (S is Sub_atomic
implies ex k being Nat st (@S`1).1 is QC-pred_symbol of k,A)
& (S is
Sub_negative implies ((@S`1).1)`1 = 1) & (S is Sub_conjunctive implies ((@S`1).
1)`1 = 2) & (S is Sub_universal implies ((@S`1).1)`1 = 3)
proof
thus S is A-Sub_VERUM implies ((@S`1).1)`1 = 0;
thus S is Sub_atomic implies ex k being Nat st (@S`1).1 is
QC-pred_symbol of k,A
proof
assume S is Sub_atomic;
then consider
k being Nat, P being QC-pred_symbol of k,A, ll being
QC-variable_list of k,A, e being Element of vSUB(A) such that
A1: S = Sub_P(P,ll,e);
S = [P!ll,e] by A1,Th9;
then S`1 = P!ll;
then @S`1 = <*P*>^ll by QC_LANG1:8;
then (@S`1).1 = P by FINSEQ_1:41;
hence thesis;
end;
thus S is Sub_negative implies ((@S`1).1)`1 = 1
proof
assume S is Sub_negative;
then consider S9 such that
A2: S = Sub_not S9;
S`1 = 'not' (S9)`1 by A2;
then @(S`1).1 = [1,0] by FINSEQ_1:41;
hence thesis;
end;
thus S is Sub_conjunctive implies ((@S`1).1)`1 = 2
proof
assume S is Sub_conjunctive;
then consider S1,S2 such that
A3: S = Sub_&(S1,S2) & S1`2 = S2`2;
S = [(S1`1) '&' (S2`1),S1`2] by A3,Def21;
then S`1 = (S1`1) '&' (S2`1);
then @S`1 = <*[2,0]*>^(@S1`1^@S2`1) by FINSEQ_1:32;
then @(S`1).1 = [2,0] by FINSEQ_1:41;
hence thesis;
end;
thus S is Sub_universal implies ((@S`1).1)`1 = 3
proof
assume S is Sub_universal;
then consider B,SQ such that
A4: S = Sub_All(B,SQ) & B is quantifiable;
S = [All(B`2,(B`1)`1),SQ] by A4,Def24;
then S`1 = All(B`2,(B`1)`1);
then @S`1 = <*[3,0]*>^(<*B`2*>^@(B`1)`1) by FINSEQ_1:32;
then (@S`1).1 = [3,0] by FINSEQ_1:41;
hence thesis;
end;
end;
theorem Th26:
S is Sub_atomic implies ((@S`1).1)`1 <> 0 & ((@S`1).1)`1 <> 1 &
((@S`1).1)`1 <> 2 & ((@S`1).1)`1 <> 3
proof
assume S is Sub_atomic;
then ex k being Nat st (@S`1).1 is QC-pred_symbol of k,A by Th25;
hence thesis by QC_LANG1:17;
end;
theorem Th27:
not (ex S st S is Sub_atomic Sub_negative or S is Sub_atomic
Sub_conjunctive or S is Sub_atomic Sub_universal or S is Sub_negative
Sub_conjunctive or S is Sub_negative Sub_universal or S is Sub_conjunctive
Sub_universal or S is A-Sub_VERUM Sub_atomic or S is A-Sub_VERUM
Sub_negative or S
is A-Sub_VERUM Sub_conjunctive or S is A-Sub_VERUM Sub_universal )
proof
let S;
A1: S is Sub_negative implies ((@S`1).1)`1 = 1 by Th25;
A2: S is Sub_conjunctive implies ((@S`1).1)`1 = 2 by Th25;
A3: S is Sub_universal implies ((@S`1).1)`1 = 3 by Th25;
S is A-Sub_VERUM implies ((@S`1).1)`1 = 0;
hence thesis by A1,A2,A3,Th26;
end;
scheme
SubFuncEx { Al() -> QC-alphabet, D()-> non empty set,
V() -> (Element of D()), A(Element of QC-Sub-WFF(Al())) -> (Element of D()),
N(Element of D()) -> (Element of D()),
C((Element of D()),(Element of D())) -> (Element of D()),
R(set,Element of QC-Sub-WFF(Al()), Element of D()) -> Element of D()} :
ex F being Function of QC-Sub-WFF(Al()), D()
st for S being Element of QC-Sub-WFF(Al())
for d1,d2 being Element of D() holds (S is Al()-Sub_VERUM implies F.S = V()) &
(S is Sub_atomic implies F.S = A(S)) & (S is Sub_negative &
d1 = F.Sub_the_argument_of S implies F.S = N(d1)) & (S is Sub_conjunctive &
d1 = F.Sub_the_left_argument_of S & d2 = F.Sub_the_right_argument_of S
implies F.S = C(d1, d2)) & (S is Sub_universal & d1 = F.Sub_the_scope_of S
implies F.S = R(Al(),S,d1))
proof
defpred Pfn[(Function of QC-Sub-WFF(Al()),D()), Nat]
means for S being Element of QC-Sub-WFF(Al()) st len @(S`1) <= $2
holds (S is Al()-Sub_VERUM implies $1.S =
V()) & (S is Sub_atomic implies $1.S = A(S)) & (S is Sub_negative implies $1.S
= N($1.Sub_the_argument_of S)) & (S is Sub_conjunctive implies $1.S = C($1.
Sub_the_left_argument_of S, $1.Sub_the_right_argument_of S)) & (S is
Sub_universal implies $1.S = R(Al(),S,$1.Sub_the_scope_of S));
defpred Pfgp[(Element of D()), (Function of QC-Sub-WFF(Al()),D()), Element of
QC-Sub-WFF(Al())] means ($3 is Al()-Sub_VERUM implies $1 = V()) &
($3 is Sub_atomic implies $1 = A($3)) & ($3 is Sub_negative implies $1
= N($2.Sub_the_argument_of
$3)) & ($3 is Sub_conjunctive implies $1 = C($2.Sub_the_left_argument_of $3, $2
.Sub_the_right_argument_of $3)) & ($3 is Sub_universal
implies $1 = R(Al(),$3,$2.Sub_the_scope_of $3));
defpred S[Nat] means
ex F being Function of QC-Sub-WFF(Al()), D() st Pfn[F, $1];
defpred Qfn[object,object] means ex S being Element of QC-Sub-WFF(Al())
st S = $1 & for
g being Function of QC-Sub-WFF(Al()),D() st
Pfn[g, (len @(S`1)) qua Nat]
holds $2 = g.S;
A1: for n be Nat st S[n] holds S[n+1]
proof
let n be Nat;
given F being Function of QC-Sub-WFF(Al()), D() such that
A2: Pfn[F, n];
defpred R[Element of QC-Sub-WFF(Al()),Element of D()]
means (len @($1`1) <> n+1
implies $2 = F.$1) & (len @($1`1) = n+1 implies Pfgp[$2,F,$1]);
A3: for S be Element of QC-Sub-WFF(Al()) ex y being Element of D() st R[S,y]
proof
let S be Element of QC-Sub-WFF(Al());
now
per cases by Th12;
case
len @(S`1) <> n+1;
take y = F.S;
thus y = F.S;
end;
case
A4: len @(S`1) = n+1 & S is Al()-Sub_VERUM;
take y = V();
thus Pfgp[y, F, S] by A4,Th27;
end;
case
A5: len @(S`1) = n+1 & S is Sub_atomic;
take y = A(S);
thus Pfgp[y, F, S] by A5,Th27;
end;
case
A6: len @(S`1) = n+1 & S is Sub_negative;
take y = N(F.Sub_the_argument_of S);
thus Pfgp[y, F, S] by A6,Th27;
end;
case
A7: len @(S`1) = n+1 & S is Sub_conjunctive;
take y = C(F.Sub_the_left_argument_of S, F.Sub_the_right_argument_of
S);
thus Pfgp[y, F, S] by A7,Th27;
end;
case
A8: len @(S`1) = n+1 & S is Sub_universal;
take y = R(Al(),S,F.Sub_the_scope_of S);
thus Pfgp[y, F, S] by A8,Th27;
end;
end;
hence thesis;
end;
consider G being Function of QC-Sub-WFF(Al()), D() such that
A9: for S being Element of QC-Sub-WFF(Al()) holds R[S,G.S] from FUNCT_2:sch
3(A3 );
take H = G;
thus Pfn[H, n+1]
proof
let S be Element of QC-Sub-WFF(Al()) such that
A10: len @(S`1) <= n+1;
thus S is Al()-Sub_VERUM implies H.S = V()
proof
now
per cases;
suppose
len @(S`1) <> n+1;
then len @(S`1) <= n & H.S = F.S by A9,A10,NAT_1:8;
hence thesis by A2;
end;
suppose
len @(S`1) = n+1;
hence thesis by A9;
end;
end;
hence thesis;
end;
thus S is Sub_atomic implies H.S = A(S)
proof
now
per cases;
suppose
len @(S`1) <> n+1;
then len @(S`1) <= n & H.S = F.S by A9,A10,NAT_1:8;
hence thesis by A2;
end;
suppose
len @(S`1) = n+1;
hence thesis by A9;
end;
end;
hence thesis;
end;
thus S is Sub_negative implies H.S = N(H.Sub_the_argument_of S)
proof
assume
A11: S is Sub_negative;
then len @((Sub_the_argument_of S)`1) <> n+1 by A10,Th22;
then
A12: H.Sub_the_argument_of S = F.Sub_the_argument_of S by A9;
now
per cases;
suppose
len @(S`1) <> n+1;
then len @(S`1) <= n & H.S = F.S by A9,A10,NAT_1:8;
hence thesis by A2,A11,A12;
end;
suppose
len @(S`1) = n+1;
hence thesis by A9,A11,A12;
end;
end;
hence thesis;
end;
thus S is Sub_conjunctive implies H.S = C(H.Sub_the_left_argument_of S,H
.Sub_the_right_argument_of S)
proof
assume
A13: S is Sub_conjunctive;
then len @((Sub_the_right_argument_of S)`1) <> n+1 by A10,Th23;
then
A14: H.Sub_the_right_argument_of S = F. Sub_the_right_argument_of S by A9;
len @((Sub_the_left_argument_of S)`1) <> n+1 by A10,A13,Th23;
then
A15: H.Sub_the_left_argument_of S = F.Sub_the_left_argument_of S by A9;
now
per cases;
suppose
len @(S`1) <> n+1;
then len @(S`1) <= n & H.S = F.S by A9,A10,NAT_1:8;
hence thesis by A2,A13,A15,A14;
end;
suppose
len @(S`1) = n+1;
hence thesis by A9,A13,A15,A14;
end;
end;
hence thesis;
end;
thus S is Sub_universal implies H.S = R(Al(),S,H.Sub_the_scope_of S)
proof
assume
A16: S is Sub_universal;
then len @((Sub_the_scope_of S)`1) <> n+1 by A10,Th24;
then
A17: H.Sub_the_scope_of S = F.Sub_the_scope_of S by A9;
now
per cases;
suppose
len @(S`1) <> n+1;
then len @(S`1) <= n & H.S = F.S by A9,A10,NAT_1:8;
hence thesis by A2,A16,A17;
end;
suppose
len @(S`1) = n+1;
hence thesis by A9,A16,A17;
end;
end;
hence thesis;
end;
end;
end;
A18: S[0]
proof
set F =the Function of QC-Sub-WFF(Al()), D();
take F;
let S be Element of QC-Sub-WFF(Al());
assume len @(S`1) <= 0;
hence thesis by QC_LANG1:10;
end;
A19: for n being Nat holds S[n] from NAT_1:sch 2(A18, A1);
A20: for x being object st x in QC-Sub-WFF(Al())
ex y being object st Qfn[x, y]
proof
let x be object;
assume x in QC-Sub-WFF(Al());
then reconsider x9 = x as Element of QC-Sub-WFF(Al());
consider F being Function of QC-Sub-WFF(Al()), D() such that
A21: Pfn[F, len @((x9)`1) qua Nat] by A19;
take F.x, x9;
thus x9 = x;
let G be Function of QC-Sub-WFF(Al()), D() such that
A22: Pfn[G, len @((x9)`1)qua Nat];
defpred Pro[Element of QC-Sub-WFF(Al())] means
len @(($1)`1) <= len@((x9)`1) implies F.$1 = G.$1;
A23: now
let S be Element of QC-Sub-WFF(Al());
thus S is Sub_atomic implies Pro[S]
proof
assume
A24: S is Sub_atomic & len @(S`1) <= len@((x9)`1);
hence F.S = A(S) by A21
.= G.S by A22,A24;
end;
thus S is Al()-Sub_VERUM implies Pro[S]
proof
assume
A25: S is Al()-Sub_VERUM & len @(S`1) <= len @((x9)`1);
hence F.S = V() by A21
.= G.S by A22,A25;
end;
thus S is Sub_negative & Pro[Sub_the_argument_of S] implies Pro[S]
proof
assume that
A26: S is Sub_negative and
A27: Pro[Sub_the_argument_of S] and
A28: len @(S`1) <= len @((x9)`1);
len @((Sub_the_argument_of S)`1) < len @(S`1) by A26,Th22;
hence F.S = N(G.Sub_the_argument_of S) by A21,A26,A27,A28,XXREAL_0:2
.= G.S by A22,A26,A28;
end;
thus S is Sub_conjunctive & Pro[Sub_the_left_argument_of S] & Pro[
Sub_the_right_argument_of S] implies Pro[S]
proof
assume that
A29: S is Sub_conjunctive and
A30: ( Pro[Sub_the_left_argument_of S])& Pro[
Sub_the_right_argument_of S] and
A31: len @(S`1) <= len @((x9)`1);
len @((Sub_the_left_argument_of S)`1) < len @(S`1) & len @((
Sub_the_right_argument_of S)`1) < len @(S`1) by A29,Th23;
hence
F.S = C(G.Sub_the_left_argument_of S, G.Sub_the_right_argument_of
S) by A21,A29,A30,A31,XXREAL_0:2
.= G.S by A22,A29,A31;
end;
thus S is Sub_universal & Pro[Sub_the_scope_of S] implies Pro[S]
proof
assume that
A32: S is Sub_universal and
A33: Pro[Sub_the_scope_of S] and
A34: len @(S`1) <= len @((x9)`1);
len @((Sub_the_scope_of S)`1) < len @(S`1) by A32,Th24;
hence F.S = R(Al(),S,G.Sub_the_scope_of S)
by A21,A32,A33,A34,XXREAL_0:2
.= G.S by A22,A32,A34;
end;
end;
for S being Element of QC-Sub-WFF(Al()) holds Pro[S] from SubQCInd2 (A23);
hence thesis;
end;
consider F being Function such that
A35: dom F = QC-Sub-WFF(Al()) and
A36: for x being object st x in QC-Sub-WFF(Al()) holds Qfn[x, F.x]
from CLASSES1:
sch 1(A20);
rng F c= D()
proof
let y be object;
assume y in rng F;
then consider x being object such that
A37: x in QC-Sub-WFF(Al()) & y = F.x by A35,FUNCT_1:def 3;
consider S being Element of QC-Sub-WFF(Al()) such that
S = x and
A38: for g being Function of QC-Sub-WFF(Al()), D() st Pfn[g, len @(S`1)qua
Nat] holds y = g.S by A36,A37;
consider G being Function of QC-Sub-WFF(Al()), D() such that
A39: Pfn[G, len @(S`1)qua Nat] by A19;
y = G.S by A38,A39;
hence thesis;
end;
then reconsider F as Function of QC-Sub-WFF(Al()), D() by A35,FUNCT_2:def 1
,RELSET_1:4;
take F;
let S be Element of QC-Sub-WFF(Al());
consider S1 being Element of QC-Sub-WFF(Al()) such that
A40: S1 = S and
A41: for g being Function of QC-Sub-WFF(Al()),D() st Pfn[g, len@(S1`1)qua
Nat] holds F.S = g.S1 by A36;
let d1,d2 be Element of D();
consider G being Function of QC-Sub-WFF(Al()), D() such that
A42: Pfn[G, len @(S1`1)qua Nat] by A19;
set S9 = Sub_the_scope_of S;
A43: ex S1 being Element of QC-Sub-WFF(Al())
st S1 = S9 & for g being Function of
QC-Sub-WFF(Al()), D() st Pfn[g, len @(S1`1) qua Nat] holds
F.S9 = g.S1 by A36;
A44: F.S = G.S by A40,A41,A42;
hence S is Al()-Sub_VERUM implies F.S = V() by A40,A42;
thus S is Sub_atomic implies F.S = A(S) by A40,A42,A44;
A45: for k being Nat st k < len @(S`1) holds Pfn[G, k]
proof
let k be Nat;
assume
A46: k < len @(S`1);
let S9 be Element of QC-Sub-WFF(Al());
assume len @((S9)`1) <= k;
then len @((S9)`1) <= len@(S`1) by A46,XXREAL_0:2;
hence thesis by A40,A42;
end;
thus S is Sub_negative & d1 = F.Sub_the_argument_of S implies F.S = N(d1)
proof
set S9 = Sub_the_argument_of S;
set k = len @((S9)`1);
A47: ex S1 being Element of QC-Sub-WFF(Al()) st S1 = S9 & for g being Function
of QC-Sub-WFF(Al()), D() st Pfn[g, len @(S1`1)qua Nat]
holds F.S9 = g.S1 by A36;
assume
A48: S is Sub_negative;
then k < len @(S`1) by Th22;
then Pfn[G, k qua Nat] by A45;
then F.S9 = G.S9 by A47;
hence thesis by A40,A42,A44,A48;
end;
thus S is Sub_conjunctive & d1 = F.Sub_the_left_argument_of S & d2 = F.
Sub_the_right_argument_of S implies F.S = C(d1, d2)
proof
set S99 = Sub_the_right_argument_of S;
set S9 = Sub_the_left_argument_of S;
set k9 = len @((S9)`1);
set k99 = len @((S99)`1);
A49: ex S2 being Element of QC-Sub-WFF(Al()) st S2 = S99 & for g being Function
of QC-Sub-WFF(Al()), D() st Pfn[g, len @(S2`1) qua Nat]
holds F.S99 = g.S2 by A36;
assume
A50: S is Sub_conjunctive;
then k9 < len @(S`1) by Th23;
then
A51: Pfn[G, k9 qua Nat] by A45;
k99 < len @(S`1) by A50,Th23;
then Pfn[G, k99 qua Nat] by A45;
then
A52: F.S99 = G.S99 by A49;
ex S1 being Element of QC-Sub-WFF(Al()) st S1 = S9 & for g being Function
of QC-Sub-WFF(Al()),D() st Pfn[g, len @(S1`1) qua Nat]
holds F.S9 = g.S1 by A36;
then F.S9 = G.S9 by A51;
hence thesis by A40,A42,A44,A50,A52;
end;
set k = len @((S9)`1);
assume
A53: S is Sub_universal;
then k < len @(S`1) by Th24;
then Pfn[G, k qua Nat] by A45;
then F.S9 = G.S9 by A43;
hence thesis by A40,A42,A44,A53;
end;
scheme
SubQCFuncUniq { Al() -> QC-alphabet, D() -> non empty set,
F1() -> (Function of QC-Sub-WFF(Al()), D()),
F2() -> (Function of QC-Sub-WFF(Al()), D()), V() -> (Element of D()),
A(set) -> (Element of D()), N(set) -> (Element of D()),
C(set,set) -> (Element of D()), R(set,set,set) -> Element of D()}
:
F1() = F2()
provided
A1: for S being Element of QC-Sub-WFF(Al()) for d1,d2 being Element of D()
holds (S is Al()-Sub_VERUM implies F1().S = V()) &
(S is Sub_atomic implies F1().S =
A(S)) & (S is Sub_negative & d1 = F1().Sub_the_argument_of S implies F1().S = N
(d1)) & (S is Sub_conjunctive & d1 = F1().Sub_the_left_argument_of S & d2 = F1(
).Sub_the_right_argument_of S implies F1().S = C(d1, d2)) & (S is Sub_universal
& d1 = F1().Sub_the_scope_of S implies F1().S = R(Al(),S, d1)) and
A2: for S being Element of QC-Sub-WFF(Al()) for d1,d2 being Element of D()
holds (S is Al()-Sub_VERUM implies F2().S = V()) &
(S is Sub_atomic implies F2().S =
A(S)) & (S is Sub_negative & d1 = F2().Sub_the_argument_of S implies F2().S = N
(d1)) & (S is Sub_conjunctive & d1 = F2().Sub_the_left_argument_of S & d2 = F2(
).Sub_the_right_argument_of S implies F2().S = C(d1, d2)) & (S is Sub_universal
& d1 = F2().Sub_the_scope_of S implies F2().S = R(Al(),S, d1))
proof
defpred Pro[Element of QC-Sub-WFF(Al())] means F1().$1 = F2().$1;
A3: for k for P being (QC-pred_symbol of k,Al()),
l being QC-variable_list of k,Al(), e
being Element of vSUB(Al()) holds Pro[Sub_P(P,l,e)]
proof
let k;
let P be (QC-pred_symbol of k,Al()),l be QC-variable_list of k,Al();
let e be Element of vSUB(Al());
thus F1().Sub_P(P,l,e) = A(Sub_P(P,l,e)) by A1
.= F2().Sub_P(P,l,e) by A2;
end;
A4: for x being bound_QC-variable of Al(), S being Element of QC-Sub-WFF(Al()),
SQ being second_Q_comp of [S,x] st [S,x] is quantifiable &
Pro[S] holds Pro[Sub_All([S,x], SQ)]
proof
let x be bound_QC-variable of Al(), S be Element of QC-Sub-WFF(Al()),
SQ being second_Q_comp of [S,x] such that
A5: [S,x] is quantifiable and
A6: F1().S = F2().S;
A7: Sub_All([S,x],SQ) is Sub_universal by A5;
Sub_the_scope_of Sub_All([S,x],SQ) = [S,x]`1 by A5,Th21;
then Sub_the_scope_of Sub_All([S,x],SQ) = S;
hence F1().Sub_All([S,x],SQ) = R(Al(),Sub_All([S,x],SQ),
F2().Sub_the_scope_of Sub_All([S,x],SQ)) by A1,A6,A7
.= F2().Sub_All([S,x],SQ) by A2,A7;
end;
A8: for S being Element of QC-Sub-WFF(Al()) st S is Al()-Sub_VERUM holds Pro[S]
proof
let S be Element of QC-Sub-WFF(Al());
assume
A9: S is Al()-Sub_VERUM;
then F1().S = V() by A1;
hence thesis by A2,A9;
end;
A10: for S1,S2 being Element of QC-Sub-WFF(Al())
st S1`2 = S2`2 & Pro[S1] & Pro[S2] holds Pro[Sub_&(S1,S2)]
proof
let S1,S2 be Element of QC-Sub-WFF(Al()) such that
A11: S1`2 = S2`2 and
A12: F1().S1 = F2().S1 & F1().S2 = F2().S2;
A13: Sub_the_right_argument_of (Sub_&(S1,S2)) = S2 by A11,Th19;
A14: Sub_&(S1,S2) is Sub_conjunctive & Sub_the_left_argument_of (Sub_&(S1,
S2)) = S1 by A11,Th18;
hence F1().Sub_&(S1,S2) = C(F2().S1,F2().S2) by A1,A12,A13
.= F2().(Sub_&(S1,S2)) by A2,A14,A13;
end;
A15: for S being Element of QC-Sub-WFF(Al()) st Pro[S] holds Pro[Sub_not(S)]
proof
let S be Element of QC-Sub-WFF(Al()) such that
A16: F1().S = F2().S;
A17: Sub_the_argument_of Sub_not(S) = S by Def30;
hence F1().Sub_not(S) = N(F2().S) by A1,A16
.= F2().Sub_not(S) by A2,A17;
end;
for S being Element of QC-Sub-WFF(Al()) holds
Pro[S] from SubQCInd(A3,A8,A15,A10,A4);
hence thesis by FUNCT_2:63;
end;
definition
let A;
let S;
func @S -> Element of [:QC-WFF(A),vSUB(A):] equals
S;
coherence
proof
ex p,e st S = [p,e] by Th8;
hence thesis;
end;
end;
reserve Z for Element of [:QC-WFF(A),vSUB(A):];
definition
let A;
let Z;
redefine func Z`1 -> Element of QC-WFF(A); :: redefines `1 (XTUPLE_0, definition)
coherence
proof
ex a,b being object st a in QC-WFF(A) & b in vSUB(A) & [a,b] = Z
by ZFMISC_1:def 2;
hence thesis;
end;
redefine func Z`2 -> CQC_Substitution of A; :: redefines `2 (XTUPLE_0, definition)
coherence
proof
ex a,b being object st a in QC-WFF(A) & b in vSUB(A) & [a,b] = Z
by ZFMISC_1:def 2;
hence thesis;
end;
end;
definition
let A;
let Z;
func S_Bound(Z) -> bound_QC-variable of A equals
x.upVar(RestrictSub(bound_in Z`1
,Z`1,Z`2),(the_scope_of Z`1)) if bound_in(Z`1) in rng(RestrictSub(bound_in Z`1,
Z`1,Z`2)) otherwise bound_in(Z`1);
coherence;
consistency;
end;
definition
let A;
let S, p;
func Quant(S,p) -> Element of QC-WFF(A) equals
All(S_Bound(@S),p);
coherence;
end;
Lm6: for F1,F2 being Function of QC-Sub-WFF(A),QC-WFF(A) st
( for S being Element of
QC-Sub-WFF(A) holds (S is A-Sub_VERUM implies F1.S = VERUM(A))
& (S is Sub_atomic implies F1.S =
(the_pred_symbol_of (S`1))! CQC_Subst(Sub_the_arguments_of S,S`2
)) & (S is Sub_negative implies F1.S = 'not' (F1.Sub_the_argument_of S) ) & (S
is Sub_conjunctive implies F1.S = (F1.Sub_the_left_argument_of S) '&' (F1.
Sub_the_right_argument_of S)) & (S is Sub_universal implies F1.S = Quant(S,F1.
Sub_the_scope_of S))) & ( for S being Element of QC-Sub-WFF(A) holds (S is
A-Sub_VERUM implies F2.S = VERUM(A)) & (S is Sub_atomic implies F2.S = (
the_pred_symbol_of (S`1))! CQC_Subst(Sub_the_arguments_of S,S`2)) & (S is
Sub_negative implies F2.S = 'not' (F2.Sub_the_argument_of S) ) & (S is
Sub_conjunctive implies F2.S = (F2.Sub_the_left_argument_of S) '&' (F2.
Sub_the_right_argument_of S)) & (S is Sub_universal implies F2.S = Quant(S,F2.
Sub_the_scope_of S))) holds F1 = F2
proof
let F1,F2 be Function of QC-Sub-WFF(A),QC-WFF(A);
deffunc C(Element of QC-WFF(A),Element of QC-WFF(A)) = $1 '&' $2;
deffunc N(Element of QC-WFF(A)) = 'not' $1;
deffunc A2(Element of QC-Sub-WFF(A)) =
(the_pred_symbol_of ($1`1))! CQC_Subst(
Sub_the_arguments_of $1,$1`2);
assume for S being Element of QC-Sub-WFF(A) holds (S is A-Sub_VERUM
implies F1.S = VERUM(A)) & (S is Sub_atomic implies F1.S = A2(S)) &
(S is Sub_negative implies F1.S = N(F1.Sub_the_argument_of S)) &
(S is Sub_conjunctive implies F1.S = C(F1
.Sub_the_left_argument_of S,F1.Sub_the_right_argument_of S)) & (S is
Sub_universal implies F1.S = Quant(S,F1.Sub_the_scope_of S));
then
A1: for S being Element of QC-Sub-WFF(A) for d1,d2 being Element of QC-WFF(A)
holds (S is A-Sub_VERUM implies F1.S = VERUM(A)) &
(S is Sub_atomic implies F1.S = A2(S)) &
(S is Sub_negative & d1 = F1.Sub_the_argument_of S implies F1.S = N(d1))
& (S is Sub_conjunctive & d1 = F1.(Sub_the_left_argument_of S) & d2 = F1.(
Sub_the_right_argument_of S) implies F1.S = C(d1,d2)) & (S is Sub_universal &
d1 = F1.Sub_the_scope_of S implies F1.S = Quant(S,d1));
assume for S being Element of QC-Sub-WFF(A) holds (S is A-Sub_VERUM
implies F2.S = VERUM(A)) & (S is Sub_atomic implies F2.S = A2(S)) &
(S is Sub_negative implies F2.S = N(F2.Sub_the_argument_of S)) &
(S is Sub_conjunctive implies F2.S = C(F2.Sub_the_left_argument_of S,
F2.Sub_the_right_argument_of S)) & (S is Sub_universal implies
F2.S = Quant(S,F2.Sub_the_scope_of S));
then
A2: for S being Element of QC-Sub-WFF(A) for d1,d2 being Element of QC-WFF(A)
holds (S is A-Sub_VERUM implies F2.S = VERUM(A)) &
(S is Sub_atomic implies F2.S = A2(S)) &
(S is Sub_negative & d1 = F2.Sub_the_argument_of S implies F2.S = N(d1))
& (S is Sub_conjunctive & d1 = F2.(Sub_the_left_argument_of S) & d2 = F2.(
Sub_the_right_argument_of S) implies F2.S = C(d1,d2)) & (S is Sub_universal &
d1 = F2.Sub_the_scope_of S implies F2.S = Quant(S,d1));
thus F1 = F2 from SubQCFuncUniq(A1,A2);
end;
begin :: Definition and Properties of Substitution
:: (Ebb et al, Chapter III, Definition 8.1/8.2)
definition
let A;
let S be Element of QC-Sub-WFF(A);
func CQC_Sub(S) -> Element of QC-WFF(A) means
:Def38:
ex F being Function of
QC-Sub-WFF(A),QC-WFF(A) st it = F.S & for S9 being Element of
QC-Sub-WFF(A) holds (S9 is
A-Sub_VERUM implies F.S9 = VERUM(A)) & ( S9 is Sub_atomic implies F.S9 = (
the_pred_symbol_of ((S9)`1))! CQC_Subst(Sub_the_arguments_of S9,(S9)`2)) & (S9
is Sub_negative implies F.S9 = 'not' (F.(Sub_the_argument_of S9))) & (S9 is
Sub_conjunctive implies F.S9 = (F.Sub_the_left_argument_of S9) '&' (F.
Sub_the_right_argument_of S9)) & (S9 is Sub_universal implies F.S9 = Quant(S9,F
.Sub_the_scope_of S9));
existence
proof
deffunc C(Element of QC-WFF(A),Element of QC-WFF(A)) = $1 '&' $2;
deffunc N(Element of QC-WFF(A)) = 'not' $1;
deffunc A2(Element of QC-Sub-WFF(A)) =
(the_pred_symbol_of ($1`1))! CQC_Subst(
Sub_the_arguments_of $1,$1`2);
consider F being Function of QC-Sub-WFF(A),QC-WFF(A) such that
A1: for S being Element of QC-Sub-WFF(A) for d1,d2 being Element of
QC-WFF(A) holds (S is A-Sub_VERUM implies F.S = VERUM(A)) &
(S is Sub_atomic implies F.
S = A2(S)) & (S is Sub_negative & d1 = F.Sub_the_argument_of S implies F.S = N(
d1)) & (S is Sub_conjunctive & d1 = F.(Sub_the_left_argument_of S) & d2 = F.(
Sub_the_right_argument_of S) implies F.S = C(d1,d2)) & (S is Sub_universal & d1
= F.Sub_the_scope_of S implies F.S = Quant(S,d1)) from SubFuncEx;
take F.S,F;
thus F.S = F.S;
thus thesis by A1;
end;
uniqueness by Lm6;
end;
theorem Th28:
S is Sub_negative implies CQC_Sub(S) = 'not' CQC_Sub( Sub_the_argument_of S)
proof
consider F being Function of QC-Sub-WFF(A),QC-WFF(A) such that
A1: CQC_Sub(S) = F.S and
A2: for S9 being Element of QC-Sub-WFF(A) holds (S9 is A-Sub_VERUM implies F.
S9 = VERUM(A)) & ( S9 is Sub_atomic implies F.S9 =
(the_pred_symbol_of ((S9)`1))!
CQC_Subst(Sub_the_arguments_of S9,(S9)`2)) & (S9 is Sub_negative implies F.S9 =
'not' (F.(Sub_the_argument_of S9))) & (S9 is Sub_conjunctive implies F.S9 = (F.
Sub_the_left_argument_of S9) '&' (F.Sub_the_right_argument_of S9)) & (S9 is
Sub_universal implies F.S9 = Quant(S9,F.Sub_the_scope_of S9)) by Def38;
consider G being Function of QC-Sub-WFF(A),QC-WFF(A) such that
A3: CQC_Sub(Sub_the_argument_of S) = G.(Sub_the_argument_of S) and
A4: for S9 being Element of QC-Sub-WFF(A) holds (S9 is A-Sub_VERUM implies G.
S9 = VERUM(A)) & ( S9 is Sub_atomic implies G.S9 =
(the_pred_symbol_of ((S9)`1))!
CQC_Subst(Sub_the_arguments_of S9,(S9)`2)) & (S9 is Sub_negative implies G.S9 =
'not' (G.(Sub_the_argument_of S9))) & (S9 is Sub_conjunctive implies G.S9 = (G.
Sub_the_left_argument_of S9) '&' (G.Sub_the_right_argument_of S9)) & (S9 is
Sub_universal implies G.S9 = Quant(S9,G.Sub_the_scope_of S9)) by Def38;
F = G by A2,A4,Lm6;
hence thesis by A1,A2,A3;
end;
theorem Th29:
CQC_Sub(Sub_not S) = 'not' CQC_Sub(S)
proof
set 9S = Sub_not S;
Sub_the_argument_of 9S = S by Def30;
hence thesis by Th28;
end;
theorem Th30:
S is Sub_conjunctive implies CQC_Sub(S) = (CQC_Sub(
Sub_the_left_argument_of S)) '&' (CQC_Sub(Sub_the_right_argument_of S))
proof
consider F being Function of QC-Sub-WFF(A),QC-WFF(A) such that
A1: CQC_Sub(S) = F.S and
A2: for S9 being Element of QC-Sub-WFF(A) holds (S9 is A-Sub_VERUM implies F.
S9 = VERUM(A)) & ( S9 is Sub_atomic implies F.S9 =
(the_pred_symbol_of ((S9)`1))!
CQC_Subst(Sub_the_arguments_of S9,(S9)`2)) & (S9 is Sub_negative implies F.S9 =
'not' (F.(Sub_the_argument_of S9))) & (S9 is Sub_conjunctive implies F.S9 = (F.
Sub_the_left_argument_of S9) '&' (F.Sub_the_right_argument_of S9)) & (S9 is
Sub_universal implies F.S9 = Quant(S9,F.Sub_the_scope_of S9)) by Def38;
consider F2 being Function of QC-Sub-WFF(A),QC-WFF(A) such that
A3: CQC_Sub(Sub_the_right_argument_of S) = F2.(Sub_the_right_argument_of S) and
A4: for S9 being Element of QC-Sub-WFF(A) holds (S9 is A-Sub_VERUM implies F2
.S9 = VERUM(A)) & ( S9 is Sub_atomic implies F2.S9 =
(the_pred_symbol_of ((S9)`1))
! CQC_Subst(Sub_the_arguments_of S9,(S9)`2)) & (S9 is Sub_negative implies F2.
S9 = 'not' (F2.(Sub_the_argument_of S9))) & (S9 is Sub_conjunctive implies F2.
S9 = (F2.Sub_the_left_argument_of S9) '&' (F2.Sub_the_right_argument_of S9)) &
(S9 is Sub_universal implies F2.S9 = Quant(S9,F2.Sub_the_scope_of S9)) by Def38
;
A5: F2 = F by A2,A4,Lm6;
consider F1 being Function of QC-Sub-WFF(A),QC-WFF(A) such that
A6: CQC_Sub(Sub_the_left_argument_of S) = F1.(Sub_the_left_argument_of S ) and
A7: for S9 being Element of QC-Sub-WFF(A) holds (S9 is A-Sub_VERUM implies F1
.S9 = VERUM(A)) & ( S9 is Sub_atomic implies F1.S9 =
(the_pred_symbol_of ((S9)`1))
! CQC_Subst(Sub_the_arguments_of S9,(S9)`2)) & (S9 is Sub_negative implies F1.
S9 = 'not' (F1.(Sub_the_argument_of S9))) & (S9 is Sub_conjunctive implies F1.
S9 = (F1.Sub_the_left_argument_of S9) '&' (F1.Sub_the_right_argument_of S9)) &
(S9 is Sub_universal implies F1.S9 = Quant(S9,F1.Sub_the_scope_of S9)) by Def38
;
F1 = F by A2,A7,Lm6;
hence thesis by A1,A2,A6,A3,A5;
end;
theorem Th31:
S1`2 = S2`2 implies CQC_Sub(Sub_&(S1,S2)) = (CQC_Sub(S1)) '&' ( CQC_Sub(S2))
proof
set S = Sub_&(S1,S2);
assume
A1: S1`2 = S2`2;
then Sub_the_left_argument_of S = S1 & Sub_the_right_argument_of S = S2 by
Th18,Th19;
hence thesis by A1,Th13,Th30;
end;
theorem Th32:
S is Sub_universal implies CQC_Sub(S) = Quant(S,CQC_Sub( Sub_the_scope_of S))
proof
consider F being Function of QC-Sub-WFF(A),QC-WFF(A) such that
A1: CQC_Sub(S) = F.S and
A2: for S9 being Element of QC-Sub-WFF(A) holds (S9 is A-Sub_VERUM implies F.
S9 = VERUM(A)) & ( S9 is Sub_atomic implies F.S9 =
(the_pred_symbol_of ((S9)`1))!
CQC_Subst(Sub_the_arguments_of S9,(S9)`2)) & (S9 is Sub_negative implies F.S9 =
'not' (F.(Sub_the_argument_of S9))) & (S9 is Sub_conjunctive implies F.S9 = (F.
Sub_the_left_argument_of S9) '&' (F.Sub_the_right_argument_of S9)) & (S9 is
Sub_universal implies F.S9 = Quant(S9,F.Sub_the_scope_of S9)) by Def38;
consider G being Function of QC-Sub-WFF(A),QC-WFF(A) such that
A3: CQC_Sub(Sub_the_scope_of S) = G.(Sub_the_scope_of S) and
A4: for S9 being Element of QC-Sub-WFF(A) holds (S9 is A-Sub_VERUM implies G.
S9 = VERUM(A)) & ( S9 is Sub_atomic implies G.S9 =
(the_pred_symbol_of ((S9)`1))!
CQC_Subst(Sub_the_arguments_of S9,(S9)`2)) & (S9 is Sub_negative implies G.S9 =
'not' (G.(Sub_the_argument_of S9))) & (S9 is Sub_conjunctive implies G.S9 = (G.
Sub_the_left_argument_of S9) '&' (G.Sub_the_right_argument_of S9)) & (S9 is
Sub_universal implies G.S9 = Quant(S9,G.Sub_the_scope_of S9)) by Def38;
F = G by A2,A4,Lm6;
hence thesis by A1,A2,A3;
end;
definition
let A;
func CQC-Sub-WFF(A) -> Subset of QC-Sub-WFF(A) equals
{S : S`1 is Element of
CQC-WFF(A)};
coherence
proof
set X = {S : S`1 is Element of CQC-WFF(A)};
X c= QC-Sub-WFF(A)
proof
let a be object;
assume a in X;
then ex S st a = S & S`1 is Element of CQC-WFF(A);
hence thesis;
end;
hence thesis;
end;
end;
registration
let A;
cluster CQC-Sub-WFF(A) -> non empty;
coherence
proof
set e =the Element of vSUB(A);
reconsider S = [VERUM(A),e] as Element of QC-Sub-WFF(A) by Def16;
S`1 = VERUM(A);
then [VERUM(A),e] in CQC-Sub-WFF(A);
hence thesis;
end;
end;
theorem Th33:
S is A-Sub_VERUM implies CQC_Sub(S) is Element of CQC-WFF(A)
proof
assume
A1: S is A-Sub_VERUM;
ex F being Function of QC-Sub-WFF(A),QC-WFF(A) st CQC_Sub(S) = F.S & for S9
being Element of QC-Sub-WFF(A) holds (S9 is A-Sub_VERUM implies
F. S9 = VERUM(A)) & (
S9 is Sub_atomic implies F.S9 = (the_pred_symbol_of ((S9)`1))! CQC_Subst(
Sub_the_arguments_of S9,(S9)`2)) & (S9 is Sub_negative implies F.S9 = 'not' (F.
(Sub_the_argument_of S9))) & (S9 is Sub_conjunctive implies F.S9 = (F.
Sub_the_left_argument_of S9) '&' (F.Sub_the_right_argument_of S9)) & (S9 is
Sub_universal implies F.S9 = Quant(S9,F.Sub_the_scope_of S9)) by Def38;
hence thesis by A1;
end;
Lm7: the_pred_symbol_of (P!ll) = P
proof
A1: (<*P*>^ll).1 = P by FINSEQ_1:41;
P!ll is atomic;
then consider
k being Nat, ll9 being QC-variable_list of k,A, P9 being (
QC-pred_symbol of k,A) such that
A2: the_pred_symbol_of (P!ll) = P9 & P!ll = P9!ll9 by QC_LANG1:def 22;
P!ll = <*P*>^ll & P9!ll9 = <*P9*>^ll9 by QC_LANG1:8;
hence thesis by A2,A1,FINSEQ_1:41;
end;
theorem Th34:
for h being FinSequence holds h is CQC-variable_list of k,A iff h
is FinSequence of bound_QC-variables(A) & len h = k
proof
let h be FinSequence;
thus h is CQC-variable_list of k,A implies h is FinSequence of
bound_QC-variables(A) & len h = k
proof
assume
A1: h is CQC-variable_list of k,A;
then rng h c= bound_QC-variables(A) by RELAT_1:def 19;
hence h is FinSequence of bound_QC-variables(A) by FINSEQ_1:def 4;
thus thesis by A1,CARD_1:def 7;
end;
thus h is FinSequence of bound_QC-variables(A) & len h = k implies h is
CQC-variable_list of k,A
proof
assume that
A2: h is FinSequence of bound_QC-variables(A) and
A3: len h = k;
rng h c= bound_QC-variables(A) by A2,FINSEQ_1:def 4;
then rng h c= QC-variables(A) by XBOOLE_1:1;
hence thesis by A2,A3,CARD_1:def 7,FINSEQ_1:def 4;
end;
end;
theorem Th35:
CQC_Sub(Sub_P(P,ll,e)) is Element of CQC-WFF(A)
proof
set l = Sub_the_arguments_of Sub_P(P,ll,e);
A1: l is CQC-variable_list of k,A by Def29;
then reconsider l as FinSequence of bound_QC-variables(A) by Th34;
reconsider s = CQC_Subst(l,Sub_P(P,ll,e)`2) as FinSequence of
bound_QC-variables(A);
len l = k by A1,CARD_1:def 7;
then
A2: len s = k by Def3;
Sub_P(P,ll,e) = [P!ll,e] by Th9;
then Sub_P(P,ll,e)`1 = P!ll;
then reconsider
P9 = the_pred_symbol_of Sub_P(P,ll,e)`1 as QC-pred_symbol of k,A by Lm7;
reconsider s as CQC-variable_list of k,A by A2,Th34;
ex F being Function of QC-Sub-WFF(A),QC-WFF(A)
st CQC_Sub(Sub_P (P,ll,e)) = F.Sub_P(P,ll,e) &
for S9 being Element of QC-Sub-WFF(A)
holds (S9 is A-Sub_VERUM implies F. S9 = VERUM(A)) &
( S9 is Sub_atomic implies F.S9 = ( the_pred_symbol_of
((S9)`1))! CQC_Subst(Sub_the_arguments_of S9,(S9)`2)) & (S9 is Sub_negative
implies F.S9 = 'not' (F.(Sub_the_argument_of S9))) & (S9 is Sub_conjunctive
implies F.S9 = (F. Sub_the_left_argument_of S9) '&' (F.
Sub_the_right_argument_of S9)) & (S9 is Sub_universal implies F.S9 = Quant(S9,F
.Sub_the_scope_of S9)) by Def38;
then CQC_Sub(Sub_P(P,ll,e)) = P9!s;
hence thesis;
end;
theorem Th36:
CQC_Sub(S) is Element of CQC-WFF(A) implies CQC_Sub(Sub_not S) is
Element of CQC-WFF(A)
proof
set S9 = Sub_not S;
assume
A1: CQC_Sub(S) is Element of CQC-WFF(A);
CQC_Sub(S9) = 'not' CQC_Sub(S) by Th29;
hence thesis by A1,CQC_LANG:8;
end;
theorem Th37:
S1`2 = S2`2 & CQC_Sub(S1) is Element of CQC-WFF(A) & CQC_Sub(S2) is
Element of CQC-WFF(A) implies CQC_Sub(Sub_&(S1,S2)) is Element of CQC-WFF(A)
proof
assume
A1: S1`2 = S2`2 & CQC_Sub(S1) is Element of CQC-WFF(A) & CQC_Sub(S2) is
Element of CQC-WFF(A);
S1`2 = S2`2 implies CQC_Sub(Sub_&(S1,S2)) = (CQC_Sub(S1)) '&' (CQC_Sub(
S2)) by Th31;
hence thesis by A1,CQC_LANG:9;
end;
reserve xSQ for second_Q_comp of [S,x];
theorem Th38:
CQC_Sub(S) is Element of CQC-WFF(A) & [S,x] is quantifiable implies
CQC_Sub(Sub_All([S,x],xSQ)) is Element of CQC-WFF(A)
proof
set S9 = Sub_All([S,x],xSQ);
assume that
A1: CQC_Sub(S) is Element of CQC-WFF(A) and
A2: [S,x] is quantifiable;
Sub_the_scope_of S9 = [S,x]`1 by A2,Th21;
then
Quant(S9,CQC_Sub(Sub_the_scope_of S9)) = All(S_Bound(@S9),CQC_Sub(S));
then Quant(S9,CQC_Sub(Sub_the_scope_of S9)) is Element of CQC-WFF(A) by A1,
CQC_LANG:13;
hence thesis by A2,Th14,Th32;
end;
reserve S for Element of CQC-Sub-WFF(A);
scheme
SubCQCInd { Al() -> QC-alphabet, Pro[set] } :
for S being Element of CQC-Sub-WFF(Al()) holds Pro[S]
provided
A1: for S,S9 being Element of CQC-Sub-WFF(Al()),
x being bound_QC-variable of Al(),
SQ being second_Q_comp of [S,x],
k being Nat,
ll being CQC-variable_list of k,Al(),
P being (QC-pred_symbol of k,Al()),
e being Element of vSUB(Al()) holds
Pro[Sub_P(P,ll,e)] &
(S is Al()-Sub_VERUM implies Pro[S]) &
(Pro[S] implies Pro[Sub_not S]) &
(S`2 = (S9)`2 & Pro[S] & Pro[S9] implies Pro[Sub_&(S,S9)]) &
([S,x] is quantifiable
& Pro[S] implies Pro[Sub_All([S,x], SQ)])
proof
defpred Pro1[Element of QC-Sub-WFF(Al())] means
$1 is Element of CQC-Sub-WFF(Al())
implies Pro[$1];
A2: for S being Element of QC-Sub-WFF(Al()) st Pro1[S] holds Pro1[Sub_not S]
proof
let S be Element of QC-Sub-WFF(Al());
assume
A3: Pro1[S];
assume Sub_not S is Element of CQC-Sub-WFF(Al());
then Sub_not S in CQC-Sub-WFF(Al());
then consider S9 being Element of QC-Sub-WFF(Al()) such that
A4: Sub_not S = S9 and
A5: (S9)`1 is Element of CQC-WFF(Al());
(S9)`1 = 'not' S`1 by A4;
then S`1 is Element of CQC-WFF(Al()) by A5,CQC_LANG:8;
then S in CQC-Sub-WFF(Al());
hence thesis by A1,A3;
end;
A6: for k being Nat, P being (QC-pred_symbol of k,Al()), ll being
QC-variable_list of k,Al(), e being Element of vSUB(Al()) holds
Pro1[Sub_P(P,ll,e)]
proof
let k be Nat, P be (QC-pred_symbol of k,Al()), ll be
QC-variable_list of k,Al(), e be Element of vSUB(Al());
assume Sub_P(P,ll,e) is Element of CQC-Sub-WFF(Al());
then Sub_P(P,ll,e) in CQC-Sub-WFF(Al());
then
A7: ex S1 being Element of QC-Sub-WFF(Al()) st Sub_P(P,ll,e) = S1 & S1`1 is
Element of CQC-WFF(Al());
Sub_P(P,ll,e) = [P!ll,e] by Th9;
then
A8: P!ll is Element of CQC-WFF(Al()) by A7;
then
A9: { ll.j : 1 <= j & j <= len ll & ll.j in fixed_QC-variables(Al()) } = {}
by CQC_LANG:7;
{ ll.i : 1 <= i & i <= len ll & ll.i in free_QC-variables(Al()) } = {}
by A8,CQC_LANG:7;
then ll is CQC-variable_list of k,Al() by A9,CQC_LANG:5;
hence thesis by A1;
end;
A10: for S1,S2 being Element of QC-Sub-WFF(Al()) st S1`2 = S2`2 & Pro1[S1] &
Pro1[S2] holds Pro1[Sub_&(S1,S2)]
proof
let S1,S2 be Element of QC-Sub-WFF(Al());
assume that
A11: S1`2 = S2`2 and
A12: ( Pro1[S1])& Pro1[S2];
assume Sub_&(S1,S2) is Element of CQC-Sub-WFF(Al());
then Sub_&(S1,S2) in CQC-Sub-WFF(Al());
then consider S9 being Element of QC-Sub-WFF(Al()) such that
A13: Sub_&(S1,S2) = S9 and
A14: (S9)`1 is Element of CQC-WFF(Al());
Sub_&(S1,S2) = [S1`1 '&' S2`1,S1`2] by A11,Def21;
then
A15: (S9)`1 = S1`1 '&' S2`1 by A13;
then S2`1 is Element of CQC-WFF(Al()) by A14,CQC_LANG:9;
then
A16: S2 in CQC-Sub-WFF(Al());
S1`1 is Element of CQC-WFF(Al()) by A14,A15,CQC_LANG:9;
then S1 in CQC-Sub-WFF(Al());
hence thesis by A1,A11,A12,A16;
end;
A17: for x being bound_QC-variable of Al(),
S being Element of QC-Sub-WFF(Al()),
SQ being second_Q_comp of [S,x]
st [S,x] is quantifiable & Pro1[S] holds Pro1[Sub_All([S,x], SQ)]
proof
let x be bound_QC-variable of Al(), S be Element of QC-Sub-WFF(Al()),
SQ being second_Q_comp of [S,x];
assume that
A18: [S,x] is quantifiable and
A19: Pro1[S];
assume Sub_All([S,x],SQ) is Element of CQC-Sub-WFF(Al());
then Sub_All([S,x],SQ) in CQC-Sub-WFF(Al());
then consider S9 being Element of QC-Sub-WFF(Al()) such that
A20: Sub_All([S,x],SQ) = S9 and
A21: (S9)`1 is Element of CQC-WFF(Al());
Sub_All([S,x],SQ) = [All([S,x]`2,([S,x]`1)`1),SQ] by A18,Def24;
then (S9)`1 = All([S,x]`2,([S,x]`1)`1) by A20;
then ([S,x]`1)`1 is Element of CQC-WFF(Al()) by A21,CQC_LANG:13;
then S in CQC-Sub-WFF(Al());
hence thesis by A1,A18,A19;
end;
A22: for S being Element of QC-Sub-WFF(Al()) st S is Al()-Sub_VERUM holds
Pro1[S] by A1;
for S being Element of QC-Sub-WFF(Al()) holds Pro1[S] from SubQCInd(A6,A22,
A2,A10,A17 );
hence thesis;
end;
definition
let A;
let S;
redefine func CQC_Sub(S) -> Element of CQC-WFF(A); :: redefines CQC_Sub (SUBSTUT1, definition)
coherence
proof
defpred P[Element of QC-Sub-WFF(A)] means CQC_Sub($1)
is Element of CQC-WFF(A);
A1: for S,S9 being Element of CQC-Sub-WFF(A),
x being bound_QC-variable of A,SQ be
second_Q_comp of [S,x], k being Nat,
ll being CQC-variable_list of k,A,
P being (QC-pred_symbol of k,A), e being Element of vSUB(A) holds
P[Sub_P(P,ll,e)] &
(S is A-Sub_VERUM implies P[S]) & (P[S] implies P[Sub_not S]) &
(S`2 = (S9)`2 & P[S] & P[S9] implies P[Sub_&(S,S9)]) &
([S,x] is quantifiable & P[S] implies P[Sub_All([S,x], SQ)])
by Th33,Th35,Th36,Th37,Th38;
for S holds P[S] from SubCQCInd(A1);
hence thesis;
end;
end;
theorem
rng @Sub c= bound_QC-variables(A);