:: by Edmund Woronowicz

::

:: Received June 1, 1990

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

begin

definition
end;

:: deftheorem defines Valuations_in VALUAT_1:def 1 :

for Al being QC-alphabet

for A being set holds Valuations_in (Al,A) = Funcs ((bound_QC-variables Al),A);

for Al being QC-alphabet

for A being set holds Valuations_in (Al,A) = Funcs ((bound_QC-variables Al),A);

registration

let Al be QC-alphabet ;

let A be non empty set ;

coherence

( not Valuations_in (Al,A) is empty & Valuations_in (Al,A) is functional ) ;

end;
let A be non empty set ;

coherence

( not Valuations_in (Al,A) is empty & Valuations_in (Al,A) is functional ) ;

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 (bound_QC-variables Al),A

for A being non empty set

for x being set st x is Element of Valuations_in (Al,A) holds

x is Function of (bound_QC-variables Al),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

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

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

ex b_{1} being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st

for v being Element of Valuations_in (Al,A) holds b_{1} . 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 b_{1}, b_{2} being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st ( for v being Element of Valuations_in (Al,A) holds b_{1} . 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 b_{2} . 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

b_{1} = b_{2}

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

ex b

for v being Element of Valuations_in (Al,A) holds b

v9 . y = v . y }

proof end;

uniqueness for b

v9 . y = v . y } ) & ( for v being Element of Valuations_in (Al,A) holds b

v9 . y = v . y } ) holds

b

proof 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, b_{5} being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds

( b_{5} = FOR_ALL (x,p) iff for v being Element of Valuations_in (Al,A) holds b_{5} . 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 Al being QC-alphabet

for A being non empty set

for x being bound_QC-variable of Al

for p, b

( b

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

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 )

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

let k be Element of 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;

definition

let Al be QC-alphabet ;

let A be non empty set ;

let k be Element of NAT ;

let ll be CQC-variable_list of k,Al;

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

*' is FinSequence of A

for b_{1} being FinSequence of A holds

( b_{1} = *' iff ( len b_{1} = k & ( for i being natural number st 1 <= i & i <= k holds

b_{1} . i = v . (ll . i) ) ) )

end;
let A be non empty set ;

let k be Element of 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 natural number st 1 <= i & i <= k holds

it . i = v . (ll . i) ) );

coherence redefine func v *' ll -> FinSequence of A means :Def3: :: VALUAT_1:def 3

( len it = k & ( for i being natural number st 1 <= i & i <= k holds

it . i = v . (ll . i) ) );

*' is FinSequence of A

proof end;

compatibility for b

( b

b

proof end;

:: deftheorem Def3 defines *' VALUAT_1:def 3 :

for Al being QC-alphabet

for A being non empty set

for k being Element of NAT

for ll being CQC-variable_list of k,Al

for v being Element of Valuations_in (Al,A)

for b_{6} being FinSequence of A holds

( b_{6} = v *' ll iff ( len b_{6} = k & ( for i being natural number st 1 <= i & i <= k holds

b_{6} . i = v . (ll . i) ) ) );

for Al being QC-alphabet

for A being non empty set

for k being Element of NAT

for ll being CQC-variable_list of k,Al

for v being Element of Valuations_in (Al,A)

for b

( b

b

definition

let Al be QC-alphabet ;

let A be non empty set ;

let k be Element of NAT ;

let ll be CQC-variable_list of k,Al;

let r be Element of relations_on A;

ex b_{1} 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 b_{1} . v = TRUE ) & ( b_{1} . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies b_{1} . v = FALSE ) & ( b_{1} . v = FALSE implies not v *' ll in r ) )

for b_{1}, b_{2} 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 b_{1} . v = TRUE ) & ( b_{1} . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies b_{1} . v = FALSE ) & ( b_{1} . v = FALSE implies not v *' ll in r ) ) ) & ( for v being Element of Valuations_in (Al,A) holds

( ( v *' ll in r implies b_{2} . v = TRUE ) & ( b_{2} . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies b_{2} . v = FALSE ) & ( b_{2} . v = FALSE implies not v *' ll in r ) ) ) holds

b_{1} = b_{2}

end;
let A be non empty set ;

let k be Element of 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 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 ) );

ex b

for v being Element of Valuations_in (Al,A) holds

( ( v *' ll in r implies b

proof end;

uniqueness for b

( ( v *' ll in r implies b

( ( v *' ll in r implies b

b

proof end;

:: deftheorem Def4 defines 'in' VALUAT_1:def 4 :

for Al being QC-alphabet

for A being non empty set

for k being Element of NAT

for ll being CQC-variable_list of k,Al

for r being Element of relations_on A

for b_{6} being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds

( b_{6} = ll 'in' r iff for v being Element of Valuations_in (Al,A) holds

( ( v *' ll in r implies b_{6} . v = TRUE ) & ( b_{6} . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies b_{6} . v = FALSE ) & ( b_{6} . v = FALSE implies not v *' ll in r ) ) );

for Al being QC-alphabet

for A being non empty set

for k being Element of NAT

for ll being CQC-variable_list of k,Al

for r being Element of relations_on A

for b

( b

( ( v *' ll in r implies b

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)

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

definition

let Al be QC-alphabet ;

let D be non empty set ;

ex b_{1} being Function of (QC-pred_symbols Al),(relations_on D) st

for P being Element of QC-pred_symbols Al

for r being Element of relations_on D holds

( not b_{1} . P = r or r = empty_rel D or the_arity_of P = the_arity_of r )

end;
let D be non empty set ;

mode interpretation of Al,D -> Function of (QC-pred_symbols Al),(relations_on D) 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 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 );

ex b

for P being Element of QC-pred_symbols Al

for r being Element of relations_on D holds

( not b

proof end;

:: deftheorem defines interpretation VALUAT_1:def 5 :

for Al being QC-alphabet

for D being non empty set

for b_{3} being Function of (QC-pred_symbols Al),(relations_on D) holds

( b_{3} 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 b_{3} . P = r or r = empty_rel D or the_arity_of P = the_arity_of r ) );

for Al being QC-alphabet

for D being non empty set

for b

( b

for r being Element of relations_on D holds

( not b

definition

let Al be QC-alphabet ;

let A be non empty set ;

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

let k be Element of 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;

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;

ex b_{1} being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st

( b_{1} = 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 Element of 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' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) )

for b_{1}, b_{2} 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

( b_{1} = 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 Element of 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' p) = '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

( b_{2} = 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 Element of 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' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) ) holds

b_{1} = b_{2}

end;
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 Element of 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' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) );

existence 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 Element of 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' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) );

ex b

( b

for x being bound_QC-variable of Al

for k being Element of 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' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) )

proof end;

uniqueness for b

( b

for x being bound_QC-variable of Al

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

( b

for x being bound_QC-variable of Al

for k being Element of 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' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) ) holds

b

proof 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 b_{5} being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds

( b_{5} = Valid (p,J) iff ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st

( b_{5} = 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 Element of 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' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) ) );

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 b

( b

( b

for x being bound_QC-variable of Al

for k being Element of 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' p) = '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 Element of 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 (('not' p),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;

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

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

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

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 )

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

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

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 )

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

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

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 (('not' p),J)) . v = 'not' ((Valid (p,J)) . v)

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 = 'not' ((Valid (p,J)) . v)

proof end;

theorem :: VALUAT_1:11

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)

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;

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 '&' ('not' p)),J)) . v = FALSE

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 '&' ('not' 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 '&' ('not' p))),J)) . v = TRUE

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 '&' ('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);

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

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

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

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 )

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

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 )

proof end;

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 )

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

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 )

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 )

proof end;

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 )

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' ('not' p)),J) = Valid (p,J)

for A being non empty set

for p being Element of CQC-WFF Al

for J being interpretation of Al,A holds Valid (('not' ('not' p)),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)

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

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

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

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;

end;
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 :Def8: :: VALUAT_1:def 8

for v being Element of Valuations_in (Al,A) holds J,v |= p;

for v being Element of Valuations_in (Al,A) holds J,v |= p;

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

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

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

end;
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 H_{1}( set ) -> Element of A = V2 . Z;

deffunc H_{2}( set ) -> set = V1 . $1;

defpred S_{1}[ set ] means for x1 being bound_QC-variable of Al st x1 = $1 holds

x1 <> Y;

A1: for x being set st x in bound_QC-variables Al holds

( ( S_{1}[x] implies H_{2}(x) in A ) & ( not S_{1}[x] implies H_{1}(x) in A ) )
by FUNCT_2:5;

consider f being Function of (bound_QC-variables Al),A such that

A2: for x being set st x in bound_QC-variables Al holds

( ( S_{1}[x] implies f . x = H_{2}(x) ) & ( not S_{1}[x] implies f . x = H_{1}(x) ) )
from FUNCT_2:sch 5(A1);

( dom f = bound_QC-variables Al & rng f c= A ) by FUNCT_2:def 1, RELAT_1:def 19;

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 )

f . x = V1 . x ) & f . Y = V2 . Z ) ; :: thesis: verum

end;
deffunc H

defpred S

x1 <> Y;

A1: for x being set st x in bound_QC-variables Al holds

( ( S

consider f being Function of (bound_QC-variables Al),A such that

A2: for x being set st x in bound_QC-variables Al holds

( ( S

( dom f = bound_QC-variables Al & rng f c= A ) by FUNCT_2:def 1, RELAT_1:def 19;

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

hence
( ( for x being bound_QC-variable of Al st x <> Y 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 ) )

thus ( x = Y implies f . Y = V2 . Z ) by A2; :: thesis: verum

end;
now :: thesis: ( x <> Y implies f . x = V1 . x )

hence
( x <> Y implies f . x = V1 . x )
; :: thesis: ( x = Y implies f . Y = V2 . Z )
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;
( ( 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

thus ( x = Y implies f . Y = V2 . Z ) by A2; :: thesis: verum

f . x = V1 . x ) & f . Y = V2 . Z ) ; :: thesis: verum

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;

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

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

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

proof end;

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 )

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

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)

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

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)

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 |= (('not' p) => p) => p

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) => 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 => (('not' p) => q)

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 => (('not' 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)))

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;

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

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

for A being non empty set

for J being interpretation of Al,A holds J |= VERUM Al

proof end;

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)

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)

proof end;

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 |= (('not' p) => p) => p

for A being non empty set

for p being Element of CQC-WFF Al

for J being interpretation of Al,A holds J |= (('not' p) => p) => p

proof end;

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 => (('not' p) => q)

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 => (('not' p) => q)

proof end;

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

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

proof end;

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

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

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

proof end;

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

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

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;