:: Coincidence Lemma and Substitution Lemma
:: 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 SUBSET_1, NUMBERS, CQC_LANG, QC_LANG1, XBOOLE_0, VALUAT_1,
FUNCT_1, FINSEQ_1, RELAT_1, TARSKI, FUNCT_4, FUNCOP_1, PARTFUN1, FUNCT_2,
MCART_1, REALSET1, XBOOLEAN, ZF_MODEL, ORDINAL4, ZF_LANG, ARYTM_3, NAT_1,
XXREAL_0, ZFMISC_1, BVFUNC_2, CLASSES2, ZF_LANG1, SUBLEMMA, CARD_1,
SUBSTUT1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, FINSEQ_1, FUNCT_1,
ORDINAL1, NAT_1, QC_LANG1, QC_LANG3, PARTFUN1, CARD_1, NUMBERS, XXREAL_0,
FUNCOP_1, CQC_LANG, RELAT_1, FUNCT_4, SEQ_4, VALUAT_1, RELSET_1, FUNCT_2,
MARGREL1, DOMAIN_1, MCART_1, SUBSTUT1;
constructors DOMAIN_1, FUNCT_4, XXREAL_0, SEQ_4, QC_LANG3, VALUAT_1, RELSET_1,
SUBSTUT1, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
QC_LANG1, CQC_LANG, XXREAL_0, RELSET_1, SUBSTUT1, FUNCT_4, XTUPLE_0;
requirements NUMERALS, SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0;
equalities FUNCOP_1;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, FINSEQ_1, FUNCT_1, VALUAT_1, XBOOLE_0, XBOOLE_1, FINSEQ_2,
CQC_LANG, QC_LANG1, ZFMISC_1, RELAT_1, QC_LANG3, FUNCOP_1, FUNCT_2,
RELSET_1, QC_LANG2, FUNCT_4, FUNCT_7, CARD_1, SUBSTUT1, XTUPLE_0;
schemes CQC_LANG, XBOOLE_0, SUBSTUT1;
begin :: Preliminaries
reserve Al for QC-alphabet;
reserve a,b,c,d for object,
i,k,n for Nat,
p,q for Element of CQC-WFF(Al),
x,y,y1 for bound_QC-variable of Al,
A for non empty set,
J for interpretation of Al,A,
v,w for Element of Valuations_in(Al,A),
f,g for Function,
P,P9 for QC-pred_symbol of k,Al,
ll,ll9 for CQC-variable_list of k,Al,
l1 for FinSequence of QC-variables(Al),
Sub,Sub9,Sub1 for CQC_Substitution of Al,
S,S9,S1,S2 for Element of CQC-Sub-WFF(Al),
s for QC-symbol of Al;
theorem Th1:
for f,g,h,h1,h2 being Function st dom h1 c= dom h & dom h2 c= dom
h holds f+*g+*h = (f+*h1)+*(g+*h2)+*h
proof
let f,g,h,h1,h2 be Function such that
A1: dom h1 c= dom h and
A2: dom h2 c= dom h;
dom (f+*h1) = (dom f \/ dom h1) & dom (g+*h2) = (dom g \/ dom h2) by
FUNCT_4:def 1;
then dom ((f+*h1)+*(g+*h2)) = ((dom f \/ dom h1) \/ (dom g \/ dom h2)) by
FUNCT_4:def 1;
then
dom ((f+*h1)+*(g+*h2)+*h) = ((dom f \/ dom h1) \/ (dom g \/ dom h2)) \/
dom h by FUNCT_4:def 1;
then dom ((f+*h1)+*(g+*h2)+*h) = (dom f \/ dom h1) \/ ((dom g \/ dom h2) \/
dom h) by XBOOLE_1:4;
then dom ((f+*h1)+*(g+*h2)+*h) = (dom f \/ dom h1) \/ (dom g \/ (dom h2 \/
dom h)) by XBOOLE_1:4;
then
dom ((f+*h1)+*(g+*h2)+*h) = (dom f \/ dom h1) \/ (dom g \/ dom h) by A2,
XBOOLE_1:12;
then dom ((f+*h1)+*(g+*h2)+*h) = ((dom f \/ dom h1) \/ dom h) \/ dom g by
XBOOLE_1:4;
then dom ((f+*h1)+*(g+*h2)+*h) = (dom f \/ (dom h1 \/ dom h)) \/ dom g by
XBOOLE_1:4;
then
A3: dom ((f+*h1)+*(g+*h2)+*h) = (dom f \/ dom h) \/ dom g by A1,XBOOLE_1:12;
A4: for b being object st b in dom (f+*g+*h)
holds (f+*g+*h).b = ((f+*h1)+*(g+*h2)+*h).b
proof
let b be object such that
b in dom (f+*g+*h);
A5: now
assume
A6: not b in dom h;
then
A7: ((f+*h1)+*(g+*h2)+*h).b = ((f+*h1)+*(g+*h2)).b by FUNCT_4:11;
A8: (f+*g+*h).b = (f+*g).b by A6,FUNCT_4:11;
A9: now
A10: not b in dom h2 by A2,A6;
assume
A11: b in dom g;
dom g c= (dom g \/ dom h2) by XBOOLE_1:7;
then b in dom g \/ dom h2 by A11;
then b in dom (g+*h2) by FUNCT_4:def 1;
then
A12: ((f+*h1)+*(g+*h2)+*h).b = (g+*h2).b by A7,FUNCT_4:13;
(f+*g+*h).b = g.b by A8,A11,FUNCT_4:13;
hence thesis by A12,A10,FUNCT_4:11;
end;
now
A13: not b in dom h1 by A1,A6;
assume
A14: not b in dom g;
not b in dom h2 by A2,A6;
then not b in dom g \/ dom h2 by A14,XBOOLE_0:def 3;
then not b in dom (g+*h2) by FUNCT_4:def 1;
then
A15: ((f+*h1)+*(g+*h2)+*h).b = (f+*h1).b by A7,FUNCT_4:11;
(f+*g+*h).b = f.b by A8,A14,FUNCT_4:11;
hence thesis by A15,A13,FUNCT_4:11;
end;
hence thesis by A9;
end;
now
assume
A16: b in dom h;
then (f+*g+*h).b = h.b by FUNCT_4:13;
hence thesis by A16,FUNCT_4:13;
end;
hence thesis by A5;
end;
dom (f+*g) = dom f \/ dom g by FUNCT_4:def 1;
then dom (f+*g+*h) = (dom f \/ dom g) \/ dom h by FUNCT_4:def 1;
hence thesis by A3,A4,FUNCT_1:2,XBOOLE_1:4;
end;
theorem Th2:
for vS1 being Function st x in dom vS1 holds (vS1|((dom vS1) \ {x
})) +* (x .--> vS1.x) = vS1
proof
let vS1 be Function;
assume x in dom vS1;
then (dom vS1 \ {x}) \/ {x} = dom vS1 \/ {x} & {x} c= dom vS1 by XBOOLE_1:39
,ZFMISC_1:31;
then (dom vS1 \ {x}) \/ {x} = dom vS1 by XBOOLE_1:12;
hence thesis by FUNCT_7:14;
end;
definition
let Al,A;
mode Val_Sub of A,Al is PartFunc of bound_QC-variables(Al),A;
end;
reserve vS,vS1,vS2 for Val_Sub of A,Al;
notation
let Al, A, v, vS;
synonym v.vS for v +* vS;
end;
definition
let Al, A, v, vS;
redefine func v.vS -> Element of Valuations_in(Al,A); :: redefines . (SUBLEMMA, synonym) → +* (FUNCT_4, definition)
coherence
proof
v is Element of Funcs(bound_QC-variables(Al),A) by VALUAT_1:def 1;
then ex f st v = f & dom f = bound_QC-variables(Al) & rng f c= A by
FUNCT_2:def 2;
then dom (v +* vS) = bound_QC-variables(Al) \/ dom vS by FUNCT_4:def 1;
then
A1: dom (v +* vS) = bound_QC-variables(Al) by XBOOLE_1:12;
rng (v +* vS) c= rng v \/ rng vS by FUNCT_4:17;
then v +* vS in Funcs(bound_QC-variables(Al),A) by A1,FUNCT_2:def 2;
hence thesis by VALUAT_1:def 1;
end;
end;
definition
let Al,S;
redefine func S`1 -> Element of CQC-WFF(Al); :: redefines `1 (XTUPLE_0, definition)
coherence
proof
S in CQC-Sub-WFF(Al);
then S in {S1 where S1 is Element of QC-Sub-WFF(Al) : S1`1 is Element of
CQC-WFF(Al)} by SUBSTUT1:def 39;
then ex S1 being Element of QC-Sub-WFF(Al) st S = S1 & S1`1 is Element of
CQC-WFF(Al);
hence thesis;
end;
end;
definition
let Al, S, A, v;
func Val_S(v,S) -> Val_Sub of A,Al equals
(@S`2)*v;
coherence;
end;
theorem Th3:
S is Al-Sub_VERUM implies CQC_Sub(S) = VERUM(Al)
proof
ex F being Function of QC-Sub-WFF(Al),QC-WFF(Al) st CQC_Sub(S) = F.S & for S9
being Element of QC-Sub-WFF(Al) holds (S9 is Al-Sub_VERUM implies
F.S9 = VERUM(Al)) & ( 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
SUBSTUT1:def 38;
hence thesis;
end;
definition
let Al, S, A, v, J;
pred J,v |= S means
:Def2:
J,v |= S`1;
end;
theorem Th4:
S is Al-Sub_VERUM implies for v holds (J,v |= CQC_Sub(S) iff J,v.
Val_S(v,S) |= S)
proof
assume
A1: S is Al-Sub_VERUM;
let v;
ex Sub st S = [VERUM(Al),Sub] by A1,SUBSTUT1:def 19;
then S`1 = VERUM(Al);
then J,v.Val_S(v,S) |= VERUM(Al) iff J,v.Val_S(v,S) |= S;
hence J,v |= CQC_Sub(S) implies J,v.Val_S(v,S) |= S by VALUAT_1:32;
J,v.Val_S(v,S) |= S implies J,v |= VERUM(Al) by VALUAT_1:32;
hence thesis by A1,Th3;
end;
theorem Th5:
i in dom ll implies ll.i is bound_QC-variable of Al
proof
assume i in dom ll;
then
A1: ll.i in rng ll by FUNCT_1:3;
rng ll c= bound_QC-variables(Al) by RELAT_1:def 19;
hence thesis by A1;
end;
theorem Th6:
S is Sub_atomic implies CQC_Sub(S) = (the_pred_symbol_of S`1)!
CQC_Subst(Sub_the_arguments_of S,S`2)
proof
ex F being Function of QC-Sub-WFF(Al),QC-WFF(Al) st CQC_Sub(S) = F.S & for S9
being Element of QC-Sub-WFF(Al) holds (S9 is Al-Sub_VERUM implies F.S9 =
VERUM(Al)) & ( 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
SUBSTUT1:def 38;
hence thesis;
end;
theorem
Sub_the_arguments_of Sub_P(P,ll,Sub) = Sub_the_arguments_of Sub_P(P9,
ll9,Sub9) implies ll = ll9
proof
assume
A1: Sub_the_arguments_of Sub_P(P,ll,Sub) = Sub_the_arguments_of Sub_P(P9
,ll9,Sub9);
consider k1 being Nat, P1 being (QC-pred_symbol of k1,Al),
ll1 being QC-variable_list of k1,Al , e1 being Element of vSUB(Al) such that
A2: Sub_the_arguments_of Sub_P(P,ll,Sub) = ll1 and
A3: Sub_P(P,ll,Sub) = Sub_P(P1,ll1,e1) by SUBSTUT1:def 29;
A4: P!ll = <*P*>^ll & P1!ll1 = <*P1*>^ll1 by QC_LANG1:8;
Sub_P(P,ll,Sub) = [P!ll,Sub] by SUBSTUT1:9;
then [P!ll,Sub] = [P1!ll1,e1] by A3,SUBSTUT1:9;
then
A5: <*P1*>^ll1 = <*P*>^ll by A4,XTUPLE_0:1;
(<*P1*>^ll1).1 = P1 & (<*P*>^ll).1 = P by FINSEQ_1:41;
then
A6: ll1 = ll by A5,FINSEQ_1:33;
consider k2 being Nat, P2 being (QC-pred_symbol of k2,Al),
ll2 being QC-variable_list of k2,Al, e2 being Element of vSUB(Al) such that
A7: Sub_the_arguments_of Sub_P(P9,ll9,Sub9) = ll2 and
A8: Sub_P(P9,ll9,Sub9) = Sub_P(P2,ll2,e2) by SUBSTUT1:def 29;
A9: P9!ll9 = <*P9*>^ll9 & P2!ll2 = <*P2*>^ll2 by QC_LANG1:8;
Sub_P(P9,ll9,Sub9) = [P9!ll9,Sub9] by SUBSTUT1:9;
then [P9!ll9,Sub9] = [P2!ll2,e2] by A8,SUBSTUT1:9;
then
A10: <*P2*>^ll2 = <*P9*>^ll9 by A9,XTUPLE_0:1;
(<*P2*>^ll2).1 = P2 & (<*P9*>^ll9).1 = P9 by FINSEQ_1:41;
hence thesis by A1,A2,A7,A6,A10,FINSEQ_1:33;
end;
definition
let k, Al, P, ll, Sub;
redefine func Sub_P(P,ll,Sub) -> Element of CQC-Sub-WFF(Al); :: redefines Sub_P (SUBSTUT1, definition)
coherence
proof
set X = { G where G is Element of QC-Sub-WFF(Al) :
G`1 is Element of CQC-WFF(Al) };
X = CQC-Sub-WFF(Al) by SUBSTUT1:def 39;
then A1: for G being Element of QC-Sub-WFF(Al) holds
G`1 is Element of CQC-WFF(Al) implies G in CQC-Sub-WFF(Al);
Sub_P(P,ll,Sub) = [P!ll,Sub] by SUBSTUT1:9;
then Sub_P(P,ll,Sub)`1 = P!ll & P!ll in CQC-WFF(Al);
hence thesis by A1;
end;
end;
theorem Th8:
CQC_Sub(Sub_P(P,ll,Sub)) = P!CQC_Subst(ll,Sub)
proof
A1: P!ll is atomic by QC_LANG1:def 18;
A2: Sub_P(P,ll,Sub) = [P!ll,Sub] by SUBSTUT1:9;
then
A3: Sub_P(P,ll,Sub)`2 = Sub;
Sub_P(P,ll,Sub)`1 = P!ll by A2;
then
Sub_the_arguments_of Sub_P(P,ll,Sub) = ll & the_pred_symbol_of (Sub_P(P,
ll, Sub)`1) = P by A1,QC_LANG1:def 22,SUBSTUT1:def 29;
hence thesis by A3,Th6;
end;
theorem
P!CQC_Subst(ll,Sub) is Element of CQC-WFF(Al)
proof
CQC_Sub(Sub_P(P,ll,Sub)) = P!CQC_Subst(ll,Sub) by Th8;
hence thesis;
end;
theorem Th10:
CQC_Subst(ll,Sub) is CQC-variable_list of k,Al
proof
reconsider ll as FinSequence of bound_QC-variables(Al) by SUBSTUT1:34;
reconsider s = CQC_Subst(ll,Sub) as FinSequence of bound_QC-variables(Al);
A1: s = CQC_Subst(@ll,Sub) by SUBSTUT1:def 5;
len ll = k by CARD_1:def 7;
then len @ll = k by SUBSTUT1:def 4;
then len s = k by A1,SUBSTUT1:def 3;
then s is CQC-variable_list of k,Al by SUBSTUT1:34;
hence thesis by A1,SUBSTUT1:def 4;
end;
registration
let Al;
let k, ll, Sub;
cluster CQC_Subst(ll,Sub) -> bound_QC-variables(Al) -valued k-element;
coherence by Th10;
end;
theorem Th11:
not x in dom S`2 implies (v.Val_S(v,S)).x = v.x
proof
assume not x in dom(S`2);
then
A1: not x in dom @S`2 by SUBSTUT1:def 2;
dom(@S`2*v) c= dom(@S`2) by RELAT_1:25;
then not x in dom Val_S(v,S) by A1;
hence thesis by FUNCT_4:11;
end;
theorem Th12:
x in dom S`2 implies (v.Val_S(v,S)).x = Val_S(v,S).x
proof
assume x in dom S`2;
then
A1: x in dom @S`2 by SUBSTUT1:def 2;
rng @S`2 c= bound_QC-variables(Al) & dom v = bound_QC-variables(Al)
by FUNCT_2:def 1;
then x in dom Val_S(v,S) by A1,RELAT_1:27;
hence thesis by FUNCT_4:13;
end;
theorem Th13:
(v.Val_S(v,Sub_P(P,ll,Sub)))*'ll = v*'(CQC_Subst(ll,Sub))
proof
set S9 = Sub_P(P,ll,Sub);
set ll9 = CQC_Subst(ll,Sub);
A1: len ll = k by CARD_1:def 7;
S9 = [P!ll,Sub] by SUBSTUT1:9;
then
A2: (S9)`2 = Sub;
A3: len ((v.Val_S(v,S9))*'ll) = k by VALUAT_1:def 3;
then
A4: dom ((v.Val_S(v,S9))*'ll) = Seg k by FINSEQ_1:def 3;
A5: for j be Nat st j in dom
((v.Val_S(v,S9))*'ll) holds (v.Val_S(v,S9))*'ll
.j = v*'(CQC_Subst(ll,Sub)).j
proof
let j be Nat such that
A6: j in dom ((v.Val_S(v,S9))*'ll);
A7: 1 <= j & j <= k by A4,A6,FINSEQ_1:1;
reconsider j as Nat;
j in Seg (len ll) by A4,A6,CARD_1:def 7;
then j in dom ll by FINSEQ_1:def 3;
then reconsider x = ll.j as bound_QC-variable of Al by Th5;
A8: now
assume
A9: ll.j in dom Sub;
then
(v.Val_S(v,S9)).(ll.j) = Val_S(v,S9).x & ll.j in dom @(S9)`2 by A2,Th12,
SUBSTUT1:def 2;
then (v.Val_S(v,S9)).(ll.j) = v.((@(S9)`2).(ll.j)) by FUNCT_1:13;
then
A10: (v.Val_S(v,S9)).(ll.j) = v.(((S9)`2).(ll.j)) by SUBSTUT1:def 2;
A11: ((v.Val_S(v,S9))*'ll).j = (v.Val_S(v,S9)).(ll.j) by A7,VALUAT_1:def 3;
v.(ll9.j) = v.(((S9)`2).(ll.j)) by A2,A1,A7,A9,SUBSTUT1:def 3;
hence thesis by A7,A10,A11,VALUAT_1:def 3;
end;
now
assume not ll.j in dom Sub;
then
A12: v.(ll9.j) = v.(ll.j) & (v.Val_S(v,S9)).(ll.j) = v.x by A2,A1,A7,Th11,
SUBSTUT1:def 3;
(v*'ll9).j = v.(ll9.j) by A7,VALUAT_1:def 3;
hence thesis by A7,A12,VALUAT_1:def 3;
end;
hence thesis by A8;
end;
len (v*'ll9) = k by VALUAT_1:def 3;
hence thesis by A3,A5,FINSEQ_2:9;
end;
theorem Th14:
Sub_P(P,ll,Sub)`1 = P!ll
proof
Sub_P(P,ll,Sub) = [P!ll,Sub] by SUBSTUT1:9;
hence thesis;
end;
theorem Th15:
for v holds (J,v |= CQC_Sub(Sub_P(P,ll,Sub)) iff J,v.Val_S(v,
Sub_P(P,ll,Sub)) |= Sub_P(P,ll,Sub))
proof
set S9 = Sub_P(P,ll,Sub);
set ll9 = CQC_Subst(ll,Sub);
reconsider p = P!ll9 as Element of CQC-WFF(Al);
reconsider ll9 as CQC-variable_list of k,Al;
let v;
A1: Valid(p,J).v = TRUE iff v*'ll9 in J.P by VALUAT_1:7;
A2: (v.Val_S(v,S9))*'ll in J.P iff Valid(P!ll,J).((v.Val_S(v,S9))) = TRUE by
VALUAT_1:7;
A3: J,v.Val_S(v,S9) |= P!ll iff J,v.Val_S(v,S9) |= Sub_P(P,ll,Sub)`1 by Th14;
J,v |= CQC_Sub(Sub_P(P,ll,Sub)) iff J,v |= p by Th8;
hence thesis by A1,A2,A3,Th13,VALUAT_1:def 7;
end;
theorem Th16:
(Sub_not S)`1 = 'not' S`1 & (Sub_not S)`2 = S`2
proof
Sub_not S = ['not' S`1,S`2] by SUBSTUT1:def 20;
hence thesis;
end;
definition
let Al,S;
redefine func Sub_not S -> Element of CQC-Sub-WFF(Al); :: redefines Sub_not (SUBSTUT1, definition)
coherence
proof
set X = { G where G is Element of QC-Sub-WFF(Al) :
G`1 is Element of CQC-WFF(Al) };
X = CQC-Sub-WFF(Al) by SUBSTUT1:def 39;
then A1: for G being Element of QC-Sub-WFF(Al) holds
G`1 is Element of CQC-WFF(Al) implies G in CQC-Sub-WFF(Al);
'not' S`1 in CQC-WFF(Al);
then (Sub_not S)`1 in CQC-WFF(Al) by Th16;
hence thesis by A1;
end;
end;
theorem Th17:
not J,v.Val_S(v,S) |= S iff J,v.Val_S(v,S) |= Sub_not S
proof
A1: not J,v.Val_S(v,S) |= S`1 iff J,v.Val_S(v,S) |= 'not' S`1 by VALUAT_1:17;
J,v.Val_S(v,S) |= 'not' S`1 iff J,v.Val_S(v,S) |= (Sub_not S)`1 by Th16;
hence thesis by A1;
end;
theorem Th18:
Val_S(v,S) = Val_S(v,Sub_not S)
proof
Sub_not S = ['not' S`1,S`2] by SUBSTUT1:def 20;
hence thesis;
end;
theorem Th19:
(for v holds (J,v |= CQC_Sub(S) iff J,v.Val_S(v,S) |= S))
implies for v holds (J,v |= CQC_Sub(Sub_not S) iff J,v.Val_S(v,Sub_not S) |=
Sub_not S)
proof
assume
A1: for v holds (J,v |= CQC_Sub(S) iff J,v.Val_S(v,S) |= S);
let v;
A2: J,v |= 'not' CQC_Sub(S) iff not J,v |= CQC_Sub(S) by VALUAT_1:17;
not J,v.Val_S(v,S) |= S iff J,v.Val_S(v,S) |= Sub_not S by Th17;
hence thesis by A1,A2,Th18,SUBSTUT1:29;
end;
definition
let Al, S1, S2;
assume
A1: S1`2 = S2`2;
func CQCSub_&(S1,S2) -> Element of CQC-Sub-WFF(Al) equals
:Def3:
Sub_&(S1,S2);
coherence
proof
set X = { G where G is Element of QC-Sub-WFF(Al) :
G`1 is Element of CQC-WFF(Al) };
X = CQC-Sub-WFF(Al) by SUBSTUT1:def 39;
then A2: for G being Element of QC-Sub-WFF(Al) holds
G`1 is Element of CQC-WFF(Al) implies G in CQC-Sub-WFF(Al);
Sub_&(S1,S2) = [(S1`1) '&' (S2`1),S1`2] by A1,SUBSTUT1:def 21;
then Sub_&(S1,S2)`1 = (S1`1) '&' (S2`1);
hence thesis by A2;
end;
end;
theorem Th20:
S1`2 = S2`2 implies CQCSub_&(S1,S2)`1 = (S1`1) '&' (S2`1) &
CQCSub_&(S1,S2)`2 = S1`2
proof
assume
A1: S1`2 = S2`2;
then Sub_&(S1,S2) = [(S1`1) '&' (S2`1),S1`2] by SUBSTUT1:def 21;
then CQCSub_&(S1,S2) = [(S1`1) '&' (S2`1),S1`2] by A1,Def3;
hence thesis;
end;
theorem Th21:
S1`2 = S2`2 implies CQCSub_&(S1,S2)`2 = S1`2
proof
assume
A1: S1`2 = S2`2;
then CQCSub_&(S1,S2) = Sub_&(S1,S2) by Def3;
then CQCSub_&(S1,S2) = [(S1`1) '&' (S2`1),S1`2] by A1,SUBSTUT1:def 21;
hence thesis;
end;
theorem
S1`2 = S2`2 implies Val_S(v,S1) = Val_S(v,CQCSub_&(S1,S2)) & Val_S(v,
S2) = Val_S(v,CQCSub_&(S1,S2)) by Th21;
theorem Th23:
S1`2 = S2`2 implies CQC_Sub(CQCSub_&(S1,S2)) = (CQC_Sub(S1)) '&'
(CQC_Sub(S2))
proof
assume
A1: S1`2 = S2`2;
then CQCSub_&(S1,S2) = Sub_&(S1,S2) by Def3;
hence thesis by A1,SUBSTUT1:31;
end;
theorem Th24:
S1`2 = S2`2 implies (J,v.Val_S(v,S1) |= S1 & J,v.Val_S(v,S2) |=
S2 iff J,v.Val_S(v,CQCSub_&(S1,S2)) |= CQCSub_&(S1,S2))
proof
assume
A1: S1`2 = S2`2;
then Val_S(v,S1) = Val_S(v,CQCSub_&(S1,S2)) by Th21;
then
A2: J,v.Val_S(v,S1) |= S1`1 & J,v.Val_S(v,S1) |= S2`1 iff J,v.Val_S(v,
CQCSub_&(S1,S2)) |= (S1`1) '&' (S2`1) by VALUAT_1:18;
J,v.Val_S(v,CQCSub_&(S1,S2)) |= (S1`1) '&' (S2`1) iff J,v.Val_S(v,
CQCSub_&(S1,S2)) |= CQCSub_&(S1,S2)`1 by A1,Th20;
hence thesis by A1,A2;
end;
theorem Th25:
S1`2 = S2`2 & (for v holds (J,v |= CQC_Sub(S1) iff J,v.Val_S(v,
S1) |= S1)) & (for v holds (J,v |= CQC_Sub(S2) iff J,v.Val_S(v,S2) |= S2))
implies for v holds (J,v |= CQC_Sub(CQCSub_&(S1,S2)) iff J,v.Val_S(v,CQCSub_&(
S1,S2)) |= CQCSub_&(S1,S2))
proof
assume that
A1: S1`2 = S2`2 and
A2: ( for v holds (J,v |= CQC_Sub(S1) iff J,v.Val_S(v,S1) |= S1))& for v
holds (J, v |= CQC_Sub(S2) iff J,v.Val_S(v,S2) |= S2);
let v;
A3: J,v |= (CQC_Sub(S1)) & J,v |= (CQC_Sub(S2)) iff J,v.Val_S(v,S1) |= S1 &
J,v.Val_S(v,S2) |= S2 by A2;
J,v |= CQC_Sub(CQCSub_&(S1,S2)) iff J,v |= (CQC_Sub(S1)) '&' (CQC_Sub(S2
)) by A1,Th23;
hence thesis by A1,A3,Th24,VALUAT_1:18;
end;
reserve B for Element of [:QC-Sub-WFF(Al),bound_QC-variables(Al):],
SQ for second_Q_comp of B;
theorem Th26:
B is quantifiable implies Sub_All(B,SQ)`1 = All(B`2,(B`1)`1) &
Sub_All(B,SQ)`2 = SQ
proof
assume B is quantifiable;
then Sub_All(B,SQ) = [All(B`2,(B`1)`1),SQ] by SUBSTUT1:def 24;
hence thesis;
end;
definition
let Al;
let B be Element of [:QC-Sub-WFF(Al),bound_QC-variables(Al):];
attr B is CQC-WFF-like means
:Def4:
B`1 in CQC-Sub-WFF(Al);
end;
registration
let Al;
cluster CQC-WFF-like for Element of [:QC-Sub-WFF(Al),
bound_QC-variables(Al):];
existence
proof
set Sub = the CQC_Substitution of Al,x =the bound_QC-variable of Al;
set B = [[VERUM(Al),Sub],x];
A1: VERUM(Al) = <*[0,0]*> by QC_LANG1:def 14;
A2: [<*[0, 0]*>,Sub] in QC-Sub-WFF(Al) by SUBSTUT1:def 16;
reconsider S = [VERUM(Al),Sub] as Element of QC-Sub-WFF(Al)
by A1,SUBSTUT1:def 16;
[VERUM(Al),Sub] in QC-Sub-WFF(Al) by A2,QC_LANG1:def 14;
then reconsider B as Element of [:QC-Sub-WFF(Al),bound_QC-variables(Al):]
by ZFMISC_1:87;
take B;
set X = { G where G is Element of QC-Sub-WFF(Al) :
G`1 is Element of CQC-WFF(Al) };
A3: X = CQC-Sub-WFF(Al) by SUBSTUT1:def 39;
S`1 is Element of CQC-WFF(Al);
then S in CQC-Sub-WFF(Al) by A3;
then B`1 in CQC-Sub-WFF(Al);
hence thesis;
end;
end;
definition
let Al, S, x;
redefine func [S,x] -> CQC-WFF-like Element of [:QC-Sub-WFF(Al), :: redefines [ (TARSKI, definition)
bound_QC-variables(Al):];
coherence
proof
[S,x]`1 = S;
hence thesis by Def4;
end;
end;
reserve B for CQC-WFF-like Element of [:QC-Sub-WFF(Al),
bound_QC-variables(Al):],
xSQ for second_Q_comp of [S,x],
SQ for second_Q_comp of B;
definition
let Al, B;
redefine func B`1 -> Element of CQC-Sub-WFF(Al); :: redefines `1 (XTUPLE_0, definition)
coherence by Def4;
end;
definition
let Al, B, SQ;
assume
A1: B is quantifiable;
func CQCSub_All(B,SQ) -> Element of CQC-Sub-WFF(Al) equals
:Def5:
Sub_All(B,SQ);
coherence
proof
set X = { G where G is Element of QC-Sub-WFF(Al) :
G`1 is Element of CQC-WFF(Al) };
X = CQC-Sub-WFF(Al) by SUBSTUT1:def 39;
then A2: for G being Element of QC-Sub-WFF(Al) holds
G`1 is Element of CQC-WFF(Al) implies G in CQC-Sub-WFF(Al);
All(B`2,(B`1)`1) in CQC-WFF(Al);
then Sub_All(B,SQ)`1 in CQC-WFF(Al) by A1,Th26;
hence thesis by A2;
end;
end;
theorem Th27:
B is quantifiable implies CQCSub_All(B,SQ) is Sub_universal
proof
assume
A1: B is quantifiable;
then Sub_All(B,SQ) is Sub_universal by SUBSTUT1:14;
hence thesis by A1,Def5;
end;
definition
let Al;
let S such that
A1: S is Sub_universal;
func CQCSub_the_scope_of S -> Element of CQC-Sub-WFF(Al) equals
:Def6:
Sub_the_scope_of S;
coherence
proof
consider B being Element of [:QC-Sub-WFF(Al),bound_QC-variables(Al):],
SQ being second_Q_comp of B such that
A2: S = Sub_All(B,SQ) and
A3: B`1 = Sub_the_scope_of S and
A4: B is quantifiable by A1,SUBSTUT1:def 34;
set X = { G where G is Element of QC-Sub-WFF(Al) :
G`1 is Element of CQC-WFF(Al) };
X = CQC-Sub-WFF(Al) by SUBSTUT1:def 39;
then A5: for G being Element of QC-Sub-WFF(Al) holds
G`1 is Element of CQC-WFF(Al) implies G in CQC-Sub-WFF(Al);
S`1 = All(B`2,(B`1)`1) by A2,A4,Th26;
then (B`1)`1 is Element of CQC-WFF(Al) by CQC_LANG:13;
hence thesis by A5,A3;
end;
end;
definition
let Al, S1, p;
assume that
A1: S1 is Sub_universal and
A2: p = CQC_Sub(CQCSub_the_scope_of S1);
func CQCQuant(S1,p) -> Element of CQC-WFF(Al) equals
:Def7:
Quant(S1,p);
coherence
proof
CQCSub_the_scope_of S1 = Sub_the_scope_of S1 by A1,Def6;
then CQC_Sub(S1) = Quant(S1,p) by A1,A2,SUBSTUT1:32;
hence thesis;
end;
end;
theorem Th28:
S is Sub_universal implies CQC_Sub(S) = CQCQuant(S,CQC_Sub(
CQCSub_the_scope_of S))
proof
assume
A1: S is Sub_universal;
then CQCSub_the_scope_of S = Sub_the_scope_of S by Def6;
then CQCQuant(S,CQC_Sub(CQCSub_the_scope_of S)) = Quant(S,CQC_Sub(
Sub_the_scope_of S)) by A1,Def7;
hence thesis by A1,SUBSTUT1:32;
end;
theorem Th29:
B is quantifiable implies CQCSub_the_scope_of(CQCSub_All(B,SQ)) = B`1
proof
assume
A1: B is quantifiable;
then
A2: CQCSub_All(B,SQ) = Sub_All(B,SQ) by Def5;
then CQCSub_All(B,SQ) is Sub_universal by A1,SUBSTUT1:14;
then
CQCSub_the_scope_of(CQCSub_All(B,SQ)) = Sub_the_scope_of(Sub_All(B,SQ))
by A2,Def6;
hence thesis by A1,SUBSTUT1:21;
end;
begin :: The Substitution Lemma
theorem Th30:
[S,x] is quantifiable implies CQCSub_the_scope_of(CQCSub_All([S,
x],xSQ)) = S & CQCQuant(CQCSub_All([S,x],xSQ),CQC_Sub(CQCSub_the_scope_of
CQCSub_All([S,x],xSQ))) = CQCQuant(CQCSub_All([S,x],xSQ),CQC_Sub(S))
proof
assume [S,x] is quantifiable;
then CQCSub_the_scope_of(CQCSub_All([S,x],xSQ)) = [S,x]`1 by Th29;
hence thesis;
end;
theorem Th31:
[S,x] is quantifiable implies CQCQuant(CQCSub_All([S,x],xSQ),
CQC_Sub(S)) = All(S_Bound(@CQCSub_All([S,x],xSQ)),CQC_Sub(S))
proof
set S1 = CQCSub_All([S,x],xSQ);
set p = CQC_Sub(CQCSub_the_scope_of S1);
A1: Quant(S1,p) = All(S_Bound(@S1),p) by SUBSTUT1:def 37;
assume
A2: [S,x] is quantifiable;
then CQCSub_All([S,x],xSQ) = Sub_All([S,x],xSQ) by Def5;
then CQCSub_All([S,x],xSQ) is Sub_universal by A2,SUBSTUT1:14;
then
A3: CQCQuant(S1,p) = Quant(S1,p) by Def7;
CQCQuant(S1,CQC_Sub(S)) = CQCQuant(S1,p) by A2,Th30;
hence thesis by A2,A3,A1,Th30;
end;
theorem
x in dom S`2 implies v.((@S`2).x) = v.Val_S(v,S).x
proof
assume x in dom S`2;
then v.Val_S(v,S).x = Val_S(v,S).x & x in dom @S`2 by Th12,SUBSTUT1:def 2;
hence thesis by FUNCT_1:13;
end;
theorem
x in dom (@S`2) implies (@S`2).x is bound_QC-variable of Al
proof
assume x in dom (@S`2);
then (@S`2).x in rng @S`2 by FUNCT_1:3;
hence thesis;
end;
theorem Th34:
[:QC-WFF(Al),vSUB(Al):] c= dom QSub(Al)
proof
let a be object;
assume a in [:QC-WFF(Al),vSUB(Al):];
then consider b,c being object such that
A1: b in QC-WFF(Al) and
A2: c in vSUB(Al) and
A3: a = [b,c] by ZFMISC_1:def 2;
reconsider Sub = c as CQC_Substitution of Al by A2;
reconsider p = b as Element of QC-WFF(Al) by A1;
A4: now
set b = {};
set a = [[p,Sub],b];
assume not p is universal;
then p,Sub PQSub b by SUBSTUT1:def 14;
then a in QSub(Al) by SUBSTUT1:def 15;
hence thesis by A3,FUNCT_1:1;
end;
now
set b = ExpandSub(bound_in p,the_scope_of p, RestrictSub(bound_in p,p,Sub)
);
set a = [[p,Sub],b];
assume p is universal;
then p,Sub PQSub b by SUBSTUT1:def 14;
then a in QSub(Al) by SUBSTUT1:def 15;
hence thesis by A3,FUNCT_1:1;
end;
hence thesis by A4;
end;
reserve B1 for Element of [:QC-Sub-WFF(Al),bound_QC-variables(Al):];
reserve SQ1 for second_Q_comp of B1;
theorem Th35:
B is quantifiable & B1 is quantifiable & Sub_All(B,SQ) = Sub_All
(B1,SQ1) implies B`2 = B1`2 & SQ = SQ1
proof
assume that
A1: B is quantifiable and
A2: B1 is quantifiable & Sub_All(B,SQ) = Sub_All(B1,SQ1);
Sub_All(B,SQ) = [All(B`2,(B`1)`1),SQ] by A1,SUBSTUT1:def 24;
then
A3: [All(B`2,(B`1)`1),SQ] = [All(B1`2,(B1`1)`1),SQ1] by A2,SUBSTUT1:def 24;
then All(B`2,(B`1)`1) = All(B1`2,(B1`1)`1) by XTUPLE_0:1;
hence thesis by A3,QC_LANG2:5,XTUPLE_0:1;
end;
theorem Th36:
B is quantifiable & B1 is quantifiable & CQCSub_All(B,SQ) =
Sub_All(B1,SQ1) implies B`2 = B1`2 & SQ = SQ1
proof
assume that
A1: B is quantifiable and
A2: B1 is quantifiable and
A3: CQCSub_All(B,SQ) = Sub_All(B1,SQ1);
Sub_All(B,SQ) = Sub_All(B1,SQ1) by A1,A3,Def5;
hence thesis by A1,A2,Th35;
end;
theorem
[S,x] is quantifiable implies Sub_the_bound_of CQCSub_All([S,x],xSQ) = x
proof
set S1 = CQCSub_All([S,x],xSQ);
assume
A1: [S,x] is quantifiable;
then S1 = Sub_All([S,x],xSQ) by Def5;
then S1 is Sub_universal by A1,SUBSTUT1:14;
then consider B being Element of [:QC-Sub-WFF(Al),bound_QC-variables(Al):],
SQ being second_Q_comp of B such that
A2: S1 = Sub_All(B,SQ) and
A3: B`2 = Sub_the_bound_of S1 and
A4: B is quantifiable by SUBSTUT1:def 33;
[S,x]`2 = B`2 by A1,A2,A4,Th36;
hence thesis by A3;
end;
theorem Th38:
[S,x] is quantifiable & x in rng RestrictSub(x,All(x,S`1),xSQ)
implies not S_Bound(@CQCSub_All([S,x],xSQ)) in rng RestrictSub(x,All(x,S`1),xSQ
) & not S_Bound(@CQCSub_All([S,x],xSQ)) in Bound_Vars(S`1)
proof
set S1 = CQCSub_All([S,x],xSQ);
assume that
A1: [S,x] is quantifiable and
A2: x in rng RestrictSub(x,All(x,S`1),xSQ);
A3: S1 = Sub_All([S,x],xSQ) by A1,Def5;
then S1`1 = All([S,x]`2,([S,x]`1)`1) by A1,Th26;
then
A4: S1`1 = All(x,([S,x]`1)`1);
then
A5: bound_in S1`1 = x by QC_LANG2:7;
set finSub = RestrictSub(bound_in S1`1,S1`1,S1`2);
A6: Dom_Bound_Vars(the_scope_of S1`1) = {s : x.s in Bound_Vars(the_scope_of
S1`1)} by SUBSTUT1:def 9;
S1`2 = xSQ by A1,A3,Th26;
then
A7: finSub = RestrictSub(x,All(x,S`1),xSQ) by A4,A5;
set Y = Dom_Bound_Vars(the_scope_of S1`1) \/ Sub_Var(finSub);
set n = upVar(finSub,the_scope_of S1`1);
NSub(the_scope_of S1`1,finSub) = NAT \ Y by SUBSTUT1:def 11;
then reconsider X = NAT \ Y as non empty Subset of QC-symbols(Al);
A8: n in NSub(the_scope_of S1`1,finSub)
proof
upVar(finSub,the_scope_of S1`1) = the Element of
NSub(the_scope_of S1`1,finSub) by SUBSTUT1:def 12;
hence thesis;
end;
Dom_Bound_Vars(the_scope_of S1`1) c= Dom_Bound_Vars(the_scope_of S1`1)
\/ Sub_Var(finSub) & n in NAT\(Dom_Bound_Vars(the_scope_of S1`1)
\/ Sub_Var(finSub)) by A8,SUBSTUT1:def 11,XBOOLE_1:7;
then not n in Dom_Bound_Vars(the_scope_of S1`1) by XBOOLE_0:def 5;
then
A9: not x.n in Bound_Vars(the_scope_of S1`1) by A6;
S1`1 = All(x,S`1) by A4;
then
A10: not x.upVar(finSub,the_scope_of S1`1) in Bound_Vars(S`1) by A9,QC_LANG2:7;
Sub_Var(finSub) c= Y & n in NAT\(Dom_Bound_Vars(the_scope_of S1`1)
\/ Sub_Var(finSub)) by A8,SUBSTUT1:def 11,XBOOLE_1:7;
then
A11: not n in Sub_Var(finSub) by XBOOLE_0:def 5;
Sub_Var(finSub) = {s : x.s in rng finSub} by SUBSTUT1:def 10;
then
A12: not x.upVar(finSub,the_scope_of S1`1) in rng finSub by A11;
S1 = @S1 by SUBSTUT1:def 35;
hence thesis by A2,A5,A7,A12,A10,SUBSTUT1:def 36;
end;
theorem Th39:
[S,x] is quantifiable & not x in rng RestrictSub(x,All(x,S`1),
xSQ) implies not S_Bound(@CQCSub_All([S,x],xSQ)) in rng RestrictSub(x,All(x,S`1
),xSQ)
proof
set S1 = CQCSub_All([S,x],xSQ);
assume that
A1: [S,x] is quantifiable and
A2: not x in rng RestrictSub(x,All(x,S`1),xSQ);
A3: S1 = Sub_All([S,x],xSQ) by A1,Def5;
then
A4: S1`1 = All([S,x]`2,([S,x]`1)`1) by A1,Th26;
then
A5: S1`1 = All(x,([S,x]`1)`1);
set finSub = RestrictSub(bound_in S1`1,S1`1,S1`2);
A6: S1 = @S1 by SUBSTUT1:def 35;
S1`1 = All(x,([S,x]`1)`1) by A4;
then
A7: bound_in(S1`1) = x by QC_LANG2:7;
S1`2 = xSQ by A1,A3,Th26;
then not bound_in(S1`1) in rng finSub by A2,A7,A5;
hence thesis by A2,A7,A6,SUBSTUT1:def 36;
end;
theorem Th40:
[S,x] is quantifiable implies not S_Bound(@CQCSub_All([S,x],xSQ)
) in rng RestrictSub(x,All(x,S`1),xSQ)
proof
assume
A1: [S,x] is quantifiable;
then x in rng RestrictSub(x,All(x,S`1),xSQ) implies thesis by Th38;
hence thesis by A1,Th39;
end;
theorem Th41:
[S,x] is quantifiable implies S`2 = ExpandSub(x,S`1,RestrictSub(
x,All(x,S`1),xSQ))
proof
set Z = [All(x,S`1),xSQ];
set q = All(x,S`1);
assume [S,x] is quantifiable;
then
A1: ([S,x]`1)`2 = (QSub(Al)).[All([S,x]`2,([S,x]`1)`1),xSQ] by SUBSTUT1:def 23;
A2: Z in [:QC-WFF(Al),vSUB(Al):] by ZFMISC_1:def 2;
[:QC-WFF(Al),vSUB(Al):] c= dom QSub(Al) by Th34;
then [Z,([S,x]`1)`2] in QSub(Al) by A2,A1,FUNCT_1:1;
then [Z,S`2] in QSub(Al);
then consider p being QC-formula of Al,Sub1,b such that
A3: [Z,S`2] = [[p,Sub1],b] and
A4: p,Sub1 PQSub b by SUBSTUT1:def 15;
Z = [p,Sub1] by A3,XTUPLE_0:1;
then
A5: All(x,S`1) = p & xSQ = Sub1 by XTUPLE_0:1;
A6: q is universal by QC_LANG1:def 21;
then
A7: bound_in q = x by QC_LANG1:def 27;
S`2 = b by A3,XTUPLE_0:1;
then
S`2 = ExpandSub(bound_in q,the_scope_of q,RestrictSub(bound_in q,q, xSQ
)) by A4,A5,A6,SUBSTUT1:def 14;
hence thesis by A6,A7,QC_LANG1:def 28;
end;
theorem
still_not-bound_in VERUM(Al) c= Bound_Vars(VERUM(Al))
by QC_LANG3:3;
theorem Th43:
still_not-bound_in (P!ll) = Bound_Vars(P!ll)
proof
set l1 = the_arguments_of (P!ll);
A1: P!ll is atomic by QC_LANG1:def 18;
then consider
n being Nat, P9 being (QC-pred_symbol of n,Al), ll9 being
QC-variable_list of n,Al such that
A2: l1 = ll9 and
A3: P!ll = P9!ll9 by QC_LANG1:def 23;
Bound_Vars(P!ll) = Bound_Vars(l1) by A1,SUBSTUT1:3;
then
A4: Bound_Vars(P!ll) = { l1.i : 1 <= i & i <= len l1 & l1.i in
bound_QC-variables(Al)} by SUBSTUT1:def 7;
still_not-bound_in (P!ll) = still_not-bound_in ll by QC_LANG3:5;
then
A5: still_not-bound_in (P!ll) = variables_in(ll,bound_QC-variables(Al)) by
QC_LANG3:2;
A6: (<*P9*>^ll9).1 = P9 & (<*P*>^ll).1 = P by FINSEQ_1:41;
P!ll = <*P*>^ll & P9!ll9 = <*P9*>^ll9 by QC_LANG1:8;
then ll9 = ll by A3,A6,FINSEQ_1:33;
hence thesis by A4,A5,A2,QC_LANG3:def 1;
end;
theorem Th44:
still_not-bound_in (p) c= Bound_Vars(p) implies
still_not-bound_in ('not' p) c= Bound_Vars('not' p)
proof
'not' p is negative by QC_LANG1:def 19;
then Bound_Vars('not' p) = Bound_Vars(the_argument_of ('not' p)) by
SUBSTUT1:4;
then
A1: Bound_Vars('not' p) = Bound_Vars(p) by QC_LANG2:1;
assume still_not-bound_in (p) c= Bound_Vars(p);
hence thesis by A1,QC_LANG3:7;
end;
theorem Th45:
still_not-bound_in p c= Bound_Vars(p) & still_not-bound_in q c=
Bound_Vars(q) implies still_not-bound_in (p '&' q) c= Bound_Vars(p '&' q)
proof
A1: still_not-bound_in (p '&' q) = still_not-bound_in p \/
still_not-bound_in q by QC_LANG3:10;
p '&' q is conjunctive by QC_LANG1:def 20;
then Bound_Vars(p '&' q) = Bound_Vars(the_left_argument_of (p '&' q)) \/
Bound_Vars(the_right_argument_of (p '&' q)) by SUBSTUT1:5;
then
Bound_Vars(p '&' q) = Bound_Vars(p) \/ Bound_Vars(the_right_argument_of
(p '&' q)) by QC_LANG2:4;
then
A2: Bound_Vars(p '&' q) = Bound_Vars(p) \/ Bound_Vars(q) by QC_LANG2:4;
assume still_not-bound_in p c= Bound_Vars(p) & still_not-bound_in q c=
Bound_Vars(q );
hence thesis by A2,A1,XBOOLE_1:13;
end;
theorem Th46:
still_not-bound_in p c= Bound_Vars(p) implies still_not-bound_in
All(x,p) c= Bound_Vars(All(x,p))
proof
A1: still_not-bound_in All(x,p) = (still_not-bound_in p) \ {x} by QC_LANG3:12;
All(x,p) is universal by QC_LANG1:def 21;
then Bound_Vars(All(x,p)) = Bound_Vars(the_scope_of All(x,p)) \/ {bound_in
All(x,p)} by SUBSTUT1:6;
then Bound_Vars(All(x,p)) = Bound_Vars(p) \/ {bound_in All(x,p)} by
QC_LANG2:7;
then
Bound_Vars(p) \ {x} c= Bound_Vars(p) & Bound_Vars(p) c= Bound_Vars(All(x
,p)) by XBOOLE_1:7,36;
then
A2: Bound_Vars(p) \ {x} c= Bound_Vars(All(x,p));
assume still_not-bound_in p c= Bound_Vars(p);
then still_not-bound_in All(x,p) c= Bound_Vars(p) \ {x} by A1,XBOOLE_1:33;
hence thesis by A2;
end;
theorem Th47:
for p holds still_not-bound_in p c= Bound_Vars(p)
proof
defpred P[Element of QC-WFF(Al)] means still_not-bound_in
$1 c= Bound_Vars($1);
Bound_Vars(VERUM(Al)) = {} by SUBSTUT1:2;
then
A1: for p,q,x,k for l being CQC-variable_list of k,Al for P being
QC-pred_symbol of k,Al holds P[VERUM(Al)] & P[P!l] &
(P[p] implies P['not' p]) & (P[p] & P[q] implies P[p '&' q]) &
(P[p] implies P[All(x,p)]) by Th43,Th44,Th45,Th46,QC_LANG3:3;
thus for p holds P[p] from CQC_LANG:sch 1(A1);
end;
notation
let Al, A, x;
let a be Element of A;
synonym x|a for x .--> a;
end;
definition
let Al, A, x;
let a be Element of A;
redefine func x|a -> Val_Sub of A,Al; :: redefines | (SUBLEMMA, synonym) → .--> (FUNCOP_1, definition)
coherence
proof
dom(x .--> a) = {x} & rng(x .--> a) = {a} by FUNCOP_1:8;
hence thesis by RELSET_1:4;
end;
end;
reserve a for Element of A;
theorem Th48:
x <> b implies v.(x|a).b = v.b
proof
assume x <> b;
then not b in dom ({x} --> a) by TARSKI:def 1;
hence thesis by FUNCT_4:11;
end;
theorem Th49:
x = y implies v.(x|a).y = a
proof
assume
A1: x = y;
then y in {x} by TARSKI:def 1;
then
A2: y in dom (x .--> a);
(x .--> a).y = a by A1,FUNCOP_1:72;
hence thesis by A2,FUNCT_4:13;
end;
theorem Th50:
J,v |= All(x,p) iff for a holds J,v.(x|a) |= p
proof
thus J,v |= All(x,p) implies for a holds J,v.(x|a) |= p
proof
assume
A1: J,v |= All(x,p);
let a;
for y st x <> y holds v.(x|a).y = v.y by Th48;
hence thesis by A1,VALUAT_1:29;
end;
thus (for a holds J,v.(x|a) |= p) implies J,v |= All(x,p)
proof
assume
A2: for a holds J,v.(x|a) |= p;
for w st for y st x <> y holds w.y = v.y holds J,w |= p
proof
let w such that
A3: for y st x <> y holds w.y = v.y;
set c = w.x;
A4: for b being object st b in dom w holds w.b = v.(x|c).b
proof
let b be object;
assume b in dom w;
then reconsider y = b as bound_QC-variable of Al;
now
assume
A5: x <> y;
then w.y = v.y by A3;
hence thesis by A5,Th48;
end;
hence thesis by Th49;
end;
v.(x|c) is Element of Funcs(bound_QC-variables(Al),A) by VALUAT_1:def 1;
then
A6: ex f st v.(x|c) = f & dom f = bound_QC-variables(Al) & rng f c= A by
FUNCT_2:def 2;
w is Element of Funcs(bound_QC-variables(Al),A) by VALUAT_1:def 1;
then ex f st w = f & dom f = bound_QC-variables(Al) & rng f c= A by
FUNCT_2:def 2;
then v.(x|c) = w by A4,A6,FUNCT_1:2;
hence thesis by A2;
end;
hence thesis by VALUAT_1:29;
end;
end;
definition
let Al, S, x, xSQ, A, v;
func NEx_Val(v,S,x,xSQ) -> Val_Sub of A,Al equals
(@RestrictSub(x,All(x,S`1),
xSQ))*v;
coherence;
end;
definition
let Al, A;
let v,w be Val_Sub of A,Al;
redefine func v+*w -> Val_Sub of A,Al; :: redefines +* (FUNCT_4, definition)
coherence
proof
dom (v+*w) = dom v \/ dom w & rng (v+*w) c= A by FUNCT_4:def 1 ;
hence thesis;
end;
end;
theorem Th51:
[S,x] is quantifiable & x in rng RestrictSub(x,All(x,S`1),xSQ)
implies S_Bound(@CQCSub_All([S,x],xSQ)) = x.upVar(RestrictSub(x,All(x,S`1),xSQ)
,S`1)
proof
set S1 = CQCSub_All([S,x],xSQ);
assume that
A1: [S,x] is quantifiable and
A2: x in rng RestrictSub(x,All(x,S`1),xSQ);
A3: S1 = Sub_All([S,x],xSQ) by A1,Def5;
then
A4: S1`2 = xSQ by A1,Th26;
A5: S1`1 = All([S,x]`2,([S,x]`1)`1) by A1,A3,Th26;
then
A6: S1`1 = All(x,([S,x]`1)`1);
then
A7: S1`1 = All(x,S`1) & x = bound_in S1`1 by QC_LANG2:7;
set finSub = RestrictSub(bound_in S1`1,S1`1,S1`2);
A8: @S1 = S1 by SUBSTUT1:def 35;
S1`1 = All(x,([S,x]`1)`1) by A5;
then bound_in(S1`1) = x by QC_LANG2:7;
then bound_in(S1`1) in rng finSub by A2,A4,A6;
then S_Bound(@S1) = x.upVar(finSub,the_scope_of S1`1) by A8,SUBSTUT1:def 36;
hence thesis by A4,A7,QC_LANG2:7;
end;
theorem Th52:
[S,x] is quantifiable & not x in rng RestrictSub(x,All(x,S`1),
xSQ) implies S_Bound(@CQCSub_All([S,x],xSQ)) = x
proof
set S1 = CQCSub_All([S,x],xSQ);
assume that
A1: [S,x] is quantifiable and
A2: not x in rng RestrictSub(x,All(x,S`1),xSQ);
A3: S1 = Sub_All([S,x],xSQ) by A1,Def5;
then
A4: S1`1 = All([S,x]`2,([S,x]`1)`1) by A1,Th26;
then
A5: S1`1 = All(x,([S,x]`1)`1);
set finSub = RestrictSub(bound_in S1`1,S1`1,S1`2);
A6: @S1 = S1 by SUBSTUT1:def 35;
S1`1 = All(x,([S,x]`1)`1) by A4;
then
A7: bound_in(S1`1) = x by QC_LANG2:7;
S1`2 = xSQ by A1,A3,Th26;
then not bound_in(S1`1) in rng finSub by A2,A7,A5;
hence thesis by A7,A6,SUBSTUT1:def 36;
end;
theorem Th53:
[S,x] is quantifiable implies for a holds Val_S(v.((S_Bound(@
CQCSub_All([S,x],xSQ)))|a),S) = NEx_Val(v.((S_Bound(@CQCSub_All([S,x],xSQ)))|a)
,S,x,xSQ)+*(x|a) & dom RestrictSub(x,All(x,S`1),xSQ) misses {x}
proof
assume
A1: [S,x] is quantifiable;
set finSub = RestrictSub(x,All(x,S`1),xSQ);
let a;
set S1 = CQCSub_All([S,x],xSQ);
set z = S_Bound(@S1);
A2: S`2 = ExpandSub(x,S`1,RestrictSub(x,All(x,S`1),xSQ)) by A1,Th41;
A3: now
reconsider F = {[x,x]} as Function;
assume
A4: not x in rng finSub;
then S`2 = finSub \/ F by A2,SUBSTUT1:def 13;
then
A5: @S`2 = finSub \/ F by SUBSTUT1:def 2;
A6: now
set q = All(x,S`1);
set X = {y1 : y1 in still_not-bound_in q & y1 is Element of dom xSQ & y1
<> x & y1 <> xSQ.y1};
assume not dom finSub misses {x};
then dom finSub /\ {x} <> {};
then consider b being object such that
A7: b in dom finSub /\ {x} by XBOOLE_0:def 1;
finSub = xSQ|X by SUBSTUT1:def 6;
then finSub = (@xSQ)|X by SUBSTUT1:def 2;
then @finSub = (@xSQ)|X by SUBSTUT1:def 2;
then dom @finSub = dom @xSQ /\ X by RELAT_1:61;
then
A8: dom @finSub c= X by XBOOLE_1:17;
b in dom finSub by A7,XBOOLE_0:def 4;
then b in dom @finSub by SUBSTUT1:def 2;
then b in X by A8;
then
A9: ex y st y = b & y in still_not-bound_in q & y is Element of dom xSQ
& y <> x & y <> xSQ.y;
b in {x} by A7,XBOOLE_0:def 4;
hence contradiction by A9,TARSKI:def 1;
end;
hence dom finSub misses {x};
dom {[x,x]} = {x} by RELAT_1:9;
then dom @finSub misses dom F by A6,SUBSTUT1:def 2;
then
A10: @finSub \/ F = (@finSub +* F) by FUNCT_4:31;
v.(z|a) is Element of Funcs(bound_QC-variables(Al),A) by VALUAT_1:def 1;
then
A11: ex f st v.(z|a) = f & dom f = bound_QC-variables(Al) & rng f c= A by
FUNCT_2:def 2;
A12: rng F = {x} by RELAT_1:9;
then dom (F*v.(z|a)) = dom F by A11,RELAT_1:27;
then
A13: dom (F*v.(z|a)) = {x} by RELAT_1:9;
A14: {[x,x]} = x .--> x by FUNCT_4:82;
for b being object st b in dom (x|a) holds (x|a).b = (F*v.(z|a)).b
proof
let b being object such that
A15: b in dom (x|a);
A16: (F*v.(z|a)).b = v.(z|a).(F.b) by A13,A15,FUNCT_1:12;
b = x by A15,TARSKI:def 1;
then (x|a).b = a & F.b = x by A14,FUNCOP_1:72;
hence thesis by A1,A4,A16,Th49,Th52;
end;
then
A17: (x|a) = (F*v.(z|a)) by A13,FUNCT_1:2;
(@finSub +* F)* v.(z|a) = (@finSub*v.(z|a)) +* (F*v.(z|a)) by A11,A12,
FUNCT_7:9;
hence Val_S(v.(z|a),S) = NEx_Val(v.(z|a),S,x,xSQ) +* (x|a) by A10,A5,A17,
SUBSTUT1:def 2;
end;
now
reconsider F = {[x,x.upVar(finSub,S`1)]} as Function;
assume
A18: x in rng finSub;
A19: now
set q = All(x,S`1);
set X = {y1 : y1 in still_not-bound_in q & y1 is Element of dom xSQ & y1
<> x & y1 <> xSQ.y1};
assume dom finSub meets {x};
then consider b being object such that
A20: b in dom finSub and
A21: b in {x} by XBOOLE_0:3;
finSub = xSQ|X by SUBSTUT1:def 6;
then finSub = (@xSQ)|X by SUBSTUT1:def 2;
then @finSub = (@xSQ)|X by SUBSTUT1:def 2;
then dom @finSub = dom @xSQ /\ X by RELAT_1:61;
then
A22: dom @finSub c= X by XBOOLE_1:17;
b in dom @finSub by A20,SUBSTUT1:def 2;
then b in X by A22;
then ex y st y = b & y in still_not-bound_in q & y is Element of dom xSQ
& y <> x & y <> xSQ.y;
hence contradiction by A21,TARSKI:def 1;
end;
hence dom finSub misses {x};
dom {[x,x.upVar(finSub,S`1)]} = {x} by RELAT_1:9;
then dom @finSub misses dom F by A19,SUBSTUT1:def 2;
then
A23: @finSub \/ F = (@finSub +* F) by FUNCT_4:31;
v.(z|a) is Element of Funcs(bound_QC-variables(Al),A) by VALUAT_1:def 1;
then
A24: ex f st v.(z|a) = f & dom f = bound_QC-variables(Al) & rng f c= A by
FUNCT_2:def 2;
rng F = {x.upVar(finSub,S`1)} by RELAT_1:9;
then dom (F*v.(z|a)) = dom F by A24,RELAT_1:27;
then
A25: dom (F*v.(z|a)) = {x} by RELAT_1:9;
A26: {[x,x.upVar(finSub,S`1)]} = x .--> x.upVar(finSub,S`1) by FUNCT_4:82;
for b being object st b in dom (x|a) holds (x|a).b = (F*v.(z|a)).b
proof
let b being object such that
A27: b in dom (x|a);
A28: (F*v.(z|a)).b = (v.(z|a)).(F.b) by A25,A27,FUNCT_1:12;
b = x by A27,TARSKI:def 1;
then (x|a).b = a & F.b = x.upVar(finSub,S`1) by A26,FUNCOP_1:72;
hence thesis by A1,A18,A28,Th49,Th51;
end;
then
A29: (x|a) = (F*v.(z|a)) by A25,FUNCT_1:2;
rng F = {x.upVar(finSub,S`1)} by RELAT_1:9;
then
A30: (@finSub +* F)*v.(z|a) = (@finSub*v.(z|a)) +* (F*v.(z|a)) by A24,FUNCT_7:9
;
S`2 = finSub \/ F by A2,A18,SUBSTUT1:def 13;
then @S`2 = finSub \/ F by SUBSTUT1:def 2;
hence Val_S(v.(z|a),S) = NEx_Val(v.(z|a),S,x,xSQ) +* (x|a) by A23,A30,A29,
SUBSTUT1:def 2;
end;
hence thesis by A3;
end;
theorem Th54:
[S,x] is quantifiable implies ((for a holds J,(v.((S_Bound(@
CQCSub_All([S,x],xSQ)))|a)). Val_S(v.((S_Bound(@CQCSub_All([S,x],xSQ)))|a),S)
|= S) iff for a holds J,(v.((S_Bound(@CQCSub_All([S,x],xSQ)))|a)). (NEx_Val(v.(
(S_Bound(@CQCSub_All([S,x],xSQ)))|a),S,x,xSQ)+*(x|a)) |= S)
proof
set S1 = CQCSub_All([S,x],xSQ);
set z = S_Bound(@S1);
assume
A1: [S,x] is quantifiable;
thus (for a holds J,(v.(z|a)).Val_S(v.(z|a),S) |= S) implies for a holds J,(
v.(z|a)).(NEx_Val(v.(z|a),S,x,xSQ)+*(x|a)) |= S
proof
assume
A2: for a holds J,(v.(z|a)).Val_S(v.(z|a),S) |= S;
let a;
Val_S(v.(z|a),S) = NEx_Val(v.(z|a),S,x,xSQ)+*(x|a) by A1,Th53;
hence thesis by A2;
end;
thus (for a holds J,(v.(z|a)).(NEx_Val(v.(z|a),S,x,xSQ)+*(x|a)) |= S)
implies for a holds J,(v.(z|a)).Val_S(v.(z|a),S) |= S
proof
assume
A3: for a holds J,(v.(z|a)).(NEx_Val(v.(z|a),S,x,xSQ)+*(x|a)) |= S;
let a;
Val_S(v.(z|a),S) = NEx_Val(v.(z|a),S,x,xSQ)+*(x|a) by A1,Th53;
hence thesis by A3;
end;
end;
theorem Th55:
[S,x] is quantifiable implies for a holds NEx_Val(v.((S_Bound(@
CQCSub_All([S,x],xSQ)))|a),S,x,xSQ) = NEx_Val(v,S,x,xSQ)
proof
assume
A1: [S,x] is quantifiable;
set finSub = RestrictSub(x,All(x,S`1),xSQ);
set NF1 = NEx_Val(v,S,x,xSQ);
set S1 = CQCSub_All([S,x],xSQ);
let a;
set z = S_Bound(@S1);
set NF = NEx_Val(v.(z|a),S,x,xSQ);
v is Element of Funcs(bound_QC-variables(Al),A) by VALUAT_1:def 1;
then ex f st v = f & dom f = bound_QC-variables(Al) & rng f c= A
by FUNCT_2:def 2;
then rng @finSub c= dom v;
then
A2: dom NF1 = dom @finSub by RELAT_1:27;
v.(z|a) is Element of Funcs(bound_QC-variables(Al),A) by VALUAT_1:def 1;
then ex f st v.(z|a) = f & dom f = bound_QC-variables(Al) & rng f c= A by
FUNCT_2:def 2;
then
A3: rng @finSub c= dom (v.(z|a));
then
A4: dom NF = dom @finSub by RELAT_1:27;
for b being object st b in dom NF holds NF.b = NF1.b
proof
let b being object such that
A5: b in dom NF;
A6: @finSub.b in rng @finSub by A4,A5,FUNCT_1:3;
then reconsider x = @finSub.b as bound_QC-variable of Al;
not z in rng finSub by A1,Th40;
then z <> x by A6,SUBSTUT1:def 2;
then
A7: v.(z|a).x = v.x by Th48;
NF.b = (v.(z|a)).x by A5,FUNCT_1:12;
hence thesis by A4,A2,A5,A7,FUNCT_1:12;
end;
hence thesis by A3,A2,FUNCT_1:2,RELAT_1:27;
end;
theorem Th56:
[S,x] is quantifiable implies ((for a holds J,(v.((S_Bound(@
CQCSub_All([S,x],xSQ)))|a)). (NEx_Val(v.((S_Bound(@CQCSub_All([S,x],xSQ)))|a),S
,x,xSQ)+*(x|a)) |= S) iff for a holds J,(v.((S_Bound(@CQCSub_All([S,x],xSQ)))|a
)). (NEx_Val(v,S,x,xSQ)+*(x|a)) |= S )
proof
set S1 = CQCSub_All([S,x],xSQ);
set z = S_Bound(@S1);
assume
A1: [S,x] is quantifiable;
thus (for a holds J,(v.(z|a)).(NEx_Val(v.(z|a),S,x,xSQ)+*(x|a)) |= S)
implies for a holds J,(v.(z|a)).(NEx_Val(v,S,x,xSQ)+*(x|a)) |= S
proof
assume
A2: for a holds J,(v.(z|a)).(NEx_Val(v.(z|a),S,x,xSQ)+*(x|a)) |= S;
let a;
NEx_Val(v.(z|a),S,x,xSQ) = NEx_Val(v,S,x,xSQ) by A1,Th55;
hence thesis by A2;
end;
thus (for a holds J,(v.(z|a)).(NEx_Val(v,S,x,xSQ)+*(x|a)) |= S) implies for
a holds J,(v.(z|a)).(NEx_Val(v.(z|a),S,x,xSQ)+*(x|a)) |= S
proof
assume
A3: for a holds J,(v.(z|a)).(NEx_Val(v,S,x,xSQ)+*(x|a)) |= S;
let a;
NEx_Val(v.(z|a),S,x,xSQ) = NEx_Val(v,S,x,xSQ) by A1,Th55;
hence thesis by A3;
end;
end;
begin :: The Coincidence Lemma
theorem Th57:
rng l1 c= bound_QC-variables(Al) implies still_not-bound_in l1 = rng l1
proof
A1: variables_in(l1,bound_QC-variables(Al)) = { l1.k : 1 <= k & k <= len l1 &
l1.k in bound_QC-variables(Al)} by QC_LANG3:def 1;
assume
A2: rng l1 c= bound_QC-variables(Al);
A3: rng l1 c= variables_in(l1,bound_QC-variables(Al))
proof
let b be object;
assume
A4: b in rng l1;
then consider k being Nat such that
A5: k in dom l1 and
A6: l1.k = b by FINSEQ_2:10;
k in Seg len l1 by A5,FINSEQ_1:def 3;
then 1 <= k & k <= len l1 by FINSEQ_1:1;
hence thesis by A2,A1,A4,A6;
end;
variables_in(l1,bound_QC-variables(Al)) c= rng l1
proof
let b be object;
assume b in variables_in(l1,bound_QC-variables(Al));
then consider k such that
A7: b = l1.k and
A8: 1 <= k & k <= len l1 and
l1.k in bound_QC-variables(Al) by A1;
k in Seg len l1 by A8,FINSEQ_1:1;
then k in dom l1 by FINSEQ_1:def 3;
hence thesis by A7,FUNCT_1:3;
end;
then variables_in(l1,bound_QC-variables(Al)) = rng l1 by A3;
hence thesis by QC_LANG3:2;
end;
theorem Th58:
dom v = bound_QC-variables(Al) & dom (x|a) = {x}
proof
v is Element of Funcs(bound_QC-variables(Al),A) by VALUAT_1:def 1;
then ex f st v = f & dom f = bound_QC-variables(Al) & rng f c= A
by FUNCT_2:def 2;
hence dom v = bound_QC-variables(Al);
thus thesis;
end;
theorem Th59:
v*'ll = ll*(v|still_not-bound_in ll)
proof
rng ll c= bound_QC-variables(Al) by RELAT_1:def 19;
then
A1: rng ll = still_not-bound_in ll by Th57;
dom (v|still_not-bound_in ll) = dom v /\ still_not-bound_in ll by RELAT_1:61;
then
dom (v|still_not-bound_in ll) = bound_QC-variables(Al) /\ still_not-bound_in
ll by Th58;
then rng ll = dom (v|still_not-bound_in ll) by A1,XBOOLE_1:28;
then
A2: dom (ll*(v|still_not-bound_in ll)) = dom ll by RELAT_1:27;
then
A3: dom (ll*(v|still_not-bound_in ll)) = Seg len ll by FINSEQ_1:def 3;
then reconsider f = ll*(v|still_not-bound_in ll) as FinSequence by
FINSEQ_1:def 2;
len f = len ll by A3,FINSEQ_1:def 3;
then
A4: len f = k by SUBSTUT1:34;
then
A5: dom f = Seg k by FINSEQ_1:def 3;
A6: for j be Nat st j in dom f holds f.j = (v*'ll).j
proof
A7: rng ll c= bound_QC-variables(Al) by RELAT_1:def 19;
let j be Nat such that
A8: j in dom f;
reconsider j as Nat;
ll.j in rng ll by A2,A8,FUNCT_1:3;
then ll.j in bound_QC-variables(Al) by A7;
then
A9: ll.j in dom v by Th58;
ll.j in still_not-bound_in ll by A1,A2,A8,FUNCT_1:3;
then ll.j in dom v /\ still_not-bound_in ll by A9,XBOOLE_0:def 4;
then
A10: (v|still_not-bound_in ll).(ll.j) = v.(ll.j) by FUNCT_1:48;
1 <= j & j <= k by A5,A8,FINSEQ_1:1;
then (v|still_not-bound_in ll).(ll.j) = (v*'ll).j by A10,VALUAT_1:def 3;
hence thesis by A2,A8,FUNCT_1:13;
end;
len (v*'ll) = k by VALUAT_1:def 3;
hence thesis by A4,A6,FINSEQ_2:9;
end;
theorem Th60:
for v,w holds (v|still_not-bound_in (P!ll) = w|
still_not-bound_in (P!ll) implies (J,v |= P!ll iff J,w |= P!ll))
proof
let v,w;
assume
A1: v|still_not-bound_in (P!ll) = w|still_not-bound_in (P!ll);
A2: still_not-bound_in (P!ll) = still_not-bound_in ll by QC_LANG3:5;
A3: w*'ll in J.P iff Valid(P!ll,J).w = TRUE by VALUAT_1:7;
A4: Valid(P!ll,J).v = TRUE iff v*'ll in J.P by VALUAT_1:7;
ll*(w|still_not-bound_in ll) in J.P iff w*'ll in J.P by Th59;
hence thesis by A1,A2,A4,A3,Th59,VALUAT_1:def 7;
end;
theorem Th61:
(for v,w holds v|still_not-bound_in p = w|still_not-bound_in p
implies (J,v |= p iff J,w |= p)) implies for v,w holds v|still_not-bound_in
'not' p = w|still_not-bound_in 'not' p implies (J,v |= 'not' p iff J,w |= 'not'
p)
proof
assume
A1: for v,w holds v|still_not-bound_in p = w|still_not-bound_in p
implies (J,v |= p iff J,w |= p);
let v,w;
A2: still_not-bound_in 'not' p = still_not-bound_in p by QC_LANG3:7;
assume v|still_not-bound_in 'not' p = w|still_not-bound_in 'not' p;
then not J,v |= p iff not J,w |= p by A1,A2;
hence thesis by VALUAT_1:17;
end;
theorem Th62:
(for v,w holds v|still_not-bound_in p = w|still_not-bound_in p
implies (J,v |= p iff J,w |= p)) & (for v,w holds v|still_not-bound_in q = w|
still_not-bound_in q implies (J,v |= q iff J,w |= q)) implies for v,w holds v|
still_not-bound_in p '&' q = w|still_not-bound_in p '&' q implies (J,v |= p '&'
q iff J,w |= p '&' q)
proof
assume
A1: ( for v,w holds v|still_not-bound_in p = w|still_not-bound_in p
implies ( J,v |= p iff J,w |= p))& for v,w holds v|still_not-bound_in q = w|
still_not-bound_in q implies (J,v |= q iff J,w |= q);
set X = (still_not-bound_in p) \/ (still_not-bound_in q);
let v,w;
A2: still_not-bound_in p '&' q = X by QC_LANG3:10;
assume v|still_not-bound_in p '&' q = w|still_not-bound_in p '&' q;
then
v|still_not-bound_in p = w|still_not-bound_in p & v|still_not-bound_in q
= w |still_not-bound_in q by A2,RELAT_1:153,XBOOLE_1:7;
then J,v |= p & J,v |= q iff J,w |= p & J,w |= q by A1;
hence thesis by VALUAT_1:18;
end;
theorem Th63:
for X being set st X c= bound_QC-variables(Al) holds dom (v|X) = dom
(v.(x|a)|X) & dom (v|X) = X
proof
let X be set;
A1: dom (v.(x|a)|X) = dom (v.(x|a)) /\ X by RELAT_1:61;
dom (v|X) = dom v /\ X by RELAT_1:61;
then
A2: dom (v|X) = bound_QC-variables(Al) /\ X by Th58;
assume X c= bound_QC-variables(Al);
hence thesis by A2,A1,Th58,XBOOLE_1:28;
end;
theorem
v|still_not-bound_in p = w|still_not-bound_in p implies v.(x|a)|
still_not-bound_in p = w.(x|a)|still_not-bound_in p
proof
assume
A1: v|still_not-bound_in p = w|still_not-bound_in p;
dom (v|still_not-bound_in p) = dom (v.(x|a)|still_not-bound_in p) by Th63;
then
A2: dom (v.(x|a)|still_not-bound_in p) = dom (w.(x|a)|still_not-bound_in p)
by A1,Th63;
for b being object
st b in dom (v.(x|a)|still_not-bound_in p) holds (v.(x|a)|
still_not-bound_in p).b = (w.(x|a)|still_not-bound_in p).b
proof
let b being object such that
A3: b in dom (v.(x|a)|still_not-bound_in p);
A4: (v.(x|a)|still_not-bound_in p).b = v.(x|a).b & (w.(x|a)|
still_not-bound_in p ).b = w.(x|a).b by A2,A3,FUNCT_1:47;
b in dom (v|still_not-bound_in p) by A3,Th63;
then
A5: (v|still_not-bound_in p).b = v.b by FUNCT_1:47;
b in dom (w|still_not-bound_in p) by A1,A3,Th63;
then
A6: v.b = w.b by A1,A5,FUNCT_1:47;
A7: now
assume
A8: b <> x;
then v.(x|a).b = v.b by Th48;
hence thesis by A4,A6,A8,Th48;
end;
now
assume
A9: b = x;
then v.(x|a).b = a by Th49;
hence thesis by A4,A9,Th49;
end;
hence thesis by A7;
end;
hence thesis by A2,FUNCT_1:2;
end;
theorem
still_not-bound_in p c= still_not-bound_in (All(x,p)) \/ {x}
proof
set X = (still_not-bound_in p) \ {x};
still_not-bound_in All(x,p) = X & {x} \/ X = {x} \/ (still_not-bound_in
p) by QC_LANG3:12,XBOOLE_1:39;
hence thesis by XBOOLE_1:7;
end;
theorem Th66:
v|(still_not-bound_in p \ {x}) = w|(still_not-bound_in p \ {x})
implies v.(x|a)|still_not-bound_in p = w.(x|a)|still_not-bound_in p
proof
A1: dom (w.(x|a)|still_not-bound_in p) = still_not-bound_in p by Th63;
then
A2: dom (v.(x|a)|still_not-bound_in p) = dom (w.(x|a)|still_not-bound_in p)
by Th63;
assume
A3: v|(still_not-bound_in p \ {x}) = w|(still_not-bound_in p \ {x});
for b being object
st b in dom (v.(x|a)|still_not-bound_in p) holds (v.(x|a)|
still_not-bound_in p).b = (w.(x|a)|still_not-bound_in p).b
proof
let b being object such that
A4: b in dom (v.(x|a)|still_not-bound_in p);
A5: (v.(x|a)|still_not-bound_in p).b = v.(x|a).b & (w.(x|a)|
still_not-bound_in p ).b = w.(x|a).b by A2,A4,FUNCT_1:47;
A6: now
assume
A7: b <> x;
then
A8: not b in {x} by TARSKI:def 1;
b in still_not-bound_in p by A4,Th63;
then
A9: b in still_not-bound_in p \ {x} by A8,XBOOLE_0:def 5;
then b in dom (w|(still_not-bound_in p \ {x})) by Th63;
then
A10: w|(still_not-bound_in p \ {x}).b = w.b by FUNCT_1:47;
A11: v.(x|a).b = v.b & w.(x|a).b = w.b by A7,Th48;
b in dom (v|(still_not-bound_in p \ {x})) by A9,Th63;
hence thesis by A3,A5,A10,A11,FUNCT_1:47;
end;
now
A12: w.(x|a)|(still_not-bound_in p).b = w.(x|a).b by A2,A4,FUNCT_1:47;
assume
A13: b = x;
v.(x|a)|(still_not-bound_in p).b = v.(x|a).b by A4,FUNCT_1:47;
then v.(x|a)|(still_not-bound_in p).b = a by A13,Th49;
hence thesis by A13,A12,Th49;
end;
hence thesis by A6;
end;
hence thesis by A1,Th63,FUNCT_1:2;
end;
theorem Th67:
(for v,w holds v|still_not-bound_in p = w|still_not-bound_in p
implies (J,v |= p iff J,w |= p)) implies for v,w holds v|still_not-bound_in All
(x,p) = w|still_not-bound_in All(x,p) implies (J,v |= All(x,p) iff J,w |= All(x
,p))
proof
assume
A1: for v,w holds (v|still_not-bound_in p = w|still_not-bound_in p
implies (J,v |= p iff J,w |= p));
set X = (still_not-bound_in p) \ {x};
let v,w;
A2: v|still_not-bound_in All(x,p) = v|X by QC_LANG3:12;
assume v|still_not-bound_in All(x,p) = w|still_not-bound_in All(x,p);
then
A3: v|X = w|X by A2,QC_LANG3:12;
A4: (for a holds J,w.(x|a) |= p) implies for a holds J,v.(x|a) |= p
proof
assume
A5: for a holds J,w.(x|a) |= p;
let a;
v.(x|a)|still_not-bound_in p = w.(x|a)|still_not-bound_in p by A3,Th66;
then J,v.(x|a) |= p iff J,w.(x|a) |= p by A1;
hence thesis by A5;
end;
(for a holds J,v.(x|a) |= p) implies for a holds J,w.(x|a) |= p
proof
assume
A6: for a holds J,v.(x|a) |= p;
let a;
v.(x|a)|still_not-bound_in p = w.(x|a)|still_not-bound_in p by A3,Th66;
then J,v.(x|a) |= p iff J,w.(x|a) |= p by A1;
hence thesis by A6;
end;
hence thesis by A4,Th50;
end;
:: Coincidence Lemma (Ebb et al, Chapter III, 5.1)
theorem Th68:
for p holds for v,w holds v|still_not-bound_in p = w|
still_not-bound_in p implies (J,v |= p iff J,w |= p)
proof
defpred P[Element of CQC-WFF(Al)] means for v,w holds v|still_not-bound_in
$1 = w|still_not-bound_in $1 implies (J,v |= $1 iff J,w |= $1);
A1: for p,q,x,k for l being CQC-variable_list of k,Al for P being
QC-pred_symbol of k,Al holds P[VERUM(Al)] & P[P!l] & (P[p] implies P['not' p])
& (P[p] & P[q] implies P[p '&' q]) & (P[p] implies P[All(x,p)])
by Th60,Th61,Th62,Th67,VALUAT_1:32;
thus for p holds P[p] from CQC_LANG:sch 1(A1);
end;
theorem Th69:
[S,x] is quantifiable implies (v.((S_Bound(@CQCSub_All([S,x],xSQ
)))|a)). (NEx_Val(v,S,x,xSQ)+*(x|a))|still_not-bound_in S`1 = (v.(NEx_Val(v,S,x
,xSQ)+*(x|a)))|still_not-bound_in S`1
proof
set S1 = CQCSub_All([S,x],xSQ);
set z = S_Bound(@S1);
set finSub = RestrictSub(x,All(x,S`1),xSQ);
set V1 = (v.(z|a)).(NEx_Val(v,S,x,xSQ)+*(x|a));
set V2 = v.(NEx_Val(v,S,x,xSQ)+*(x|a));
set X = still_not-bound_in S`1;
A1: dom V1 = dom (v.(z|a)) \/ dom (NEx_Val(v,S,x,xSQ)+*(x|a)) by FUNCT_4:def 1;
dom (v.(z|a)) = bound_QC-variables(Al) by Th58;
then dom (v.(z|a)) = dom v by Th58;
then
A2: dom V1 = dom V2 by A1,FUNCT_4:def 1;
assume
A3: [S,x] is quantifiable;
A4: now
assume not x in rng finSub;
then
A5: z = x by A3,Th52;
for b being object st b in dom V1 holds V1.b = V2.b
proof
let b being object such that
A6: b in dom V1;
A7: now
assume
A8: b <> z;
A9: now
A10: not b in dom (x|a) by A5,A8,TARSKI:def 1;
assume not b in dom NEx_Val(v,S,x,xSQ);
then not b in dom NEx_Val(v,S,x,xSQ) \/ dom (x|a) by A10,
XBOOLE_0:def 3;
then
A11: not b in dom (NEx_Val(v,S,x,xSQ)+*(x|a)) by FUNCT_4:def 1;
reconsider x = b as bound_QC-variable of Al by A6;
V1.b = (v.(z|a)).b by A11,FUNCT_4:11;
then V1.b = v.x by A8,Th48;
hence thesis by A11,FUNCT_4:11;
end;
now
dom (NEx_Val(v,S,x,xSQ)+*(x|a)) = dom NEx_Val(v,S,x,xSQ) \/ dom
(x|a) by FUNCT_4:def 1;
then
A12: dom NEx_Val(v,S,x,xSQ) c= dom (NEx_Val(v,S,x,xSQ)+*(x| a)) by
XBOOLE_1:7;
assume
A13: b in dom NEx_Val(v,S,x,xSQ);
then V1.b = (NEx_Val(v,S,x,xSQ)+*(x|a)).b by A12,FUNCT_4:13;
hence thesis by A13,A12,FUNCT_4:13;
end;
hence thesis by A9;
end;
now
assume b = z;
then b in {x} by A5,TARSKI:def 1;
then
A14: b in dom (x|a);
dom (NEx_Val(v,S,x,xSQ)+*(x|a)) = dom NEx_Val(v,S,x,xSQ) \/ dom (
x|a) by FUNCT_4:def 1;
then
A15: dom (x|a) c= dom (NEx_Val(v,S,x,xSQ)+*(x|a)) by XBOOLE_1:7;
then V1.b = (NEx_Val(v,S,x,xSQ)+*(x|a)).b by A14,FUNCT_4:13;
hence thesis by A14,A15,FUNCT_4:13;
end;
hence thesis by A7;
end;
hence thesis by A2,FUNCT_1:2;
end;
now
assume
A16: x in rng finSub;
A17: dom (V1|X) = (dom (v.(z|a)) \/ dom (NEx_Val(v,S,x,xSQ)+*(x|a))) /\ X
by A1,RELAT_1:61;
A18: for b being object st b in dom (V1|X) holds V1|X.b = V2|X.b
proof
A19: X c= Bound_Vars(S`1) by Th47;
let b being object such that
A20: b in dom (V1|X);
b in X by A17,A20,XBOOLE_0:def 4;
then
A21: b <> z by A3,A16,A19,Th38;
A22: V2|X = v|X +* (NEx_Val(v,S,x,xSQ)+*(x|a))|X by FUNCT_4:71;
A23: V1|X = (v.(z|a))|X +* (NEx_Val(v,S,x,xSQ)+*(x|a))|X by FUNCT_4:71;
then
A24: dom (V1|X) = dom (v.(z|a)|X) \/ dom ((NEx_Val(v,S,x,xSQ)+*(x|a))|X)
by FUNCT_4:def 1;
A25: now
assume
A26: not b in dom ((NEx_Val(v,S,x,xSQ)+*(x|a))|X);
then
A27: b in dom (v.(z|a)|X) by A20,A24,XBOOLE_0:def 3;
then b in dom (v.(z|a)) /\ X by RELAT_1:61;
then
A28: b in X by XBOOLE_0:def 4;
b in bound_QC-variables(Al) by A20;
then b in dom v by Th58;
then
A29: b in dom v /\ X by A28,XBOOLE_0:def 4;
V1|X.b = (v.(z|a))|X.b by A23,A26,FUNCT_4:11;
then V1|X.b = v.(z|a).b by A27,FUNCT_1:47;
then
A30: V1|X.b = v.b by A21,Th48;
V2|X.b = v|X.b by A22,A26,FUNCT_4:11;
hence thesis by A30,A29,FUNCT_1:48;
end;
now
assume
A31: b in dom ((NEx_Val(v,S,x,xSQ)+*(x|a))|X);
then V1|X.b = (NEx_Val(v,S,x,xSQ)+*(x|a))|X.b by A23,FUNCT_4:13;
hence thesis by A22,A31,FUNCT_4:13;
end;
hence thesis by A25;
end;
dom (V2|X) = dom (V1) /\ X by A2,RELAT_1:61;
hence thesis by A18,FUNCT_1:2,RELAT_1:61;
end;
hence thesis by A4;
end;
theorem Th70:
[S,x] is quantifiable implies ((for a holds J,(v.((S_Bound(@
CQCSub_All([S,x],xSQ)))|a)).(NEx_Val(v,S,x,xSQ)+*(x|a)) |= S) iff for a holds J
,v.(NEx_Val(v,S,x,xSQ)+*(x|a)) |= S )
proof
set S1 = CQCSub_All([S,x],xSQ);
set z = S_Bound(@S1);
assume
A1: [S,x] is quantifiable;
thus (for a holds J,(v.(z|a)).(NEx_Val(v,S,x,xSQ)+*(x|a)) |= S) implies for
a holds J,v.(NEx_Val(v,S,x,xSQ)+*(x|a)) |= S
proof
set X = still_not-bound_in S`1;
assume
A2: for a holds J,(v.(z|a)).(NEx_Val(v,S,x,xSQ)+*(x|a)) |= S;
let a;
set V1 = (v.(z|a)).(NEx_Val(v,S,x,xSQ)+*(x|a));
set V2 = v.(NEx_Val(v,S,x,xSQ)+*(x|a));
V1|X = V2|X by A1,Th69;
then
A3: J,V1 |= S`1 iff J,V2 |= S`1 by Th68;
J,V1 |= S by A2;
hence thesis by A3;
end;
thus (for a holds J,v.(NEx_Val(v,S,x,xSQ)+*(x|a)) |= S) implies for a holds
J,(v.(z|a)).(NEx_Val(v,S,x,xSQ)+*(x|a)) |= S
proof
set X = still_not-bound_in S`1;
assume
A4: for a holds J,v.(NEx_Val(v,S,x,xSQ)+*(x|a)) |= S;
let a;
set V1 = (v.(z|a)).(NEx_Val(v,S,x,xSQ)+*(x|a));
set V2 = v.(NEx_Val(v,S,x,xSQ)+*(x|a));
V1|X = V2|X by A1,Th69;
then
A5: J,V1 |= S`1 iff J,V2 |= S`1 by Th68;
J,V2 |= S by A4;
hence thesis by A5;
end;
end;
theorem Th71:
dom NEx_Val(v,S,x,xSQ) = dom RestrictSub(x,All(x,S`1),xSQ)
proof
rng (@RestrictSub(x,All(x,S`1),xSQ)) c= bound_QC-variables(Al);
then rng (@RestrictSub(x,All(x,S`1),xSQ)) c= dom v by Th58;
then dom NEx_Val(v,S,x,xSQ) = dom (@RestrictSub(x,All(x,S`1),xSQ)) by
RELAT_1:27;
hence thesis by SUBSTUT1:def 2;
end;
theorem Th72:
(for a holds J,v.(NEx_Val(v,S,x,xSQ)+*(x|a)) |= S) iff for a
holds J,(v.NEx_Val(v,S,x,xSQ)).(x|a) |= S
proof
thus (for a holds J,v.(NEx_Val(v,S,x,xSQ)+*(x|a)) |= S) implies for a holds
J,(v.NEx_Val(v,S,x,xSQ)).(x|a) |= S
proof
assume
A1: for a holds J,v.(NEx_Val(v,S,x,xSQ)+*(x|a)) |= S;
let a;
v.(NEx_Val(v,S,x,xSQ)+*(x|a)) = (v.NEx_Val(v,S,x,xSQ)).(x|a) by FUNCT_4:14;
hence thesis by A1;
end;
thus (for a holds J,(v.NEx_Val(v,S,x,xSQ)).(x|a) |= S) implies for a holds J
,v.(NEx_Val(v,S,x,xSQ)+*(x|a)) |= S
proof
assume
A2: for a holds J,(v.NEx_Val(v,S,x,xSQ)).(x|a) |= S;
let a;
v.(NEx_Val(v,S,x,xSQ)+*(x|a)) = (v.NEx_Val(v,S,x,xSQ)).(x|a) by FUNCT_4:14;
hence thesis by A2;
end;
end;
theorem Th73:
(for a holds J,(v.NEx_Val(v,S,x,xSQ)).(x|a) |= S) iff for a
holds J,(v.NEx_Val(v,S,x,xSQ)).(x|a) |= S`1
by Def2;
theorem Th74:
for v,vS,vS1,vS2 st (for y st y in dom vS1 holds not y in
still_not-bound_in ll) & (for y st y in dom vS2 holds vS2.y = v.y) & dom vS
misses dom vS2 holds (v.vS)*'ll = (v.(vS+*vS1+*vS2))*'ll
proof
let v,vS,vS1,vS2 such that
A1: for y st y in dom vS1 holds not y in still_not-bound_in ll and
A2: for y st y in dom vS2 holds vS2.y = v.y and
A3: dom vS misses dom vS2;
set ll2 = (v.(vS+*vS1+*vS2))*'ll;
set ll1 = (v.vS)*'ll;
A4: len ll1 = k by VALUAT_1:def 3;
then
A5: dom ll1 = Seg k by FINSEQ_1:def 3;
A6: len ll2 = k by VALUAT_1:def 3;
for i be Nat st i in dom ll1 holds ll1.i = ll2.i
proof
let i be Nat such that
A7: i in dom ll1;
A8: i in dom ll2 by A6,A5,A7,FINSEQ_1:def 3;
reconsider i as Nat;
A9: dom ll2 c= dom ll by RELAT_1:25;
A10: now
reconsider x = ll.i as bound_QC-variable of Al by A8,A9,Th5;
assume
A11: ll.i in dom (vS+*vS1+*vS2);
A12: now
A13: now
len ll = k by SUBSTUT1:34;
then
A14: i <= len ll by A5,A7,FINSEQ_1:1;
1 <= i by A5,A7,FINSEQ_1:1;
then
x in { ll.n : 1 <= n & n <= len ll & ll.n in bound_QC-variables(Al)
} by A14;
then
A15: x in variables_in(ll,bound_QC-variables(Al)) by QC_LANG3:def 1;
assume x in dom vS1;
then not x in still_not-bound_in ll by A1;
hence contradiction by A15,QC_LANG3:2;
end;
assume
A16: not x in dom vS2;
then
A17: (vS+*vS1+*vS2).x = (vS+*vS1).x by FUNCT_4:11;
A18: x in dom (vS+*vS1) by A11,A16,FUNCT_4:12;
now
assume
A19: not x in dom vS1;
then (vS+*vS1+*vS2).x = vS.x by A17,FUNCT_4:11;
then
A20: (v+*(vS+*vS1+*vS2)).x = vS.x by A11,FUNCT_4:13;
x in dom vS by A18,A19,FUNCT_4:12;
then v.(vS+*vS1+*vS2).x = (v+*vS).x by A20,FUNCT_4:13;
then ll2.i = (v.vS).x by A8,FUNCT_1:12;
hence thesis by A7,FUNCT_1:12;
end;
hence thesis by A13;
end;
now
assume
A21: x in dom vS2;
then (vS+*vS1+*vS2).x = vS2.x by FUNCT_4:13;
then (vS+*vS1+*vS2).x = v.x by A2,A21;
then (v+*(vS+*vS1+*vS2)).x = v.x by A11,FUNCT_4:13;
then
A22: ll2.i = v.x by A8,FUNCT_1:12;
not x in dom vS by A3,A21,XBOOLE_0:3;
then (v+*vS).x = v.x by FUNCT_4:11;
hence thesis by A7,A22,FUNCT_1:12;
end;
hence thesis by A12;
end;
now
assume
A23: not ll.i in dom (vS+*vS1+*vS2);
then not ll.i in dom (vS +* vS1) by FUNCT_4:12;
then not ll.i in dom vS by FUNCT_4:12;
then (v+*vS).(ll.i) = v.(ll.i) by FUNCT_4:11;
then
A24: ll1.i = v.(ll.i) by A7,FUNCT_1:12;
(v+*(vS+*vS1+*vS2)).(ll.i) = v.(ll.i) by A23,FUNCT_4:11;
hence thesis by A8,A24,FUNCT_1:12;
end;
hence thesis by A10;
end;
hence thesis by A4,A6,FINSEQ_2:9;
end;
theorem Th75:
for v,vS,vS1,vS2 st (for y st y in dom vS1 holds not y in
still_not-bound_in (P!ll)) & (for y st y in dom vS2 holds vS2.y = v.y) & dom vS
misses dom vS2 holds J,v.vS |= P!ll iff J,v.(vS+*vS1+*vS2) |= P!ll
proof
let v,vS,vS1,vS2 such that
A1: for y st y in dom vS1 holds not y in still_not-bound_in (P!ll) and
A2: ( for y st y in dom vS2 holds vS2.y = v.y)& dom vS misses dom vS2;
A3: for y st y in dom vS1 holds not y in still_not-bound_in ll
proof
let y;
assume y in dom vS1;
then not y in still_not-bound_in (P!ll) by A1;
hence thesis by QC_LANG3:5;
end;
A4: (v.(vS+*vS1+*vS2))*'ll in J.P iff Valid(P!ll,J).(v.(vS+*vS1+*vS2)) =
TRUE by VALUAT_1:7;
Valid(P!ll,J).(v.vS) = TRUE iff (v.vS)*'ll in J.P by VALUAT_1:7;
hence thesis by A2,A3,A4,Th74,VALUAT_1:def 7;
end;
theorem Th76:
(for v,vS,vS1,vS2 st (for y st y in dom vS1 holds not y in
still_not-bound_in p) & (for y st y in dom vS2 holds vS2.y = v.y) & dom vS
misses dom vS2 holds J,v.vS |= p iff J,v.(vS+*vS1+*vS2) |= p) implies for v,vS,
vS1,vS2 st (for y st y in dom vS1 holds not y in still_not-bound_in 'not' p) &
(for y st y in dom vS2 holds vS2.y = v.y) & dom vS misses dom vS2 holds J,v.vS
|= 'not' p iff J,v.(vS+*vS1+*vS2) |= 'not' p
proof
assume
A1: for v,vS,vS1,vS2 st (for y st y in dom vS1 holds not y in
still_not-bound_in p) & (for y st y in dom vS2 holds vS2.y = v.y) & dom vS
misses dom vS2 holds J,v.vS |= p iff J,v.(vS+*vS1+*vS2) |= p;
let v,vS,vS1,vS2 such that
A2: for y st y in dom vS1 holds not y in still_not-bound_in 'not' p and
A3: ( for y st y in dom vS2 holds vS2.y = v.y)& dom vS misses dom vS2;
for y st y in dom vS1 holds not y in still_not-bound_in p
proof
let y;
assume y in dom vS1;
then not y in still_not-bound_in 'not' p by A2;
hence thesis by QC_LANG3:7;
end;
then not J,v.vS |= p iff not J,v.(vS+*vS1+*vS2) |= p by A1,A3;
hence thesis by VALUAT_1:17;
end;
theorem Th77:
(for v,vS,vS1,vS2 st (for y st y in dom vS1 holds not y in
still_not-bound_in p) & (for y st y in dom vS2 holds vS2.y = v.y) & dom vS
misses dom vS2 holds J,v.vS |= p iff J,v.(vS+*vS1+*vS2) |= p) & (for v,vS,vS1,
vS2 st (for y st y in dom vS1 holds not y in still_not-bound_in q) & (for y st
y in dom vS2 holds vS2.y = v.y) & dom vS misses dom vS2 holds J,v.vS |= q iff J
,v.(vS+*vS1+*vS2) |= q) implies for v,vS,vS1,vS2 st (for y st y in dom vS1
holds not y in still_not-bound_in p '&' q) & (for y st y in dom vS2 holds vS2.y
= v.y) & dom vS misses dom vS2 holds J,v.vS |= p '&' q iff J,v.(vS+*vS1+*vS2)
|= p '&' q
proof
assume
A1: ( for v,vS,vS1,vS2 st (for y st y in dom vS1 holds not y in
still_not-bound_in p) & (for y st y in dom vS2 holds vS2.y = v.y) & dom vS
misses dom vS2 holds J, v.vS |= p iff J,v.(vS+*vS1+*vS2) |= p)& for v,vS,vS1,
vS2 st (for y st y in dom vS1 holds not y in still_not-bound_in q) & (for y st
y in dom vS2 holds vS2.y = v.y) & dom vS misses dom vS2 holds J,v.vS |= q iff J
,v.(vS+*vS1+*vS2) |= q;
let v,vS,vS1,vS2 such that
A2: for y st y in dom vS1 holds not y in still_not-bound_in p '&' q and
A3: ( for y st y in dom vS2 holds vS2.y = v.y)& dom vS misses dom vS2;
A4: for y st y in dom vS1 holds (not y in still_not-bound_in p) & not y in
still_not-bound_in q
proof
let y;
assume y in dom vS1;
then not y in still_not-bound_in (p '&' q) by A2;
then not y in (still_not-bound_in p) \/ (still_not-bound_in q) by
QC_LANG3:10;
hence thesis by XBOOLE_0:def 3;
end;
A5: J,v.(vS+*vS1+*vS2) |= p & J,v.(vS+*vS1+*vS2) |= q implies J,v.vS |= p &
J,v.vS |= q
proof
assume
A6: J,v.(vS+*vS1+*vS2) |= p & J,v.(vS+*vS1+*vS2) |= q;
( for y st y in dom vS1 holds not y in still_not-bound_in p)& for y
st y in dom vS1 holds not y in still_not-bound_in q by A4;
hence thesis by A1,A3,A6;
end;
J,v.vS |= p & J,v.vS |= q implies J,v.(vS+*vS1+*vS2) |= p & J,v.(vS+*
vS1+*vS2) |= q
proof
assume
A7: J,v.vS |= p & J,v.vS |= q;
( for y st y in dom vS1 holds not y in still_not-bound_in p)& for y
st y in dom vS1 holds not y in still_not-bound_in q by A4;
hence thesis by A1,A3,A7;
end;
hence thesis by A5,VALUAT_1:18;
end;
theorem Th78:
(for y st y in dom vS1 holds not y in still_not-bound_in All(x,p
)) implies for y st y in (dom vS1) \ {x} holds not y in still_not-bound_in p
proof
assume
A1: for y st y in dom vS1 holds not y in still_not-bound_in All(x,p);
let y such that
A2: y in (dom vS1) \ {x};
(dom vS1) \ {x} c= dom vS1 by XBOOLE_1:36;
then not y in still_not-bound_in All(x,p) by A1,A2;
then
A3: not y in (still_not-bound_in p) \ {x} by QC_LANG3:12;
A4: {x} \/ ((still_not-bound_in p) \ {x}) = {x} \/ still_not-bound_in p by
XBOOLE_1:39;
not y in {x} by A2,XBOOLE_0:def 5;
then not y in {x} \/ ((still_not-bound_in p) \ {x}) by A3,XBOOLE_0:def 3;
hence thesis by A4,XBOOLE_0:def 3;
end;
theorem Th79:
for vS1 being Function holds (for y st y in dom vS1 holds vS1.y
= v.y) & dom vS misses dom vS1 implies for y st y in (dom vS1) \ {x} holds vS1|
((dom vS1) \ {x}).y = (v.vS).y
proof
let vS1 be Function;
assume that
A1: for y st y in dom vS1 holds vS1.y = v.y and
A2: dom vS misses dom vS1;
let y such that
A3: y in (dom vS1) \ {x};
y in dom vS1 /\ ((dom vS1) \ {x}) by A3,XBOOLE_0:def 4;
then vS1|((dom vS1) \ {x}).y = vS1.y by FUNCT_1:48;
then
A4: vS1|((dom vS1) \ {x}).y = v.y by A1,A3;
not y in dom vS by A2,A3,XBOOLE_0:3;
hence thesis by A4,FUNCT_4:11;
end;
theorem Th80:
(for v,vS,vS1,vS2 st (for y st y in dom vS1 holds not y in
still_not-bound_in p) & (for y st y in dom vS2 holds vS2.y = v.y) & dom vS
misses dom vS2 holds J,v.vS |= p iff J,v.(vS+*vS1+*vS2) |= p) implies for v,vS,
vS1,vS2 st (for y st y in dom vS1 holds not y in still_not-bound_in All(x,p)) &
(for y st y in dom vS2 holds vS2.y = v.y) & dom vS misses dom vS2 holds J,v.vS
|= All(x,p) iff J,v.(vS+*vS1+*vS2) |= All(x,p)
proof
assume
A1: for v,vS,vS1,vS2 st (for y st y in dom vS1 holds not y in
still_not-bound_in p) & (for y st y in dom vS2 holds vS2.y = v.y) & dom vS
misses dom vS2 holds J,v.vS |= p iff J,v.(vS+*vS1+*vS2) |= p;
let v,vS,vS1,vS2 such that
A2: for y st y in dom vS1 holds not y in still_not-bound_in All(x,p) and
A3: ( for y st y in dom vS2 holds vS2.y = v.y)& dom vS misses dom vS2;
set vS19 = vS1|((dom vS1) \ {x});
set vS29 = vS2|((dom vS2) \ {x});
A4: for y st y in dom vS29 holds vS29.y = (v.vS).y by A3,Th79;
A5: dom vS29 misses {x} by XBOOLE_1:63,79;
A6: for y st y in dom vS19 holds not y in still_not-bound_in p by A2,Th78;
A7: (for a holds J,(v.vS).(x|a) |= p) implies for a holds J,(v.vS).((x|a)+*
vS19+*vS29) |= p
proof
assume
A8: for a holds J,(v.vS).(x|a) |= p;
let a;
dom vS29 misses dom (x|a) by A5;
then J,(v.vS).(x|a) |= p iff J,(v.vS).((x|a)+*vS19+*vS29) |= p by A1,A6,A4;
hence thesis by A8;
end;
A9: dom vS19 misses {x} by XBOOLE_1:63,79;
A10: for a holds (v.vS).((x|a)+*vS19+*vS29) = v.(vS+*vS1+*vS2).(x|a)
proof
let a;
dom vS19 misses dom (x|a) by A9;
then (v.vS).((x|a)+*vS19+*vS29) = (v+*vS)+*(vS19+*(x|a)+*vS29) by
FUNCT_4:35;
then
A11: (v.vS).((x|a)+*vS19+*vS29) = (v+*vS)+*(vS19+*((x|a)+*vS29)) by FUNCT_4:14;
dom vS29 misses dom (x|a) by A5;
then (v.vS).((x|a)+*vS19+*vS29) = (v+*vS)+*(vS19+*(vS29+*(x|a))) by A11,
FUNCT_4:35;
then
A12: (v.vS).((x|a)+*vS19+*vS29) = (v+*vS)+*((vS19+*vS29)+*(x|a)) by FUNCT_4:14;
A13: now
assume x in dom vS1;
then
A14: vS19 +* (x .--> vS1.x) = vS1 by Th2;
A15: now
assume not x in dom vS2;
then vS29 = vS2|(dom vS2) by ZFMISC_1:57;
then vS29 = vS2;
then
A16: vS29 +* {} = vS2;
dom {} c= dom (x|a) & dom (x .--> vS1.x) = dom (x|a);
hence
(v.vS).((x|a)+*vS19+*vS29) = (v+*vS)+*((vS1+*vS2)+*(x|a)) by A12,A14
,A16,Th1;
end;
now
A17: dom (x .--> vS2.x) = dom (x|a);
A18: dom (x .--> vS1.x) = dom (x|a);
assume x in dom vS2;
then vS29 +* (x .--> vS2.x) = vS2 by Th2;
hence
(v.vS).((x|a)+*vS19+*vS29) = (v+*vS)+*((vS1+*vS2)+*(x|a)) by A12,A14
,A18,A17,Th1;
end;
hence (v.vS).((x|a)+*vS19+*vS29) = (v+*vS)+*((vS1+*vS2)+*(x|a)) by A15;
end;
now
A19: dom {} c= dom (x|a);
assume not x in dom vS1;
then vS19 = vS1|(dom vS1) by ZFMISC_1:57;
then
A20: vS19 = vS1;
then
A21: vS19 +* {} = vS1;
A22: now
A23: dom (x .--> vS2.x) = dom (x|a);
assume x in dom vS2;
then vS29 +* (x .--> vS2.x) = vS2 by Th2;
hence
(v.vS).((x|a)+*vS19+*vS29) = (v+*vS)+*((vS1+*vS2)+*(x|a)) by A12,A21
,A19,A23,Th1;
end;
now
assume not x in dom vS2;
then vS29 = vS2|(dom vS2) by ZFMISC_1:57;
hence
(v.vS).((x|a)+*vS19+*vS29) = (v+*vS)+*((vS1+*vS2)+*(x|a)) by A12,A20;
end;
hence (v.vS).((x|a)+*vS19+*vS29) = (v+*vS)+*((vS1+*vS2)+*(x|a)) by A22;
end;
then (v.vS).((x|a)+*vS19+*vS29) = (v+*vS)+*(vS1+*vS2)+*(x|a) by A13,
FUNCT_4:14;
then (v.vS).((x|a)+*vS19+*vS29) = ((v+*vS)+*vS1+*vS2)+*(x|a) by FUNCT_4:14;
then (v.vS).((x|a)+*vS19+*vS29) = (v+*(vS+*vS1)+*vS2)+*(x|a) by FUNCT_4:14;
hence thesis by FUNCT_4:14;
end;
A24: (for a holds J,v.(vS+*vS1+*vS2).(x|a) |= p) implies for a holds J,(v.vS
).((x|a)+*vS19+*vS29) |= p
proof
assume
A25: for a holds J,v.(vS+*vS1+*vS2).(x|a) |= p;
let a;
(v.vS).((x|a)+*vS19+*vS29) = v.(vS+*vS1+*vS2).(x|a) by A10;
hence thesis by A25;
end;
A26: (for a holds J,(v.vS).((x|a)+*vS19+*vS29) |= p) implies for a holds J,(
v.vS).(x|a) |= p
proof
assume
A27: for a holds J,(v.vS).((x|a)+*vS19+*vS29) |= p;
let a;
dom vS29 misses dom (x|a) by A5;
then J,(v.vS).(x|a) |= p iff J,(v.vS).((x|a)+*vS19+*vS29) |= p by A1,A6,A4;
hence thesis by A27;
end;
(for a holds J,(v.vS).((x|a)+*vS19+*vS29) |= p) implies for a holds J,v
.(vS+*vS1+*vS2).(x|a) |= p
proof
assume
A28: for a holds J,(v.vS).((x|a)+*vS19+*vS29) |= p;
let a;
(v.vS).((x|a)+*vS19+*vS29) = v.(vS+*vS1+*vS2).(x|a) by A10;
hence thesis by A28;
end;
hence thesis by A7,A26,A24,Th50;
end;
theorem Th81:
for p holds for v,vS,vS1,vS2 st (for y st y in dom vS1 holds not
y in still_not-bound_in p) & (for y st y in dom vS2 holds vS2.y = v.y) & dom vS
misses dom vS2 holds J,v.vS |= p iff J,v.(vS+*vS1+*vS2) |= p
proof
defpred P[Element of CQC-WFF(Al)] means for v,vS,vS1,vS2 st
(for y st y in dom vS1 holds not y in still_not-bound_in $1) &
(for y st y in dom vS2 holds vS2.y = v.y) & dom vS misses dom vS2 holds
J,v.vS |= $1 iff J,v.(vS+*vS1+*vS2) |= $1;
A1: for p,q,x,k for l being CQC-variable_list of k,Al for P being
QC-pred_symbol of k,Al holds P[VERUM(Al)] & P[P!l] & (P[p] implies P['not' p])
& (P[p] & P[q] implies P[p '&' q]) & (P[p] implies P[All(x,p)])
by Th75,Th76,Th77,Th80,VALUAT_1:32;
thus for p holds P[p] from CQC_LANG:sch 1(A1);
end;
definition
let Al, p;
func RSub1(p) -> set means
:Def9:
b in it iff ex x st x = b & not x in still_not-bound_in p;
existence
proof
defpred P[object] means ex x st x = $1 & not x in still_not-bound_in p;
consider X being set such that
A1: for b being object holds b in X iff b in bound_QC-variables(Al) & P[b]
from
XBOOLE_0:sch 1;
take X;
thus thesis by A1;
end;
uniqueness
proof
let X1,X2 be set;
assume that
A2: for b holds b in X1 iff ex x st x = b & not x in still_not-bound_in p and
A3: for b holds b in X2 iff ex x st x = b & not x in still_not-bound_in p;
now
let b be object;
b in X1 iff ex x st x = b & not x in still_not-bound_in p by A2;
hence b in X1 iff b in X2 by A3;
end;
hence thesis by TARSKI:2;
end;
end;
definition
let Al, p, Sub;
func RSub2(p,Sub) -> set means
:Def10:
b in it iff ex x st x = b & x in still_not-bound_in p & x = (@Sub).x;
existence
proof
defpred P[object] means
ex x st x = $1 & x in still_not-bound_in p & x = (@
Sub).x;
consider X being set such that
A1: for b being object holds b in X iff b in bound_QC-variables(Al) & P[b]
from
XBOOLE_0:sch 1;
take X;
thus thesis by A1;
end;
uniqueness
proof
let X1,X2 be set;
assume that
A2: for b holds b in X1 iff ex x st x = b & x in still_not-bound_in p
& x = (@Sub).x and
A3: for b holds b in X2 iff ex x st x = b & x in still_not-bound_in p
& x = (@Sub).x;
now
let b be object;
b in X1 iff ex x st x = b & x in still_not-bound_in p & x = (@Sub).x
by A2;
hence b in X1 iff b in X2 by A3;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Th82:
dom ((@Sub)|RSub1(p)) misses dom ((@Sub)|RSub2(p,Sub))
proof
now
assume dom ((@Sub)|RSub1(p)) meets dom ((@Sub)|RSub2(p,Sub));
then consider a being object such that
A1: a in dom ((@Sub)|RSub1(p)) /\ dom ((@Sub)|RSub2(p,Sub)) by XBOOLE_0:4;
dom ((@Sub)|RSub1(p)) = dom (@Sub) /\ RSub1(p) & dom ((@Sub)|RSub2(p,
Sub)) = (dom (@Sub) /\ RSub2(p,Sub)) by RELAT_1:61;
then a in (dom (@Sub) /\ (dom (@Sub) /\ RSub1(p))) /\ RSub2(p,Sub) by A1,
XBOOLE_1:16;
then a in dom (@Sub) /\ dom (@Sub) /\ RSub1(p) /\ RSub2(p,Sub) by
XBOOLE_1:16;
then a in dom (@Sub) /\ (RSub1(p) /\ RSub2(p,Sub)) by XBOOLE_1:16;
then
A2: a in RSub1(p) /\ RSub2(p,Sub) by XBOOLE_0:def 4;
then a in RSub2(p,Sub) by XBOOLE_0:def 4;
then
A3: ex b being bound_QC-variable of Al st b = a & b in still_not-bound_in p & b
= (@Sub).b by Def10;
a in RSub1(p) by A2,XBOOLE_0:def 4;
then ex b being bound_QC-variable of Al st b = a & not b in
still_not-bound_in p by Def9;
hence contradiction by A3;
end;
hence thesis;
end;
theorem Th83:
@RestrictSub(x,All(x,p),Sub) = @Sub \ ((@Sub)|RSub1(All(x,p)) +*
(@Sub)|RSub2(All(x,p),Sub))
proof
set X = {y : y in still_not-bound_in All(x,p) & y is Element of dom Sub & y
<> x & y <> Sub.y};
thus @RestrictSub(x,All(x,p),Sub) c= @Sub \ ((@Sub)|RSub1(All(x,p)) +* (@Sub
)|RSub2(All(x,p),Sub))
proof
let b be object;
A1: dom ((@Sub)|RSub1(All(x,p))) misses dom ((@Sub)|RSub2(All(x,p),Sub))
by Th82;
assume b in @RestrictSub(x,All(x,p),Sub);
then b in RestrictSub(x,All(x,p),Sub) by SUBSTUT1:def 2;
then b in Sub|X by SUBSTUT1:def 6;
then b in (@Sub)|X by SUBSTUT1:def 2;
then
A2: b in @Sub /\ [:X,rng (@Sub):] by RELAT_1:67;
then b in [:X,rng @Sub:] by XBOOLE_0:def 4;
then consider c,d being object such that
A3: c in X and
d in rng @Sub and
A4: b = [c,d] by ZFMISC_1:def 2;
A5: ex y1 st y1 = c & y1 in still_not-bound_in All(x,p) & y1 is Element of
dom Sub & y1 <> x & y1 <> Sub.y1 by A3;
now
assume c in RSub2(All(x,p),Sub);
then ex y st y = c & y in still_not-bound_in All(x,p) & y = (@Sub).y by
Def10;
hence contradiction by A5,SUBSTUT1:def 2;
end;
then not b in [:RSub2(All(x,p),Sub),rng @Sub:] by A4,ZFMISC_1:87;
then not b in @Sub /\ [:RSub2(All(x,p),Sub),rng @Sub:] by XBOOLE_0:def 4;
then
A6: not b in (@Sub)|RSub2(All(x,p),Sub) by RELAT_1:67;
now
assume c in RSub1(All(x,p));
then ex y st y = c & not y in still_not-bound_in All(x,p) by Def9;
hence contradiction by A5;
end;
then not b in [:RSub1(All(x,p)),rng @Sub:] by A4,ZFMISC_1:87;
then not b in @Sub /\ [:RSub1(All(x,p)),rng @Sub:] by XBOOLE_0:def 4;
then not b in (@Sub)|RSub1(All(x,p)) by RELAT_1:67;
then not b in (@Sub)|RSub1(All(x,p)) \/ (@Sub)|RSub2(All(x,p),Sub) by A6,
XBOOLE_0:def 3;
then
A7: not b in (@Sub)|RSub1(All(x,p)) +* (@Sub)|RSub2(All(x,p),Sub) by A1,
FUNCT_4:31;
b in @Sub by A2,XBOOLE_0:def 4;
hence thesis by A7,XBOOLE_0:def 5;
end;
thus @Sub \ ((@Sub)|RSub1(All(x,p)) +* (@Sub)|RSub2(All(x,p),Sub)) c= @
RestrictSub(x,All(x,p),Sub)
proof
A8: dom ((@Sub)|RSub1(All(x,p))) misses dom ((@Sub)|RSub2(All(x,p),Sub))
by Th82;
let b be object;
assume
A9: b in @Sub \ ((@Sub)|RSub1(All(x,p)) +* (@Sub)|RSub2(All(x,p),Sub) );
then
A10: b in @Sub by XBOOLE_0:def 5;
consider c,d being object such that
A11: b = [c,d] by A9,RELAT_1:def 1;
A12: c in dom (@Sub) by A10,A11,FUNCT_1:1;
then reconsider z = c as bound_QC-variable of Al;
A13: d = (@Sub).c by A10,A11,FUNCT_1:1;
then
A14: d in rng @Sub by A12,FUNCT_1:3;
not b in ((@Sub)|RSub1(All(x,p)) +* (@Sub)|RSub2(All(x,p),Sub)) by A9,
XBOOLE_0:def 5;
then
A15: not b in (@Sub)|RSub1(All(x,p)) \/ (@Sub)|RSub2(All(x,p),Sub) by A8,
FUNCT_4:31;
then not b in (@Sub)|RSub1(All(x,p)) by XBOOLE_0:def 3;
then not b in (@Sub /\ [:RSub1(All(x,p)),rng @Sub:]) by RELAT_1:67;
then not [z,d] in [:RSub1(All(x,p)),rng @Sub:] by A10,A11,XBOOLE_0:def 4;
then
A16: not z in RSub1(All(x,p)) by A14,ZFMISC_1:87;
then
A17: z in still_not-bound_in All(x,p) by Def9;
then z in (still_not-bound_in p) \ {x} by QC_LANG3:12;
then not z in {x} by XBOOLE_0:def 5;
then
A18: z <> x by TARSKI:def 1;
A19: d in rng @Sub by A12,A13,FUNCT_1:3;
not b in (@Sub)|RSub2(All(x,p), Sub) by A15,XBOOLE_0:def 3;
then not b in (@Sub /\ [:RSub2(All(x,p),Sub),rng @Sub:]) by RELAT_1:67;
then not [z,d] in [:RSub2(All(x,p),Sub),rng @Sub:] by A10,A11,
XBOOLE_0:def 4;
then not z in RSub2(All(x,p),Sub) by A19,ZFMISC_1:87;
then not z in still_not-bound_in All(x,p) or z <> (@Sub).z by Def10;
then
A20: z <> Sub.z by A16,Def9,SUBSTUT1:def 2;
A21: d in rng @Sub by A12,A13,FUNCT_1:3;
z is Element of dom Sub by A12,SUBSTUT1:def 2;
then z in X by A17,A18,A20;
then [z,d] in [:X,rng @Sub:] by A21,ZFMISC_1:87;
then b in @Sub /\ [:X,rng (@Sub):] by A10,A11,XBOOLE_0:def 4;
then b in (@Sub)|X by RELAT_1:67;
then b in Sub|X by SUBSTUT1:def 2;
then b in RestrictSub(x,All(x,p),Sub) by SUBSTUT1:def 6;
hence thesis by SUBSTUT1:def 2;
end;
end;
theorem Th84:
dom @RestrictSub(x,p,Sub) misses dom ((@Sub)|RSub1(p)) \/ dom ((
@Sub)|RSub2(p,Sub))
proof
set X = {y : y in still_not-bound_in p & y is Element of dom Sub & y <> x &
y <> Sub.y};
A1: dom ((@Sub)|RSub2(p,Sub)) = dom @Sub /\ RSub2(p,Sub) by RELAT_1:61;
RestrictSub(x,p,Sub) = Sub|X by SUBSTUT1:def 6;
then RestrictSub(x,p,Sub) = (@Sub|X) by SUBSTUT1:def 2;
then dom @RestrictSub(x,p,Sub) = dom (@Sub|X) by SUBSTUT1:def 2;
then
A2: dom @RestrictSub(x,p,Sub) = dom @Sub /\ X by RELAT_1:61;
A3: dom ((@Sub)|RSub1(p)) = dom @Sub /\ RSub1(p) by RELAT_1:61;
now
assume dom @RestrictSub(x,p,Sub) meets dom ((@Sub)|RSub1(p)) \/ dom ((@
Sub)|RSub2(p,Sub));
then consider b being object such that
A4: b in dom @RestrictSub(x,p,Sub) and
A5: b in dom ((@Sub)|RSub1(p)) \/ dom ((@Sub)|RSub2(p,Sub)) by XBOOLE_0:3;
b in X by A2,A4,XBOOLE_0:def 4;
then
A6: ex y st b = y & y in still_not-bound_in p & y is Element of dom Sub &
y <> x & y <> Sub.y;
A7: now
assume b in dom ((@Sub)|RSub2(p,Sub));
then b in RSub2(p,Sub) by A1,XBOOLE_0:def 4;
then ex y1 st y1 = b & y1 in still_not-bound_in p & y1 = (@ Sub).y1 by
Def10;
hence contradiction by A6,SUBSTUT1:def 2;
end;
now
assume b in dom ((@Sub)|RSub1(p));
then b in RSub1(p) by A3,XBOOLE_0:def 4;
then ex y1 st y1 = b & not y1 in still_not-bound_in p by Def9;
hence contradiction by A6;
end;
hence contradiction by A5,A7,XBOOLE_0:def 3;
end;
hence thesis;
end;
theorem Th85:
[S,x] is quantifiable implies @(CQCSub_All([S,x],xSQ))`2 = @
RestrictSub(x,All(x,S`1),xSQ) +* (@xSQ)|RSub1(All(x,S`1)) +* (@xSQ)|RSub2(All(x
,S`1),xSQ)
proof
set S1 = CQCSub_All([S,x],xSQ);
A1: (@xSQ)|RSub2(All(x,S`1),xSQ) c= @xSQ by RELAT_1:59;
dom ((@xSQ)|RSub1(All(x,S`1))) misses dom ((@xSQ)|RSub2(All(x,S`1),xSQ))
by Th82;
then
A2: ((@xSQ)|RSub1(All(x,S`1)) +* (@xSQ)|RSub2(All(x,S`1),xSQ)) = ((@xSQ)|
RSub1(All(x,S`1)) \/ (@xSQ)|RSub2(All(x,S`1),xSQ)) by FUNCT_4:31;
assume
A3: [S,x] is quantifiable;
then S1 = Sub_All([S,x],xSQ) by Def5;
then
A4: @S1`2 = @xSQ by A3,Th26;
A5: @RestrictSub(x,All(x,S`1),xSQ) = @xSQ \ ((@xSQ)|RSub1(All(x,S`1)) +* (@
xSQ)|RSub2(All(x,S`1),xSQ)) by Th83;
then reconsider
F = @xSQ \ ((@xSQ)|RSub1(All(x,S`1)) +* (@xSQ)|RSub2(All(x,S`1),
xSQ)) as PartFunc of bound_QC-variables(Al),bound_QC-variables(Al);
dom F misses (dom ((@xSQ)|RSub1(All(x,S`1))) \/ dom ((@xSQ)|RSub2(All(x
,S`1),xSQ))) by A5,Th84;
then
A6: dom F misses dom ((@xSQ)|RSub1(All(x,S`1)) +* (@xSQ)|RSub2(All(x,S`1),
xSQ)) by FUNCT_4:def 1;
((@xSQ)|RSub1(All(x,S`1)) +* (@xSQ)|RSub2(All(x,S`1),xSQ)) \/ F = ((@xSQ
)| RSub1(All(x,S`1)) +* (@xSQ)|RSub2(All(x,S`1),xSQ)) \/ @xSQ & (@xSQ)|RSub1(
All( x,S`1)) c= @xSQ by RELAT_1:59,XBOOLE_1:39;
then
((@xSQ)|RSub1(All(x,S`1)) +* (@xSQ)|RSub2(All(x,S`1),xSQ)) \/ F = @ xSQ
by A2,A1,XBOOLE_1:8,12;
then F +* ((@xSQ)|RSub1(All(x,S`1)) +* (@xSQ)|RSub2(All(x,S`1),xSQ)) = @xSQ
by A6,FUNCT_4:31;
hence thesis by A4,A5,FUNCT_4:14;
end;
theorem Th86:
[S,x] is quantifiable implies ex vS1,vS2 st (for y st y in dom
vS1 holds not y in still_not-bound_in All(x,S`1)) & (for y st y in dom vS2
holds vS2.y = v.y) & dom NEx_Val(v,S,x,xSQ) misses dom vS2 & v.Val_S(v,
CQCSub_All([S,x],xSQ)) = v.(NEx_Val(v,S,x,xSQ) +* vS1 +* vS2)
proof
set S1 = CQCSub_All([S,x],xSQ);
assume [S,x] is quantifiable;
then
A1: Val_S(v,S1) = ((@RestrictSub(x,All(x,S`1),xSQ) +* (@xSQ)|RSub1(All(x,S`1
))) +* (@xSQ)|RSub2(All(x,S`1),xSQ))*v by Th85;
take vS1 = (@xSQ)|RSub1(All(x,S`1))*v;
take vS2 = (@xSQ)|RSub2(All(x,S`1),xSQ)*v;
rng ((@xSQ)|RSub1(All(x,S`1))) c= bound_QC-variables(Al);
then
A2: rng ((@xSQ)|RSub1(All(x,S`1))) c= dom v by Th58;
thus for y st y in dom vS1 holds not y in still_not-bound_in All(x,S`1)
proof
let y;
assume y in dom vS1;
then y in dom ((@xSQ)|RSub1(All(x,S`1))) by A2,RELAT_1:27;
then y in dom @xSQ /\ RSub1(All(x,S`1)) by RELAT_1:61;
then y in RSub1(All(x,S`1)) by XBOOLE_0:def 4;
then ex y1 st y1 = y & not y1 in still_not-bound_in All(x,S`1 ) by Def9;
hence thesis;
end;
rng ((@xSQ)|RSub2(All(x,S`1),xSQ)) c= bound_QC-variables(Al);
then
A3: rng ((@xSQ)|RSub2(All(x,S`1),xSQ)) c= dom v by Th58;
thus for y st y in dom vS2 holds vS2.y = v.y
proof
let y;
assume y in dom vS2;
then
A4: y in dom ((@xSQ)|RSub2(All(x,S`1),xSQ)) by A3,RELAT_1:27;
then y in dom @xSQ /\ RSub2(All(x,S`1),xSQ) by RELAT_1:61;
then y in RSub2(All(x,S`1),xSQ) by XBOOLE_0:def 4;
then
ex y1 st y1 = y & y1 in still_not-bound_in All(x,S`1) & y1 = (@xSQ).y1
by Def10;
then v.y = v.(((@xSQ)|RSub2(All(x,S`1),xSQ)).y) by A4,FUNCT_1:47;
hence thesis by A4,FUNCT_1:13;
end;
thus dom NEx_Val(v,S,x,xSQ) misses dom vS2
proof
set X = {y : y in still_not-bound_in All(x,S`1) & y is Element of dom xSQ
& y <> x & y <> xSQ.y};
RestrictSub(x,All(x,S`1),xSQ) = (xSQ|X) by SUBSTUT1:def 6;
then RestrictSub(x,All(x,S`1),xSQ) = (@xSQ)|X by SUBSTUT1:def 2;
then dom NEx_Val(v,S,x,xSQ) = dom ((@xSQ)|X) by Th71;
then
A5: dom NEx_Val(v,S,x,xSQ) = dom (@xSQ) /\ X by RELAT_1:61;
dom vS2 = dom ((@xSQ)|RSub2(All(x,S`1),xSQ)) by A3,RELAT_1:27;
then
A6: dom vS2 = dom @xSQ /\ RSub2(All(x,S`1),xSQ) by RELAT_1:61;
now
assume dom NEx_Val(v,S,x,xSQ) meets dom vS2;
then consider b being object such that
A7: b in dom NEx_Val(v,S,x,xSQ) and
A8: b in dom vS2 by XBOOLE_0:3;
b in X by A5,A7,XBOOLE_0:def 4;
then
A9: ex y st y = b & y in still_not-bound_in All(x,S`1) & y is Element of
dom xSQ & y <> x & y <> xSQ.y;
b in RSub2(All(x,S`1),xSQ) by A6,A8,XBOOLE_0:def 4;
then
ex y1 st y1 = b & y1 in still_not-bound_in All(x,S`1) & y1 = (@xSQ).
y1 by Def10;
hence contradiction by A9,SUBSTUT1:def 2;
end;
hence thesis;
end;
(@RestrictSub(x,All(x,S`1),xSQ) +* (@xSQ)|RSub1(All(x,S`1)))*v = (@
RestrictSub(x,All(x,S`1),xSQ)*v) +* ((@xSQ)|RSub1(All(x,S`1))*v) by A2,
FUNCT_7:9;
hence thesis by A1,A3,FUNCT_7:9;
end;
theorem Th87:
[S,x] is quantifiable implies for v holds (J,v.NEx_Val(v,S,x,xSQ
) |= All(x,S`1) iff J,v.Val_S(v,CQCSub_All([S,x],xSQ)) |= CQCSub_All([S,x],xSQ)
)
proof
set S1 = CQCSub_All([S,x],xSQ);
assume
A1: [S,x] is quantifiable;
then S1 = Sub_All([S,x],xSQ) by Def5;
then S1`1 = All([S,x]`2,([S,x]`1)`1) by A1,Th26;
then S1`1 = All(x,([S,x]`1)`1);
then
A2: S1`1 = All(x,S`1);
let v;
consider vS1,vS2 such that
A3: ( ( for y st y in dom vS1 holds not y in still_not-bound_in All(x,S
`1))& for y st y in dom vS2 holds vS2.y = v.y )& dom NEx_Val(v,S,x,xSQ) misses
dom vS2 and
A4: v.Val_S(v,S1) = v.(NEx_Val(v,S,x,xSQ) +* vS1 +* vS2) by A1,Th86;
J,v.NEx_Val(v,S,x,xSQ) |= All(x,S`1) iff J,v.(NEx_Val(v,S,x,xSQ) +* vS1
+* vS2) |= All(x,S`1) by A3,Th81;
hence thesis by A4,A2;
end;
theorem Th88:
[S,x] is quantifiable & (for v holds (J,v |= CQC_Sub(S) iff J,v.
Val_S(v,S) |= S)) implies for v holds (J,v |= CQC_Sub(CQCSub_All([S,x],xSQ))
iff J,v.Val_S(v,CQCSub_All([S,x],xSQ)) |= CQCSub_All([S,x],xSQ))
proof
assume that
A1: [S,x] is quantifiable and
A2: for v holds (J,v |= CQC_Sub(S) iff J,v.Val_S(v,S) |= S);
let v;
set S1 = CQCSub_All([S,x],xSQ);
set z = S_Bound(@S1);
A3: (for a holds J,(v.(z|a)).Val_S(v.(z|a),S) |= S) iff for a holds J,(v.(z
|a)).(NEx_Val(v.(z|a),S,x,xSQ)+*(x|a)) |= S by A1,Th54;
set q = CQC_Sub(S);
A4: J,v |= All(z,q) iff for a holds J,v.(z|a) |= q by Th50;
A5: (for a holds J,v.(z|a) |= q) implies for a holds J,(v.(z|a)).Val_S(v.(z|
a),S) |= S
by A2;
A6: (for a holds J,(v.(z|a)).Val_S(v.(z|a),S) |= S) implies for a holds J,v.
(z|a) |= q
proof
assume
A7: for a holds J,(v.(z|a)).Val_S(v.(z|a),S) |= S;
let a;
J,(v.(z|a)).Val_S(v.(z|a),S) |= S by A7;
hence thesis by A2;
end;
set p = CQC_Sub(CQCSub_the_scope_of S1);
A8: J,v |= CQCQuant(S1,p) iff J,v |= CQCQuant(S1,CQC_Sub(S)) by A1,Th30;
A9: (for a holds J,(v.(z|a)).(NEx_Val(v,S,x,xSQ)+*(x|a)) |= S) iff for a
holds J,v.(NEx_Val(v,S,x,xSQ)+*(x|a)) |= S by A1,Th70;
A10: J,v.NEx_Val(v,S,x,xSQ) |= All(x,S`1) implies for a holds J,(v.NEx_Val(v
,S,x,xSQ)).(x|a) |= S
by Th50;
A11: (for a holds J,(v.NEx_Val(v,S,x,xSQ)).(x|a) |= S) implies J,v.NEx_Val(v
,S,x,xSQ) |= All(x,S`1)
proof
assume for a holds J,(v.NEx_Val(v,S,x,xSQ)).(x|a) |= S;
then for a holds J,(v.NEx_Val(v,S,x,xSQ)).(x|a) |= S`1 by Th73;
hence thesis by Th50;
end;
S1 is Sub_universal by A1,Th27;
hence thesis by A1,A8,A4,A5,A6,A3,A9,A11,A10,Th28,Th31,Th56,Th72,Th87;
end;
scheme
SubCQCInd1 { 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[CQCSub_&(S,S9)]) &
([S,x] is quantifiable & Pro[S] implies Pro[CQCSub_All([S,x], SQ)])
proof
A2: for S,S9 being Element of CQC-Sub-WFF(Al()),
x being bound_QC-variable of Al(),
xSQ being second_Q_comp of [S,x] holds
[S,x] is quantifiable & Pro[S] implies Pro[Sub_All([S,x],xSQ)]
proof
let S,S9 be Element of CQC-Sub-WFF(Al());
let x be bound_QC-variable of Al();
let xSQ be second_Q_comp of [S,x];
assume that
A3: [S,x] is quantifiable and
A4: Pro[S];
Pro[CQCSub_All([S,x], xSQ)] by A1,A3,A4;
hence thesis by A3,Def5;
end;
for S,S9 being Element of CQC-Sub-WFF(Al()) holds
S`2 = (S9)`2 & Pro[S] & Pro[S9] implies Pro[Sub_&(S,S9)]
proof
let S,S9 be Element of CQC-Sub-WFF(Al());
assume that
A5: S`2 = (S9)`2 and
A6: ( Pro[S])& Pro[S9];
CQCSub_&(S,S9) = Sub_&(S,S9) by A5,Def3;
hence thesis by A1,A5,A6;
end;
then
A7: for S,S9 being Element of CQC-Sub-WFF(Al()),
x being bound_QC-variable of Al(),
SQ be 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)])
by A1,A2;
thus thesis from SUBSTUT1:sch 5(A7);
end;
:: Substitution Lemma (Ebb et al, Chapter III, 8.3)
theorem
for S, v holds (J,v |= CQC_Sub(S) iff J,v.Val_S(v,S) |= S)
proof
defpred Pro[Element of CQC-Sub-WFF(Al)] means for v holds (J,v |= CQC_Sub($1)
iff J,v.Val_S(v,$1) |= $1);
A1: for S,S9 being Element of CQC-Sub-WFF(Al), x being bound_QC-variable of Al,
SQ be 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[CQCSub_&(S,S9)]) & ([S,x] is quantifiable &
Pro[S] implies Pro[CQCSub_All([S,x], SQ)]) by Th4,Th15,Th19,Th25,Th88;
thus for S holds Pro[S] from SubCQCInd1(A1);
end;