:: Coincidence Lemma and Substitution Lemma :: by Patrick Braselmann and Peter Koepke :: :: Received September 25, 2004 :: Copyright (c) 2004-2018 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; 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 :: SUBLEMMA:1 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; theorem :: SUBLEMMA:2 for vS1 being Function st x in dom vS1 holds (vS1|((dom vS1) \ {x })) +* (x .--> vS1.x) = vS1; 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); end; definition let Al,S; redefine func S`1 -> Element of CQC-WFF(Al); end; definition let Al, S, A, v; func Val_S(v,S) -> Val_Sub of A,Al equals :: SUBLEMMA:def 1 (@S`2)*v; end; theorem :: SUBLEMMA:3 S is Al-Sub_VERUM implies CQC_Sub(S) = VERUM(Al); definition let Al, S, A, v, J; pred J,v |= S means :: SUBLEMMA:def 2 J,v |= S`1; end; theorem :: SUBLEMMA:4 S is Al-Sub_VERUM implies for v holds (J,v |= CQC_Sub(S) iff J,v. Val_S(v,S) |= S); theorem :: SUBLEMMA:5 i in dom ll implies ll.i is bound_QC-variable of Al; theorem :: SUBLEMMA:6 S is Sub_atomic implies CQC_Sub(S) = (the_pred_symbol_of S`1)! CQC_Subst(Sub_the_arguments_of S,S`2); theorem :: SUBLEMMA:7 Sub_the_arguments_of Sub_P(P,ll,Sub) = Sub_the_arguments_of Sub_P(P9, ll9,Sub9) implies ll = ll9; definition let k, Al, P, ll, Sub; redefine func Sub_P(P,ll,Sub) -> Element of CQC-Sub-WFF(Al); end; theorem :: SUBLEMMA:8 CQC_Sub(Sub_P(P,ll,Sub)) = P!CQC_Subst(ll,Sub); theorem :: SUBLEMMA:9 P!CQC_Subst(ll,Sub) is Element of CQC-WFF(Al); theorem :: SUBLEMMA:10 CQC_Subst(ll,Sub) is CQC-variable_list of k,Al; registration let Al; let k, ll, Sub; cluster CQC_Subst(ll,Sub) -> bound_QC-variables(Al) -valued k-element; end; theorem :: SUBLEMMA:11 not x in dom S`2 implies (v.Val_S(v,S)).x = v.x; theorem :: SUBLEMMA:12 x in dom S`2 implies (v.Val_S(v,S)).x = Val_S(v,S).x; theorem :: SUBLEMMA:13 (v.Val_S(v,Sub_P(P,ll,Sub)))*'ll = v*'(CQC_Subst(ll,Sub)); theorem :: SUBLEMMA:14 Sub_P(P,ll,Sub)`1 = P!ll; theorem :: SUBLEMMA:15 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)); theorem :: SUBLEMMA:16 (Sub_not S)`1 = 'not' S`1 & (Sub_not S)`2 = S`2; definition let Al,S; redefine func Sub_not S -> Element of CQC-Sub-WFF(Al); end; theorem :: SUBLEMMA:17 not J,v.Val_S(v,S) |= S iff J,v.Val_S(v,S) |= Sub_not S; theorem :: SUBLEMMA:18 Val_S(v,S) = Val_S(v,Sub_not S); theorem :: SUBLEMMA:19 (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); definition let Al, S1, S2; assume S1`2 = S2`2; func CQCSub_&(S1,S2) -> Element of CQC-Sub-WFF(Al) equals :: SUBLEMMA:def 3 Sub_&(S1,S2); end; theorem :: SUBLEMMA:20 S1`2 = S2`2 implies CQCSub_&(S1,S2)`1 = (S1`1) '&' (S2`1) & CQCSub_&(S1,S2)`2 = S1`2; theorem :: SUBLEMMA:21 S1`2 = S2`2 implies CQCSub_&(S1,S2)`2 = S1`2; theorem :: SUBLEMMA:22 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)); theorem :: SUBLEMMA:23 S1`2 = S2`2 implies CQC_Sub(CQCSub_&(S1,S2)) = (CQC_Sub(S1)) '&' (CQC_Sub(S2)); theorem :: SUBLEMMA:24 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)); theorem :: SUBLEMMA:25 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)); reserve B for Element of [:QC-Sub-WFF(Al),bound_QC-variables(Al):], SQ for second_Q_comp of B; theorem :: SUBLEMMA:26 B is quantifiable implies Sub_All(B,SQ)`1 = All(B`2,(B`1)`1) & Sub_All(B,SQ)`2 = SQ; definition let Al; let B be Element of [:QC-Sub-WFF(Al),bound_QC-variables(Al):]; attr B is CQC-WFF-like means :: SUBLEMMA:def 4 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):]; end; definition let Al, S, x; redefine func [S,x] -> CQC-WFF-like Element of [:QC-Sub-WFF(Al), bound_QC-variables(Al):]; 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); end; definition let Al, B, SQ; assume B is quantifiable; func CQCSub_All(B,SQ) -> Element of CQC-Sub-WFF(Al) equals :: SUBLEMMA:def 5 Sub_All(B,SQ); end; theorem :: SUBLEMMA:27 B is quantifiable implies CQCSub_All(B,SQ) is Sub_universal; definition let Al; let S such that S is Sub_universal; func CQCSub_the_scope_of S -> Element of CQC-Sub-WFF(Al) equals :: SUBLEMMA:def 6 Sub_the_scope_of S; end; definition let Al, S1, p; assume that S1 is Sub_universal and p = CQC_Sub(CQCSub_the_scope_of S1); func CQCQuant(S1,p) -> Element of CQC-WFF(Al) equals :: SUBLEMMA:def 7 Quant(S1,p); end; theorem :: SUBLEMMA:28 S is Sub_universal implies CQC_Sub(S) = CQCQuant(S,CQC_Sub( CQCSub_the_scope_of S)); theorem :: SUBLEMMA:29 B is quantifiable implies CQCSub_the_scope_of(CQCSub_All(B,SQ)) = B`1; begin :: The Substitution Lemma theorem :: SUBLEMMA:30 [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)); theorem :: SUBLEMMA:31 [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)); theorem :: SUBLEMMA:32 x in dom S`2 implies v.((@S`2).x) = v.Val_S(v,S).x; theorem :: SUBLEMMA:33 x in dom (@S`2) implies (@S`2).x is bound_QC-variable of Al; theorem :: SUBLEMMA:34 [:QC-WFF(Al),vSUB(Al):] c= dom QSub(Al); reserve B1 for Element of [:QC-Sub-WFF(Al),bound_QC-variables(Al):]; reserve SQ1 for second_Q_comp of B1; theorem :: SUBLEMMA:35 B is quantifiable & B1 is quantifiable & Sub_All(B,SQ) = Sub_All (B1,SQ1) implies B`2 = B1`2 & SQ = SQ1; theorem :: SUBLEMMA:36 B is quantifiable & B1 is quantifiable & CQCSub_All(B,SQ) = Sub_All(B1,SQ1) implies B`2 = B1`2 & SQ = SQ1; theorem :: SUBLEMMA:37 [S,x] is quantifiable implies Sub_the_bound_of CQCSub_All([S,x],xSQ) = x; theorem :: SUBLEMMA:38 [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); theorem :: SUBLEMMA:39 [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); theorem :: SUBLEMMA:40 [S,x] is quantifiable implies not S_Bound(@CQCSub_All([S,x],xSQ) ) in rng RestrictSub(x,All(x,S`1),xSQ); theorem :: SUBLEMMA:41 [S,x] is quantifiable implies S`2 = ExpandSub(x,S`1,RestrictSub( x,All(x,S`1),xSQ)); theorem :: SUBLEMMA:42 still_not-bound_in VERUM(Al) c= Bound_Vars(VERUM(Al)); theorem :: SUBLEMMA:43 still_not-bound_in (P!ll) = Bound_Vars(P!ll); theorem :: SUBLEMMA:44 still_not-bound_in (p) c= Bound_Vars(p) implies still_not-bound_in ('not' p) c= Bound_Vars('not' p); theorem :: SUBLEMMA:45 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); theorem :: SUBLEMMA:46 still_not-bound_in p c= Bound_Vars(p) implies still_not-bound_in All(x,p) c= Bound_Vars(All(x,p)); theorem :: SUBLEMMA:47 for p holds still_not-bound_in p c= Bound_Vars(p); 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; end; reserve a for Element of A; theorem :: SUBLEMMA:48 x <> b implies v.(x|a).b = v.b; theorem :: SUBLEMMA:49 x = y implies v.(x|a).y = a; theorem :: SUBLEMMA:50 J,v |= All(x,p) iff for a holds J,v.(x|a) |= p; definition let Al, S, x, xSQ, A, v; func NEx_Val(v,S,x,xSQ) -> Val_Sub of A,Al equals :: SUBLEMMA:def 8 (@RestrictSub(x,All(x,S`1), xSQ))*v; end; definition let Al, A; let v,w be Val_Sub of A,Al; redefine func v+*w -> Val_Sub of A,Al; end; theorem :: SUBLEMMA:51 [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); theorem :: SUBLEMMA:52 [S,x] is quantifiable & not x in rng RestrictSub(x,All(x,S`1), xSQ) implies S_Bound(@CQCSub_All([S,x],xSQ)) = x; theorem :: SUBLEMMA:53 [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}; theorem :: SUBLEMMA:54 [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); theorem :: SUBLEMMA:55 [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); theorem :: SUBLEMMA:56 [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 ); begin :: The Coincidence Lemma theorem :: SUBLEMMA:57 rng l1 c= bound_QC-variables(Al) implies still_not-bound_in l1 = rng l1; theorem :: SUBLEMMA:58 dom v = bound_QC-variables(Al) & dom (x|a) = {x}; theorem :: SUBLEMMA:59 v*'ll = ll*(v|still_not-bound_in ll); theorem :: SUBLEMMA:60 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)); theorem :: SUBLEMMA:61 (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); theorem :: SUBLEMMA:62 (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); theorem :: SUBLEMMA:63 for X being set st X c= bound_QC-variables(Al) holds dom (v|X) = dom (v.(x|a)|X) & dom (v|X) = X; theorem :: SUBLEMMA:64 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; theorem :: SUBLEMMA:65 still_not-bound_in p c= still_not-bound_in (All(x,p)) \/ {x}; theorem :: SUBLEMMA:66 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; theorem :: SUBLEMMA:67 (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)); :: Coincidence Lemma (Ebb et al, Chapter III, 5.1) theorem :: SUBLEMMA:68 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); theorem :: SUBLEMMA:69 [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; theorem :: SUBLEMMA:70 [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 ); theorem :: SUBLEMMA:71 dom NEx_Val(v,S,x,xSQ) = dom RestrictSub(x,All(x,S`1),xSQ); theorem :: SUBLEMMA:72 (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; theorem :: SUBLEMMA:73 (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; theorem :: SUBLEMMA:74 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; theorem :: SUBLEMMA:75 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; theorem :: SUBLEMMA:76 (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; theorem :: SUBLEMMA:77 (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; theorem :: SUBLEMMA:78 (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; theorem :: SUBLEMMA:79 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; theorem :: SUBLEMMA:80 (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); theorem :: SUBLEMMA:81 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; definition let Al, p; func RSub1(p) -> set means :: SUBLEMMA:def 9 b in it iff ex x st x = b & not x in still_not-bound_in p; end; definition let Al, p, Sub; func RSub2(p,Sub) -> set means :: SUBLEMMA:def 10 b in it iff ex x st x = b & x in still_not-bound_in p & x = (@Sub).x; end; theorem :: SUBLEMMA:82 dom ((@Sub)|RSub1(p)) misses dom ((@Sub)|RSub2(p,Sub)); theorem :: SUBLEMMA:83 @RestrictSub(x,All(x,p),Sub) = @Sub \ ((@Sub)|RSub1(All(x,p)) +* (@Sub)|RSub2(All(x,p),Sub)); theorem :: SUBLEMMA:84 dom @RestrictSub(x,p,Sub) misses dom ((@Sub)|RSub1(p)) \/ dom (( @Sub)|RSub2(p,Sub)); theorem :: SUBLEMMA:85 [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); theorem :: SUBLEMMA:86 [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); theorem :: SUBLEMMA:87 [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) ); theorem :: SUBLEMMA:88 [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)); scheme :: SUBLEMMA:sch 1 SubCQCInd1 { Al() -> QC-alphabet, Pro[set] } : for S being Element of CQC-Sub-WFF(Al()) holds Pro[S] provided 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)]); :: Substitution Lemma (Ebb et al, Chapter III, 8.3) theorem :: SUBLEMMA:89 for S, v holds (J,v |= CQC_Sub(S) iff J,v.Val_S(v,S) |= S);