:: SUBLEMMA semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: SUBLEMMA:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th2: :: SUBLEMMA:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for vS1 being Function st x in dom vS1 holds
(vS1 | ((dom vS1) \ {x})) +* (x .--> (vS1 . x)) = vS1
proof end;

definition
let A be non empty set ;
mode Val_Sub of A is PartFunc of bound_QC-variables ,A;
end;

definition
let A be non empty set ;
let v be Element of Valuations_in A;
let vS be Val_Sub of A;
func v . vS -> Element of Valuations_in A equals :: SUBLEMMA:def 1
v +* vS;
coherence
v +* vS is Element of Valuations_in A
proof end;
end;

:: deftheorem defines . SUBLEMMA:def 1 :
for A being non empty set
for v being Element of Valuations_in A
for vS being Val_Sub of A holds v . vS = v +* vS;

definition
let S be Element of CQC-Sub-WFF ;
:: original: `1
redefine func S `1 -> Element of CQC-WFF ;
coherence
S `1 is Element of CQC-WFF
proof end;
end;

definition
let S be Element of CQC-Sub-WFF ;
let A be non empty set ;
let v be Element of Valuations_in A;
func Val_S v,S -> Val_Sub of A equals :: SUBLEMMA:def 2
(@ (S `2 )) * v;
coherence
(@ (S `2 )) * v is Val_Sub of A ;
end;

:: deftheorem defines Val_S SUBLEMMA:def 2 :
for S being Element of CQC-Sub-WFF
for A being non empty set
for v being Element of Valuations_in A holds Val_S v,S = (@ (S `2 )) * v;

theorem Th3: :: SUBLEMMA:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Element of CQC-Sub-WFF st S is Sub_VERUM holds
CQC_Sub S = VERUM
proof end;

definition
let S be Element of CQC-Sub-WFF ;
let A be non empty set ;
let v be Element of Valuations_in A;
let J be interpretation of A;
pred J,v |= S means :Def3: :: SUBLEMMA:def 3
J,v |= S `1 ;
end;

:: deftheorem Def3 defines |= SUBLEMMA:def 3 :
for S being Element of CQC-Sub-WFF
for A being non empty set
for v being Element of Valuations_in A
for J being interpretation of A holds
( J,v |= S iff J,v |= S `1 );

theorem Th4: :: SUBLEMMA:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for J being interpretation of A
for S being Element of CQC-Sub-WFF st S is Sub_VERUM holds
for v being Element of Valuations_in A holds
( J,v |= CQC_Sub S iff J,v . (Val_S v,S) |= S )
proof end;

theorem Th5: :: SUBLEMMA:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, i being Nat
for ll being CQC-variable_list of k st i in dom ll holds
ll . i is bound_QC-variable
proof end;

theorem Th6: :: SUBLEMMA:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Element of CQC-Sub-WFF st S is Sub_atomic holds
CQC_Sub S = (the_pred_symbol_of (S `1 )) ! (CQC_Subst (Sub_the_arguments_of S),(S `2 ))
proof end;

theorem :: SUBLEMMA:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for P, P' being QC-pred_symbol of k
for ll, ll' being CQC-variable_list of k
for Sub, Sub' being CQC_Substitution st Sub_the_arguments_of (Sub_P P,ll,Sub) = Sub_the_arguments_of (Sub_P P',ll',Sub') holds
ll = ll'
proof end;

definition
let k be Nat;
let P be QC-pred_symbol of k;
let ll be CQC-variable_list of k;
let Sub be CQC_Substitution;
:: original: Sub_P
redefine func Sub_P P,ll,Sub -> Element of CQC-Sub-WFF ;
coherence
Sub_P P,ll,Sub is Element of CQC-Sub-WFF
proof end;
end;

theorem :: SUBLEMMA:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th9: :: SUBLEMMA:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for P being QC-pred_symbol of k
for ll being CQC-variable_list of k
for Sub being CQC_Substitution holds CQC_Sub (Sub_P P,ll,Sub) = P ! (CQC_Subst ll,Sub)
proof end;

theorem :: SUBLEMMA:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for P being QC-pred_symbol of k
for ll being CQC-variable_list of k
for Sub being CQC_Substitution holds P ! (CQC_Subst ll,Sub) is Element of CQC-WFF
proof end;

theorem Th11: :: SUBLEMMA:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for ll being CQC-variable_list of k
for Sub being CQC_Substitution holds CQC_Subst ll,Sub is CQC-variable_list of k
proof end;

definition
let k be Nat;
let ll be CQC-variable_list of k;
let Sub be CQC_Substitution;
:: original: CQC_Subst
redefine func CQC_Subst ll,Sub -> CQC-variable_list of k;
coherence
CQC_Subst ll,Sub is CQC-variable_list of k by Th11;
end;

theorem Th12: :: SUBLEMMA:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for A being non empty set
for v being Element of Valuations_in A
for S being Element of CQC-Sub-WFF st not x in dom (S `2 ) holds
(v . (Val_S v,S)) . x = v . x
proof end;

theorem Th13: :: SUBLEMMA:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for A being non empty set
for v being Element of Valuations_in A
for S being Element of CQC-Sub-WFF st x in dom (S `2 ) holds
(v . (Val_S v,S)) . x = (Val_S v,S) . x
proof end;

theorem Th14: :: SUBLEMMA:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for A being non empty set
for v being Element of Valuations_in A
for P being QC-pred_symbol of k
for ll being CQC-variable_list of k
for Sub being CQC_Substitution holds (v . (Val_S v,(Sub_P P,ll,Sub))) *' ll = v *' (CQC_Subst ll,Sub)
proof end;

theorem Th15: :: SUBLEMMA:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for P being QC-pred_symbol of k
for ll being CQC-variable_list of k
for Sub being CQC_Substitution holds (Sub_P P,ll,Sub) `1 = P ! ll
proof end;

theorem Th16: :: SUBLEMMA:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for A being non empty set
for J being interpretation of A
for P being QC-pred_symbol of k
for ll being CQC-variable_list of k
for Sub being CQC_Substitution
for v being Element of Valuations_in A 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 end;

theorem Th17: :: SUBLEMMA:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Element of CQC-Sub-WFF holds
( (Sub_not S) `1 = 'not' (S `1 ) & (Sub_not S) `2 = S `2 )
proof end;

definition
let S be Element of CQC-Sub-WFF ;
:: original: Sub_not
redefine func Sub_not S -> Element of CQC-Sub-WFF ;
coherence
Sub_not S is Element of CQC-Sub-WFF
proof end;
end;

theorem Th18: :: SUBLEMMA:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for J being interpretation of A
for v being Element of Valuations_in A
for S being Element of CQC-Sub-WFF holds
( not J,v . (Val_S v,S) |= S iff J,v . (Val_S v,S) |= Sub_not S )
proof end;

theorem Th19: :: SUBLEMMA:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for v being Element of Valuations_in A
for S being Element of CQC-Sub-WFF holds Val_S v,S = Val_S v,(Sub_not S)
proof end;

theorem Th20: :: SUBLEMMA:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for J being interpretation of A
for S being Element of CQC-Sub-WFF st ( for v being Element of Valuations_in A holds
( J,v |= CQC_Sub S iff J,v . (Val_S v,S) |= S ) ) holds
for v being Element of Valuations_in A holds
( J,v |= CQC_Sub (Sub_not S) iff J,v . (Val_S v,(Sub_not S)) |= Sub_not S )
proof end;

definition
let S1, S2 be Element of CQC-Sub-WFF ;
assume A1: S1 `2 = S2 `2 ;
func CQCSub_& S1,S2 -> Element of CQC-Sub-WFF equals :Def4: :: SUBLEMMA:def 4
 Sub_& S1,S2;
coherence
Sub_& S1,S2 is Element of CQC-Sub-WFF
proof end;
end;

:: deftheorem Def4 defines CQCSub_& SUBLEMMA:def 4 :
for S1, S2 being Element of CQC-Sub-WFF st S1 `2 = S2 `2 holds
CQCSub_& S1,S2 = Sub_& S1,S2;

theorem Th21: :: SUBLEMMA:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being Element of CQC-Sub-WFF st S1 `2 = S2 `2 holds
( (CQCSub_& S1,S2) `1 = (S1 `1 ) '&' (S2 `1 ) & (CQCSub_& S1,S2) `2 = S1 `2 )
proof end;

theorem Th22: :: SUBLEMMA:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being Element of CQC-Sub-WFF st S1 `2 = S2 `2 holds
(CQCSub_& S1,S2) `2 = S1 `2
proof end;

theorem Th23: :: SUBLEMMA:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for v being Element of Valuations_in A
for S1, S2 being Element of CQC-Sub-WFF st S1 `2 = S2 `2 holds
( Val_S v,S1 = Val_S v,(CQCSub_& S1,S2) & Val_S v,S2 = Val_S v,(CQCSub_& S1,S2) ) by Th22;

theorem Th24: :: SUBLEMMA:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being Element of CQC-Sub-WFF st S1 `2 = S2 `2 holds
CQC_Sub (CQCSub_& S1,S2) = (CQC_Sub S1) '&' (CQC_Sub S2)
proof end;

theorem Th25: :: SUBLEMMA:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for J being interpretation of A
for v being Element of Valuations_in A
for S1, S2 being Element of CQC-Sub-WFF st S1 `2 = S2 `2 holds
( ( 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 end;

theorem Th26: :: SUBLEMMA:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for J being interpretation of A
for S1, S2 being Element of CQC-Sub-WFF st S1 `2 = S2 `2 & ( for v being Element of Valuations_in A holds
( J,v |= CQC_Sub S1 iff J,v . (Val_S v,S1) |= S1 ) ) & ( for v being Element of Valuations_in A holds
( J,v |= CQC_Sub S2 iff J,v . (Val_S v,S2) |= S2 ) ) holds
for v being Element of Valuations_in A holds
( J,v |= CQC_Sub (CQCSub_& S1,S2) iff J,v . (Val_S v,(CQCSub_& S1,S2)) |= CQCSub_& S1,S2 )
proof end;

theorem Th27: :: SUBLEMMA:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B being Element of [:QC-Sub-WFF ,bound_QC-variables :]
for SQ being second_Q_comp of B st B is quantifiable holds
( (Sub_All B,SQ) `1 = All (B `2 ),((B `1 ) `1 ) & (Sub_All B,SQ) `2 = SQ )
proof end;

definition
let B be Element of [:QC-Sub-WFF ,bound_QC-variables :];
attr B is CQC-WFF-like means :Def5: :: SUBLEMMA:def 5
B `1 in CQC-Sub-WFF ;
end;

:: deftheorem Def5 defines CQC-WFF-like SUBLEMMA:def 5 :
for B being Element of [:QC-Sub-WFF ,bound_QC-variables :] holds
( B is CQC-WFF-like iff B `1 in CQC-Sub-WFF );

registration
cluster CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :];
existence
ex b1 being Element of [:QC-Sub-WFF ,bound_QC-variables :] st b1 is CQC-WFF-like
proof end;
end;

definition
let S be Element of CQC-Sub-WFF ;
let x be bound_QC-variable;
:: original: [
redefine func [S,x] -> CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :];
coherence
[S,x] is CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :]
proof end;
end;

definition
let B be CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :];
:: original: `1
redefine func B `1 -> Element of CQC-Sub-WFF ;
coherence
B `1 is Element of CQC-Sub-WFF by Def5;
end;

definition
let B be CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :];
let SQ be second_Q_comp of B;
assume A1: B is quantifiable ;
func CQCSub_All B,SQ -> Element of CQC-Sub-WFF equals :Def6: :: SUBLEMMA:def 6
 Sub_All B,SQ;
coherence
Sub_All B,SQ is Element of CQC-Sub-WFF
proof end;
end;

:: deftheorem Def6 defines CQCSub_All SUBLEMMA:def 6 :
for B being CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :]
for SQ being second_Q_comp of B st B is quantifiable holds
CQCSub_All B,SQ = Sub_All B,SQ;

theorem Th28: :: SUBLEMMA:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B being CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :]
for SQ being second_Q_comp of B st B is quantifiable holds
CQCSub_All B,SQ is Sub_universal
proof end;

definition
let S be Element of CQC-Sub-WFF ;
assume A1: S is Sub_universal ;
func CQCSub_the_scope_of S -> Element of CQC-Sub-WFF equals :Def7: :: SUBLEMMA:def 7
 Sub_the_scope_of S;
coherence
Sub_the_scope_of S is Element of CQC-Sub-WFF
proof end;
end;

:: deftheorem Def7 defines CQCSub_the_scope_of SUBLEMMA:def 7 :
for S being Element of CQC-Sub-WFF st S is Sub_universal holds
CQCSub_the_scope_of S = Sub_the_scope_of S;

definition
let S1 be Element of CQC-Sub-WFF ;
let p be Element of CQC-WFF ;
assume A1: ( S1 is Sub_universal & p = CQC_Sub (CQCSub_the_scope_of S1) ) ;
func CQCQuant S1,p -> Element of CQC-WFF equals :Def8: :: SUBLEMMA:def 8
 Quant S1,p;
coherence
Quant S1,p is Element of CQC-WFF
proof end;
end;

:: deftheorem Def8 defines CQCQuant SUBLEMMA:def 8 :
for S1 being Element of CQC-Sub-WFF
for p being Element of CQC-WFF st S1 is Sub_universal & p = CQC_Sub (CQCSub_the_scope_of S1) holds
CQCQuant S1,p = Quant S1,p;

theorem Th29: :: SUBLEMMA:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Element of CQC-Sub-WFF st S is Sub_universal holds
CQC_Sub S = CQCQuant S,(CQC_Sub (CQCSub_the_scope_of S))
proof end;

theorem Th30: :: SUBLEMMA:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B being CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :]
for SQ being second_Q_comp of B st B is quantifiable holds
CQCSub_the_scope_of (CQCSub_All B,SQ) = B `1
proof end;

theorem Th31: :: SUBLEMMA:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
( 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 end;

theorem Th32: :: SUBLEMMA:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
CQCQuant (CQCSub_All [S,x],xSQ),(CQC_Sub S) = All (S_Bound (@ (CQCSub_All [S,x],xSQ))),(CQC_Sub S)
proof end;

theorem :: SUBLEMMA:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for A being non empty set
for v being Element of Valuations_in A
for S being Element of CQC-Sub-WFF st x in dom (S `2 ) holds
v . ((@ (S `2 )) . x) = (v . (Val_S v,S)) . x
proof end;

theorem :: SUBLEMMA:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for S being Element of CQC-Sub-WFF st x in dom (@ (S `2 )) holds
(@ (S `2 )) . x is bound_QC-variable
proof end;

theorem Th35: :: SUBLEMMA:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
[:QC-WFF ,vSUB :] c= dom QSub
proof end;

theorem Th36: :: SUBLEMMA:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B being CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :]
for SQ being second_Q_comp of B
for B1 being Element of [:QC-Sub-WFF ,bound_QC-variables :]
for SQ1 being second_Q_comp of B1 st B is quantifiable & B1 is quantifiable & Sub_All B,SQ = Sub_All B1,SQ1 holds
( B `2 = B1 `2 & SQ = SQ1 )
proof end;

theorem Th37: :: SUBLEMMA:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B being CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :]
for SQ being second_Q_comp of B
for B1 being Element of [:QC-Sub-WFF ,bound_QC-variables :]
for SQ1 being second_Q_comp of B1 st B is quantifiable & B1 is quantifiable & CQCSub_All B,SQ = Sub_All B1,SQ1 holds
( B `2 = B1 `2 & SQ = SQ1 )
proof end;

theorem :: SUBLEMMA:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
Sub_the_bound_of (CQCSub_All [S,x],xSQ) = x
proof end;

theorem Th39: :: SUBLEMMA:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & x in rng (RestrictSub x,(All x,(S `1 )),xSQ) holds
( 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 end;

theorem Th40: :: SUBLEMMA:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & not x in rng (RestrictSub x,(All x,(S `1 )),xSQ) holds
not S_Bound (@ (CQCSub_All [S,x],xSQ)) in rng (RestrictSub x,(All x,(S `1 )),xSQ)
proof end;

theorem Th41: :: SUBLEMMA:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
not S_Bound (@ (CQCSub_All [S,x],xSQ)) in rng (RestrictSub x,(All x,(S `1 )),xSQ)
proof end;

theorem Th42: :: SUBLEMMA:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
S `2 = ExpandSub x,(S `1 ),(RestrictSub x,(All x,(S `1 )),xSQ)
proof end;

theorem :: SUBLEMMA:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
still_not-bound_in VERUM c= Bound_Vars VERUM by QC_LANG3:7, SUBSTUT1:2;

theorem Th44: :: SUBLEMMA:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for P being QC-pred_symbol of k
for ll being CQC-variable_list of k holds still_not-bound_in (P ! ll) c= Bound_Vars (P ! ll)
proof end;

theorem Th45: :: SUBLEMMA:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF st still_not-bound_in p c= Bound_Vars p holds
still_not-bound_in ('not' p) c= Bound_Vars ('not' p)
proof end;

theorem Th46: :: SUBLEMMA:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of CQC-WFF st still_not-bound_in p c= Bound_Vars p & still_not-bound_in q c= Bound_Vars q holds
still_not-bound_in (p '&' q) c= Bound_Vars (p '&' q)
proof end;

theorem Th47: :: SUBLEMMA:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for x being bound_QC-variable st still_not-bound_in p c= Bound_Vars p holds
still_not-bound_in (All x,p) c= Bound_Vars (All x,p)
proof end;

theorem Th48: :: SUBLEMMA:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF holds still_not-bound_in p c= Bound_Vars p
proof end;

definition
let A be non empty set ;
let a be Element of A;
let x be bound_QC-variable;
func x | a -> Val_Sub of A equals :: SUBLEMMA:def 9
x .--> a;
coherence
x .--> a is Val_Sub of A
proof end;
end;

:: deftheorem defines | SUBLEMMA:def 9 :
for A being non empty set
for a being Element of A
for x being bound_QC-variable holds x | a = x .--> a;

theorem Th49: :: SUBLEMMA:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for b being set
for x being bound_QC-variable
for A being non empty set
for v being Element of Valuations_in A
for a being Element of A st x <> b holds
(v . (x | a)) . b = v . b
proof end;

theorem Th50: :: SUBLEMMA:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being bound_QC-variable
for A being non empty set
for v being Element of Valuations_in A
for a being Element of A st x = y holds
(v . (x | a)) . y = a
proof end;

theorem Th51: :: SUBLEMMA:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for x being bound_QC-variable
for A being non empty set
for J being interpretation of A
for v being Element of Valuations_in A holds
( J,v |= All x,p iff for a being Element of A holds J,v . (x | a) |= p )
proof end;

definition
let S be Element of CQC-Sub-WFF ;
let x be bound_QC-variable;
let xSQ be second_Q_comp of [S,x];
let A be non empty set ;
let v be Element of Valuations_in A;
func NEx_Val v,S,x,xSQ -> Val_Sub of A equals :: SUBLEMMA:def 10
(@ (RestrictSub x,(All x,(S `1 )),xSQ)) * v;
coherence
(@ (RestrictSub x,(All x,(S `1 )),xSQ)) * v is Val_Sub of A ;
end;

:: deftheorem defines NEx_Val SUBLEMMA:def 10 :
for S being Element of CQC-Sub-WFF
for x being bound_QC-variable
for xSQ being second_Q_comp of [S,x]
for A being non empty set
for v being Element of Valuations_in A holds NEx_Val v,S,x,xSQ = (@ (RestrictSub x,(All x,(S `1 )),xSQ)) * v;

definition
let A be non empty set ;
let v, w be Val_Sub of A;
:: original: +*
redefine func v +* w -> Val_Sub of A;
coherence
v +* w is Val_Sub of A
proof end;
end;

theorem Th52: :: SUBLEMMA:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & x in rng (RestrictSub x,(All x,(S `1 )),xSQ) holds
S_Bound (@ (CQCSub_All [S,x],xSQ)) = x. (upVar (RestrictSub x,(All x,(S `1 )),xSQ),(S `1 ))
proof end;

theorem Th53: :: SUBLEMMA:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & not x in rng (RestrictSub x,(All x,(S `1 )),xSQ) holds
S_Bound (@ (CQCSub_All [S,x],xSQ)) = x
proof end;

theorem Th54: :: SUBLEMMA:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for A being non empty set
for v being Element of Valuations_in A
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
for a being Element of 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 end;

theorem Th55: :: SUBLEMMA:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for A being non empty set
for J being interpretation of A
for v being Element of Valuations_in A
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
( ( for a being Element of 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 being Element of 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 end;

theorem Th56: :: SUBLEMMA:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for A being non empty set
for v being Element of Valuations_in A
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
for a being Element of A holds NEx_Val (v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)),S,x,xSQ = NEx_Val v,S,x,xSQ
proof end;

theorem Th57: :: SUBLEMMA:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for A being non empty set
for J being interpretation of A
for v being Element of Valuations_in A
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
( ( for a being Element of 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 being Element of A holds J,(v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a)) |= S )
proof end;

theorem Th58: :: SUBLEMMA:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for l1 being FinSequence of QC-variables st rng l1 c= bound_QC-variables holds
still_not-bound_in l1 = rng l1
proof end;

theorem Th59: :: SUBLEMMA:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for A being non empty set
for v being Element of Valuations_in A
for a being Element of A holds
( dom v = bound_QC-variables & dom (x | a) = {x} )
proof end;

theorem Th60: :: SUBLEMMA:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for A being non empty set
for v being Element of Valuations_in A
for ll being CQC-variable_list of k holds v *' ll = ll * (v | (still_not-bound_in ll))
proof end;

theorem Th61: :: SUBLEMMA:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for A being non empty set
for J being interpretation of A
for P being QC-pred_symbol of k
for ll being CQC-variable_list of k
for v, w being Element of Valuations_in A st v | (still_not-bound_in (P ! ll)) = w | (still_not-bound_in (P ! ll)) holds
( J,v |= P ! ll iff J,w |= P ! ll )
proof end;

theorem Th62: :: SUBLEMMA:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for A being non empty set
for J being interpretation of A st ( for v, w being Element of Valuations_in A st v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
( J,v |= p iff J,w |= p ) ) holds
for v, w being Element of Valuations_in A st v | (still_not-bound_in ('not' p)) = w | (still_not-bound_in ('not' p)) holds
( J,v |= 'not' p iff J,w |= 'not' p )
proof end;

theorem Th63: :: SUBLEMMA:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of CQC-WFF
for A being non empty set
for J being interpretation of A st ( for v, w being Element of Valuations_in A st v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
( J,v |= p iff J,w |= p ) ) & ( for v, w being Element of Valuations_in A st v | (still_not-bound_in q) = w | (still_not-bound_in q) holds
( J,v |= q iff J,w |= q ) ) holds
for v, w being Element of Valuations_in A st v | (still_not-bound_in (p '&' q)) = w | (still_not-bound_in (p '&' q)) holds
( J,v |= p '&' q iff J,w |= p '&' q )
proof end;

theorem Th64: :: SUBLEMMA:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for A being non empty set
for v being Element of Valuations_in A
for a being Element of A
for X being set st X c= bound_QC-variables holds
( dom (v | X) = dom ((v . (x | a)) | X) & dom (v | X) = X )
proof end;

theorem :: SUBLEMMA:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for x being bound_QC-variable
for A being non empty set
for v, w being Element of Valuations_in A
for a being Element of A st v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
(v . (x | a)) | (still_not-bound_in p) = (w . (x | a)) | (still_not-bound_in p)
proof end;

theorem :: SUBLEMMA:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for x being bound_QC-variable holds still_not-bound_in p c= (still_not-bound_in (All x,p)) \/ {x}
proof end;

theorem Th67: :: SUBLEMMA:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for x being bound_QC-variable
for A being non empty set
for v, w being Element of Valuations_in A
for a being Element of A st v | ((still_not-bound_in p) \ {x}) = w | ((still_not-bound_in p) \ {x}) holds
(v . (x | a)) | (still_not-bound_in p) = (w . (x | a)) | (still_not-bound_in p)
proof end;

theorem Th68: :: SUBLEMMA:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for x being bound_QC-variable
for A being non empty set
for J being interpretation of A st ( for v, w being Element of Valuations_in A st v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
( J,v |= p iff J,w |= p ) ) holds
for v, w being Element of Valuations_in A st v | (still_not-bound_in (All x,p)) = w | (still_not-bound_in (All x,p)) holds
( J,v |= All x,p iff J,w |= All x,p )
proof end;

theorem :: SUBLEMMA:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th70: :: SUBLEMMA:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for J being interpretation of A
for p being Element of CQC-WFF
for v, w being Element of Valuations_in A st v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
( J,v |= p iff J,w |= p )
proof end;

theorem Th71: :: SUBLEMMA:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for A being non empty set
for v being Element of Valuations_in A
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x]
for a being Element of A st [S,x] is quantifiable holds
((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 end;

theorem Th72: :: SUBLEMMA:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for A being non empty set
for J being interpretation of A
for v being Element of Valuations_in A
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
( ( for a being Element of A holds J,(v . ((S_Bound (@ (CQCSub_All [S,x],xSQ))) | a)) . ((NEx_Val v,S,x,xSQ) +* (x | a)) |= S ) iff for a being Element of A holds J,v . ((NEx_Val v,S,x,xSQ) +* (x | a)) |= S )
proof end;

theorem Th73: :: SUBLEMMA:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for A being non empty set
for v being Element of Valuations_in A
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] holds dom (NEx_Val v,S,x,xSQ) = dom (RestrictSub x,(All x,(S `1 )),xSQ)
proof end;

theorem Th74: :: SUBLEMMA:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for A being non empty set
for v being Element of Valuations_in A
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x]
for a being Element of A st [S,x] is quantifiable holds
v . ((NEx_Val v,S,x,xSQ) +* (x | a)) = (v . (NEx_Val v,S,x,xSQ)) . (x | a) by FUNCT_4:15;

theorem Th75: :: SUBLEMMA:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for A being non empty set
for J being interpretation of A
for v being Element of Valuations_in A
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
( ( for a being Element of A holds J,v . ((NEx_Val v,S,x,xSQ) +* (x | a)) |= S ) iff for a being Element of A holds J,(v . (NEx_Val v,S,x,xSQ)) . (x | a) |= S )
proof end;

theorem Th76: :: SUBLEMMA:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for A being non empty set
for J being interpretation of A
for v being Element of Valuations_in A
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] holds
( ( for a being Element of A holds J,(v . (NEx_Val v,S,x,xSQ)) . (x | a) |= S ) iff for a being Element of A holds J,(v . (NEx_Val v,S,x,xSQ)) . (x | a) |= S `1 )
proof end;

theorem :: SUBLEMMA:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th78: :: SUBLEMMA:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for A being non empty set
for ll being CQC-variable_list of k
for v being Element of Valuations_in A
for vS, vS1, vS2 being Val_Sub of A st ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in ll ) & ( for y being bound_QC-variable 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 end;

theorem Th79: :: SUBLEMMA:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for A being non empty set
for J being interpretation of A
for P being QC-pred_symbol of k
for ll being CQC-variable_list of k
for v being Element of Valuations_in A
for vS, vS1, vS2 being Val_Sub of A st ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in (P ! ll) ) & ( for y being bound_QC-variable 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 end;

theorem Th80: :: SUBLEMMA:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for A being non empty set
for J being interpretation of A st ( for v being Element of Valuations_in A
for vS, vS1, vS2 being Val_Sub of A st ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in p ) & ( for y being bound_QC-variable 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 ) ) holds
for v being Element of Valuations_in A
for vS, vS1, vS2 being Val_Sub of A st ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in ('not' p) ) & ( for y being bound_QC-variable 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 end;

theorem Th81: :: SUBLEMMA:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of CQC-WFF
for A being non empty set
for J being interpretation of A st ( for v being Element of Valuations_in A
for vS, vS1, vS2 being Val_Sub of A st ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in p ) & ( for y being bound_QC-variable 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 being Element of Valuations_in A
for vS, vS1, vS2 being Val_Sub of A st ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in q ) & ( for y being bound_QC-variable 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 ) ) holds
for v being Element of Valuations_in A
for vS, vS1, vS2 being Val_Sub of A st ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in (p '&' q) ) & ( for y being bound_QC-variable 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 end;

theorem Th82: :: SUBLEMMA:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for x being bound_QC-variable
for A being non empty set
for vS1 being Val_Sub of A st ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in (All x,p) ) holds
for y being bound_QC-variable st y in (dom vS1) \ {x} holds
not y in still_not-bound_in p
proof end;

theorem Th83: :: SUBLEMMA:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for A being non empty set
for v being Element of Valuations_in A
for vS being Val_Sub of A
for vS1 being Function st ( for y being bound_QC-variable st y in dom vS1 holds
vS1 . y = v . y ) & dom vS misses dom vS1 holds
for y being bound_QC-variable st y in (dom vS1) \ {x} holds
(vS1 | ((dom vS1) \ {x})) . y = (v . vS) . y
proof end;

theorem Th84: :: SUBLEMMA:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for x being bound_QC-variable
for A being non empty set
for J being interpretation of A st ( for v being Element of Valuations_in A
for vS, vS1, vS2 being Val_Sub of A st ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in p ) & ( for y being bound_QC-variable 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 ) ) holds
for v being Element of Valuations_in A
for vS, vS1, vS2 being Val_Sub of A st ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in (All x,p) ) & ( for y being bound_QC-variable 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 end;

theorem Th85: :: SUBLEMMA:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for J being interpretation of A
for p being Element of CQC-WFF
for v being Element of Valuations_in A
for vS, vS1, vS2 being Val_Sub of A st ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in p ) & ( for y being bound_QC-variable 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 end;

definition
let p be Element of CQC-WFF ;
func RSub1 p -> set means :Def11: :: SUBLEMMA:def 11
for b being set holds
( b in it iff ex x being bound_QC-variable st
( x = b & not x in still_not-bound_in p ) );
existence
ex b1 being set st
for b being set holds
( b in b1 iff ex x being bound_QC-variable st
( x = b & not x in still_not-bound_in p ) )
proof end;
uniqueness
for b1, b2 being set st ( for b being set holds
( b in b1 iff ex x being bound_QC-variable st
( x = b & not x in still_not-bound_in p ) ) ) & ( for b being set holds
( b in b2 iff ex x being bound_QC-variable st
( x = b & not x in still_not-bound_in p ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines RSub1 SUBLEMMA:def 11 :
for p being Element of CQC-WFF
for b2 being set holds
( b2 = RSub1 p iff for b being set holds
( b in b2 iff ex x being bound_QC-variable st
( x = b & not x in still_not-bound_in p ) ) );

definition
let p be Element of CQC-WFF ;
let Sub be CQC_Substitution;
func RSub2 p,Sub -> set means :Def12: :: SUBLEMMA:def 12
for b being set holds
( b in it iff ex x being bound_QC-variable st
( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) );
existence
ex b1 being set st
for b being set holds
( b in b1 iff ex x being bound_QC-variable st
( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) )
proof end;
uniqueness
for b1, b2 being set st ( for b being set holds
( b in b1 iff ex x being bound_QC-variable st
( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) ) ) & ( for b being set holds
( b in b2 iff ex x being bound_QC-variable st
( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines RSub2 SUBLEMMA:def 12 :
for p being Element of CQC-WFF
for Sub being CQC_Substitution
for b3 being set holds
( b3 = RSub2 p,Sub iff for b being set holds
( b in b3 iff ex x being bound_QC-variable st
( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) ) );

theorem Th86: :: SUBLEMMA:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for Sub being CQC_Substitution holds dom ((@ Sub) | (RSub1 p)) misses dom ((@ Sub) | (RSub2 p,Sub))
proof end;

theorem Th87: :: SUBLEMMA:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for x being bound_QC-variable
for Sub being CQC_Substitution holds @ (RestrictSub x,(All x,p),Sub) = (@ Sub) \ (((@ Sub) | (RSub1 (All x,p))) +* ((@ Sub) | (RSub2 (All x,p),Sub)))
proof end;

theorem Th88: :: SUBLEMMA:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for x being bound_QC-variable
for Sub being CQC_Substitution holds dom (@ (RestrictSub x,p,Sub)) misses (dom ((@ Sub) | (RSub1 p))) \/ (dom ((@ Sub) | (RSub2 p,Sub)))
proof end;

theorem Th89: :: SUBLEMMA:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
@ ((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 end;

theorem Th90: :: SUBLEMMA:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for A being non empty set
for v being Element of Valuations_in A
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
ex vS1, vS2 being Val_Sub of A st
( ( for y being bound_QC-variable st y in dom vS1 holds
not y in still_not-bound_in (All x,(S `1 )) ) & ( for y being bound_QC-variable 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 end;

theorem Th91: :: SUBLEMMA:91  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for A being non empty set
for J being interpretation of A
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
for v being Element of Valuations_in A 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 end;

theorem Th92: :: SUBLEMMA:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for A being non empty set
for J being interpretation of A
for S being Element of CQC-Sub-WFF
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & ( for v being Element of Valuations_in A holds
( J,v |= CQC_Sub S iff J,v . (Val_S v,S) |= S ) ) holds
for v being Element of Valuations_in A 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 end;

scheme :: SUBLEMMA:sch 1
SubCQCInd1{ P1[ set ] } :
for S being Element of CQC-Sub-WFF holds P1[S]
provided
A1: for S, S' being Element of CQC-Sub-WFF
for x being bound_QC-variable
for SQ being second_Q_comp of [S,x]
for k being Nat
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k
for e being Element of vSUB holds
( P1[ Sub_P P,ll,e] & ( S is Sub_VERUM implies P1[S] ) & ( P1[S] implies P1[ Sub_not S] ) & ( S `2 = S' `2 & P1[S] & P1[S'] implies P1[ CQCSub_& S,S'] ) & ( [S,x] is quantifiable & P1[S] implies P1[ CQCSub_All [S,x],SQ] ) )
proof end;

theorem :: SUBLEMMA:93  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for J being interpretation of A
for S being Element of CQC-Sub-WFF
for v being Element of Valuations_in A holds
( J,v |= CQC_Sub S iff J,v . (Val_S v,S) |= S )
proof end;