:: Variables in Formulae of the First Order Language
:: by Czes{\l}aw Byli\'nski and Grzegorz Bancerek
::
:: Received November 23, 1989
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies SUBSET_1, NUMBERS, QC_LANG1, FINSEQ_1, XBOOLE_0, FUNCT_1,
ZF_LANG, XXREAL_0, CLASSES2, REALSET1, BVFUNC_2, XBOOLEAN, MARGREL1,
ZF_LANG1, TARSKI, ZFMISC_1, QC_LANG2, RCOMP_1, ZF_MODEL, QC_LANG3, NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, FUNCT_1,
FUNCT_2, FINSEQ_1, QC_LANG1, QC_LANG2, XXREAL_0;
constructors FUNCT_2, XXREAL_0, MEMBERED, QC_LANG2, RELSET_1;
registrations SUBSET_1, ORDINAL1, RELSET_1, QC_LANG1, XXREAL_0;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI, QC_LANG1;
equalities QC_LANG1;
expansions QC_LANG1;
theorems TARSKI, ZFMISC_1, FUNCT_2, QC_LANG1, QC_LANG2, XBOOLE_1, XTUPLE_0,
ORDINAL1;
schemes QC_LANG1;
begin
reserve i,k for Nat;
scheme
QCFuncUniq { Al() -> QC-alphabet, D() -> non empty set,
F1,F2() -> (Function of QC-WFF(Al()), D()),
V() -> (Element of D()),
A,N(set) -> (Element of D()),
C(set,set) -> (Element of D()),
Q(set,set) -> Element of D()}
:
F1() = F2()
provided
A1: for p being Element of QC-WFF(Al()) for d1,d2 being Element of D() holds
(p = VERUM(Al()) implies F1().p = V()) &
(p is atomic implies F1().p = A(p)) & (p is negative &
d1 = F1().the_argument_of p implies F1().p = N(d1)) &
(p is conjunctive & d1 = F1().the_left_argument_of p &
d2 = F1().the_right_argument_of p implies F1().p = C(
d1, d2)) & (p is universal & d1 = F1().the_scope_of p implies
F1().p = Q(p, d1)) and
A2: for p being Element of QC-WFF(Al()) for d1,d2 being Element of D() holds
(p = VERUM(Al()) implies F2().p = V()) & (p is atomic implies F2().p = A(p)) &
(p is negative & d1 = F2().the_argument_of p implies F2().p = N(d1)) &
(p is conjunctive & d1 = F2().the_left_argument_of p &
d2 = F2().the_right_argument_of p implies F2().p = C(d1, d2)) &
(p is universal & d1 = F2().the_scope_of p implies F2().p = Q(p, d1))
proof
defpred Prop[Element of QC-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()
holds Prop[P!l]
proof
let k;
let P be (QC-pred_symbol of k, Al()),l be QC-variable_list of k, Al();
A4: P!l is atomic;
hence F1().(P!l) = A(P!l) by A1
.= F2().(P!l) by A2,A4;
end;
A5: for x being bound_QC-variable of Al(), p being Element of QC-WFF(Al())
holds Prop[p] implies Prop[All(x,p)]
proof
let x be bound_QC-variable of Al(), p be Element of QC-WFF(Al()) such that
A6: F1().p = F2().p;
A7: All(x,p) is universal;
then the_scope_of All(x,p) = p by QC_LANG1:def 28;
hence
F1().All(x,p) = Q(All(x,p), F2().the_scope_of All(x,p)) by A1,A6,A7
.= F2().All(x,p) by A2,A7;
end;
A8: for p,q being Element of QC-WFF(Al())
st Prop[p] & Prop[q] holds Prop[p '&' q]
proof
let p,q being Element of QC-WFF(Al()) such that
A9: F1().p = F2().p & F1().q = F2().q;
A10: p '&' q is conjunctive;
then
A11: the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q)
= q by QC_LANG1:def 25,def 26;
hence F1().(p '&' q) = C(F2().p,F2().q) by A1,A9,A10
.= F2().(p '&' q) by A2,A10,A11;
end;
A12: for p being Element of QC-WFF(Al()) st Prop[p] holds Prop['not' p]
proof
let p be Element of QC-WFF(Al()) such that
A13: F1().p = F2().p;
A14: 'not' p is negative;
then
A15: the_argument_of 'not' p = p by QC_LANG1:def 24;
hence F1().'not' p = N(F2().p) by A1,A13,A14
.= F2().'not' p by A2,A14,A15;
end;
F1().VERUM(Al()) = V() by A1;
then
A16: Prop[VERUM(Al())] by A2;
for p being Element of QC-WFF(Al()) holds
Prop[p] from QC_LANG1:sch 1(A3,A16,A12,A8,A5);
hence thesis by FUNCT_2:63;
end;
scheme
QCDefD { Al() -> QC-alphabet,
D() -> non empty set,
V() -> (Element of D()),
p() -> (Element of QC-WFF(Al())),
A(Element of QC-WFF(Al())) -> (Element of D()),
N(Element of D()) -> (Element of D()),
C((Element of D()),Element of D()) -> (Element of D()),
Q((Element of QC-WFF(Al())),
Element of D()) -> Element of D()}
:
(ex d being (Element of D()), F being Function of QC-WFF(Al()),
D() st d = F.p() & for p being Element of QC-WFF(Al())
for d1,d2 being Element of D() holds
(p = VERUM(Al()) 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 Element of D() st (ex F being Function of QC-WFF(Al()),
D() st x1 = F.p() & for p being Element of QC-WFF(Al())
for d1,d2 being Element of D() holds
(p = VERUM(Al()) 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(Al()), D() st x2 = F.p() &
for p being Element of QC-WFF(Al()) for d1,d2 being Element of D()
holds (p = VERUM(Al()) 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
proof
thus ex d being (Element of D()), F being Function of QC-WFF(Al()), D()
st d = F.p() & for p being Element of QC-WFF(Al())
for d1,d2 being Element of D() holds (p = VERUM(Al())
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))
proof
consider F being Function of QC-WFF(Al()), D() such that
A1: F.VERUM(Al()) = V() & for p being Element of QC-WFF(Al())
holds (p is atomic implies F.p = A(p)) &
(p is negative implies F.p = N(F.the_argument_of p)) &
(p is conjunctive implies F.p = C(F.the_left_argument_of p,
F.the_right_argument_of p)) &
(p is universal implies F.p = Q(p, F.the_scope_of p)) from QC_LANG1:sch 3;
take F.p(), F;
thus thesis by A1;
end;
let x1,x2 be Element of D();
given F1 being Function of QC-WFF(Al()), D() such that
A2: x1 = F1.p() and
A3: for p being Element of QC-WFF(Al()) for d1,d2 being Element of D() holds (
p = VERUM(Al()) implies F1.p = V()) & (p is atomic implies F1.p = A(p)) &
(p is negative & d1 = F1.the_argument_of p implies F1.p = N(d1)) &
(p is conjunctive & d1 = F1.the_left_argument_of p &
d2 = F1.the_right_argument_of p implies F1.p = C(d1, d2)) &
(p is universal & d1 = F1.the_scope_of p implies F1.p = Q(p, d1));
given F2 being Function of QC-WFF(Al()), D() such that
A4: x2 = F2.p() and
A5: for p being Element of QC-WFF(Al()) for d1,d2 being Element of D()
holds (p = VERUM(Al()) implies F2.p = V()) &
(p is atomic implies F2.p = A(p)) & (p is negative &
d1 = F2.the_argument_of p implies F2.p = N(d1)) & (p is conjunctive &
d1 = F2.the_left_argument_of p & d2 = F2.the_right_argument_of p
implies F2.p= C(d1, d2)) & (p is universal & d1 = F2.the_scope_of p
implies F2.p = Q(p, d1));
F1 = F2 from QCFuncUniq(A3,A5);
hence thesis by A2,A4;
end;
scheme
QCDResult9VERUM { Al() -> QC-alphabet, D() -> non empty set,
F(Element of QC-WFF(Al())) -> (Element of D()), V() -> (Element of D()),
A(Element of QC-WFF(Al())) -> (Element of D()),
N(Element of D()) -> (Element of D()), C((Element of D()),
Element of D()) -> (Element of D()), Q((Element of QC-WFF(Al())),
Element of D()) -> Element of D()} : F(VERUM(Al())) = V()
provided
A1: for p being QC-formula of Al(), d being Element of D() holds d = F(p)
iff ex F being Function of QC-WFF(Al()), D() st d = F.p &
for p being Element of QC-WFF(Al()) for
d1,d2 being Element of D() holds (p = VERUM(Al())
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))
proof
ex F being Function of QC-WFF(Al()), D() st F(VERUM(Al())) = F.VERUM(Al()) &
for p being Element of QC-WFF(Al()) for d1,d2 being Element of D() holds
(p = VERUM(Al()) 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 A1;
hence thesis;
end;
scheme
QCDResult9atomic { Al() -> QC-alphabet, D() -> non empty set,
V() -> (Element of D()), F(Element of QC-WFF(Al())) -> (Element of D()),
p() -> QC-formula of Al(), A(Element of QC-WFF(Al())) -> (Element of D()),
N(Element of D()) -> (Element of D()), C((Element of D()),
Element of D()) -> (Element of D()),
Q((Element of QC-WFF(Al())), Element of D()) -> Element of D()}
:
F(p()) = A(p())
provided
A1: for p being QC-formula of Al(), d being Element of D() holds d = F(p)
iff ex F being Function of QC-WFF(Al()), D() st d = F.p &
for p being Element of QC-WFF(Al()) for
d1,d2 being Element of D() holds (p = VERUM(Al()) 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)) and
A2: p() is atomic
proof
ex F being Function of QC-WFF(Al()), D() st F(p()) = F.p() & for p being
Element of QC-WFF(Al()) for d1,d2 being Element of D() holds
( p = VERUM(Al()) 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 A1;
hence thesis by A2;
end;
scheme
QCDResult9negative { Al() -> QC-alphabet, D() -> non empty set,
V() -> (Element of D()), p() -> QC-formula of Al(),
A(Element of QC-WFF(Al())) -> (Element of D()),
N(Element of D()) -> (Element of D()), C((Element of D()),
Element of D()) -> (Element of D()), Q((Element of QC-WFF(Al())),
Element of D()) -> (Element of D()), F(Element of QC-WFF(Al()))
-> (Element of D()) }
:
F(p()) = N(F(the_argument_of p()))
provided
A1: for p being QC-formula of Al(), d being Element of D() holds d = F(p)
iff ex F being Function of QC-WFF(Al()), D() st d = F.p
& for p being Element of QC-WFF(Al()) for
d1,d2 being Element of D() holds (p = VERUM(Al()) 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)) and
A2: p() is negative
proof
consider F being Function of QC-WFF(Al()), D() such that
A3: F(p()) = F.p() and
A4: for p being Element of QC-WFF(Al()) for d1,d2 being Element of D() holds
(p = VERUM(Al()) 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 A1;
F.(the_argument_of p()) = F(the_argument_of p()) by A1,A4;
hence thesis by A2,A3,A4;
end;
scheme
QCDResult9conjunctive { Al() -> QC-alphabet, D() -> non empty set,
V() -> (Element of D()), A(Element of QC-WFF(Al())) -> (Element of D()),
N(Element of D()) -> (Element of D()), C((Element of D()),
Element of D()) -> (Element of D()), Q((Element of QC-WFF(Al())),
Element of D()) -> (Element of D()),
F(Element of QC-WFF(Al())) -> (Element of D()),
p() -> QC-formula of Al() } : for d1,d2 being Element of D() st d1 = F(
the_left_argument_of p()) & d2 = F(the_right_argument_of p())
holds F(p()) = C(d1,d2)
provided
A1: for p being QC-formula of Al(), d being Element of D() holds d = F(p)
iff ex F being Function of QC-WFF(Al()), D() st d = F.p &
for p being Element of QC-WFF(Al()) for
d1,d2 being Element of D() holds (p = VERUM(Al()) 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)) and
A2: p() is conjunctive
proof
consider F being Function of QC-WFF(Al()), D() such that
A3: F(p()) = F.p() and
A4: for p being Element of QC-WFF(Al()) for d1,d2 being Element of D()
holds (p = VERUM(Al()) 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 A1;
let d1,d2 be Element of D();
assume d1 = F(the_left_argument_of p()) & d2 = F(the_right_argument_of p());
then F.(the_left_argument_of p()) = d1 & F.(the_right_argument_of p()) = d2
by A1,A4;
hence thesis by A2,A3,A4;
end;
scheme
QCDResult9universal { Al() -> QC-alphabet, D() -> non empty set,
V() -> (Element of D()), p() -> QC-formula of Al(),
A(Element of QC-WFF(Al())) -> (Element of D()),
N(Element of D()) -> (Element of D()), C((Element of D()),
Element of D()) -> (Element of D()), Q((Element of QC-WFF(Al())),
Element of D()) -> (Element of D()),
F(Element of QC-WFF(Al())) -> (Element of D()) }
:
F(p()) = Q(p(),F(the_scope_of p()))
provided
A1: for p being QC-formula of Al(), d being Element of D() holds d = F(p)
iff ex F being Function of QC-WFF(Al()), D() st d = F.p &
for p being Element of QC-WFF(Al()) for
d1,d2 being Element of D() holds (p = VERUM(Al()) 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)) and
A2: p() is universal
proof
consider F being Function of QC-WFF(Al()), D() such that
A3: F(p()) = F.p() and
A4: for p being Element of QC-WFF(Al()) for d1,d2 being Element of D() holds
(p = VERUM(Al()) 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 A1;
F.(the_scope_of p()) = F(the_scope_of p()) by A1,A4;
hence thesis by A2,A3,A4;
end;
reserve A for QC-alphabet;
reserve x for bound_QC-variable of A;
reserve a for free_QC-variable of A;
reserve p,q for Element of QC-WFF(A);
reserve l for FinSequence of QC-variables(A);
reserve P,Q for QC-pred_symbol of A;
reserve V for non empty Subset of QC-variables(A);
reserve s,t for QC-symbol of A;
theorem
P is QC-pred_symbol of the_arity_of P, A
proof
set k = the_arity_of P;
set QCP = {Q : the_arity_of Q = k };
P in QCP;
hence thesis;
end;
definition
let A,l,V;
func variables_in(l,V) -> Subset of V equals
{ l.k : 1 <= k & k <= len l & l.k in V };
coherence
proof
set A = { l.k : 1 <= k & k <= len l & l.k in V };
A c= V
proof
let x be object;
assume x in A;
then ex k st l.k = x & 1 <= k & k <= len l & l.k in V;
hence thesis;
end;
hence thesis;
end;
end;
theorem
still_not-bound_in l = variables_in(l,bound_QC-variables(A));
Lm1:
now
let A be QC-alphabet;
deffunc F1(Element of QC-WFF(A)) = still_not-bound_in $1;
deffunc A1(Element of QC-WFF(A)) =
still_not-bound_in(the_arguments_of $1);
deffunc Q1(Element of QC-WFF(A),
Subset of bound_QC-variables(A)) = $2 \ {bound_in $1};
deffunc N1(Subset of bound_QC-variables(A)) = $1;
deffunc C1(Subset of bound_QC-variables(A),
Subset of bound_QC-variables(A)) = $1 \/ $2;
thus
for p being QC-formula of A, d being Subset of bound_QC-variables(A)
holds d = F1(p) iff ex F being Function of QC-WFF(A),
(bool bound_QC-variables(A)) st d = 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 = A1(p)) & (p is negative &
d1 = F.the_argument_of p implies F.p = N1(d1))
& (p is conjunctive & d1 = F.the_left_argument_of p & d2 = F.
the_right_argument_of p implies F.p = C1(d1,d2)) &
(p is universal & d1 = F.the_scope_of p implies F.p = Q1(p,d1))
proof
let p be QC-formula of A, d be Subset of bound_QC-variables(A);
thus d = still_not-bound_in p implies ex F being Function of QC-WFF(A),
(bool bound_QC-variables(A)) st d = 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 = still_not-bound_in(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})
proof
assume d = still_not-bound_in p;
then consider
F being Function of QC-WFF(A), bool bound_QC-variables(A) such that
A1: d = F.p & for p being Element of QC-WFF(A) holds F.VERUM(A) = {} & (p is
atomic implies F.p = { (the_arguments_of p).k : 1 <= k & k <= len
the_arguments_of p & (the_arguments_of p).k in bound_QC-variables(A)}) &
(p is negative implies F.p = F.the_argument_of p) &
(p is conjunctive implies F.p =
(F.the_left_argument_of p) \/ (F.the_right_argument_of p)) &
(p is universal implies F.p = (F.the_scope_of p) \ {bound_in p})
by QC_LANG1:def 30;
take F;
thus d = F.p by A1;
let p be Element of QC-WFF(A);
let d1,d2 be Subset of bound_QC-variables(A);
thus (p = VERUM(A) implies F.p = {}(bound_QC-variables(A))) & (p is atomic
implies F.p = still_not-bound_in (the_arguments_of p)) & (p is negative & d1 =
F.the_argument_of p implies F.p = d1) by A1;
thus thesis by A1;
end;
given F being Function of QC-WFF(A), (bool bound_QC-variables(A)) such that
A2: d = F.p and
A3: 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 = still_not-bound_in(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});
now
let p be Element of QC-WFF(A);
thus F.VERUM(A) = {} by A3;
thus p is atomic implies F.p = { (the_arguments_of p).k : 1 <= k & k <=
len the_arguments_of p & (the_arguments_of p).k in bound_QC-variables(A)}
proof
assume p is atomic;
then F.p = still_not-bound_in the_arguments_of p by A3;
hence thesis;
end;
thus p is negative implies F.p = F.the_argument_of p by A3;
thus p is conjunctive implies F.p = (F.the_left_argument_of p) \/ (F.
the_right_argument_of p) by A3;
assume p is universal;
hence F.p = (F.the_scope_of p) \ {bound_in p} by A3;
end;
hence thesis by A2,QC_LANG1:def 30;
end;
end;
theorem Th3:
still_not-bound_in VERUM(A) = {}
proof
deffunc F1(Element of QC-WFF(A)) = still_not-bound_in $1;
deffunc A1(Element of QC-WFF(A)) =
still_not-bound_in(the_arguments_of $1);
deffunc Q1(Element of QC-WFF(A),
Subset of bound_QC-variables(A)) = $2 \ {bound_in $1};
deffunc N1(Subset of bound_QC-variables(A)) = $1;
deffunc C1(Subset of bound_QC-variables(A),
Subset of bound_QC-variables(A)) = $1 \/ $2;
A1: for p being QC-formula of A, d being Subset of bound_QC-variables(A)
holds d = F1(p) iff ex F being Function of QC-WFF(A),
(bool bound_QC-variables(A)) st d = 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 = A1(p)) & (p is negative &
d1 = F.the_argument_of p implies F.p = N1(d1))
& (p is conjunctive & d1 = F.the_left_argument_of p & d2 = F.
the_right_argument_of p implies F.p = C1(d1,d2)) &
(p is universal & d1 = F.the_scope_of p implies F.p = Q1(p,d1))
by Lm1;
thus F1(VERUM(A)) = {} bound_QC-variables(A) from QCDResult9VERUM(A1)
.= {};
end;
theorem Th4:
for p being QC-formula of A st p is atomic holds still_not-bound_in p
= still_not-bound_in the_arguments_of p
proof
deffunc F1(Element of QC-WFF(A)) = still_not-bound_in $1;
deffunc A1(Element of QC-WFF(A)) =
still_not-bound_in(the_arguments_of $1);
deffunc Q1(Element of QC-WFF(A),
Subset of bound_QC-variables(A)) = $2 \ {bound_in $1};
deffunc N1(Subset of bound_QC-variables(A)) = $1;
deffunc C1(Subset of bound_QC-variables(A),
Subset of bound_QC-variables(A)) = $1 \/ $2;
A1: for p being QC-formula of A, d being Subset of bound_QC-variables(A)
holds d = F1(p) iff ex F being Function of QC-WFF(A),
(bool bound_QC-variables(A)) st d = 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 = A1(p)) & (p is negative &
d1 = F.the_argument_of p implies F.p = N1(d1))
& (p is conjunctive & d1 = F.the_left_argument_of p & d2 = F.
the_right_argument_of p implies F.p = C1(d1,d2)) &
(p is universal & d1 = F.the_scope_of p implies F.p = Q1(p,d1))
by Lm1;
let p be QC-formula of A such that
A2: p is atomic;
thus F1(p) = A1(p) from QCDResult9atomic(A1,A2);
end;
theorem
for P being QC-pred_symbol of k,A for l being QC-variable_list of k, A
holds still_not-bound_in (P!l) = still_not-bound_in l
proof
let P be QC-pred_symbol of k, A;
let l be QC-variable_list of k, A;
A1: P!l is atomic;
then the_arguments_of (P!l) = l by QC_LANG1:def 23;
hence thesis by A1,Th4;
end;
theorem Th6:
for p being QC-formula of A st p is negative holds still_not-bound_in
p = still_not-bound_in the_argument_of p
proof
deffunc F1(Element of QC-WFF(A)) = still_not-bound_in $1;
deffunc A1(Element of QC-WFF(A)) =
still_not-bound_in(the_arguments_of $1);
deffunc Q1(Element of QC-WFF(A),
Subset of bound_QC-variables(A)) = $2 \ {bound_in $1};
deffunc N1(Subset of bound_QC-variables(A)) = $1;
deffunc C1(Subset of bound_QC-variables(A),
Subset of bound_QC-variables(A)) = $1 \/ $2;
A1: for p being QC-formula of A, d being Subset of bound_QC-variables(A)
holds d = F1(p) iff ex F being Function of QC-WFF(A),
(bool bound_QC-variables(A)) st d = 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 = A1(p)) & (p is negative &
d1 = F.the_argument_of p implies F.p = N1(d1))
& (p is conjunctive & d1 = F.the_left_argument_of p & d2 = F.
the_right_argument_of p implies F.p = C1(d1,d2)) &
(p is universal & d1 = F.the_scope_of p implies F.p = Q1(p,d1))
by Lm1;
let p be QC-formula of A such that
A2: p is negative;
thus F1(p) = N1(F1(the_argument_of p)) from QCDResult9negative(A1,A2 );
end;
theorem Th7:
for p being QC-formula of A holds still_not-bound_in 'not' p =
still_not-bound_in p
proof
let p be QC-formula of A;
A1: 'not' p is negative;
then the_argument_of 'not' p = p by QC_LANG1:def 24;
hence thesis by A1,Th6;
end;
theorem Th8:
still_not-bound_in FALSUM(A) = {}
proof
still_not-bound_in FALSUM(A)
= still_not-bound_in 'not' VERUM(A) by QC_LANG2:def 1
.= still_not-bound_in VERUM(A) by Th7 .= {} by Th3;
hence thesis;
end;
theorem Th9:
for p being QC-formula of A st p is conjunctive holds
still_not-bound_in p = (still_not-bound_in the_left_argument_of p) \/ (
still_not-bound_in the_right_argument_of p)
proof
deffunc F1(Element of QC-WFF(A)) = still_not-bound_in $1;
deffunc A1(Element of QC-WFF(A)) =
still_not-bound_in(the_arguments_of $1);
deffunc Q1(Element of QC-WFF(A),
Subset of bound_QC-variables(A)) = $2 \ {bound_in $1};
deffunc N1(Subset of bound_QC-variables(A)) = $1;
deffunc C1(Subset of bound_QC-variables(A),
Subset of bound_QC-variables(A)) = $1 \/ $2;
A1: for p being QC-formula of A, d being Subset of bound_QC-variables(A)
holds d = F1(p) iff ex F being Function of QC-WFF(A),
(bool bound_QC-variables(A)) st d = 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 = A1(p)) & (p is negative &
d1 = F.the_argument_of p implies F.p = N1(d1))
& (p is conjunctive & d1 = F.the_left_argument_of p & d2 = F.
the_right_argument_of p implies F.p = C1(d1,d2)) &
(p is universal & d1 = F.the_scope_of p implies F.p = Q1(p,d1))
by Lm1;
let p be QC-formula of A such that
A2: p is conjunctive;
for d1,d2 being Subset of bound_QC-variables(A) st d1 = F1(
the_left_argument_of p) & d2 = F1(the_right_argument_of p) holds F1(p) = C1(d1,
d2) from QCDResult9conjunctive(A1,A2);
hence thesis;
end;
theorem Th10:
for p,q being QC-formula of A holds still_not-bound_in(p '&' q) = (
still_not-bound_in p) \/ (still_not-bound_in q)
proof
let p,q be QC-formula of A;
set pq = p '&' q;
A1: pq is conjunctive;
then the_left_argument_of pq = p & the_right_argument_of pq = q by
QC_LANG1:def 25,def 26;
hence thesis by A1,Th9;
end;
theorem Th11:
for p being QC-formula of A st p is universal holds
still_not-bound_in p = (still_not-bound_in the_scope_of p) \ {bound_in p}
proof
deffunc F1(Element of QC-WFF(A)) = still_not-bound_in $1;
deffunc A1(Element of QC-WFF(A)) =
still_not-bound_in(the_arguments_of $1);
deffunc Q1(Element of QC-WFF(A),
Subset of bound_QC-variables(A)) = $2 \ {bound_in $1};
deffunc N1(Subset of bound_QC-variables(A)) = $1;
deffunc C1(Subset of bound_QC-variables(A),
Subset of bound_QC-variables(A)) = $1 \/ $2;
A1: for p being QC-formula of A, d being Subset of bound_QC-variables(A)
holds d = F1(p) iff ex F being Function of QC-WFF(A),
(bool bound_QC-variables(A)) st d = 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 = A1(p)) & (p is negative &
d1 = F.the_argument_of p implies F.p = N1(d1))
& (p is conjunctive & d1 = F.the_left_argument_of p & d2 = F.
the_right_argument_of p implies F.p = C1(d1,d2)) &
(p is universal & d1 = F.the_scope_of p implies F.p = Q1(p,d1)) by Lm1;
let p be QC-formula of A such that
A2: p is universal;
thus F1(p) = Q1(p,F1(the_scope_of p)) from QCDResult9universal(A1,A2 );
end;
theorem Th12:
for p being QC-formula of A holds still_not-bound_in All(x,p) = (
still_not-bound_in p) \ {x}
proof
let p be QC-formula of A;
set a = All(x,p);
A1: a is universal;
then the_scope_of a = p & bound_in a = x by QC_LANG1:def 27,def 28;
hence thesis by A1,Th11;
end;
theorem Th13:
for p being QC-formula of A st p is disjunctive holds
still_not-bound_in p = (still_not-bound_in the_left_disjunct_of p) \/ (
still_not-bound_in the_right_disjunct_of p)
proof
let p be QC-formula of A;
set p1 = the_left_disjunct_of p;
set p2 = the_right_disjunct_of p;
assume p is disjunctive;
then p = (the_left_disjunct_of p) 'or' (the_right_disjunct_of p) by
QC_LANG2:37;
then p = 'not'('not' p1 '&' 'not' p2) by QC_LANG2:def 3;
then still_not-bound_in p = still_not-bound_in 'not' p1 '&' 'not' p2 by Th7
.= (still_not-bound_in 'not' p1) \/ (still_not-bound_in 'not' p2) by Th10
.= (still_not-bound_in p1) \/ (still_not-bound_in 'not' p2) by Th7
.= (still_not-bound_in p1) \/ (still_not-bound_in p2) by Th7;
hence thesis;
end;
theorem
for p,q being QC-formula of A holds still_not-bound_in p 'or' q = (
still_not-bound_in p) \/ (still_not-bound_in q)
proof
let p,q be QC-formula of A;
A1: the_right_disjunct_of(p 'or' q) = q by QC_LANG2:29;
p 'or' q is disjunctive & the_left_disjunct_of(p 'or' q) = p by QC_LANG2:29
,def 10;
hence thesis by A1,Th13;
end;
theorem Th15:
for p being QC-formula of A st p is conditional holds
still_not-bound_in p = (still_not-bound_in the_antecedent_of p) \/ (
still_not-bound_in the_consequent_of p)
proof
let p be QC-formula of A;
set p1 = the_antecedent_of p;
set p2 = the_consequent_of p;
assume p is conditional;
then p = (the_antecedent_of p) => (the_consequent_of p) by QC_LANG2:38;
then p = 'not'(p1 '&' 'not' p2) by QC_LANG2:def 2;
then still_not-bound_in p = still_not-bound_in p1 '&' 'not' p2 by Th7
.= (still_not-bound_in p1) \/ (still_not-bound_in 'not' p2) by Th10
.= (still_not-bound_in p1) \/ (still_not-bound_in p2) by Th7;
hence thesis;
end;
theorem Th16:
for p,q being QC-formula of A holds still_not-bound_in p => q = (
still_not-bound_in p) \/ (still_not-bound_in q)
proof
let p,q be QC-formula of A;
A1: the_consequent_of(p => q) = q by QC_LANG2:30;
p => q is conditional & the_antecedent_of(p => q) = p by QC_LANG2:30,def 11;
hence thesis by A1,Th15;
end;
theorem Th17:
for p being QC-formula of A st p is biconditional holds
still_not-bound_in p = (still_not-bound_in the_left_side_of p) \/ (
still_not-bound_in the_right_side_of p)
proof
let p be QC-formula of A;
set p1 = the_left_side_of p;
set p2 = the_right_side_of p;
assume p is biconditional;
then p = (the_left_side_of p) <=> (the_right_side_of p) by QC_LANG2:39;
then p = (p1 => p2) '&' (p2 => p1) by QC_LANG2:def 4;
then still_not-bound_in p = (still_not-bound_in p1 => p2) \/ (
still_not-bound_in p2 => p1) by Th10
.= (still_not-bound_in p1) \/ (still_not-bound_in p2) \/ (
still_not-bound_in p2 => p1) by Th16
.= (still_not-bound_in p1) \/ (still_not-bound_in p2) \/ ((
still_not-bound_in p1) \/ (still_not-bound_in p2)) by Th16
.= (still_not-bound_in p1) \/ (still_not-bound_in p2);
hence thesis;
end;
theorem
for p,q being QC-formula of A holds still_not-bound_in p <=> q = (
still_not-bound_in p) \/ (still_not-bound_in q)
proof
let p,q be QC-formula of A;
A1: the_right_side_of(p <=> q) = q by QC_LANG2:31;
p <=> q is biconditional & the_left_side_of(p <=> q) = p by QC_LANG2:31
,def 12;
hence thesis by A1,Th17;
end;
theorem Th19:
for p being QC-formula of A holds still_not-bound_in Ex(x,p) = (
still_not-bound_in p) \ {x}
proof
let p be QC-formula of A;
Ex(x,p) = 'not' All(x,'not' p) by QC_LANG2:def 5;
hence still_not-bound_in Ex(x,p) = still_not-bound_in All(x,'not' p) by Th7
.= (still_not-bound_in 'not' p) \ {x} by Th12
.= (still_not-bound_in p) \ {x} by Th7;
end;
theorem
VERUM(A) is closed & FALSUM(A) is closed ::by Th7,Th12,QC_LANG1:def 30;
by Th3,Th8;
theorem Th21:
for p being QC-formula of A holds p is closed iff 'not' p is closed
by Th7;
theorem Th22:
for p,q being QC-formula of A holds p is closed & q is closed iff p
'&' q is closed
proof
let p,q be QC-formula of A;
thus p is closed & q is closed implies p '&' q is closed
proof
assume still_not-bound_in p = {} & still_not-bound_in q = {};
then (still_not-bound_in p) \/ (still_not-bound_in q) = {};
hence still_not-bound_in p '&' q = {} by Th10;
end;
assume
A1: still_not-bound_in p '&' q = {};
still_not-bound_in p '&' q = (still_not-bound_in p) \/ (
still_not-bound_in q) by Th10;
hence still_not-bound_in p={} & still_not-bound_in q={} by A1,XBOOLE_1:15;
end;
theorem Th23:
for p being QC-formula of A holds All(x,p) is closed iff
still_not-bound_in p c= {x}
proof
let p be QC-formula of A;
thus All(x,p) is closed implies still_not-bound_in p c= {x}
proof
assume still_not-bound_in All(x,p) = {};
then {} = (still_not-bound_in p) \ {x} by Th12;
hence thesis by XBOOLE_1:37;
end;
assume still_not-bound_in p c= {x};
then {} = (still_not-bound_in p) \ {x} by XBOOLE_1:37;
hence still_not-bound_in All(x,p) = {} by Th12;
end;
theorem
for p being QC-formula of A st p is closed holds All(x,p) is closed
proof
let p be QC-formula of A;
assume still_not-bound_in p = {};
then still_not-bound_in p c= {x} by XBOOLE_1:2;
hence thesis by Th23;
end;
theorem
for p,q being QC-formula of A holds p is closed & q is closed iff p 'or' q
is closed
proof
let p,q be QC-formula of A;
A1: p 'or' q = 'not'('not' p '&' 'not' q) by QC_LANG2:def 3;
'not' p '&' 'not' q is closed iff 'not' p is closed & 'not' q is closed
by Th22;
hence thesis by A1,Th21;
end;
theorem Th26:
for p,q being QC-formula of A holds p is closed &
q is closed iff p => q is closed
proof
let p,q be QC-formula of A;
A1: p => q = 'not'(p '&' 'not' q) by QC_LANG2:def 2;
p '&' 'not' q is closed iff p is closed & 'not' q is closed by Th22;
hence thesis by A1,Th21;
end;
theorem
for p,q being QC-formula of A holds p is closed & q is closed iff p <=> q
is closed
proof
let p,q be QC-formula of A;
p <=> q = (p => q) '&' (q => p) by QC_LANG2:def 4;
then p <=> q is closed iff p => q is closed & q => p is closed by Th22;
hence thesis by Th26;
end;
theorem Th28:
for p being QC-formula of A holds Ex(x,p) is closed iff
still_not-bound_in p c= {x}
proof
let p be QC-formula of A;
thus Ex(x,p) is closed implies still_not-bound_in p c= {x}
proof
assume still_not-bound_in Ex(x,p) = {};
then {} = (still_not-bound_in p) \ {x} by Th19;
hence thesis by XBOOLE_1:37;
end;
assume still_not-bound_in p c= {x};
then {} = (still_not-bound_in p) \ {x} by XBOOLE_1:37;
hence still_not-bound_in Ex(x,p) = {} by Th19;
end;
theorem
for p being QC-formula of A st p is closed holds Ex(x,p) is closed
proof
let p be QC-formula of A;
assume still_not-bound_in p = {};
then still_not-bound_in p c= {x} by XBOOLE_1:2;
hence thesis by Th28;
end;
definition
let A,s;
func x.s -> bound_QC-variable of A equals
[4,s];
coherence
proof
4 in {4} by TARSKI:def 1;
hence thesis by ZFMISC_1:def 2;
end;
end;
theorem
ex t st x.t = x
proof
consider i,t being object such that
A1: i in {4} and
A2: t in QC-symbols(A) and
A3: [i,t] = x by ZFMISC_1:def 2;
reconsider t as QC-symbol of A by A2;
take t;
thus thesis by A1,A3,TARSKI:def 1;
end;
definition
let A,k;
func (A)a.k -> free_QC-variable of A equals
[6,k];
coherence
proof
A1: k in NAT by ORDINAL1:def 12;
6 in {6} by TARSKI:def 1;
hence thesis by ZFMISC_1:def 2,A1;
end;
end;
theorem
ex i st (A)a.i = a
proof
consider x,y being object such that
A1: x in {6} and
A2: y in NAT and
A3: [x,y] = a by ZFMISC_1:def 2;
reconsider i = y as Nat by A2;
take i;
thus thesis by A1,A3,TARSKI:def 1;
end;
theorem
for c being Element of fixed_QC-variables(A) for a being Element of
free_QC-variables(A) holds c <> a
proof
let c be Element of fixed_QC-variables(A);
let a be Element of free_QC-variables(A);
consider a1,a2 being object such that
A1: a1 in {6} and
a2 in NAT and
A2: a = [a1,a2] by ZFMISC_1:def 2;
consider c1,c2 being object such that
A3: c1 in {5} and
c2 in QC-symbols(A) and
A4: c = [c1,c2] by ZFMISC_1:def 2;
A5: c1 = 5 by A3,TARSKI:def 1;
a1 = 6 by A1,TARSKI:def 1;
hence thesis by A2,A4,A5,XTUPLE_0:1;
end;
theorem
for c being Element of fixed_QC-variables(A) for x being Element of
bound_QC-variables(A) holds c <> x
proof
let c be Element of fixed_QC-variables(A);
let x be Element of bound_QC-variables(A);
consider x1,x2 being object such that
A1: x1 in {4} and
x2 in QC-symbols(A) and
A2: x = [x1,x2] by ZFMISC_1:def 2;
consider c1,c2 being object such that
A3: c1 in {5} and
c2 in QC-symbols(A) and
A4: c = [c1,c2] by ZFMISC_1:def 2;
A5: c1 = 5 by A3,TARSKI:def 1;
x1 = 4 by A1,TARSKI:def 1;
hence thesis by A2,A4,A5,XTUPLE_0:1;
end;
theorem
for a being Element of free_QC-variables(A) for x being Element of
bound_QC-variables(A) holds a <> x
proof
let a be Element of free_QC-variables(A);
let x be Element of bound_QC-variables(A);
consider x1,x2 being object such that
A1: x1 in {4} and
x2 in QC-symbols(A) and
A2: x = [x1,x2] by ZFMISC_1:def 2;
consider a1,a2 being object such that
A3: a1 in {6} and
a2 in NAT and
A4: a = [a1,a2] by ZFMISC_1:def 2;
A5: a1 = 6 by A3,TARSKI:def 1;
x1 = 4 by A1,TARSKI:def 1;
hence thesis by A2,A4,A5,XTUPLE_0:1;
end;
definition
let A,V,p;
func Vars(p,V) -> Subset of V means
: Def4:
ex F being Function of QC-WFF(A),
bool V st it = 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 = variables_in
(the_arguments_of p,V)) & (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);
correctness
proof
deffunc Q(Element of QC-WFF(A),Subset of V) = $2;
deffunc C(Subset of V,Subset of V) = $1 \/ $2;
deffunc N(Subset of V) = $1;
deffunc A(Element of QC-WFF(A)) = variables_in(the_arguments_of $1,V);
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 QCDefD;
end;
end;
Lm2: now
let A,V;
deffunc F1(Element of QC-WFF(A)) = Vars($1,V);
deffunc A(Element of QC-WFF(A)) = variables_in(the_arguments_of $1,V);
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;
A1: for 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 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)) by Def4;
thus F1(VERUM(A)) = {}(V) from QCDResult9VERUM(A1)
.= {};
thus p is atomic implies Vars(p,V) = variables_in(the_arguments_of p,V)
proof
assume
A2: p is atomic;
thus F1(p) = A(p) from QCDResult9atomic(A1,A2);
end;
thus p is negative implies Vars(p,V) = Vars(the_argument_of p,V)
proof
assume
A3: p is negative;
thus F1(p) = N(F1(the_argument_of p)) from QCDResult9negative(A1, A3);
end;
thus p is conjunctive implies Vars(p,V) = Vars(the_left_argument_of p,V) \/
Vars(the_right_argument_of p,V)
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 QCDResult9conjunctive(
A1,A4);
hence thesis;
end;
thus p is universal implies Vars(p,V) = Vars(the_scope_of p,V)
proof
assume
A5: p is universal;
thus F1(p) = Q(p,F1(the_scope_of p)) from QCDResult9universal(A1, A5);
end;
end;
theorem
Vars(VERUM(A),V) = {} by Lm2;
theorem Th36:
p is atomic implies Vars(p,V) = variables_in(the_arguments_of p,
V) & Vars(p,V) = { (the_arguments_of p).k : 1 <= k & k <= len (the_arguments_of
p) & (the_arguments_of p).k in V }
proof
assume p is atomic;
hence Vars(p,V) = variables_in(the_arguments_of p, V) by Lm2;
hence thesis;
end;
theorem Th37:
for P being QC-pred_symbol of k, A for l being QC-variable_list of
k, A holds Vars(P!l,V) = variables_in(l, V) &
Vars((P!l),V) = { l.i : 1 <= i & i
<= len l & l.i in V }
proof
let P be QC-pred_symbol of k, A;
let l be QC-variable_list of k, A;
A1: P!l is atomic;
then the_arguments_of (P!l) = l by QC_LANG1:def 23;
hence thesis by A1,Th36;
end;
theorem
p is negative implies Vars(p,V) = Vars(the_argument_of p,V) by Lm2;
theorem Th39:
Vars('not' p,V) = Vars(p,V)
proof
set 9p = 'not' p;
A1: 9p is negative;
then the_argument_of 9p = p by QC_LANG1:def 24;
hence thesis by A1,Lm2;
end;
theorem Th40:
Vars(FALSUM(A),V) = {}
proof
FALSUM(A) = 'not' VERUM(A) by QC_LANG2:def 1;
hence Vars(FALSUM(A),V) = Vars(VERUM(A),V) by Th39 .= {} by Lm2;
end;
theorem
p is conjunctive implies Vars(p,V) = Vars(the_left_argument_of p,V) \/
Vars(the_right_argument_of p,V) by Lm2;
theorem Th42:
Vars(p '&' q,V) = Vars(p,V) \/ Vars(q,V)
proof
set pq = p '&' q;
A1: p '&' q is conjunctive;
then the_left_argument_of pq = p & the_right_argument_of pq = q by
QC_LANG1:def 25,def 26;
hence thesis by A1,Lm2;
end;
theorem
p is universal implies Vars(p,V) = Vars(the_scope_of p,V) by Lm2;
theorem Th44:
Vars(All(x,p),V) = Vars(p,V)
proof
A1: All(x,p) is universal;
then the_scope_of All(x,p) = p by QC_LANG1:def 28;
hence thesis by A1,Lm2;
end;
theorem Th45:
p is disjunctive implies Vars(p,V) = Vars(the_left_disjunct_of p
,V) \/ Vars(the_right_disjunct_of p,V)
proof
set p1 = the_left_disjunct_of p;
set p2 = the_right_disjunct_of p;
assume p is disjunctive;
then p = p1 'or' p2 by QC_LANG2:37;
then p = 'not'('not' p1 '&' 'not' p2) by QC_LANG2:def 3;
hence Vars(p,V) = Vars('not' p1 '&' 'not' p2, V) by Th39
.= Vars('not' p1, V) \/ Vars('not' p2, V) by Th42
.= Vars(p1, V) \/ Vars('not' p2, V) by Th39
.= Vars(the_left_disjunct_of p,V) \/ Vars(the_right_disjunct_of p,V) by
Th39;
end;
theorem
Vars(p 'or' q, V) = Vars(p,V) \/ Vars(q,V)
proof
A1: the_right_disjunct_of p 'or' q = q by QC_LANG2:29;
p 'or' q is disjunctive & the_left_disjunct_of p 'or' q = p by QC_LANG2:29
,def 10;
hence thesis by A1,Th45;
end;
theorem Th47:
p is conditional implies Vars(p,V) = Vars(the_antecedent_of p,V)
\/ Vars(the_consequent_of p,V)
proof
set p1 = the_antecedent_of p;
set p2 = the_consequent_of p;
assume p is conditional;
then p = p1 => p2 by QC_LANG2:38;
then p = 'not'(p1 '&' 'not' p2) by QC_LANG2:def 2;
hence Vars(p,V) = Vars(p1 '&' 'not' p2, V) by Th39
.= Vars(p1, V) \/ Vars('not' p2, V) by Th42
.= Vars(the_antecedent_of p,V) \/ Vars(the_consequent_of p,V) by Th39;
end;
theorem Th48:
Vars(p => q,V) = Vars(p,V) \/ Vars(q,V)
proof
A1: the_consequent_of p => q = q by QC_LANG2:30;
p => q is conditional & the_antecedent_of p => q = p by QC_LANG2:30,def 11;
hence thesis by A1,Th47;
end;
theorem Th49:
p is biconditional implies Vars(p,V) = Vars(the_left_side_of p,V
) \/ Vars(the_right_side_of p,V)
proof
set p1 = the_left_side_of p;
set p2 = the_right_side_of p;
assume p is biconditional;
then p = p1 <=> p2 by QC_LANG2:39;
then p = (p1 => p2) '&' (p2 => p1) by QC_LANG2:def 4;
hence Vars(p,V) = Vars(p1 => p2, V) \/ Vars(p2 => p1, V) by Th42
.= Vars(p1,V) \/ Vars(p2,V) \/ Vars(p2 => p1, V) by Th48
.= Vars(p1,V) \/ Vars(p2,V) \/ (Vars(p1,V) \/ Vars(p2,V)) by Th48
.= Vars(the_left_side_of p,V) \/ Vars(the_right_side_of p,V);
end;
theorem
Vars(p <=> q,V) = Vars(p,V) \/ Vars(q,V)
proof
A1: the_right_side_of p <=> q = q by QC_LANG2:31;
p <=> q is biconditional & the_left_side_of p <=> q = p by QC_LANG2:31,def 12
;
hence thesis by A1,Th49;
end;
theorem
p is existential implies Vars(p,V) = Vars(the_argument_of the_scope_of
the_argument_of p, V)
proof
set p1 = the_argument_of the_scope_of the_argument_of p;
set x = bound_in the_argument_of p;
assume p is existential;
then p = Ex(x,p1) by QC_LANG2:40;
then p = 'not' All(x,'not' p1) by QC_LANG2:def 5;
then Vars(p,V) = Vars(All(x,'not' p1), V) by Th39
.= Vars('not' p1, V) by Th44
.= Vars(p1, V) by Th39;
hence thesis;
end;
theorem
Vars(Ex(x,p), V) = Vars(p,V)
proof
Ex(x,p) = 'not' All(x,'not' p) by QC_LANG2:def 5;
hence Vars(Ex(x,p), V) = Vars(All(x,'not' p), V) by Th39
.= Vars('not' p, V) by Th44
.= Vars(p, V) by Th39;
end;
definition
let A,p;
func Free p -> Subset of free_QC-variables(A) equals
Vars(p,free_QC-variables(A));
correctness;
end;
theorem
Free VERUM(A) = {} by Lm2;
theorem
for P being QC-pred_symbol of k, A for l being QC-variable_list of k, A
holds Free(P!l) = { l.i : 1 <= i & i <= len l & l.i in free_QC-variables(A)}
by Th37;
theorem
Free 'not' p = Free p by Th39;
theorem
Free FALSUM(A) = {} by Th40;
theorem
Free(p '&' q) = Free p \/ Free q by Th42;
theorem
Free(All(x,p)) = Free(p) by Th44;
theorem
Free(p 'or' q) = Free p \/ Free q
proof
p 'or' q = 'not'('not' p '&' 'not' q) by QC_LANG2:def 3;
hence Free(p 'or' q) = Free('not' p '&' 'not' q) by Th39
.= Free 'not' p \/ Free 'not' q by Th42
.= Free p \/ Free 'not' q by Th39
.= Free p \/ Free q by Th39;
end;
theorem Th60:
Free(p => q) = Free p \/ Free q
proof
p => q = 'not'(p '&' 'not' q) by QC_LANG2:def 2;
hence Free(p => q) = Free(p '&' 'not' q) by Th39
.= Free p \/ Free 'not' q by Th42
.= Free p \/ Free q by Th39;
end;
theorem
Free(p <=> q) = Free p \/ Free q
proof
p <=> q = (p => q) '&' (q => p) by QC_LANG2:def 4;
hence Free(p <=> q) = Free (p => q) \/ Free (q => p) by Th42
.= Free p \/ Free q \/ Free (q => p) by Th60
.= Free p \/ Free q \/ (Free p \/ Free q) by Th60
.= Free p \/ Free q;
end;
theorem
Free Ex(x,p) = Free p
proof
Ex(x,p) = 'not' All(x,'not' p) by QC_LANG2:def 5;
hence Free Ex(x,p) = Free All(x,'not' p) by Th39
.= Free 'not' p by Th44
.= Free p by Th39;
end;
definition
let A,p;
func Fixed p -> Subset of fixed_QC-variables(A) equals
Vars(p,fixed_QC-variables(A));
correctness;
end;
theorem
Fixed VERUM(A) = {} by Lm2;
theorem
for P being QC-pred_symbol of k,A for l being QC-variable_list of k,A
holds Fixed(P!l) = { l.i : 1 <= i & i <= len l & l.i in fixed_QC-variables(A)}
by Th37;
theorem
Fixed 'not' p = Fixed p by Th39;
theorem
Fixed FALSUM(A) = {}
proof
thus Fixed FALSUM(A) = Fixed 'not' VERUM(A) by QC_LANG2:def 1
.= Fixed VERUM(A) by Th39 .= {} by Lm2;
end;
theorem
Fixed(p '&' q) = Fixed p \/ Fixed q by Th42;
theorem
Fixed(All(x,p)) = Fixed(p) by Th44;
theorem
Fixed(p 'or' q) = Fixed p \/ Fixed q
proof
p 'or' q = 'not'('not' p '&' 'not' q) by QC_LANG2:def 3;
hence Fixed(p 'or' q) = Fixed('not' p '&' 'not' q) by Th39
.= Fixed 'not' p \/ Fixed 'not' q by Th42
.= Fixed p \/ Fixed 'not' q by Th39
.= Fixed p \/ Fixed q by Th39;
end;
theorem Th70:
Fixed(p => q) = Fixed p \/ Fixed q
proof
p => q = 'not'(p '&' 'not' q) by QC_LANG2:def 2;
hence Fixed(p => q) = Fixed(p '&' 'not' q) by Th39
.= Fixed p \/ Fixed 'not' q by Th42
.= Fixed p \/ Fixed q by Th39;
end;
theorem
Fixed(p <=> q) = Fixed p \/ Fixed q
proof
p <=> q = (p => q) '&' (q => p) by QC_LANG2:def 4;
hence Fixed(p <=> q) = Fixed (p => q) \/ Fixed (q => p) by Th42
.= Fixed p \/ Fixed q \/ Fixed (q => p) by Th70
.= Fixed p \/ Fixed q \/ (Fixed q \/ Fixed p) by Th70
.= Fixed p \/ Fixed q;
end;
theorem
Fixed Ex(x,p) = Fixed p
proof
Ex(x,p) = 'not' All(x,'not' p) by QC_LANG2:def 5;
hence Fixed Ex(x,p) = Fixed All(x,'not' p) by Th39
.= Fixed 'not' p by Th44
.= Fixed p by Th39;
end;