:: Interpretation and Satisfiability in the First Order Logic
:: by Edmund Woronowicz
::
:: Copyright (c) 1990-2019 Association of Mizar Users

definition
let Al be QC-alphabet ;
let A be set ;
func Valuations_in (Al,A) -> set equals :: VALUAT_1:def 1
Funcs ((),A);
coherence
Funcs ((),A) is set
;
end;

:: deftheorem defines Valuations_in VALUAT_1:def 1 :
for Al being QC-alphabet
for A being set holds Valuations_in (Al,A) = Funcs ((),A);

registration
let Al be QC-alphabet ;
let A be non empty set ;
cluster Valuations_in (Al,A) -> functional non empty ;
coherence
( not Valuations_in (Al,A) is empty & Valuations_in (Al,A) is functional )
;
end;

theorem Th1: :: VALUAT_1:1
for Al being QC-alphabet
for A being non empty set
for x being set st x is Element of Valuations_in (Al,A) holds
x is Function of (),A
proof end;

definition
let Al be QC-alphabet ;
let A be non empty set ;
:: original: Valuations_in
redefine func Valuations_in (Al,A) -> FUNCTION_DOMAIN of bound_QC-variables Al,A;
coherence
Valuations_in (Al,A) is FUNCTION_DOMAIN of bound_QC-variables Al,A
proof end;
end;

definition
let Al be QC-alphabet ;
let A be non empty set ;
let x be bound_QC-variable of Al;
let p be Element of Funcs ((Valuations_in (Al,A)),BOOLEAN);
func FOR_ALL (x,p) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) means :Def2: :: VALUAT_1:def 2
for v being Element of Valuations_in (Al,A) holds it . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v9 . y = v . y
}
;
existence
ex b1 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st
for v being Element of Valuations_in (Al,A) holds b1 . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v9 . y = v . y
}
proof end;
uniqueness
for b1, b2 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st ( for v being Element of Valuations_in (Al,A) holds b1 . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v9 . y = v . y
}
) & ( for v being Element of Valuations_in (Al,A) holds b2 . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v9 . y = v . y
}
) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines FOR_ALL VALUAT_1:def 2 :
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for p, b5 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds
( b5 = FOR_ALL (x,p) iff for v being Element of Valuations_in (Al,A) holds b5 . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v9 . y = v . y
}
);

theorem Th2: :: VALUAT_1:2
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds
( (FOR_ALL (x,p)) . v = FALSE iff ex v1 being Element of Valuations_in (Al,A) st
( p . v1 = FALSE & ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) ) )
proof end;

theorem Th3: :: VALUAT_1:3
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds
( (FOR_ALL (x,p)) . v = TRUE iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) holds
p . v1 = TRUE )
proof end;

notation
let Al be QC-alphabet ;
let A be non empty set ;
let k be Nat;
let ll be CQC-variable_list of k,Al;
let v be Element of Valuations_in (Al,A);
synonym v *' ll for A * Al;
end;

definition
let Al be QC-alphabet ;
let A be non empty set ;
let k be Nat;
let ll be CQC-variable_list of k,Al;
let v be Element of Valuations_in (Al,A);
:: original: *'
redefine func v *' ll -> FinSequence of A means :Def3: :: VALUAT_1:def 3
( len it = k & ( for i being Nat st 1 <= i & i <= k holds
it . i = v . (ll . i) ) );
coherence
*' is FinSequence of A
proof end;
compatibility
for b1 being FinSequence of A holds
( b1 = *' iff ( len b1 = k & ( for i being Nat st 1 <= i & i <= k holds
b1 . i = v . (ll . i) ) ) )
proof end;
end;

:: deftheorem Def3 defines *' VALUAT_1:def 3 :
for Al being QC-alphabet
for A being non empty set
for k being Nat
for ll being CQC-variable_list of k,Al
for v being Element of Valuations_in (Al,A)
for b6 being FinSequence of A holds
( b6 = v *' ll iff ( len b6 = k & ( for i being Nat st 1 <= i & i <= k holds
b6 . i = v . (ll . i) ) ) );

definition
let Al be QC-alphabet ;
let A be non empty set ;
let k be Nat;
let ll be CQC-variable_list of k,Al;
let r be Element of relations_on A;
func ll 'in' r -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) means :Def4: :: VALUAT_1:def 4
for v being Element of Valuations_in (Al,A) holds
( ( v *' ll in r implies it . v = TRUE ) & ( it . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies it . v = FALSE ) & ( it . v = FALSE implies not v *' ll in r ) );
existence
ex b1 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st
for v being Element of Valuations_in (Al,A) holds
( ( v *' ll in r implies b1 . v = TRUE ) & ( b1 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies b1 . v = FALSE ) & ( b1 . v = FALSE implies not v *' ll in r ) )
proof end;
uniqueness
for b1, b2 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st ( for v being Element of Valuations_in (Al,A) holds
( ( v *' ll in r implies b1 . v = TRUE ) & ( b1 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies b1 . v = FALSE ) & ( b1 . v = FALSE implies not v *' ll in r ) ) ) & ( for v being Element of Valuations_in (Al,A) holds
( ( v *' ll in r implies b2 . v = TRUE ) & ( b2 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies b2 . v = FALSE ) & ( b2 . v = FALSE implies not v *' ll in r ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines 'in' VALUAT_1:def 4 :
for Al being QC-alphabet
for A being non empty set
for k being Nat
for ll being CQC-variable_list of k,Al
for r being Element of relations_on A
for b6 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds
( b6 = ll 'in' r iff for v being Element of Valuations_in (Al,A) holds
( ( v *' ll in r implies b6 . v = TRUE ) & ( b6 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies b6 . v = FALSE ) & ( b6 . v = FALSE implies not v *' ll in r ) ) );

definition
let Al be QC-alphabet ;
let A be non empty set ;
let F be Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN));
let p be Element of CQC-WFF Al;
:: original: .
redefine func F . p -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN);
coherence
F . p is Element of Funcs ((Valuations_in (Al,A)),BOOLEAN)
proof end;
end;

definition
let Al be QC-alphabet ;
let D be non empty set ;
mode interpretation of Al,D -> Function of (),() means :: VALUAT_1:def 5
for P being Element of QC-pred_symbols Al
for r being Element of relations_on D holds
( not it . P = r or r = empty_rel D or the_arity_of P = the_arity_of r );
existence
ex b1 being Function of (),() st
for P being Element of QC-pred_symbols Al
for r being Element of relations_on D holds
( not b1 . P = r or r = empty_rel D or the_arity_of P = the_arity_of r )
proof end;
end;

:: deftheorem defines interpretation VALUAT_1:def 5 :
for Al being QC-alphabet
for D being non empty set
for b3 being Function of (),() holds
( b3 is interpretation of Al,D iff for P being Element of QC-pred_symbols Al
for r being Element of relations_on D holds
( not b3 . P = r or r = empty_rel D or the_arity_of P = the_arity_of r ) );

definition
let Al be QC-alphabet ;
let A be non empty set ;
let k be Nat;
let J be interpretation of Al,A;
let P be QC-pred_symbol of k,Al;
:: original: .
redefine func J . P -> Element of relations_on A;
coherence
J . P is Element of relations_on A
by FUNCT_2:5;
end;

definition
let Al be QC-alphabet ;
let A be non empty set ;
let J be interpretation of Al,A;
let p be Element of CQC-WFF Al;
func Valid (p,J) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) means :Def6: :: VALUAT_1:def 6
ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( it = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = ll 'in' (J . P) & F . () = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) );
existence
ex b1 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( b1 = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = ll 'in' (J . P) & F . () = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) )
proof end;
uniqueness
for b1, b2 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( b1 = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = ll 'in' (J . P) & F . () = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) ) & ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( b2 = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = ll 'in' (J . P) & F . () = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines Valid VALUAT_1:def 6 :
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 b5 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds
( b5 = Valid (p,J) iff ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( b5 = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = ll 'in' (J . P) & F . () = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) ) );

Lm1: 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 holds
( Valid ((VERUM Al),J) = (Valuations_in (Al,A)) --> TRUE & ( for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds Valid ((P ! ll),J) = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF Al holds Valid ((),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF Al holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable of Al holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) )

proof end;

theorem :: VALUAT_1:4
for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A holds Valid ((VERUM Al),J) = (Valuations_in (Al,A)) --> TRUE by Lm1;

theorem Th5: :: VALUAT_1:5
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for J being interpretation of Al,A holds (Valid ((VERUM Al),J)) . v = TRUE
proof end;

theorem :: VALUAT_1:6
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 J being interpretation of Al,A
for P being QC-pred_symbol of k,Al holds Valid ((P ! ll),J) = ll 'in' (J . P) by Lm1;

theorem Th7: :: VALUAT_1:7
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
for p being Element of CQC-WFF Al
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for r being Element of relations_on A st p = P ! ll & r = J . P holds
( v *' ll in r iff (Valid (p,J)) . v = TRUE )
proof end;

theorem Th8: :: VALUAT_1:8
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
for p being Element of CQC-WFF Al
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for r being Element of relations_on A st p = P ! ll & r = J . P holds
( not v *' ll in r iff (Valid (p,J)) . v = FALSE )
proof end;

theorem :: VALUAT_1:9
for Al being QC-alphabet
for A being non empty set
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds Valid ((),J) = 'not' (Valid (p,J)) by Lm1;

theorem Th10: :: VALUAT_1:10
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds (Valid ((),J)) . v = 'not' ((Valid (p,J)) . v)
proof end;

theorem :: VALUAT_1:11
for Al being QC-alphabet
for A being non empty set
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) by Lm1;

theorem Th12: :: VALUAT_1:12
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds (Valid ((p '&' q),J)) . v = ((Valid (p,J)) . v) '&' ((Valid (q,J)) . v)
proof end;

theorem :: VALUAT_1:13
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) by Lm1;

theorem Th14: :: VALUAT_1:14
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds (Valid ((p '&' ()),J)) . v = FALSE
proof end;

theorem :: VALUAT_1:15
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds (Valid (('not' (p '&' ())),J)) . v = TRUE
proof end;

definition
let Al be QC-alphabet ;
let A be non empty set ;
let p be Element of CQC-WFF Al;
let J be interpretation of Al,A;
let v be Element of Valuations_in (Al,A);
pred J,v |= p means :Def7: :: VALUAT_1:def 7
(Valid (p,J)) . v = TRUE ;
end;

:: deftheorem Def7 defines |= VALUAT_1:def 7 :
for Al being QC-alphabet
for A being non empty set
for p being Element of CQC-WFF Al
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds
( J,v |= p iff (Valid (p,J)) . v = TRUE );

theorem :: VALUAT_1:16
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
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al holds
( J,v |= P ! ll iff (ll 'in' (J . P)) . v = TRUE ) by Lm1;

theorem :: VALUAT_1:17
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= 'not' p iff not J,v |= p )
proof end;

theorem :: VALUAT_1:18
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= p '&' q iff ( J,v |= p & J,v |= q ) )
proof end;

theorem Th19: :: VALUAT_1:19
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= All (x,p) iff (FOR_ALL (x,(Valid (p,J)))) . v = TRUE ) by Lm1;

theorem Th20: :: VALUAT_1:20
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= All (x,p) iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) holds
(Valid (p,J)) . v1 = TRUE )
proof end;

theorem :: VALUAT_1:21
for Al being QC-alphabet
for A being non empty set
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds Valid (('not' ()),J) = Valid (p,J)
proof end;

theorem Th22: :: VALUAT_1:22
for Al being QC-alphabet
for A being non empty set
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds Valid ((p '&' p),J) = Valid (p,J)
proof end;

theorem Th23: :: VALUAT_1:23
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= p => q iff ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE ) )
proof end;

theorem Th24: :: VALUAT_1:24
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= p => q iff ( J,v |= p implies J,v |= q ) )
proof end;

theorem Th25: :: VALUAT_1:25
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st (FOR_ALL (x,p)) . v = TRUE holds
p . v = TRUE
proof end;

definition
let Al be QC-alphabet ;
let A be non empty set ;
let J be interpretation of Al,A;
let p be Element of CQC-WFF Al;
pred J |= p means :: VALUAT_1:def 8
for v being Element of Valuations_in (Al,A) holds J,v |= p;
end;

:: deftheorem defines |= VALUAT_1:def 8 :
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 holds
( J |= p iff for v being Element of Valuations_in (Al,A) holds J,v |= p );

Lm2: for u, w, z being Element of BOOLEAN holds 'not' (('not' (u '&' ())) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE
proof end;

Lm3: now :: thesis: for Al being QC-alphabet
for A being non empty set
for Y, Z being bound_QC-variable of Al
for V1, V2 being Element of Valuations_in (Al,A) ex v being Element of Valuations_in (Al,A) st
( ( for x being bound_QC-variable of Al st x <> Y holds
v . x = V1 . x ) & v . Y = V2 . Z )
let Al be QC-alphabet ; :: thesis: for A being non empty set
for Y, Z being bound_QC-variable of Al
for V1, V2 being Element of Valuations_in (Al,A) ex v being Element of Valuations_in (Al,A) st
( ( for x being bound_QC-variable of Al st x <> Y holds
v . x = V1 . x ) & v . Y = V2 . Z )

let A be non empty set ; :: thesis: for Y, Z being bound_QC-variable of Al
for V1, V2 being Element of Valuations_in (Al,A) ex v being Element of Valuations_in (Al,A) st
( ( for x being bound_QC-variable of Al st x <> Y holds
v . x = V1 . x ) & v . Y = V2 . Z )

let Y, Z be bound_QC-variable of Al; :: thesis: for V1, V2 being Element of Valuations_in (Al,A) ex v being Element of Valuations_in (Al,A) st
( ( for x being bound_QC-variable of Al st x <> Y holds
v . x = V1 . x ) & v . Y = V2 . Z )

let V1, V2 be Element of Valuations_in (Al,A); :: thesis: ex v being Element of Valuations_in (Al,A) st
( ( for x being bound_QC-variable of Al st x <> Y holds
v . x = V1 . x ) & v . Y = V2 . Z )

thus ex v being Element of Valuations_in (Al,A) st
( ( for x being bound_QC-variable of Al st x <> Y holds
v . x = V1 . x ) & v . Y = V2 . Z ) :: thesis: verum
proof
deffunc H1( object ) -> Element of A = V2 . Z;
deffunc H2( object ) -> set = V1 . $1; defpred S1[ object ] means for x1 being bound_QC-variable of Al st x1 =$1 holds
x1 <> Y;
A1: for x being object st x in bound_QC-variables Al holds
( ( S1[x] implies H2(x) in A ) & ( not S1[x] implies H1(x) in A ) ) by FUNCT_2:5;
consider f being Function of (),A such that
A2: for x being object st x in bound_QC-variables Al holds
( ( S1[x] implies f . x = H2(x) ) & ( not S1[x] implies f . x = H1(x) ) ) from ( dom f = bound_QC-variables Al & rng f c= A ) by ;
then reconsider f = f as Element of Valuations_in (Al,A) by FUNCT_2:def 2;
take f ; :: thesis: ( ( for x being bound_QC-variable of Al st x <> Y holds
f . x = V1 . x ) & f . Y = V2 . Z )

now :: thesis: for x being bound_QC-variable of Al holds
( ( x <> Y implies f . x = V1 . x ) & ( x = Y implies f . Y = V2 . Z ) )
let x be bound_QC-variable of Al; :: thesis: ( ( x <> Y implies f . x = V1 . x ) & ( x = Y implies f . Y = V2 . Z ) )
now :: thesis: ( x <> Y implies f . x = V1 . x )
assume A3: x <> Y ; :: thesis: f . x = V1 . x
( ( for x1 being bound_QC-variable of Al st x1 = x holds
x1 <> Y ) implies f . x = V1 . x ) by A2;
hence f . x = V1 . x by A3; :: thesis: verum
end;
hence ( x <> Y implies f . x = V1 . x ) ; :: thesis: ( x = Y implies f . Y = V2 . Z )
thus ( x = Y implies f . Y = V2 . Z ) by A2; :: thesis: verum
end;
hence ( ( for x being bound_QC-variable of Al st x <> Y holds
f . x = V1 . x ) & f . Y = V2 . Z ) ; :: thesis: verum
end;
end;

theorem :: VALUAT_1:26
for Al being QC-alphabet
for A being non empty set
for Y, Z being bound_QC-variable of Al
for V1, V2 being Element of Valuations_in (Al,A) ex v being Element of Valuations_in (Al,A) st
( ( for x being bound_QC-variable of Al st x <> Y holds
v . x = V1 . x ) & v . Y = V2 . Z ) by Lm3;

theorem Th27: :: VALUAT_1:27
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al
for J being interpretation of Al,A st not x in still_not-bound_in p holds
for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (p,J)) . v = (Valid (p,J)) . w
proof end;

theorem Th28: :: VALUAT_1:28
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A st J,v |= p & not x in still_not-bound_in p holds
for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
J,w |= p by Th27;

theorem Th29: :: VALUAT_1:29
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds
( J,v |= All (x,p) iff for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
J,w |= p )
proof end;

theorem Th30: :: VALUAT_1:30
for Al being QC-alphabet
for A being non empty set
for x, y being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A
for s9 being QC-formula of Al st x <> y & p = s9 . x & q = s9 . y holds
for v being Element of Valuations_in (Al,A) st v . x = v . y holds
(Valid (p,J)) . v = (Valid (q,J)) . v
proof end;

theorem Th31: :: VALUAT_1:31
for Al being QC-alphabet
for x, y being bound_QC-variable of Al
for s9 being QC-formula of Al st x <> y & not x in still_not-bound_in s9 holds
not x in still_not-bound_in (s9 . y)
proof end;

theorem Th32: :: VALUAT_1:32
for Al being QC-alphabet
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 |= VERUM Al
proof end;

theorem Th33: :: VALUAT_1:33
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= (p '&' q) => (q '&' p)
proof end;

theorem Th34: :: VALUAT_1:34
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= (() => p) => p
proof end;

theorem Th35: :: VALUAT_1:35
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= p => (() => q)
proof end;

theorem Th36: :: VALUAT_1:36
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p, q, t being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t)))
proof end;

theorem :: VALUAT_1:37
for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A st J,v |= p & J,v |= p => q holds
J,v |= q by Th24;

theorem Th38: :: VALUAT_1:38
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for v being Element of Valuations_in (Al,A)
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds J,v |= (All (x,p)) => p
proof end;

theorem :: VALUAT_1:39
for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A holds J |= VERUM Al by Th32;

theorem :: VALUAT_1:40
for Al being QC-alphabet
for A being non empty set
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds J |= (p '&' q) => (q '&' p) by Th33;

theorem :: VALUAT_1:41
for Al being QC-alphabet
for A being non empty set
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds J |= (() => p) => p by Th34;

theorem :: VALUAT_1:42
for Al being QC-alphabet
for A being non empty set
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A holds J |= p => (() => q) by Th35;

theorem :: VALUAT_1:43
for Al being QC-alphabet
for A being non empty set
for p, q, t being Element of CQC-WFF Al
for J being interpretation of Al,A holds J |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t))) by Th36;

theorem :: VALUAT_1:44
for Al being QC-alphabet
for A being non empty set
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A st J |= p & J |= p => q holds
J |= q
proof end;

theorem :: VALUAT_1:45
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al
for J being interpretation of Al,A holds J |= (All (x,p)) => p by Th38;

theorem :: VALUAT_1:46
for Al being QC-alphabet
for A being non empty set
for x being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A st J |= p => q & not x in still_not-bound_in p holds
J |= p => (All (x,q))
proof end;

theorem :: VALUAT_1:47
for Al being QC-alphabet
for A being non empty set
for x, y being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A
for s being QC-formula of Al st p = s . x & q = s . y & not x in still_not-bound_in s & J |= p holds
J |= q
proof end;