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


begin

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

scheme :: QC_LANG3:sch 2
QCDefD{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Element of QC-WFF , F4( Element of QC-WFF ) -> Element of F1(), F5( Element of F1()) -> Element of F1(), F6( Element of F1(), Element of F1()) -> Element of F1(), F7( Element of QC-WFF , Element of F1()) -> Element of F1() } :
( ex d being Element of F1() ex F being Function of QC-WFF,F1() st
( d = F . F3() & ( for p being Element of QC-WFF
for d1, d2 being Element of F1() holds
( ( p = VERUM implies F . p = F2() ) & ( 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) ) ) ) ) & ( for x1, x2 being Element of F1() st ex F being Function of QC-WFF,F1() st
( x1 = F . F3() & ( for p being Element of QC-WFF
for d1, d2 being Element of F1() holds
( ( p = VERUM implies F . p = F2() ) & ( 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) ) ) ) ) & ex F being Function of QC-WFF,F1() st
( x2 = F . F3() & ( for p being Element of QC-WFF
for d1, d2 being Element of F1() holds
( ( p = VERUM implies F . p = F2() ) & ( 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) ) ) ) ) holds
x1 = x2 ) )
proof end;

scheme :: QC_LANG3:sch 3
QCDResult9VERUM{ F1() -> non empty set , F2( Element of QC-WFF ) -> Element of F1(), F3() -> Element of F1(), F4( Element of QC-WFF ) -> Element of F1(), F5( Element of F1()) -> Element of F1(), F6( Element of F1(), Element of F1()) -> Element of F1(), F7( Element of QC-WFF , Element of F1()) -> Element of F1() } :
F2(VERUM) = F3()
provided
A1: for p being QC-formula
for d being Element of F1() holds
( d = F2(p) iff ex F being Function of QC-WFF,F1() st
( d = F . p & ( for p being Element of QC-WFF
for d1, d2 being Element of F1() holds
( ( p = VERUM 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) ) ) ) ) )
proof end;

scheme :: QC_LANG3:sch 4
QCDResult9atomic{ F1() -> non empty set , F2() -> Element of F1(), F3( Element of QC-WFF ) -> Element of F1(), F4() -> QC-formula, F5( Element of QC-WFF ) -> Element of F1(), F6( Element of F1()) -> Element of F1(), F7( Element of F1(), Element of F1()) -> Element of F1(), F8( Element of QC-WFF , Element of F1()) -> Element of F1() } :
F3(F4()) = F5(F4())
provided
A1: for p being QC-formula
for d being Element of F1() holds
( d = F3(p) iff ex F being Function of QC-WFF,F1() st
( d = F . p & ( for p being Element of QC-WFF
for d1, d2 being Element of F1() holds
( ( p = VERUM implies F . p = F2() ) & ( 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 atomic
proof end;

scheme :: QC_LANG3:sch 5
QCDResult9negative{ F1() -> non empty set , F2() -> Element of F1(), F3() -> QC-formula, F4( Element of QC-WFF ) -> Element of F1(), F5( Element of F1()) -> Element of F1(), F6( Element of F1(), Element of F1()) -> Element of F1(), F7( Element of QC-WFF , Element of F1()) -> Element of F1(), F8( Element of QC-WFF ) -> Element of F1() } :
F8(F3()) = F5(F8((the_argument_of F3())))
provided
A1: for p being QC-formula
for d being Element of F1() holds
( d = F8(p) iff ex F being Function of QC-WFF,F1() st
( d = F . p & ( for p being Element of QC-WFF
for d1, d2 being Element of F1() holds
( ( p = VERUM implies F . p = F2() ) & ( 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: F3() is negative
proof end;

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

scheme :: QC_LANG3:sch 7
QCDResult9universal{ F1() -> non empty set , F2() -> Element of F1(), F3() -> QC-formula, F4( Element of QC-WFF ) -> Element of F1(), F5( Element of F1()) -> Element of F1(), F6( Element of F1(), Element of F1()) -> Element of F1(), F7( Element of QC-WFF , Element of F1()) -> Element of F1(), F8( Element of QC-WFF ) -> Element of F1() } :
F8(F3()) = F7(F3(),F8((the_scope_of F3())))
provided
A1: for p being QC-formula
for d being Element of F1() holds
( d = F8(p) iff ex F being Function of QC-WFF,F1() st
( d = F . p & ( for p being Element of QC-WFF
for d1, d2 being Element of F1() holds
( ( p = VERUM implies F . p = F2() ) & ( 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: F3() is universal
proof end;

theorem :: QC_LANG3:1
canceled;

theorem :: QC_LANG3:2
canceled;

theorem :: QC_LANG3:3
for P being QC-pred_symbol holds P is QC-pred_symbol of (the_arity_of P)
proof end;

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

:: deftheorem QC_LANG3:def 1 :
canceled;

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

theorem :: QC_LANG3:4
canceled;

theorem :: QC_LANG3:5
canceled;

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

deffunc H1( Element of QC-WFF ) -> Element of bool bound_QC-variables = still_not-bound_in $1;

deffunc H2( Element of QC-WFF ) -> Element of bool bound_QC-variables = still_not-bound_in (the_arguments_of $1);

deffunc H3( Subset of bound_QC-variables) -> Subset of bound_QC-variables = $1;

deffunc H4( Subset of bound_QC-variables, Subset of bound_QC-variables) -> Element of bool bound_QC-variables = $1 \/ $2;

deffunc H5( Element of QC-WFF , Subset of bound_QC-variables) -> Element of bool bound_QC-variables = $2 \ {(bound_in $1)};

Lm1: for p being QC-formula
for d being Subset of bound_QC-variables holds
( d = H1(p) iff ex F being Function of QC-WFF,(bool bound_QC-variables) st
( d = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of bound_QC-variables holds
( ( p = VERUM implies F . p = {} bound_QC-variables ) & ( 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) ) ) ) ) )
proof end;

theorem Th7: :: QC_LANG3:7
still_not-bound_in VERUM = {}
proof end;

theorem Th8: :: QC_LANG3:8
for p being QC-formula st p is atomic holds
still_not-bound_in p = still_not-bound_in (the_arguments_of p)
proof end;

theorem :: QC_LANG3:9
for k being Element of NAT
for P being QC-pred_symbol of k
for l being QC-variable_list of k holds still_not-bound_in (P ! l) = still_not-bound_in l
proof end;

theorem Th10: :: QC_LANG3:10
for p being QC-formula st p is negative holds
still_not-bound_in p = still_not-bound_in (the_argument_of p)
proof end;

theorem Th11: :: QC_LANG3:11
for p being QC-formula holds still_not-bound_in ('not' p) = still_not-bound_in p
proof end;

theorem Th12: :: QC_LANG3:12
still_not-bound_in FALSUM = {} by Th7, Th11, QC_LANG2:def 1;

theorem Th13: :: QC_LANG3:13
for p being QC-formula 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 Th14: :: QC_LANG3:14
for p, q being QC-formula holds still_not-bound_in (p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q)
proof end;

theorem Th15: :: QC_LANG3:15
for p being QC-formula st p is universal holds
still_not-bound_in p = (still_not-bound_in (the_scope_of p)) \ {(bound_in p)}
proof end;

theorem Th16: :: QC_LANG3:16
for x being bound_QC-variable
for p being QC-formula holds still_not-bound_in (All (x,p)) = (still_not-bound_in p) \ {x}
proof end;

theorem Th17: :: QC_LANG3:17
for p being QC-formula 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:18
for p, q being QC-formula holds still_not-bound_in (p 'or' q) = (still_not-bound_in p) \/ (still_not-bound_in q)
proof end;

theorem Th19: :: QC_LANG3:19
for p being QC-formula 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 Th20: :: QC_LANG3:20
for p, q being QC-formula holds still_not-bound_in (p => q) = (still_not-bound_in p) \/ (still_not-bound_in q)
proof end;

theorem Th21: :: QC_LANG3:21
for p being QC-formula 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:22
for p, q being QC-formula holds still_not-bound_in (p <=> q) = (still_not-bound_in p) \/ (still_not-bound_in q)
proof end;

theorem Th23: :: QC_LANG3:23
for x being bound_QC-variable
for p being QC-formula holds still_not-bound_in (Ex (x,p)) = (still_not-bound_in p) \ {x}
proof end;

theorem :: QC_LANG3:24
( VERUM is closed & FALSUM is closed ) by Th7, Th12, QC_LANG1:def 30;

theorem Th25: :: QC_LANG3:25
for p being QC-formula holds
( p is closed iff 'not' p is closed )
proof end;

theorem Th26: :: QC_LANG3:26
for p, q being QC-formula holds
( ( p is closed & q is closed ) iff p '&' q is closed )
proof end;

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

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

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

theorem Th30: :: QC_LANG3:30
for p, q being QC-formula holds
( ( p is closed & q is closed ) iff p => q is closed )
proof end;

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

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

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

definition
let k be Element of NAT ;
func x. k -> bound_QC-variable equals :: QC_LANG3:def 3
[4,k];
coherence
[4,k] is bound_QC-variable
proof end;
end;

:: deftheorem defines x. QC_LANG3:def 3 :
for k being Element of NAT holds x. k = [4,k];

theorem :: QC_LANG3:34
canceled;

theorem :: QC_LANG3:35
canceled;

theorem :: QC_LANG3:36
for x being bound_QC-variable ex i being Element of NAT st x. i = x
proof end;

definition
let k be Element of NAT ;
func a. k -> free_QC-variable equals :: QC_LANG3:def 4
[6,k];
coherence
[6,k] is free_QC-variable
proof end;
end;

:: deftheorem defines a. QC_LANG3:def 4 :
for k being Element of NAT holds a. k = [6,k];

theorem :: QC_LANG3:37
canceled;

theorem :: QC_LANG3:38
canceled;

theorem :: QC_LANG3:39
for a being free_QC-variable ex i being Element of NAT st a. i = a
proof end;

theorem :: QC_LANG3:40
for c being Element of fixed_QC-variables
for a being Element of free_QC-variables holds c <> a
proof end;

theorem :: QC_LANG3:41
for c being Element of fixed_QC-variables
for x being Element of bound_QC-variables holds c <> x
proof end;

theorem :: QC_LANG3:42
for a being Element of free_QC-variables
for x being Element of bound_QC-variables holds a <> x
proof end;

definition
let V be non empty Subset of QC-variables;
let p be Element of QC-WFF ;
func Vars (p,V) -> Subset of V means :Def5: :: QC_LANG3:def 5
 ex F being Function of QC-WFF,(bool V) st
( it = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of V holds
( ( p = VERUM 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,(bool V) st
( b1 = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of V holds
( ( p = VERUM 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,(bool V) st
( b1 = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of V holds
( ( p = VERUM 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,(bool V) st
( b2 = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of V holds
( ( p = VERUM 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 Def5 defines Vars QC_LANG3:def 5 :
for V being non empty Subset of QC-variables
for p being Element of QC-WFF
for b3 being Subset of V holds
( b3 = Vars (p,V) iff ex F being Function of QC-WFF,(bool V) st
( b3 = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of V holds
( ( p = VERUM 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
let V be non empty Subset of QC-variables; :: thesis: ( H6( VERUM ) = {} & ( for p being Element of QC-WFF st p is atomic holds
Vars (p,V) = variables_in ((the_arguments_of p),V) ) & ( for p being Element of QC-WFF st p is negative holds
Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF 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 st p is universal holds
Vars (p,V) = Vars ((the_scope_of p),V) ) )
deffunc H6( Element of QC-WFF ) -> Subset of V = Vars ($1,V);
deffunc H7( Element of QC-WFF ) -> Subset of V = variables_in ((the_arguments_of $1),V);
deffunc H8( Subset of V) -> Subset of V = $1;
deffunc H9( Subset of V, Subset of V) -> Element of bool V = $1 \/ $2;
deffunc H10( Element of QC-WFF , Subset of V) -> Subset of V = $2;
A1: for p being Element of QC-WFF
for X being Subset of V holds
( X = H6(p) iff ex F being Function of QC-WFF,(bool V) st
( X = F . p & ( for p being Element of QC-WFF
for d1, d2 being Subset of V holds
( ( p = VERUM implies F . p = {} V ) & ( p is atomic implies F . p = H7(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H8(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H9(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H10(p,d1) ) ) ) ) ) by Def5;
thus H6( VERUM ) = {} V from QC_LANG3:sch 3(A1)
.= {} ; :: thesis: ( ( for p being Element of QC-WFF st p is atomic holds
Vars (p,V) = variables_in ((the_arguments_of p),V) ) & ( for p being Element of QC-WFF st p is negative holds
Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF 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 st p is universal holds
Vars (p,V) = Vars ((the_scope_of p),V) ) )
thus for p being Element of QC-WFF st p is atomic holds
Vars (p,V) = variables_in ((the_arguments_of p),V) :: thesis: ( ( for p being Element of QC-WFF st p is negative holds
Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF 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 st p is universal holds
Vars (p,V) = Vars ((the_scope_of p),V) ) )
proof
let p be Element of QC-WFF ; :: 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 H6(p) = H7(p) from QC_LANG3:sch 4(A1, A2); :: thesis: verum
end;
thus for p being Element of QC-WFF st p is negative holds
Vars (p,V) = Vars ((the_argument_of p),V) :: thesis: ( ( for p being Element of QC-WFF 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 st p is universal holds
Vars (p,V) = Vars ((the_scope_of p),V) ) )
proof
let p be Element of QC-WFF ; :: 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 H6(p) = H8(H6( the_argument_of p)) from QC_LANG3:sch 5(A1, A3); :: thesis: verum
end;
thus for p being Element of QC-WFF 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 st p is universal holds
Vars (p,V) = Vars ((the_scope_of p),V)
proof
let p be Element of QC-WFF ; :: 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 = H6( the_left_argument_of p) & d2 = H6( the_right_argument_of p) holds
H6(p) = H9(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 st p is universal holds
Vars (p,V) = Vars ((the_scope_of p),V) :: thesis: verum
proof
let p be Element of QC-WFF ; :: 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 H6(p) = H10(p,H6( the_scope_of p)) from QC_LANG3:sch 7(A1, A5); :: thesis: verum
end;
end;

theorem :: QC_LANG3:43
canceled;

theorem :: QC_LANG3:44
canceled;

theorem :: QC_LANG3:45
canceled;

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

theorem Th47: :: QC_LANG3:47
for p being Element of QC-WFF
for V being non empty Subset of QC-variables 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 Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in V ) } )
proof end;

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

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

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

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

theorem :: QC_LANG3:52
for p being Element of QC-WFF
for V being non empty Subset of QC-variables 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 Th53: :: QC_LANG3:53
for p, q being Element of QC-WFF
for V being non empty Subset of QC-variables holds Vars ((p '&' q),V) = (Vars (p,V)) \/ (Vars (q,V))
proof end;

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

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

theorem Th56: :: QC_LANG3:56
for p being Element of QC-WFF
for V being non empty Subset of QC-variables 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:57
for p, q being Element of QC-WFF
for V being non empty Subset of QC-variables holds Vars ((p 'or' q),V) = (Vars (p,V)) \/ (Vars (q,V))
proof end;

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

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

theorem Th60: :: QC_LANG3:60
for p being Element of QC-WFF
for V being non empty Subset of QC-variables 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:61
for p, q being Element of QC-WFF
for V being non empty Subset of QC-variables holds Vars ((p <=> q),V) = (Vars (p,V)) \/ (Vars (q,V))
proof end;

theorem :: QC_LANG3:62
for p being Element of QC-WFF
for V being non empty Subset of QC-variables 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:63
for x being bound_QC-variable
for p being Element of QC-WFF
for V being non empty Subset of QC-variables holds Vars ((Ex (x,p)),V) = Vars (p,V)
proof end;

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

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

theorem :: QC_LANG3:64
canceled;

theorem :: QC_LANG3:65
Free VERUM = {} by Lm2;

theorem :: QC_LANG3:66
for k being Element of NAT
for P being QC-pred_symbol of k
for l being QC-variable_list of k holds Free (P ! l) = { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables ) } by Th48;

theorem :: QC_LANG3:67
for p being Element of QC-WFF holds Free ('not' p) = Free p by Th50;

theorem :: QC_LANG3:68
Free FALSUM = {} by Th51;

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

theorem :: QC_LANG3:70
for x being bound_QC-variable
for p being Element of QC-WFF holds Free (All (x,p)) = Free p by Th55;

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

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

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

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

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

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

theorem :: QC_LANG3:75
canceled;

theorem Th76: :: QC_LANG3:76
Fixed VERUM = {} by Lm2;

theorem :: QC_LANG3:77
for k being Element of NAT
for P being QC-pred_symbol of k
for l being QC-variable_list of k holds Fixed (P ! l) = { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in fixed_QC-variables ) } by Th48;

theorem :: QC_LANG3:78
for p being Element of QC-WFF holds Fixed ('not' p) = Fixed p by Th50;

theorem :: QC_LANG3:79
Fixed FALSUM = {} by Th50, Th76, QC_LANG2:def 1;

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

theorem :: QC_LANG3:81
for x being bound_QC-variable
for p being Element of QC-WFF holds Fixed (All (x,p)) = Fixed p by Th55;

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

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

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

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