:: Variables in Formulae of the First Order Language
:: by Czes{\l}aw Byli\'nski and Grzegorz Bancerek
::
:: Received November 23, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users


scheme :: QC_LANG3:sch 1
QCFuncUniq{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Function of (QC-WFF F1()),F2(), F4() -> Function of (QC-WFF F1()),F2(), F5() -> Element of F2(), F6( set ) -> Element of F2(), F7( set ) -> Element of F2(), F8( set , set ) -> Element of F2(), F9( set , set ) -> Element of F2() } :
F3() = F4()
provided
A1: for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F3() . p = F5() ) & ( p is atomic implies F3() . p = F6(p) ) & ( p is negative & d1 = F3() . (the_argument_of p) implies F3() . p = F7(d1) ) & ( p is conjunctive & d1 = F3() . (the_left_argument_of p) & d2 = F3() . (the_right_argument_of p) implies F3() . p = F8(d1,d2) ) & ( p is universal & d1 = F3() . (the_scope_of p) implies F3() . p = F9(p,d1) ) ) and
A2: for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F4() . p = F5() ) & ( p is atomic implies F4() . p = F6(p) ) & ( p is negative & d1 = F4() . (the_argument_of p) implies F4() . p = F7(d1) ) & ( p is conjunctive & d1 = F4() . (the_left_argument_of p) & d2 = F4() . (the_right_argument_of p) implies F4() . p = F8(d1,d2) ) & ( p is universal & d1 = F4() . (the_scope_of p) implies F4() . p = F9(p,d1) ) )
proof end;

scheme :: QC_LANG3:sch 2
QCDefD{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Element of F2(), F4() -> Element of QC-WFF F1(), F5( Element of QC-WFF F1()) -> Element of F2(), F6( Element of F2()) -> Element of F2(), F7( Element of F2(), Element of F2()) -> Element of F2(), F8( Element of QC-WFF F1(), Element of F2()) -> Element of F2() } :
( ex d being Element of F2() ex F being Function of (QC-WFF F1()),F2() st
( d = F . F4() & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) & ( for x1, x2 being Element of F2() st ex F being Function of (QC-WFF F1()),F2() st
( x1 = F . F4() & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) & ex F being Function of (QC-WFF F1()),F2() st
( x2 = F . F4() & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) holds
x1 = x2 ) )
proof end;

scheme :: QC_LANG3:sch 3
QCDResult9VERUM{ F1() -> QC-alphabet , F2() -> non empty set , F3( Element of QC-WFF F1()) -> Element of F2(), F4() -> Element of F2(), F5( Element of QC-WFF F1()) -> Element of F2(), F6( Element of F2()) -> Element of F2(), F7( Element of F2(), Element of F2()) -> Element of F2(), F8( Element of QC-WFF F1(), Element of F2()) -> Element of F2() } :
F3((VERUM F1())) = F4()
provided
A1: for p being QC-formula of F1()
for d being Element of F2() holds
( d = F3(p) iff ex F being Function of (QC-WFF F1()),F2() st
( d = F . p & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F4() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) )
proof end;

scheme :: QC_LANG3:sch 4
QCDResult9atomic{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Element of F2(), F4( Element of QC-WFF F1()) -> Element of F2(), F5() -> QC-formula of F1(), F6( Element of QC-WFF F1()) -> Element of F2(), F7( Element of F2()) -> Element of F2(), F8( Element of F2(), Element of F2()) -> Element of F2(), F9( Element of QC-WFF F1(), Element of F2()) -> Element of F2() } :
F4(F5()) = F6(F5())
provided
A1: for p being QC-formula of F1()
for d being Element of F2() holds
( d = F4(p) iff ex F being Function of (QC-WFF F1()),F2() st
( d = F . p & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F6(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F7(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F8(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F9(p,d1) ) ) ) ) ) and
A2: F5() is atomic
proof end;

scheme :: QC_LANG3:sch 5
QCDResult9negative{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Element of F2(), F4() -> QC-formula of F1(), F5( Element of QC-WFF F1()) -> Element of F2(), F6( Element of F2()) -> Element of F2(), F7( Element of F2(), Element of F2()) -> Element of F2(), F8( Element of QC-WFF F1(), Element of F2()) -> Element of F2(), F9( Element of QC-WFF F1()) -> Element of F2() } :
F9(F4()) = F6(F9((the_argument_of F4())))
provided
A1: for p being QC-formula of F1()
for d being Element of F2() holds
( d = F9(p) iff ex F being Function of (QC-WFF F1()),F2() st
( d = F . p & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) ) and
A2: F4() is negative
proof end;

scheme :: QC_LANG3:sch 6
QCDResult9conjunctive{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Element of F2(), F4( Element of QC-WFF F1()) -> Element of F2(), F5( Element of F2()) -> Element of F2(), F6( Element of F2(), Element of F2()) -> Element of F2(), F7( Element of QC-WFF F1(), Element of F2()) -> Element of F2(), F8( Element of QC-WFF F1()) -> Element of F2(), F9() -> QC-formula of F1() } :
for d1, d2 being Element of F2() st d1 = F8((the_left_argument_of F9())) & d2 = F8((the_right_argument_of F9())) holds
F8(F9()) = F6(d1,d2)
provided
A1: for p being QC-formula of F1()
for d being Element of F2() holds
( d = F8(p) iff ex F being Function of (QC-WFF F1()),F2() st
( d = F . p & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F4(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F5(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F6(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F7(p,d1) ) ) ) ) ) and
A2: F9() is conjunctive
proof end;

scheme :: QC_LANG3:sch 7
QCDResult9universal{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Element of F2(), F4() -> QC-formula of F1(), F5( Element of QC-WFF F1()) -> Element of F2(), F6( Element of F2()) -> Element of F2(), F7( Element of F2(), Element of F2()) -> Element of F2(), F8( Element of QC-WFF F1(), Element of F2()) -> Element of F2(), F9( Element of QC-WFF F1()) -> Element of F2() } :
F9(F4()) = F8(F4(),F9((the_scope_of F4())))
provided
A1: for p being QC-formula of F1()
for d being Element of F2() holds
( d = F9(p) iff ex F being Function of (QC-WFF F1()),F2() st
( d = F . p & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) ) and
A2: F4() is universal
proof end;

theorem :: QC_LANG3:1
for A being QC-alphabet
for P being QC-pred_symbol of A holds P is QC-pred_symbol of (the_arity_of P),A
proof end;

definition
let A be QC-alphabet ;
let l be FinSequence of QC-variables A;
let V be non empty Subset of (QC-variables A);
func variables_in (l,V) -> Subset of V equals :: QC_LANG3:def 1
 { (l . k) where k is Nat : ( 1 <= k & k <= len l & l . k in V ) } ;
coherence
{ (l . k) where k is Nat : ( 1 <= k & k <= len l & l . k in V ) } is Subset of V
proof end;
end;

:: deftheorem defines variables_in QC_LANG3:def 1 :
for A being QC-alphabet
for l being FinSequence of QC-variables A
for V being non empty Subset of (QC-variables A) holds variables_in (l,V) = { (l . k) where k is Nat : ( 1 <= k & k <= len l & l . k in V ) } ;

theorem :: QC_LANG3:2
for A being QC-alphabet
for l being FinSequence of QC-variables A holds still_not-bound_in l = variables_in (l,(bound_QC-variables A)) ;

Lm1: now :: thesis: for A being QC-alphabet
for p being QC-formula of A
for d being Subset of (bound_QC-variables A) holds
( d = H1(p) iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( d = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H4(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H5(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H3(p,d1) ) ) ) ) )
let A be QC-alphabet ; :: thesis: for p being QC-formula of A
for d being Subset of (bound_QC-variables A) holds
( d = H1(p) iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( d = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H4(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H5(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H3(p,d1) ) ) ) ) )
deffunc H1( Element of QC-WFF A) -> Element of bool (bound_QC-variables A) = still_not-bound_in $1;
deffunc H2( Element of QC-WFF A) -> Element of bool (bound_QC-variables A) = still_not-bound_in (the_arguments_of $1);
deffunc H3( Element of QC-WFF A, Subset of (bound_QC-variables A)) -> Element of bool (bound_QC-variables A) = $2 \ {(bound_in $1)};
deffunc H4( Subset of (bound_QC-variables A)) -> Subset of (bound_QC-variables A) = $1;
deffunc H5( Subset of (bound_QC-variables A), Subset of (bound_QC-variables A)) -> Element of bool (bound_QC-variables A) = $1 \/ $2;
thus for p being QC-formula of A
for d being Subset of (bound_QC-variables A) holds
( d = H1(p) iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( d = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H4(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H5(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H3(p,d1) ) ) ) ) ) :: thesis: verum
proof
let p be QC-formula of A; :: thesis: for d being Subset of (bound_QC-variables A) holds
( d = H1(p) iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( d = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H4(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H5(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H3(p,d1) ) ) ) ) )
let d be Subset of (bound_QC-variables A); :: thesis: ( d = H1(p) iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( d = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H4(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H5(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H3(p,d1) ) ) ) ) )
thus ( d = still_not-bound_in p implies ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( d = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) ) ) ) :: thesis: ( ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( d = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H4(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H5(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H3(p,d1) ) ) ) ) implies d = H1(p) )
proof
assume d = still_not-bound_in p ; :: thesis: ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( d = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) ) )
then consider F being Function of (QC-WFF A),(bool (bound_QC-variables A)) such that
A1: ( d = F . p & ( for p being Element of QC-WFF A holds
( F . (VERUM A) = {} & ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Nat : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ) & ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) ) ) ) by QC_LANG1:def 30;
take F ; :: thesis: ( d = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) ) )
thus d = F . p by A1; :: thesis: for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) )
let p be Element of QC-WFF A; :: thesis: for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) )
let d1, d2 be Subset of (bound_QC-variables A); :: thesis: ( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) )
thus ( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) ) by A1; :: thesis: ( ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) )
thus ( ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) by A1; :: thesis: verum
end;
given F being Function of (QC-WFF A),(bool (bound_QC-variables A)) such that A2: d = F . p and
A3: for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) ; :: thesis: d = H1(p)
now :: thesis: for p being Element of QC-WFF A holds
( F . (VERUM A) = {} & ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Nat : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ) & ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) )
let p be Element of QC-WFF A; :: thesis: ( F . (VERUM A) = {} & ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Nat : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ) & ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) )
thus F . (VERUM A) = {} by A3; :: thesis: ( ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Nat : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ) & ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) )
thus ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Nat : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ) :: thesis: ( ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) )
proof
assume p is atomic ; :: thesis: F . p = { ((the_arguments_of p) . k) where k is Nat : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) }
then F . p = still_not-bound_in (the_arguments_of p) by A3;
hence F . p = { ((the_arguments_of p) . k) where k is Nat : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ; :: thesis: verum
end;
thus ( p is negative implies F . p = F . (the_argument_of p) ) by A3; :: thesis: ( ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) )
thus ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) by A3; :: thesis: ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} )
assume p is universal ; :: thesis: F . p = (F . (the_scope_of p)) \ {(bound_in p)}
hence F . p = (F . (the_scope_of p)) \ {(bound_in p)} by A3; :: thesis: verum
end;
hence d = H1(p) by A2, QC_LANG1:def 30; :: thesis: verum
end;
end;

theorem Th3: :: QC_LANG3:3
for A being QC-alphabet holds still_not-bound_in (VERUM A) = {}
proof end;

theorem Th4: :: QC_LANG3:4
for A being QC-alphabet
for p being QC-formula of A st p is atomic holds
still_not-bound_in p = still_not-bound_in (the_arguments_of p)
proof end;

theorem :: QC_LANG3:5
for k being Nat
for A being QC-alphabet
for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds still_not-bound_in (P ! l) = still_not-bound_in l
proof end;

theorem Th6: :: QC_LANG3:6
for A being QC-alphabet
for p being QC-formula of A st p is negative holds
still_not-bound_in p = still_not-bound_in (the_argument_of p)
proof end;

theorem Th7: :: QC_LANG3:7
for A being QC-alphabet
for p being QC-formula of A holds still_not-bound_in ('not' p) = still_not-bound_in p
proof end;

theorem Th8: :: QC_LANG3:8
for A being QC-alphabet holds still_not-bound_in (FALSUM A) = {}
proof end;

theorem Th9: :: QC_LANG3:9
for A being QC-alphabet
for p being QC-formula of A st p is conjunctive holds
still_not-bound_in p = (still_not-bound_in (the_left_argument_of p)) \/ (still_not-bound_in (the_right_argument_of p))
proof end;

theorem Th10: :: QC_LANG3:10
for A being QC-alphabet
for p, q being QC-formula of A holds still_not-bound_in (p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q)
proof end;

theorem Th11: :: QC_LANG3:11
for A being QC-alphabet
for p being QC-formula of A st p is universal holds
still_not-bound_in p = (still_not-bound_in (the_scope_of p)) \ {(bound_in p)}
proof end;

theorem Th12: :: QC_LANG3:12
for A being QC-alphabet
for x being bound_QC-variable of A
for p being QC-formula of A holds still_not-bound_in (All (x,p)) = (still_not-bound_in p) \ {x}
proof end;

theorem Th13: :: QC_LANG3:13
for A being QC-alphabet
for p being QC-formula of A st p is disjunctive holds
still_not-bound_in p = (still_not-bound_in (the_left_disjunct_of p)) \/ (still_not-bound_in (the_right_disjunct_of p))
proof end;

theorem :: QC_LANG3:14
for A being QC-alphabet
for p, q being QC-formula of A holds still_not-bound_in (p 'or' q) = (still_not-bound_in p) \/ (still_not-bound_in q)
proof end;

theorem Th15: :: QC_LANG3:15
for A being QC-alphabet
for p being QC-formula of A st p is conditional holds
still_not-bound_in p = (still_not-bound_in (the_antecedent_of p)) \/ (still_not-bound_in (the_consequent_of p))
proof end;

theorem Th16: :: QC_LANG3:16
for A being QC-alphabet
for p, q being QC-formula of A holds still_not-bound_in (p => q) = (still_not-bound_in p) \/ (still_not-bound_in q)
proof end;

theorem Th17: :: QC_LANG3:17
for A being QC-alphabet
for p being QC-formula of A st p is biconditional holds
still_not-bound_in p = (still_not-bound_in (the_left_side_of p)) \/ (still_not-bound_in (the_right_side_of p))
proof end;

theorem :: QC_LANG3:18
for A being QC-alphabet
for p, q being QC-formula of A holds still_not-bound_in (p <=> q) = (still_not-bound_in p) \/ (still_not-bound_in q)
proof end;

theorem Th19: :: QC_LANG3:19
for A being QC-alphabet
for x being bound_QC-variable of A
for p being QC-formula of A holds still_not-bound_in (Ex (x,p)) = (still_not-bound_in p) \ {x}
proof end;

theorem :: QC_LANG3:20
for A being QC-alphabet holds
( VERUM A is closed & FALSUM A is closed ) by Th3, Th8;

theorem Th21: :: QC_LANG3:21
for A being QC-alphabet
for p being QC-formula of A holds
( p is closed iff 'not' p is closed ) by Th7;

theorem Th22: :: QC_LANG3:22
for A being QC-alphabet
for p, q being QC-formula of A holds
( ( p is closed & q is closed ) iff p '&' q is closed )
proof end;

theorem Th23: :: QC_LANG3:23
for A being QC-alphabet
for x being bound_QC-variable of A
for p being QC-formula of A holds
( All (x,p) is closed iff still_not-bound_in p c= {x} )
proof end;

theorem :: QC_LANG3:24
for A being QC-alphabet
for x being bound_QC-variable of A
for p being QC-formula of A st p is closed holds
All (x,p) is closed
proof end;

theorem :: QC_LANG3:25
for A being QC-alphabet
for p, q being QC-formula of A holds
( ( p is closed & q is closed ) iff p 'or' q is closed )
proof end;

theorem Th26: :: QC_LANG3:26
for A being QC-alphabet
for p, q being QC-formula of A holds
( ( p is closed & q is closed ) iff p => q is closed )
proof end;

theorem :: QC_LANG3:27
for A being QC-alphabet
for p, q being QC-formula of A holds
( ( p is closed & q is closed ) iff p <=> q is closed )
proof end;

theorem Th28: :: QC_LANG3:28
for A being QC-alphabet
for x being bound_QC-variable of A
for p being QC-formula of A holds
( Ex (x,p) is closed iff still_not-bound_in p c= {x} )
proof end;

theorem :: QC_LANG3:29
for A being QC-alphabet
for x being bound_QC-variable of A
for p being QC-formula of A st p is closed holds
Ex (x,p) is closed
proof end;

definition
let A be QC-alphabet ;
let s be QC-symbol of A;
func x. s -> bound_QC-variable of A equals :: QC_LANG3:def 2
[4,s];
coherence
[4,s] is bound_QC-variable of A
proof end;
end;

:: deftheorem defines x. QC_LANG3:def 2 :
for A being QC-alphabet
for s being QC-symbol of A holds x. s = [4,s];

theorem :: QC_LANG3:30
for A being QC-alphabet
for x being bound_QC-variable of A ex t being QC-symbol of A st x. t = x
proof end;

definition
let A be QC-alphabet ;
let k be Nat;
func A a. k -> free_QC-variable of A equals :: QC_LANG3:def 3
[6,k];
coherence
[6,k] is free_QC-variable of A
proof end;
end;

:: deftheorem defines a. QC_LANG3:def 3 :
for A being QC-alphabet
for k being Nat holds A a. k = [6,k];

theorem :: QC_LANG3:31
for A being QC-alphabet
for a being free_QC-variable of A ex i being Nat st A a. i = a
proof end;

theorem :: QC_LANG3:32
for A being QC-alphabet
for c being Element of fixed_QC-variables A
for a being Element of free_QC-variables A holds c <> a
proof end;

theorem :: QC_LANG3:33
for A being QC-alphabet
for c being Element of fixed_QC-variables A
for x being Element of bound_QC-variables A holds c <> x
proof end;

theorem :: QC_LANG3:34
for A being QC-alphabet
for a being Element of free_QC-variables A
for x being Element of bound_QC-variables A holds a <> x
proof end;

definition
let A be QC-alphabet ;
let V be non empty Subset of (QC-variables A);
let p be Element of QC-WFF A;
func Vars (p,V) -> Subset of V means :Def4: :: QC_LANG3:def 4
 ex F being Function of (QC-WFF A),(bool V) st
( it = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of V holds
( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = variables_in ((the_arguments_of p),V) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 ) ) ) );
correctness
existence
ex b1 being Subset of V ex F being Function of (QC-WFF A),(bool V) st
( b1 = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of V holds
( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = variables_in ((the_arguments_of p),V) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 ) ) ) );
uniqueness
for b1, b2 being Subset of V st ex F being Function of (QC-WFF A),(bool V) st
( b1 = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of V holds
( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = variables_in ((the_arguments_of p),V) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 ) ) ) ) & ex F being Function of (QC-WFF A),(bool V) st
( b2 = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of V holds
( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = variables_in ((the_arguments_of p),V) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 ) ) ) ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def4 defines Vars QC_LANG3:def 4 :
for A being QC-alphabet
for V being non empty Subset of (QC-variables A)
for p being Element of QC-WFF A
for b4 being Subset of V holds
( b4 = Vars (p,V) iff ex F being Function of (QC-WFF A),(bool V) st
( b4 = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of V holds
( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = variables_in ((the_arguments_of p),V) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 ) ) ) ) );

Lm2: now :: thesis: for A being QC-alphabet
for V being non empty Subset of (QC-variables A) holds
( H1( VERUM A) = {} & ( for p being Element of QC-WFF A st p is atomic holds
Vars (p,V) = variables_in ((the_arguments_of p),V) ) & ( for p being Element of QC-WFF A st p is negative holds
Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF A st p is conjunctive holds
Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds
Vars (p,V) = Vars ((the_scope_of p),V) ) )
let A be QC-alphabet ; :: thesis: for V being non empty Subset of (QC-variables A) holds
( H1( VERUM A) = {} & ( for p being Element of QC-WFF A st p is atomic holds
Vars (p,V) = variables_in ((the_arguments_of p),V) ) & ( for p being Element of QC-WFF A st p is negative holds
Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF A st p is conjunctive holds
Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds
Vars (p,V) = Vars ((the_scope_of p),V) ) )
let V be non empty Subset of (QC-variables A); :: thesis: ( H1( VERUM A) = {} & ( for p being Element of QC-WFF A st p is atomic holds
Vars (p,V) = variables_in ((the_arguments_of p),V) ) & ( for p being Element of QC-WFF A st p is negative holds
Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF A st p is conjunctive holds
Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds
Vars (p,V) = Vars ((the_scope_of p),V) ) )
deffunc H1( Element of QC-WFF A) -> Subset of V = Vars ($1,V);
deffunc H2( Element of QC-WFF A) -> Subset of V = variables_in ((the_arguments_of $1),V);
deffunc H3( Subset of V) -> Subset of V = $1;
deffunc H4( Subset of V, Subset of V) -> Element of bool V = $1 \/ $2;
deffunc H5( Element of QC-WFF A, Subset of V) -> Subset of V = $2;
A1: for p being Element of QC-WFF A
for X being Subset of V holds
( X = H1(p) iff ex F being Function of (QC-WFF A),(bool V) st
( X = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of V holds
( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H3(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H4(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H5(p,d1) ) ) ) ) ) by Def4;
thus H1( VERUM A) = {} V from QC_LANG3:sch 3(A1)
.= {} ; :: thesis: ( ( for p being Element of QC-WFF A st p is atomic holds
Vars (p,V) = variables_in ((the_arguments_of p),V) ) & ( for p being Element of QC-WFF A st p is negative holds
Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF A st p is conjunctive holds
Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds
Vars (p,V) = Vars ((the_scope_of p),V) ) )
thus for p being Element of QC-WFF A st p is atomic holds
Vars (p,V) = variables_in ((the_arguments_of p),V) :: thesis: ( ( for p being Element of QC-WFF A st p is negative holds
Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF A st p is conjunctive holds
Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds
Vars (p,V) = Vars ((the_scope_of p),V) ) )
proof
let p be Element of QC-WFF A; :: thesis: ( p is atomic implies Vars (p,V) = variables_in ((the_arguments_of p),V) )
assume A2: p is atomic ; :: thesis: Vars (p,V) = variables_in ((the_arguments_of p),V)
thus H1(p) = H2(p) from QC_LANG3:sch 4(A1, A2); :: thesis: verum
end;
thus for p being Element of QC-WFF A st p is negative holds
Vars (p,V) = Vars ((the_argument_of p),V) :: thesis: ( ( for p being Element of QC-WFF A st p is conjunctive holds
Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds
Vars (p,V) = Vars ((the_scope_of p),V) ) )
proof
let p be Element of QC-WFF A; :: thesis: ( p is negative implies Vars (p,V) = Vars ((the_argument_of p),V) )
assume A3: p is negative ; :: thesis: Vars (p,V) = Vars ((the_argument_of p),V)
thus H1(p) = H3(H1( the_argument_of p)) from QC_LANG3:sch 5(A1, A3); :: thesis: verum
end;
thus for p being Element of QC-WFF A st p is conjunctive holds
Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) :: thesis: for p being Element of QC-WFF A st p is universal holds
Vars (p,V) = Vars ((the_scope_of p),V)
proof
let p be Element of QC-WFF A; :: thesis: ( p is conjunctive implies Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) )
assume A4: p is conjunctive ; :: thesis: Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V))
for d1, d2 being Subset of V st d1 = H1( the_left_argument_of p) & d2 = H1( the_right_argument_of p) holds
H1(p) = H4(d1,d2) from QC_LANG3:sch 6(A1, A4);
 hence Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ; :: thesis: verum
end;
thus for p being Element of QC-WFF A st p is universal holds
Vars (p,V) = Vars ((the_scope_of p),V) :: thesis: verum
proof
let p be Element of QC-WFF A; :: thesis: ( p is universal implies Vars (p,V) = Vars ((the_scope_of p),V) )
assume A5: p is universal ; :: thesis: Vars (p,V) = Vars ((the_scope_of p),V)
thus H1(p) = H5(p,H1( the_scope_of p)) from QC_LANG3:sch 7(A1, A5); :: thesis: verum
end;
end;

theorem :: QC_LANG3:35
for A being QC-alphabet
for V being non empty Subset of (QC-variables A) holds Vars ((VERUM A),V) = {} by Lm2;

theorem Th36: :: QC_LANG3:36
for A being QC-alphabet
for p being Element of QC-WFF A
for V being non empty Subset of (QC-variables A) st p is atomic holds
( Vars (p,V) = variables_in ((the_arguments_of p),V) & Vars (p,V) = { ((the_arguments_of p) . k) where k is Nat : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in V ) } )
proof end;

theorem Th37: :: QC_LANG3:37
for k being Nat
for A being QC-alphabet
for V being non empty Subset of (QC-variables A)
for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds
( Vars ((P ! l),V) = variables_in (l,V) & Vars ((P ! l),V) = { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in V ) } )
proof end;

theorem :: QC_LANG3:38
for A being QC-alphabet
for p being Element of QC-WFF A
for V being non empty Subset of (QC-variables A) st p is negative holds
Vars (p,V) = Vars ((the_argument_of p),V) by Lm2;

theorem Th39: :: QC_LANG3:39
for A being QC-alphabet
for p being Element of QC-WFF A
for V being non empty Subset of (QC-variables A) holds Vars (('not' p),V) = Vars (p,V)
proof end;

theorem Th40: :: QC_LANG3:40
for A being QC-alphabet
for V being non empty Subset of (QC-variables A) holds Vars ((FALSUM A),V) = {}
proof end;

theorem :: QC_LANG3:41
for A being QC-alphabet
for p being Element of QC-WFF A
for V being non empty Subset of (QC-variables A) st p is conjunctive holds
Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) by Lm2;

theorem Th42: :: QC_LANG3:42
for A being QC-alphabet
for p, q being Element of QC-WFF A
for V being non empty Subset of (QC-variables A) holds Vars ((p '&' q),V) = (Vars (p,V)) \/ (Vars (q,V))
proof end;

theorem :: QC_LANG3:43
for A being QC-alphabet
for p being Element of QC-WFF A
for V being non empty Subset of (QC-variables A) st p is universal holds
Vars (p,V) = Vars ((the_scope_of p),V) by Lm2;

theorem Th44: :: QC_LANG3:44
for A being QC-alphabet
for x being bound_QC-variable of A
for p being Element of QC-WFF A
for V being non empty Subset of (QC-variables A) holds Vars ((All (x,p)),V) = Vars (p,V)
proof end;

theorem Th45: :: QC_LANG3:45
for A being QC-alphabet
for p being Element of QC-WFF A
for V being non empty Subset of (QC-variables A) st p is disjunctive holds
Vars (p,V) = (Vars ((the_left_disjunct_of p),V)) \/ (Vars ((the_right_disjunct_of p),V))
proof end;

theorem :: QC_LANG3:46
for A being QC-alphabet
for p, q being Element of QC-WFF A
for V being non empty Subset of (QC-variables A) holds Vars ((p 'or' q),V) = (Vars (p,V)) \/ (Vars (q,V))
proof end;

theorem Th47: :: QC_LANG3:47
for A being QC-alphabet
for p being Element of QC-WFF A
for V being non empty Subset of (QC-variables A) st p is conditional holds
Vars (p,V) = (Vars ((the_antecedent_of p),V)) \/ (Vars ((the_consequent_of p),V))
proof end;

theorem Th48: :: QC_LANG3:48
for A being QC-alphabet
for p, q being Element of QC-WFF A
for V being non empty Subset of (QC-variables A) holds Vars ((p => q),V) = (Vars (p,V)) \/ (Vars (q,V))
proof end;

theorem Th49: :: QC_LANG3:49
for A being QC-alphabet
for p being Element of QC-WFF A
for V being non empty Subset of (QC-variables A) st p is biconditional holds
Vars (p,V) = (Vars ((the_left_side_of p),V)) \/ (Vars ((the_right_side_of p),V))
proof end;

theorem :: QC_LANG3:50
for A being QC-alphabet
for p, q being Element of QC-WFF A
for V being non empty Subset of (QC-variables A) holds Vars ((p <=> q),V) = (Vars (p,V)) \/ (Vars (q,V))
proof end;

theorem :: QC_LANG3:51
for A being QC-alphabet
for p being Element of QC-WFF A
for V being non empty Subset of (QC-variables A) st p is existential holds
Vars (p,V) = Vars ((the_argument_of (the_scope_of (the_argument_of p))),V)
proof end;

theorem :: QC_LANG3:52
for A being QC-alphabet
for x being bound_QC-variable of A
for p being Element of QC-WFF A
for V being non empty Subset of (QC-variables A) holds Vars ((Ex (x,p)),V) = Vars (p,V)
proof end;

definition
let A be QC-alphabet ;
let p be Element of QC-WFF A;
func Free p -> Subset of (free_QC-variables A) equals :: QC_LANG3:def 5
 Vars (p,(free_QC-variables A));
correctness
coherence
Vars (p,(free_QC-variables A)) is Subset of (free_QC-variables A);
;
end;

:: deftheorem defines Free QC_LANG3:def 5 :
for A being QC-alphabet
for p being Element of QC-WFF A holds Free p = Vars (p,(free_QC-variables A));

theorem :: QC_LANG3:53
for A being QC-alphabet holds Free (VERUM A) = {} by Lm2;

theorem :: QC_LANG3:54
for k being Nat
for A being QC-alphabet
for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds Free (P ! l) = { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } by Th37;

theorem :: QC_LANG3:55
for A being QC-alphabet
for p being Element of QC-WFF A holds Free ('not' p) = Free p by Th39;

theorem :: QC_LANG3:56
for A being QC-alphabet holds Free (FALSUM A) = {} by Th40;

theorem :: QC_LANG3:57
for A being QC-alphabet
for p, q being Element of QC-WFF A holds Free (p '&' q) = (Free p) \/ (Free q) by Th42;

theorem :: QC_LANG3:58
for A being QC-alphabet
for x being bound_QC-variable of A
for p being Element of QC-WFF A holds Free (All (x,p)) = Free p by Th44;

theorem :: QC_LANG3:59
for A being QC-alphabet
for p, q being Element of QC-WFF A holds Free (p 'or' q) = (Free p) \/ (Free q)
proof end;

theorem Th60: :: QC_LANG3:60
for A being QC-alphabet
for p, q being Element of QC-WFF A holds Free (p => q) = (Free p) \/ (Free q)
proof end;

theorem :: QC_LANG3:61
for A being QC-alphabet
for p, q being Element of QC-WFF A holds Free (p <=> q) = (Free p) \/ (Free q)
proof end;

theorem :: QC_LANG3:62
for A being QC-alphabet
for x being bound_QC-variable of A
for p being Element of QC-WFF A holds Free (Ex (x,p)) = Free p
proof end;

definition
let A be QC-alphabet ;
let p be Element of QC-WFF A;
func Fixed p -> Subset of (fixed_QC-variables A) equals :: QC_LANG3:def 6
 Vars (p,(fixed_QC-variables A));
correctness
coherence
Vars (p,(fixed_QC-variables A)) is Subset of (fixed_QC-variables A);
;
end;

:: deftheorem defines Fixed QC_LANG3:def 6 :
for A being QC-alphabet
for p being Element of QC-WFF A holds Fixed p = Vars (p,(fixed_QC-variables A));

theorem :: QC_LANG3:63
for A being QC-alphabet holds Fixed (VERUM A) = {} by Lm2;

theorem :: QC_LANG3:64
for k being Nat
for A being QC-alphabet
for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds Fixed (P ! l) = { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } by Th37;

theorem :: QC_LANG3:65
for A being QC-alphabet
for p being Element of QC-WFF A holds Fixed ('not' p) = Fixed p by Th39;

theorem :: QC_LANG3:66
for A being QC-alphabet holds Fixed (FALSUM A) = {}
proof end;

theorem :: QC_LANG3:67
for A being QC-alphabet
for p, q being Element of QC-WFF A holds Fixed (p '&' q) = (Fixed p) \/ (Fixed q) by Th42;

theorem :: QC_LANG3:68
for A being QC-alphabet
for x being bound_QC-variable of A
for p being Element of QC-WFF A holds Fixed (All (x,p)) = Fixed p by Th44;

theorem :: QC_LANG3:69
for A being QC-alphabet
for p, q being Element of QC-WFF A holds Fixed (p 'or' q) = (Fixed p) \/ (Fixed q)
proof end;

theorem Th70: :: QC_LANG3:70
for A being QC-alphabet
for p, q being Element of QC-WFF A holds Fixed (p => q) = (Fixed p) \/ (Fixed q)
proof end;

theorem :: QC_LANG3:71
for A being QC-alphabet
for p, q being Element of QC-WFF A holds Fixed (p <=> q) = (Fixed p) \/ (Fixed q)
proof end;

theorem :: QC_LANG3:72
for A being QC-alphabet
for x being bound_QC-variable of A
for p being Element of QC-WFF A holds Fixed (Ex (x,p)) = Fixed p
proof end;