:: Coincidence Lemma and Substitution Lemma
:: by Patrick Braselmann and Peter Koepke
::
:: Received September 25, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users

theorem Th1: :: 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

proof end;

theorem Th2: :: SUBLEMMA:2

for Al being QC-alphabet
for x being bound_QC-variable of Al
for vS1 being Function st x in dom vS1 holds
(vS1 | ((dom vS1) \ {x})) +* (x .--> (vS1 . x)) = vS1

proof end;

definition

let Al be QC-alphabet ;
let A be non empty set ;
mode Val_Sub of A,Al is PartFunc of (bound_QC-variables Al),A;

end;

notation

let Al be QC-alphabet ;
let A be non empty set ;
let v be Element of Valuations_in (Al,A);
let vS be Val_Sub of A,Al;
synonym v . vS for Al +* A;

end;

definition

let Al be QC-alphabet ;
let A be non empty set ;
let v be Element of Valuations_in (Al,A);
let vS be Val_Sub of A,Al;
:: original: .
redefine func v . vS -> Element of Valuations_in (Al,A);
coherence
. is Element of Valuations_in (Al,A)

proof end;

end;

definition

let Al be QC-alphabet ;
let S be Element of CQC-Sub-WFF Al;
:: original: `1
redefine func S `1 -> Element of CQC-WFF Al;
coherence
S `1 is Element of CQC-WFF Al

proof end;

end;

definition

let Al be QC-alphabet ;
let S be Element of CQC-Sub-WFF Al;
let A be non empty set ;
let v be Element of Valuations_in (Al,A);

func Val_S (v,S) -> Val_Sub of A,Al equals :: SUBLEMMA:def 1
(@ (S `2)) * v;

coherence
(@ (S `2)) * v is Val_Sub of A,Al ;

end;

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

theorem Th3: :: SUBLEMMA:3

for Al being QC-alphabet
for S being Element of CQC-Sub-WFF Al st S is Al -Sub_VERUM holds
CQC_Sub S = VERUM Al

proof end;

definition

let Al be QC-alphabet ;
let S be Element of CQC-Sub-WFF Al;
let A be non empty set ;
let v be Element of Valuations_in (Al,A);
let J be interpretation of Al,A;

pred J,v |= S means :Def2: :: SUBLEMMA:def 2
J,v |= S `1 ;

end;

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

theorem Th4: :: SUBLEMMA:4

for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A
for S being Element of CQC-Sub-WFF Al st S is Al -Sub_VERUM holds
for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S )

proof end;

theorem Th5: :: SUBLEMMA:5

for Al being QC-alphabet
for i, k being Nat
for ll being CQC-variable_list of k,Al st i in dom ll holds
ll . i is bound_QC-variable of Al

proof end;

theorem Th6: :: SUBLEMMA:6

for Al being QC-alphabet
for S being Element of CQC-Sub-WFF Al 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

for Al being QC-alphabet
for k being Nat
for P, P9 being QC-pred_symbol of k,Al
for ll, ll9 being CQC-variable_list of k,Al
for Sub, Sub9 being CQC_Substitution of Al st Sub_the_arguments_of (Sub_P (P,ll,Sub)) = Sub_the_arguments_of (Sub_P (P9,ll9,Sub9)) holds
ll = ll9

proof end;

definition

let k be Nat;
let Al be QC-alphabet ;
let P be QC-pred_symbol of k,Al;
let ll be CQC-variable_list of k,Al;
let Sub be CQC_Substitution of Al;
:: original: Sub_P
redefine func Sub_P (P,ll,Sub) -> Element of CQC-Sub-WFF Al;
coherence
Sub_P (P,ll,Sub) is Element of CQC-Sub-WFF Al

proof end;

end;

theorem Th8: :: SUBLEMMA:8

for Al being QC-alphabet
for k being Nat
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al holds CQC_Sub (Sub_P (P,ll,Sub)) = P ! (CQC_Subst (ll,Sub))

proof end;

theorem :: SUBLEMMA:9

for Al being QC-alphabet
for k being Nat
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al holds P ! (CQC_Subst (ll,Sub)) is Element of CQC-WFF Al

proof end;

theorem Th10: :: SUBLEMMA:10

for Al being QC-alphabet
for k being Nat
for ll being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al holds CQC_Subst (ll,Sub) is CQC-variable_list of k,Al

proof end;

registration

let Al be QC-alphabet ;
let k be Nat;
let ll be CQC-variable_list of k,Al;
let Sub be CQC_Substitution of Al;

cluster CQC_Subst (ll,Sub) -> bound_QC-variables Al -valued k -element ;

coherence
( CQC_Subst (ll,Sub) is bound_QC-variables Al -valued & CQC_Subst (ll,Sub) is k -element ) by Th10;

end;

theorem Th11: :: SUBLEMMA:11

for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al st not x in dom (S `2) holds
(v . (Val_S (v,S))) . x = v . x

proof end;

theorem Th12: :: SUBLEMMA:12

for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al st x in dom (S `2) holds
(v . (Val_S (v,S))) . x = (Val_S (v,S)) . x

proof end;

theorem Th13: :: SUBLEMMA:13

for Al being QC-alphabet
for k being Nat
for A being non empty set
for v being Element of Valuations_in (Al,A)
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al holds (v . (Val_S (v,(Sub_P (P,ll,Sub))))) *' ll = v *' (CQC_Subst (ll,Sub))

proof end;

theorem Th14: :: SUBLEMMA:14

for Al being QC-alphabet
for k being Nat
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al holds (Sub_P (P,ll,Sub)) `1 = P ! ll

proof end;

theorem Th15: :: SUBLEMMA:15

for Al being QC-alphabet
for k being Nat
for A being non empty set
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al
for v being Element of Valuations_in (Al,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 Th16: :: SUBLEMMA:16

for Al being QC-alphabet
for S being Element of CQC-Sub-WFF Al holds
( (Sub_not S) `1 = 'not' (S `1) & (Sub_not S) `2 = S `2 )

proof end;

definition

let Al be QC-alphabet ;
let S be Element of CQC-Sub-WFF Al;
:: original: Sub_not
redefine func Sub_not S -> Element of CQC-Sub-WFF Al;
coherence
Sub_not S is Element of CQC-Sub-WFF Al

proof end;

end;

theorem Th17: :: SUBLEMMA:17

for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al holds
( not J,v . (Val_S (v,S)) |= S iff J,v . (Val_S (v,S)) |= Sub_not S )

proof end;

theorem Th18: :: SUBLEMMA:18

for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al holds Val_S (v,S) = Val_S (v,(Sub_not S))

proof end;

theorem Th19: :: SUBLEMMA:19

for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A
for S being Element of CQC-Sub-WFF Al st ( for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S ) ) holds
for v being Element of Valuations_in (Al,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 Al be QC-alphabet ;
let S1, S2 be Element of CQC-Sub-WFF Al;
assume A1: S1 `2 = S2 `2 ;

func CQCSub_& (S1,S2) -> Element of CQC-Sub-WFF Al equals :Def3: :: SUBLEMMA:def 3
Sub_& (S1,S2);

coherence
Sub_& (S1,S2) is Element of CQC-Sub-WFF Al

proof end;

end;

:: deftheorem Def3 defines CQCSub_& SUBLEMMA:def 3 :
for Al being QC-alphabet
for S1, S2 being Element of CQC-Sub-WFF Al st S1 `2 = S2 `2 holds
CQCSub_& (S1,S2) = Sub_& (S1,S2);

theorem Th20: :: SUBLEMMA:20

for Al being QC-alphabet
for S1, S2 being Element of CQC-Sub-WFF Al st S1 `2 = S2 `2 holds
( (CQCSub_& (S1,S2)) `1 = (S1 `1) '&' (S2 `1) & (CQCSub_& (S1,S2)) `2 = S1 `2 )

proof end;

theorem Th21: :: SUBLEMMA:21

for Al being QC-alphabet
for S1, S2 being Element of CQC-Sub-WFF Al st S1 `2 = S2 `2 holds
(CQCSub_& (S1,S2)) `2 = S1 `2

proof end;

theorem :: SUBLEMMA:22

for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for S1, S2 being Element of CQC-Sub-WFF Al 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 Th21;

theorem Th23: :: SUBLEMMA:23

for Al being QC-alphabet
for S1, S2 being Element of CQC-Sub-WFF Al st S1 `2 = S2 `2 holds
CQC_Sub (CQCSub_& (S1,S2)) = (CQC_Sub S1) '&' (CQC_Sub S2)

proof end;

theorem Th24: :: SUBLEMMA:24

for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A)
for S1, S2 being Element of CQC-Sub-WFF Al 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 Th25: :: SUBLEMMA:25

for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A
for S1, S2 being Element of CQC-Sub-WFF Al st S1 `2 = S2 `2 & ( for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S1 iff J,v . (Val_S (v,S1)) |= S1 ) ) & ( for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S2 iff J,v . (Val_S (v,S2)) |= S2 ) ) holds
for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub (CQCSub_& (S1,S2)) iff J,v . (Val_S (v,(CQCSub_& (S1,S2)))) |= CQCSub_& (S1,S2) )

proof end;

theorem Th26: :: SUBLEMMA:26

for Al being QC-alphabet
for B being Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
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 Al be QC-alphabet ;
let B be Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):];

attr B is CQC-WFF-like means :Def4: :: SUBLEMMA:def 4
B `1 in CQC-Sub-WFF Al;

end;

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

registration

let Al be QC-alphabet ;

cluster CQC-WFF-like for Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):];

existence
ex b₁ being Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):] st b₁ is CQC-WFF-like

proof end;

end;

definition

let Al be QC-alphabet ;
let S be Element of CQC-Sub-WFF Al;
let x be bound_QC-variable of Al;
:: original: [
redefine func [S,x] -> CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):];
coherence
[S,x] is CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]

proof end;

end;

definition

let Al be QC-alphabet ;
let B be CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):];
:: original: `1
redefine func B `1 -> Element of CQC-Sub-WFF Al;
coherence
B `1 is Element of CQC-Sub-WFF Al by Def4;

end;

definition

let Al be QC-alphabet ;
let B be CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):];
let SQ be second_Q_comp of B;
assume A1: B is quantifiable ;

func CQCSub_All (B,SQ) -> Element of CQC-Sub-WFF Al equals :Def5: :: SUBLEMMA:def 5
Sub_All (B,SQ);

coherence
Sub_All (B,SQ) is Element of CQC-Sub-WFF Al

proof end;

end;

:: deftheorem Def5 defines CQCSub_All SUBLEMMA:def 5 :
for Al being QC-alphabet
for B being CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
for SQ being second_Q_comp of B st B is quantifiable holds
CQCSub_All (B,SQ) = Sub_All (B,SQ);

theorem Th27: :: SUBLEMMA:27

for Al being QC-alphabet
for B being CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
for SQ being second_Q_comp of B st B is quantifiable holds
CQCSub_All (B,SQ) is Sub_universal

proof end;

definition

let Al be QC-alphabet ;
let S be Element of CQC-Sub-WFF Al;
assume A1: S is Sub_universal ;

func CQCSub_the_scope_of S -> Element of CQC-Sub-WFF Al equals :Def6: :: SUBLEMMA:def 6
Sub_the_scope_of S;

coherence
Sub_the_scope_of S is Element of CQC-Sub-WFF Al

proof end;

end;

:: deftheorem Def6 defines CQCSub_the_scope_of SUBLEMMA:def 6 :
for Al being QC-alphabet
for S being Element of CQC-Sub-WFF Al st S is Sub_universal holds
CQCSub_the_scope_of S = Sub_the_scope_of S;

definition

let Al be QC-alphabet ;
let S1 be Element of CQC-Sub-WFF Al;
let p be Element of CQC-WFF Al;
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: :: SUBLEMMA:def 7
Quant (S1,p);

coherence
Quant (S1,p) is Element of CQC-WFF Al

proof end;

end;

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

theorem Th28: :: SUBLEMMA:28

for Al being QC-alphabet
for S being Element of CQC-Sub-WFF Al st S is Sub_universal holds
CQC_Sub S = CQCQuant (S,(CQC_Sub (CQCSub_the_scope_of S)))

proof end;

theorem Th29: :: SUBLEMMA:29

for Al being QC-alphabet
for B being CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
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 Th30: :: SUBLEMMA:30

for Al being QC-alphabet
for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
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 Th31: :: SUBLEMMA:31

for Al being QC-alphabet
for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
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:32

for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al st x in dom (S `2) holds
v . ((@ (S `2)) . x) = (v . (Val_S (v,S))) . x

proof end;

theorem :: SUBLEMMA:33

for Al being QC-alphabet
for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al st x in dom (@ (S `2)) holds
(@ (S `2)) . x is bound_QC-variable of Al

proof end;

theorem Th34: :: SUBLEMMA:34

for Al being QC-alphabet holds [:(QC-WFF Al),(vSUB Al):] c= dom (QSub Al)

proof end;

theorem Th35: :: SUBLEMMA:35

for Al being QC-alphabet
for B being CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
for SQ being second_Q_comp of B
for B1 being Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
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 Th36: :: SUBLEMMA:36

for Al being QC-alphabet
for B being CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
for SQ being second_Q_comp of B
for B1 being Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):]
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:37

for Al being QC-alphabet
for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
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 Th38: :: SUBLEMMA:38

for Al being QC-alphabet
for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
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 Th39: :: SUBLEMMA:39

for Al being QC-alphabet
for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
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 Th40: :: SUBLEMMA:40

for Al being QC-alphabet
for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
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 Th41: :: SUBLEMMA:41

for Al being QC-alphabet
for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
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:42

for Al being QC-alphabet holds still_not-bound_in (VERUM Al) c= Bound_Vars (VERUM Al) by QC_LANG3:3;

theorem Th43: :: SUBLEMMA:43

for Al being QC-alphabet
for k being Nat
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al holds still_not-bound_in (P ! ll) = Bound_Vars (P ! ll)

proof end;

theorem Th44: :: SUBLEMMA:44

for Al being QC-alphabet
for p being Element of CQC-WFF Al 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 Th45: :: SUBLEMMA:45

for Al being QC-alphabet
for p, q being Element of CQC-WFF Al 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 Th46: :: SUBLEMMA:46

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al 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 Th47: :: SUBLEMMA:47

for Al being QC-alphabet
for p being Element of CQC-WFF Al holds still_not-bound_in p c= Bound_Vars p

proof end;

notation

let Al be QC-alphabet ;
let A be non empty set ;
let x be bound_QC-variable of Al;
let a be Element of A;
synonym x | a for Al .--> A;

end;

definition

let Al be QC-alphabet ;
let A be non empty set ;
let x be bound_QC-variable of Al;
let a be Element of A;
:: original: |
redefine func x | a -> Val_Sub of A,Al;
coherence
| is Val_Sub of A,Al

proof end;

end;

theorem Th48: :: SUBLEMMA:48

for Al being QC-alphabet
for b being object
for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for a being Element of A st x <> b holds
(v . (x | a)) . b = v . b

proof end;

theorem Th49: :: SUBLEMMA:49

for Al being QC-alphabet
for x, y being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for a being Element of A st x = y holds
(v . (x | a)) . y = a

proof end;

theorem Th50: :: SUBLEMMA:50

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds
( J,v |= All (x,p) iff for a being Element of A holds J,v . (x | a) |= p )

proof end;

definition

let Al be QC-alphabet ;
let S be Element of CQC-Sub-WFF Al;
let x be bound_QC-variable of Al;
let xSQ be second_Q_comp of [S,x];
let A be non empty set ;
let v be Element of Valuations_in (Al,A);

func NEx_Val (v,S,x,xSQ) -> Val_Sub of A,Al equals :: SUBLEMMA:def 8
(@ (RestrictSub (x,(All (x,(S `1))),xSQ))) * v;

coherence
(@ (RestrictSub (x,(All (x,(S `1))),xSQ))) * v is Val_Sub of A,Al ;

end;

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

definition

let Al be QC-alphabet ;
let A be non empty set ;
let v, w be Val_Sub of A,Al;
:: original: .
redefine func v +* w -> Val_Sub of A,Al;
coherence
. is Val_Sub of A,Al

proof end;

end;

theorem Th51: :: SUBLEMMA:51

for Al being QC-alphabet
for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
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 Th52: :: SUBLEMMA:52

for Al being QC-alphabet
for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
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 Th53: :: SUBLEMMA:53

for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
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 Th54: :: SUBLEMMA:54

for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
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 Th55: :: SUBLEMMA:55

for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
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 Th56: :: SUBLEMMA:56

for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
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 Th57: :: SUBLEMMA:57

for Al being QC-alphabet
for l1 being FinSequence of QC-variables Al st rng l1 c= bound_QC-variables Al holds
still_not-bound_in l1 = rng l1

proof end;

theorem Th58: :: SUBLEMMA:58

for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for a being Element of A holds
( dom v = bound_QC-variables Al & dom (x | a) = {x} )

proof end;

theorem Th59: :: SUBLEMMA:59

for Al being QC-alphabet
for k being Nat
for A being non empty set
for v being Element of Valuations_in (Al,A)
for ll being CQC-variable_list of k,Al holds v *' ll = ll * (v | (still_not-bound_in ll))

proof end;

theorem Th60: :: SUBLEMMA:60

for Al being QC-alphabet
for k being Nat
for A being non empty set
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for v, w being Element of Valuations_in (Al,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 Th61: :: SUBLEMMA:61

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for A being non empty set
for J being interpretation of Al,A st ( for v, w being Element of Valuations_in (Al,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 (Al,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 Th62: :: SUBLEMMA:62

for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for A being non empty set
for J being interpretation of Al,A st ( for v, w being Element of Valuations_in (Al,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 (Al,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 (Al,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 Th63: :: SUBLEMMA:63

for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for a being Element of A
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 end;

theorem :: SUBLEMMA:64

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for A being non empty set
for v, w being Element of Valuations_in (Al,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:65

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds still_not-bound_in p c= (still_not-bound_in (All (x,p))) \/ {x}

proof end;

theorem Th66: :: SUBLEMMA:66

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for A being non empty set
for v, w being Element of Valuations_in (Al,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 Th67: :: SUBLEMMA:67

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A st ( for v, w being Element of Valuations_in (Al,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 (Al,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;

:: Coincidence Lemma (Ebb et al, Chapter III, 5.1)

theorem Th68: :: SUBLEMMA:68

for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A
for p being Element of CQC-WFF Al
for v, w being Element of Valuations_in (Al,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 Th69: :: SUBLEMMA:69

for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
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 Th70: :: SUBLEMMA:70

for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
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 Th71: :: SUBLEMMA:71

for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
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 Th72: :: SUBLEMMA:72

for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
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 )

proof end;

theorem Th73: :: SUBLEMMA:73

for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
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 ) by Def2;

theorem Th74: :: SUBLEMMA:74

for Al being QC-alphabet
for k being Nat
for A being non empty set
for ll being CQC-variable_list of k,Al
for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in ll ) & ( for y being bound_QC-variable of Al 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 Th75: :: SUBLEMMA:75

for Al being QC-alphabet
for k being Nat
for A being non empty set
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (P ! ll) ) & ( for y being bound_QC-variable of Al 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 Th76: :: SUBLEMMA:76

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for A being non empty set
for J being interpretation of Al,A st ( for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in p ) & ( for y being bound_QC-variable of Al 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 (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in ('not' p) ) & ( for y being bound_QC-variable of Al 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 Th77: :: SUBLEMMA:77

for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for A being non empty set
for J being interpretation of Al,A st ( for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in p ) & ( for y being bound_QC-variable of Al 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 (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in q ) & ( for y being bound_QC-variable of Al 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 (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (p '&' q) ) & ( for y being bound_QC-variable of Al 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 Th78: :: SUBLEMMA:78

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for A being non empty set
for vS1 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (All (x,p)) ) holds
for y being bound_QC-variable of Al st y in (dom vS1) \ {x} holds
not y in still_not-bound_in p

proof end;

theorem Th79: :: SUBLEMMA:79

for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for vS being Val_Sub of A,Al
for vS1 being Function st ( for y being bound_QC-variable of Al st y in dom vS1 holds
vS1 . y = v . y ) & dom vS misses dom vS1 holds
for y being bound_QC-variable of Al st y in (dom vS1) \ {x} holds
(vS1 | ((dom vS1) \ {x})) . y = (v . vS) . y

proof end;

theorem Th80: :: SUBLEMMA:80

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A st ( for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in p ) & ( for y being bound_QC-variable of Al 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 (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (All (x,p)) ) & ( for y being bound_QC-variable of Al 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 Th81: :: SUBLEMMA:81

for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A
for p being Element of CQC-WFF Al
for v being Element of Valuations_in (Al,A)
for vS, vS1, vS2 being Val_Sub of A,Al st ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in p ) & ( for y being bound_QC-variable of Al 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 Al be QC-alphabet ;
let p be Element of CQC-WFF Al;

func RSub1 p -> set means :Def9: :: SUBLEMMA:def 9
for b being object holds
( b in it iff ex x being bound_QC-variable of Al st
( x = b & not x in still_not-bound_in p ) );

existence
ex b₁ being set st
for b being object holds
( b in b₁ iff ex x being bound_QC-variable of Al st
( x = b & not x in still_not-bound_in p ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for b being object holds
( b in b₁ iff ex x being bound_QC-variable of Al st
( x = b & not x in still_not-bound_in p ) ) ) & ( for b being object holds
( b in b₂ iff ex x being bound_QC-variable of Al st
( x = b & not x in still_not-bound_in p ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines RSub1 SUBLEMMA:def 9 :
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for b₃ being set holds
( b₃ = RSub1 p iff for b being object holds
( b in b₃ iff ex x being bound_QC-variable of Al st
( x = b & not x in still_not-bound_in p ) ) );

definition

let Al be QC-alphabet ;
let p be Element of CQC-WFF Al;
let Sub be CQC_Substitution of Al;

func RSub2 (p,Sub) -> set means :Def10: :: SUBLEMMA:def 10
for b being object holds
( b in it iff ex x being bound_QC-variable of Al st
( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) );

existence
ex b₁ being set st
for b being object holds
( b in b₁ iff ex x being bound_QC-variable of Al st
( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for b being object holds
( b in b₁ iff ex x being bound_QC-variable of Al st
( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) ) ) & ( for b being object holds
( b in b₂ iff ex x being bound_QC-variable of Al st
( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines RSub2 SUBLEMMA:def 10 :
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for Sub being CQC_Substitution of Al
for b₄ being set holds
( b₄ = RSub2 (p,Sub) iff for b being object holds
( b in b₄ iff ex x being bound_QC-variable of Al st
( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) ) );

theorem Th82: :: SUBLEMMA:82

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for Sub being CQC_Substitution of Al holds dom ((@ Sub) | (RSub1 p)) misses dom ((@ Sub) | (RSub2 (p,Sub)))

proof end;

theorem Th83: :: SUBLEMMA:83

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for Sub being CQC_Substitution of Al holds @ (RestrictSub (x,(All (x,p)),Sub)) = (@ Sub) \ (((@ Sub) | (RSub1 (All (x,p)))) +* ((@ Sub) | (RSub2 ((All (x,p)),Sub))))

proof end;

theorem Th84: :: SUBLEMMA:84

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for Sub being CQC_Substitution of Al holds dom (@ (RestrictSub (x,p,Sub))) misses (dom ((@ Sub) | (RSub1 p))) \/ (dom ((@ Sub) | (RSub2 (p,Sub))))

proof end;

theorem Th85: :: SUBLEMMA:85

for Al being QC-alphabet
for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al
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 Th86: :: SUBLEMMA:86

for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for v being Element of Valuations_in (Al,A)
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
ex vS1, vS2 being Val_Sub of A,Al st
( ( for y being bound_QC-variable of Al st y in dom vS1 holds
not y in still_not-bound_in (All (x,(S `1))) ) & ( for y being bound_QC-variable of Al 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 Th87: :: SUBLEMMA:87

for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable holds
for v being Element of Valuations_in (Al,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 Th88: :: SUBLEMMA:88

for Al being QC-alphabet
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A
for S being Element of CQC-Sub-WFF Al
for xSQ being second_Q_comp of [S,x] st [S,x] is quantifiable & ( for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S ) ) holds
for v being Element of Valuations_in (Al,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{ F₁() -> QC-alphabet , P₁[ set ] } :

for S being Element of CQC-Sub-WFF F₁() holds P₁[S]

provided

A1: for S, S9 being Element of CQC-Sub-WFF F₁()
for x being bound_QC-variable of F₁()
for SQ being second_Q_comp of [S,x]
for k being Nat
for ll being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁()
for e being Element of vSUB F₁() holds
( P₁[ Sub_P (P,ll,e)] & ( S is F₁() -Sub_VERUM implies P₁[S] ) & ( P₁[S] implies P₁[ Sub_not S] ) & ( S `2 = S9 `2 & P₁[S] & P₁[S9] implies P₁[ CQCSub_& (S,S9)] ) & ( [S,x] is quantifiable & P₁[S] implies P₁[ CQCSub_All ([S,x],SQ)] ) )

proof end;

:: Substitution Lemma (Ebb et al, Chapter III, 8.3)

theorem :: SUBLEMMA:89

for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A
for S being Element of CQC-Sub-WFF Al
for v being Element of Valuations_in (Al,A) holds
( J,v |= CQC_Sub S iff J,v . (Val_S (v,S)) |= S )

proof end;