:: by Patrick Braselmann and Peter Koepke

::

:: Received September 25, 2004

:: Copyright (c) 2004-2012 Association of Mizar Users

begin

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

(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

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;
let A be non empty set ;

mode Val_Sub of A,Al is PartFunc of (bound_QC-variables Al),A;

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;
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;

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)

end;
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;

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

end;
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;

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);

coherence

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

end;
let S be Element of CQC-Sub-WFF Al;

let A be non empty set ;

let v be Element of Valuations_in (Al,A);

coherence

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

:: 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;

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

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;

end;
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;

:: 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 );

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 )

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 k, i being Element of NAT

for ll being CQC-variable_list of k,Al st i in dom ll holds

ll . i is bound_QC-variable of Al

for k, i being Element of 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)))

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 Element of 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

for k being Element of 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 Element of 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

end;
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;

theorem Th8: :: SUBLEMMA:8

for Al being QC-alphabet

for k being Element of 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))

for k being Element of 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 Element of 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

for k being Element of 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 Element of 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

for k being Element of 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 Element of NAT ;

let ll be CQC-variable_list of k,Al;

let Sub be CQC_Substitution of Al;

coherence

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

end;
let k be Element of NAT ;

let ll be CQC-variable_list of k,Al;

let Sub be CQC_Substitution of Al;

coherence

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

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

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

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 Element of 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))

for k being Element of 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 Element of 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

for k being Element of 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 Element of 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) )

for k being Element of 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 )

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

end;
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;

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 )

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))

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 )

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 ;

coherence

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

end;
let S1, S2 be Element of CQC-Sub-WFF Al;

assume A1: S1 `2 = S2 `2 ;

coherence

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

proof 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);

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 )

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

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

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)

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) )

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) )

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 )

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
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 );

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 ;

existence

ex b_{1} being Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):] st b_{1} is CQC-WFF-like

end;
existence

ex b

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;

:: 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):]

end;
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;

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;
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;

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 ;

coherence

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

end;
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 ;

coherence

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

proof 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);

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

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 X1: S is Sub_universal ;

Sub_the_scope_of S is Element of CQC-Sub-WFF Al

end;
let S be Element of CQC-Sub-WFF Al;

assume X1: 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;

Sub_the_scope_of S is Element of CQC-Sub-WFF Al

proof 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;

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) ;

coherence

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

end;
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) ;

coherence

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

proof 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);

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)))

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

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;

begin

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)) )

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))

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

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

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 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 )

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 )

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

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) )

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))

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))

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)))

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 Th43: :: SUBLEMMA:43

for Al being QC-alphabet

for k being Element of 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)

for k being Element of 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)

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)

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))

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

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;
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;

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

end;
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;

theorem Th48: :: SUBLEMMA:48

for Al being QC-alphabet

for b being set

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

for b being set

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

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 )

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);

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

end;
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;

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

:: 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;

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

end;
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;

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)))

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

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} )

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 )

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)

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 )

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;

begin

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

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} )

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 Element of 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))

for k being Element of 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 Element of 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 )

for k being Element of 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 )

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 )

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 )

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)

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}

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)

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) )

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 )

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))

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 )

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))

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 )

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 )

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 )

proof end;

theorem Th74: :: SUBLEMMA:74

for Al being QC-alphabet

for k being Element of 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

for k being Element of 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 Element of 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 )

for k being Element of 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 )

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 )

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

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

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) )

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 )

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;

ex b_{1} being set st

for b being set holds

( b in b_{1} iff ex x being bound_QC-variable of Al st

( x = b & not x in still_not-bound_in p ) )

for b_{1}, b_{2} being set st ( for b being set holds

( b in b_{1} iff ex x being bound_QC-variable of Al st

( x = b & not x in still_not-bound_in p ) ) ) & ( for b being set holds

( b in b_{2} iff ex x being bound_QC-variable of Al st

( x = b & not x in still_not-bound_in p ) ) ) holds

b_{1} = b_{2}

end;
let p be Element of CQC-WFF Al;

func RSub1 p -> set means :Def9: :: SUBLEMMA:def 9

for b being set 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 for b being set holds

( b in it iff ex x being bound_QC-variable of Al st

( x = b & not x in still_not-bound_in p ) );

ex b

for b being set holds

( b in b

( x = b & not x in still_not-bound_in p ) )

proof end;

uniqueness for b

( b in b

( x = b & not x in still_not-bound_in p ) ) ) & ( for b being set holds

( b in b

( x = b & not x in still_not-bound_in p ) ) ) holds

b

proof end;

:: deftheorem Def9 defines RSub1 SUBLEMMA:def 9 :

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for b_{3} being set holds

( b_{3} = RSub1 p iff for b being set holds

( b in b_{3} iff ex x being bound_QC-variable of Al st

( x = b & not x in still_not-bound_in p ) ) );

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for b

( b

( b in b

( 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;

ex b_{1} being set st

for b being set holds

( b in b_{1} iff ex x being bound_QC-variable of Al st

( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) )

for b_{1}, b_{2} being set st ( for b being set holds

( b in b_{1} 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 set holds

( b in b_{2} iff ex x being bound_QC-variable of Al st

( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) ) ) holds

b_{1} = b_{2}

end;
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 set 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 for b being set 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 ) );

ex b

for b being set holds

( b in b

( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) )

proof end;

uniqueness for b

( b in b

( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) ) ) & ( for b being set holds

( b in b

( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) ) ) holds

b

proof 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_{4} being set holds

( b_{4} = RSub2 (p,Sub) iff for b being set holds

( b in b_{4} iff ex x being bound_QC-variable of Al st

( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) ) );

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for Sub being CQC_Substitution of Al

for b

( b

( b in b

( 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)))

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))))

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))))

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)))

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) )

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) )

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) )

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_{1}() -> QC-alphabet , P_{1}[ set ] } :

provided

SubCQCInd1{ F

provided

A1:
for S, S9 being Element of CQC-Sub-WFF F_{1}()

for x being bound_QC-variable of F_{1}()

for SQ being second_Q_comp of [S,x]

for k being Element of NAT

for ll being CQC-variable_list of k,F_{1}()

for P being QC-pred_symbol of k,F_{1}()

for e being Element of vSUB F_{1}() holds

( P_{1}[ Sub_P (P,ll,e)] & ( S is F_{1}() -Sub_VERUM implies P_{1}[S] ) & ( P_{1}[S] implies P_{1}[ Sub_not S] ) & ( S `2 = S9 `2 & P_{1}[S] & P_{1}[S9] implies P_{1}[ CQCSub_& (S,S9)] ) & ( [S,x] is quantifiable & P_{1}[S] implies P_{1}[ CQCSub_All ([S,x],SQ)] ) )

for x being bound_QC-variable of F

for SQ being second_Q_comp of [S,x]

for k being Element of 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

( P

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 )

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;