:: VALUAT_1 semantic presentation

definition

let c₁ be set ;
func Valuations_in c₁ -> set equals :: VALUAT_1:def 1
Funcs bound_QC-variables ,a₁;
coherence ;

end;

:: deftheorem Def1 defines Valuations_in VALUAT_1:def 1 :

registration

let c₁ be non empty set ;
cluster Valuations_in a₁ -> non empty functional ;
coherence

proof end;

end;

theorem Th1: :: VALUAT_1:1

canceled;

theorem Th2: :: VALUAT_1:2

for b₁ being non empty set
for b₂ being set st b₂ is Element of Valuations_in b₁ holds
b₂ is Function of bound_QC-variables ,b₁

proof end;

definition

let c₁ be non empty set ;
redefine func Valuations_in as Valuations_in c₁ -> FUNCTION_DOMAIN of bound_QC-variables ,a₁;
coherence

proof end;

end;

definition

let c₁ be Function;
attr a₁ is boolean-valued means :Def2: :: VALUAT_1:def 2
rng a₁ c= BOOLEAN ;

end;

:: deftheorem Def2 defines boolean-valued VALUAT_1:def 2 :

registration

cluster boolean-valued set ;
existence

proof end;

end;

registration

let c₁ be boolean-valued Function;
let c₂ be set ;
cluster a₁ . a₂ -> boolean ;
coherence

proof end;

end;

registration

let c₁ be set ;
cluster -> boolean-valued Element of Funcs a₁,BOOLEAN ;
coherence

proof end;

end;

definition

let c₁ be boolean-valued Function;
func 'not' c₁ -> Function means :Def3: :: VALUAT_1:def 3
( dom a₂ = dom a₁ & ( for b₁ being set st b₁ in dom a₁ holds
a₂ . b₁ = 'not' (a₁ . b₁) ) );
existence

proof end;

uniqueness

proof end;

let c₂ be boolean-valued Function;
func c₁ '&' c₂ -> Function means :Def4: :: VALUAT_1:def 4
( dom a₃ = (dom a₁) /\ (dom a₂) & ( for b₁ being set st b₁ in dom a₃ holds
a₃ . b₁ = (a₁ . b₁) '&' (a₂ . b₁) ) );
existence

proof end;

uniqueness

proof end;

commutativity ;

end;

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

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

registration

let c₁ be boolean-valued Function;
cluster 'not' a₁ -> boolean-valued ;
coherence

proof end;

let c₂ be boolean-valued Function;
cluster a₁ '&' a₂ -> boolean-valued ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be Element of Funcs c₁,BOOLEAN ;
redefine func 'not' as 'not' c₂ -> Element of Funcs a₁,BOOLEAN means :Def5: :: VALUAT_1:def 5
for b₁ being Element of a₁ holds a₃ . b₁ = 'not' (a₂ . b₁);
coherence

proof end;

compatibility

proof end;

let c₃ be Element of Funcs c₁,BOOLEAN ;
redefine func '&' as c₂ '&' c₃ -> Element of Funcs a₁,BOOLEAN means :Def6: :: VALUAT_1:def 6
for b₁ being Element of a₁ holds a₄ . b₁ = (a₂ . b₁) '&' (a₃ . b₁);
coherence

proof end;

compatibility

proof end;

end;

:: deftheorem Def5 defines 'not' VALUAT_1:def 5 :

:: deftheorem Def6 defines '&' VALUAT_1:def 6 :

definition

let c₁ be non empty set ;
let c₂ be bound_QC-variable;
let c₃ be Element of Funcs (Valuations_in c₁),BOOLEAN ;
func FOR_ALL c₂,c₃ -> Element of Funcs (Valuations_in a₁),BOOLEAN means :Def7: :: VALUAT_1:def 7
for b₁ being Element of Valuations_in a₁ holds a₄ . b₁ = ALL { (a₃ . b₂) where B is Element of Valuations_in a₁ : for b₁ being bound_QC-variable st a₂ <> b₃ holds
b₂ . b₃ = b₁ . b₃ } ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines FOR_ALL VALUAT_1:def 7 :

theorem Th3: :: VALUAT_1:3

canceled;

theorem Th4: :: VALUAT_1:4

canceled;

theorem Th5: :: VALUAT_1:5

canceled;

theorem Th6: :: VALUAT_1:6

canceled;

theorem Th7: :: VALUAT_1:7

for b₁ being non empty set
for b₂ being bound_QC-variable
for b₃ being Element of Valuations_in b₁
for b₄ being Element of Funcs (Valuations_in b₁),BOOLEAN holds
( (FOR_ALL b₂,b₄) . b₃ = FALSE iff ex b₅ being Element of Valuations_in b₁ st
( b₄ . b₅ = FALSE & ( for b₆ being bound_QC-variable st b₂ <> b₆ holds
b₅ . b₆ = b₃ . b₆ ) ) )

proof end;

theorem Th8: :: VALUAT_1:8

for b₁ being non empty set
for b₂ being bound_QC-variable
for b₃ being Element of Valuations_in b₁
for b₄ being Element of Funcs (Valuations_in b₁),BOOLEAN holds
( (FOR_ALL b₂,b₄) . b₃ = TRUE iff for b₅ being Element of Valuations_in b₁ st ( for b₆ being bound_QC-variable st b₂ <> b₆ holds
b₅ . b₆ = b₃ . b₆ ) holds
b₄ . b₅ = TRUE )

proof end;

notation

let c₁ be non empty set ;
let c₂ be Nat;
let c₃ be CQC-variable_list of c₂;
let c₄ be Element of Valuations_in c₁;
synonym c₄ *' c₃ for c₂ * c₁;

end;

definition

let c₁ be non empty set ;
let c₂ be Nat;
let c₃ be CQC-variable_list of c₂;
let c₄ be Element of Valuations_in c₁;
redefine func *' as c₄ *' c₃ -> FinSequence of a₁ means :Def8: :: VALUAT_1:def 8
( len a₅ = a₂ & ( for b₁ being Nat st 1 <= b₁ & b₁ <= a₂ holds
a₅ . b₁ = a₄ . (a₃ . b₁) ) );
coherence

proof end;

compatibility

proof end;

end;

:: deftheorem Def8 defines *' VALUAT_1:def 8 :

definition

let c₁ be non empty set ;
let c₂ be Nat;
let c₃ be CQC-variable_list of c₂;
let c₄ be Element of relations_on c₁;
func c₃ 'in' c₄ -> Element of Funcs (Valuations_in a₁),BOOLEAN means :Def9: :: VALUAT_1:def 9
for b₁ being Element of Valuations_in a₁ holds
( ( b₁ *' a₃ in a₄ implies a₅ . b₁ = TRUE ) & ( not b₁ *' a₃ in a₄ implies a₅ . b₁ = FALSE ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines 'in' VALUAT_1:def 9 :

definition

let c₁ be non empty set ;
let c₂ be Function of CQC-WFF , Funcs (Valuations_in c₁),BOOLEAN ;
let c₃ be Element of CQC-WFF ;
redefine func . as c₂ . c₃ -> Element of Funcs (Valuations_in a₁),BOOLEAN ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
mode interpretation of c₁ -> Function of QC-pred_symbols , relations_on a₁ means :: VALUAT_1:def 10
for b₁ being Element of QC-pred_symbols
for b₂ being Element of relations_on a₁ holds
( not a₂ . b₁ = b₂ or b₂ = empty_rel a₁ or the_arity_of b₁ = the_arity_of b₂ );
existence

proof end;

end;

:: deftheorem Def10 defines interpretation VALUAT_1:def 10 :

definition

let c₁ be non empty set ;
let c₂ be Nat;
let c₃ be interpretation of c₁;
let c₄ be QC-pred_symbol of c₂;
redefine func . as c₃ . c₄ -> Element of relations_on a₁;
coherence by FUNCT_2:7;

end;

definition

let c₁ be non empty set ;
let c₂ be interpretation of c₁;
let c₃ be Element of CQC-WFF ;
func Valid c₃,c₂ -> Element of Funcs (Valuations_in a₁),BOOLEAN means :Def11: :: VALUAT_1:def 11
ex b₁ being Function of CQC-WFF , Funcs (Valuations_in a₁),BOOLEAN st
( a₄ = b₁ . a₃ & b₁ . VERUM = (Valuations_in a₁) --> TRUE & ( for b₂, b₃ being Element of CQC-WFF
for b₄ being bound_QC-variable
for b₅ being Nat
for b₆ being CQC-variable_list of b₅
for b₇ being QC-pred_symbol of b₅ holds
( b₁ . (b₇ ! b₆) = b₆ 'in' (a₂ . b₇) & b₁ . ('not' b₂) = 'not' (b₁ . b₂) & b₁ . (b₂ '&' b₃) = (b₁ . b₂) '&' (b₁ . b₃) & b₁ . (All b₄,b₂) = FOR_ALL b₄,(b₁ . b₂) ) ) );
correctness

proof end;

end;

:: deftheorem Def11 defines Valid VALUAT_1:def 11 :

Lemma13: for b₁ being Element of CQC-WFF
for b₂ being non empty set
for b₃ being interpretation of b₂ holds
( Valid VERUM ,b₃ = (Valuations_in b₂) --> TRUE & ( for b₄ being Nat
for b₅ being CQC-variable_list of b₄
for b₆ being QC-pred_symbol of b₄ holds Valid (b₆ ! b₅),b₃ = b₅ 'in' (b₃ . b₆) ) & ( for b₄ being Element of CQC-WFF holds Valid ('not' b₄),b₃ = 'not' (Valid b₄,b₃) ) & ( for b₄ being Element of CQC-WFF holds Valid (b₁ '&' b₄),b₃ = (Valid b₁,b₃) '&' (Valid b₄,b₃) ) & ( for b₄ being bound_QC-variable holds Valid (All b₄,b₁),b₃ = FOR_ALL b₄,(Valid b₁,b₃) ) )

proof end;

theorem Th9: :: VALUAT_1:9

canceled;

theorem Th10: :: VALUAT_1:10

canceled;

theorem Th11: :: VALUAT_1:11

canceled;

theorem Th12: :: VALUAT_1:12

canceled;

theorem Th13: :: VALUAT_1:13

for b₁ being non empty set
for b₂ being interpretation of b₁ holds Valid VERUM ,b₂ = (Valuations_in b₁) --> TRUE by Lemma13;

theorem Th14: :: VALUAT_1:14

for b₁ being non empty set
for b₂ being Element of Valuations_in b₁
for b₃ being interpretation of b₁ holds (Valid VERUM ,b₃) . b₂ = TRUE

proof end;

theorem Th15: :: VALUAT_1:15

for b₁ being Nat
for b₂ being non empty set
for b₃ being CQC-variable_list of b₁
for b₄ being interpretation of b₂
for b₅ being QC-pred_symbol of b₁ holds Valid (b₅ ! b₃),b₄ = b₃ 'in' (b₄ . b₅) by Lemma13;

theorem Th16: :: VALUAT_1:16

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of Valuations_in b₂
for b₄ being CQC-variable_list of b₁
for b₅ being Element of CQC-WFF
for b₆ being interpretation of b₂
for b₇ being QC-pred_symbol of b₁
for b₈ being Element of relations_on b₂ st b₅ = b₇ ! b₄ & b₈ = b₆ . b₇ holds
( b₃ *' b₄ in b₈ iff (Valid b₅,b₆) . b₃ = TRUE )

proof end;

theorem Th17: :: VALUAT_1:17

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of Valuations_in b₂
for b₄ being CQC-variable_list of b₁
for b₅ being Element of CQC-WFF
for b₆ being interpretation of b₂
for b₇ being QC-pred_symbol of b₁
for b₈ being Element of relations_on b₂ st b₅ = b₇ ! b₄ & b₈ = b₆ . b₇ holds
( not b₃ *' b₄ in b₈ iff (Valid b₅,b₆) . b₃ = FALSE )

proof end;

theorem Th18: :: VALUAT_1:18

canceled;

theorem Th19: :: VALUAT_1:19

for b₁ being non empty set
for b₂ being Element of CQC-WFF
for b₃ being interpretation of b₁ holds Valid ('not' b₂),b₃ = 'not' (Valid b₂,b₃) by Lemma13;

theorem Th20: :: VALUAT_1:20

for b₁ being non empty set
for b₂ being Element of Valuations_in b₁
for b₃ being Element of CQC-WFF
for b₄ being interpretation of b₁ holds (Valid ('not' b₃),b₄) . b₂ = 'not' ((Valid b₃,b₄) . b₂)

proof end;

theorem Th21: :: VALUAT_1:21

for b₁ being non empty set
for b₂, b₃ being Element of CQC-WFF
for b₄ being interpretation of b₁ holds Valid (b₂ '&' b₃),b₄ = (Valid b₂,b₄) '&' (Valid b₃,b₄) by Lemma13;

theorem Th22: :: VALUAT_1:22

for b₁ being non empty set
for b₂ being Element of Valuations_in b₁
for b₃, b₄ being Element of CQC-WFF
for b₅ being interpretation of b₁ holds (Valid (b₃ '&' b₄),b₅) . b₂ = ((Valid b₃,b₅) . b₂) '&' ((Valid b₄,b₅) . b₂)

proof end;

theorem Th23: :: VALUAT_1:23

for b₁ being non empty set
for b₂ being bound_QC-variable
for b₃ being Element of CQC-WFF
for b₄ being interpretation of b₁ holds Valid (All b₂,b₃),b₄ = FOR_ALL b₂,(Valid b₃,b₄) by Lemma13;

theorem Th24: :: VALUAT_1:24

for b₁ being non empty set
for b₂ being Element of Valuations_in b₁
for b₃ being Element of CQC-WFF
for b₄ being interpretation of b₁ holds (Valid (b₃ '&' ('not' b₃)),b₄) . b₂ = FALSE

proof end;

theorem Th25: :: VALUAT_1:25

for b₁ being non empty set
for b₂ being Element of Valuations_in b₁
for b₃ being Element of CQC-WFF
for b₄ being interpretation of b₁ holds (Valid ('not' (b₃ '&' ('not' b₃))),b₄) . b₂ = TRUE

proof end;

definition

let c₁ be non empty set ;
let c₂ be Element of CQC-WFF ;
let c₃ be interpretation of c₁;
let c₄ be Element of Valuations_in c₁;
pred c₃,c₄ |= c₂ means :Def12: :: VALUAT_1:def 12
(Valid a₂,a₃) . a₄ = TRUE ;

end;

:: deftheorem Def12 defines |= VALUAT_1:def 12 :

theorem Th26: :: VALUAT_1:26

canceled;

theorem Th27: :: VALUAT_1:27

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of Valuations_in b₂
for b₄ being CQC-variable_list of b₁
for b₅ being interpretation of b₂
for b₆ being QC-pred_symbol of b₁ holds
( b₅,b₃ |= b₆ ! b₄ iff (b₄ 'in' (b₅ . b₆)) . b₃ = TRUE )

proof end;

theorem Th28: :: VALUAT_1:28

for b₁ being non empty set
for b₂ being Element of Valuations_in b₁
for b₃ being Element of CQC-WFF
for b₄ being interpretation of b₁ holds
( b₄,b₂ |= 'not' b₃ iff not b₄,b₂ |= b₃ )

proof end;

theorem Th29: :: VALUAT_1:29

for b₁ being non empty set
for b₂ being Element of Valuations_in b₁
for b₃, b₄ being Element of CQC-WFF
for b₅ being interpretation of b₁ holds
( b₅,b₂ |= b₃ '&' b₄ iff ( b₅,b₂ |= b₃ & b₅,b₂ |= b₄ ) )

proof end;

theorem Th30: :: VALUAT_1:30

proof end;

theorem Th31: :: VALUAT_1:31

for b₁ being non empty set
for b₂ being bound_QC-variable
for b₃ being Element of Valuations_in b₁
for b₄ being Element of CQC-WFF
for b₅ being interpretation of b₁ holds
( b₅,b₃ |= All b₂,b₄ iff for b₆ being Element of Valuations_in b₁ st ( for b₇ being bound_QC-variable st b₂ <> b₇ holds
b₆ . b₇ = b₃ . b₇ ) holds
(Valid b₄,b₅) . b₆ = TRUE )

proof end;

theorem Th32: :: VALUAT_1:32

for b₁ being non empty set
for b₂ being Element of CQC-WFF
for b₃ being interpretation of b₁ holds Valid ('not' ('not' b₂)),b₃ = Valid b₂,b₃

proof end;

theorem Th33: :: VALUAT_1:33

for b₁ being non empty set
for b₂ being Element of CQC-WFF
for b₃ being interpretation of b₁ holds Valid (b₂ '&' b₂),b₃ = Valid b₂,b₃

proof end;

theorem Th34: :: VALUAT_1:34

canceled;

theorem Th35: :: VALUAT_1:35

for b₁ being non empty set
for b₂ being Element of Valuations_in b₁
for b₃, b₄ being Element of CQC-WFF
for b₅ being interpretation of b₁ holds
( b₅,b₂ |= b₃ => b₄ iff ( (Valid b₃,b₅) . b₂ = FALSE or (Valid b₄,b₅) . b₂ = TRUE ) )

proof end;

theorem Th36: :: VALUAT_1:36

for b₁ being non empty set
for b₂ being Element of Valuations_in b₁
for b₃, b₄ being Element of CQC-WFF
for b₅ being interpretation of b₁ holds
( b₅,b₂ |= b₃ => b₄ iff ( b₅,b₂ |= b₃ implies b₅,b₂ |= b₄ ) )

proof end;

theorem Th37: :: VALUAT_1:37

for b₁ being non empty set
for b₂ being bound_QC-variable
for b₃ being Element of Valuations_in b₁
for b₄ being Element of Funcs (Valuations_in b₁),BOOLEAN st (FOR_ALL b₂,b₄) . b₃ = TRUE holds
b₄ . b₃ = TRUE

proof end;

definition

let c₁ be non empty set ;
let c₂ be interpretation of c₁;
let c₃ be Element of CQC-WFF ;
pred c₂ |= c₃ means :Def13: :: VALUAT_1:def 13
for b₁ being Element of Valuations_in a₁ holds a₂,b₁ |= a₃;

end;

:: deftheorem Def13 defines |= VALUAT_1:def 13 :

Lemma28: for b₁, b₂, b₃ being Element of BOOLEAN holds 'not' (('not' (b₁ '&' ('not' b₂))) '&' (('not' (b₂ '&' b₃)) '&' (b₁ '&' b₃))) = TRUE

proof end;

scheme :: VALUAT_1:sch 1
s1{ F₁() -> non empty set , F₂() -> bound_QC-variable, F₃() -> bound_QC-variable, F₄() -> Element of Valuations_in F₁(), F₅() -> Element of Valuations_in F₁() } :

ex b₁ being Element of Valuations_in F₁() st
( ( for b₂ being bound_QC-variable st b₂ <> F₂() holds
b₁ . b₂ = F₄() . b₂ ) & b₁ . F₂() = F₅() . F₃() )

proof end;

theorem Th38: :: VALUAT_1:38

canceled;

theorem Th39: :: VALUAT_1:39

for b₁ being non empty set
for b₂ being bound_QC-variable
for b₃ being Element of CQC-WFF
for b₄ being interpretation of b₁ st not b₂ in still_not-bound_in b₃ holds
for b₅, b₆ being Element of Valuations_in b₁ st ( for b₇ being bound_QC-variable st b₂ <> b₇ holds
b₆ . b₇ = b₅ . b₇ ) holds
(Valid b₃,b₄) . b₅ = (Valid b₃,b₄) . b₆

proof end;

theorem Th40: :: VALUAT_1:40

for b₁ being non empty set
for b₂ being bound_QC-variable
for b₃ being Element of Valuations_in b₁
for b₄ being Element of CQC-WFF
for b₅ being interpretation of b₁ st b₅,b₃ |= b₄ & not b₂ in still_not-bound_in b₄ holds
for b₆ being Element of Valuations_in b₁ st ( for b₇ being bound_QC-variable st b₂ <> b₇ holds
b₆ . b₇ = b₃ . b₇ ) holds
b₅,b₆ |= b₄

proof end;

theorem Th41: :: VALUAT_1:41

proof end;

theorem Th42: :: VALUAT_1:42

for b₁ being non empty set
for b₂, b₃ being bound_QC-variable
for b₄, b₅ being Element of CQC-WFF
for b₆ being interpretation of b₁
for b₇ being QC-formula st b₂ <> b₃ & b₄ = b₇ . b₂ & b₅ = b₇ . b₃ holds
for b₈ being Element of Valuations_in b₁ st b₈ . b₂ = b₈ . b₃ holds
(Valid b₄,b₆) . b₈ = (Valid b₅,b₆) . b₈

proof end;

theorem Th43: :: VALUAT_1:43

for b₁, b₂ being bound_QC-variable
for b₃ being QC-formula st b₁ <> b₂ & not b₁ in still_not-bound_in b₃ holds
not b₁ in still_not-bound_in (b₃ . b₂)

proof end;

theorem Th44: :: VALUAT_1:44

for b₁ being non empty set
for b₂ being Element of Valuations_in b₁
for b₃ being interpretation of b₁ holds b₃,b₂ |= VERUM

proof end;

theorem Th45: :: VALUAT_1:45

for b₁ being non empty set
for b₂ being Element of Valuations_in b₁
for b₃, b₄ being Element of CQC-WFF
for b₅ being interpretation of b₁ holds b₅,b₂ |= (b₃ '&' b₄) => (b₄ '&' b₃)

proof end;

theorem Th46: :: VALUAT_1:46

for b₁ being non empty set
for b₂ being Element of Valuations_in b₁
for b₃ being Element of CQC-WFF
for b₄ being interpretation of b₁ holds b₄,b₂ |= (('not' b₃) => b₃) => b₃

proof end;

theorem Th47: :: VALUAT_1:47

for b₁ being non empty set
for b₂ being Element of Valuations_in b₁
for b₃, b₄ being Element of CQC-WFF
for b₅ being interpretation of b₁ holds b₅,b₂ |= b₃ => (('not' b₃) => b₄)

proof end;

theorem Th48: :: VALUAT_1:48

for b₁ being non empty set
for b₂ being Element of Valuations_in b₁
for b₃, b₄, b₅ being Element of CQC-WFF
for b₆ being interpretation of b₁ holds b₆,b₂ |= (b₃ => b₄) => (('not' (b₄ '&' b₅)) => ('not' (b₃ '&' b₅)))

proof end;

theorem Th49: :: VALUAT_1:49

for b₁ being non empty set
for b₂ being Element of Valuations_in b₁
for b₃, b₄ being Element of CQC-WFF
for b₅ being interpretation of b₁ st b₅,b₂ |= b₃ & b₅,b₂ |= b₃ => b₄ holds
b₅,b₂ |= b₄ by Th36;

theorem Th50: :: VALUAT_1:50

for b₁ being non empty set
for b₂ being bound_QC-variable
for b₃ being Element of Valuations_in b₁
for b₄ being Element of CQC-WFF
for b₅ being interpretation of b₁ holds b₅,b₃ |= (All b₂,b₄) => b₄

proof end;

theorem Th51: :: VALUAT_1:51

for b₁ being non empty set
for b₂ being interpretation of b₁ holds b₂ |= VERUM

proof end;

theorem Th52: :: VALUAT_1:52

for b₁ being non empty set
for b₂, b₃ being Element of CQC-WFF
for b₄ being interpretation of b₁ holds b₄ |= (b₂ '&' b₃) => (b₃ '&' b₂)

proof end;

theorem Th53: :: VALUAT_1:53

for b₁ being non empty set
for b₂ being Element of CQC-WFF
for b₃ being interpretation of b₁ holds b₃ |= (('not' b₂) => b₂) => b₂

proof end;

theorem Th54: :: VALUAT_1:54

for b₁ being non empty set
for b₂, b₃ being Element of CQC-WFF
for b₄ being interpretation of b₁ holds b₄ |= b₂ => (('not' b₂) => b₃)

proof end;

theorem Th55: :: VALUAT_1:55

for b₁ being non empty set
for b₂, b₃, b₄ being Element of CQC-WFF
for b₅ being interpretation of b₁ holds b₅ |= (b₂ => b₃) => (('not' (b₃ '&' b₄)) => ('not' (b₂ '&' b₄)))

proof end;

theorem Th56: :: VALUAT_1:56

for b₁ being non empty set
for b₂, b₃ being Element of CQC-WFF
for b₄ being interpretation of b₁ st b₄ |= b₂ & b₄ |= b₂ => b₃ holds
b₄ |= b₃

proof end;

theorem Th57: :: VALUAT_1:57

for b₁ being non empty set
for b₂ being bound_QC-variable
for b₃ being Element of CQC-WFF
for b₄ being interpretation of b₁ holds b₄ |= (All b₂,b₃) => b₃

proof end;

theorem Th58: :: VALUAT_1:58

for b₁ being non empty set
for b₂ being bound_QC-variable
for b₃, b₄ being Element of CQC-WFF
for b₅ being interpretation of b₁ st b₅ |= b₃ => b₄ & not b₂ in still_not-bound_in b₃ holds
b₅ |= b₃ => (All b₂,b₄)

proof end;

theorem Th59: :: VALUAT_1:59

for b₁ being non empty set
for b₂, b₃ being bound_QC-variable
for b₄, b₅ being Element of CQC-WFF
for b₆ being interpretation of b₁
for b₇ being QC-formula st b₄ = b₇ . b₂ & b₅ = b₇ . b₃ & not b₂ in still_not-bound_in b₇ & b₆ |= b₄ holds
b₆ |= b₅

proof end;