:: A First Order Language
:: by Piotr Rudnicki and Andrzej Trybulec
::
:: Received August 8, 1989
:: Copyright (c) 1990-2011 Association of Mizar Users


begin

theorem :: QC_LANG1:1
for D1 being non empty set
for D2 being set
for k being Element of D1 holds [:{k},D2:] c= [:D1,D2:]
proof end;

theorem Th2: :: QC_LANG1:2
for D1 being non empty set
for D2 being set
for k1, k2, k3 being Element of D1 holds [:{k1,k2,k3},D2:] c= [:D1,D2:]
proof end;

definition
func QC-variables -> set equals :: QC_LANG1:def 1
[:{4,5,6},NAT:];
coherence
[:{4,5,6},NAT:] is set ;
end;

:: deftheorem defines QC-variables QC_LANG1:def 1 :
QC-variables = [:{4,5,6},NAT:];

registration
cluster QC-variables -> non empty ;
coherence
not QC-variables is empty ;
end;

theorem :: QC_LANG1:3
canceled;

theorem Th4: :: QC_LANG1:4
QC-variables c= [:NAT,NAT:] by Th2;

definition
mode QC-variable is Element of QC-variables ;
func bound_QC-variables -> Subset of QC-variables equals :: QC_LANG1:def 2
[:{4},NAT:];
coherence
[:{4},NAT:] is Subset of QC-variables
proof end;
func fixed_QC-variables -> Subset of QC-variables equals :: QC_LANG1:def 3
[:{5},NAT:];
coherence
[:{5},NAT:] is Subset of QC-variables
proof end;
func free_QC-variables -> Subset of QC-variables equals :: QC_LANG1:def 4
[:{6},NAT:];
coherence
[:{6},NAT:] is Subset of QC-variables
proof end;
func QC-pred_symbols -> set equals :: QC_LANG1:def 5
 { [k,l] where k, l is Element of NAT : 7 <= k } ;
coherence
{ [k,l] where k, l is Element of NAT : 7 <= k } is set ;
end;

:: deftheorem defines bound_QC-variables QC_LANG1:def 2 :
bound_QC-variables = [:{4},NAT:];

:: deftheorem defines fixed_QC-variables QC_LANG1:def 3 :
fixed_QC-variables = [:{5},NAT:];

:: deftheorem defines free_QC-variables QC_LANG1:def 4 :
free_QC-variables = [:{6},NAT:];

:: deftheorem defines QC-pred_symbols QC_LANG1:def 5 :
QC-pred_symbols = { [k,l] where k, l is Element of NAT : 7 <= k } ;

registration
cluster bound_QC-variables -> non empty ;
coherence
not bound_QC-variables is empty ;
cluster fixed_QC-variables -> non empty ;
coherence
not fixed_QC-variables is empty ;
cluster free_QC-variables -> non empty ;
coherence
not free_QC-variables is empty ;
cluster QC-pred_symbols -> non empty ;
coherence
not QC-pred_symbols is empty
proof end;
end;

theorem :: QC_LANG1:5
canceled;

theorem :: QC_LANG1:6
canceled;

theorem :: QC_LANG1:7
canceled;

theorem :: QC_LANG1:8
canceled;

theorem :: QC_LANG1:9
canceled;

theorem Th10: :: QC_LANG1:10
QC-pred_symbols c= [:NAT,NAT:]
proof end;

definition
mode QC-pred_symbol is Element of QC-pred_symbols ;
end;

definition
let P be Element of QC-pred_symbols ;
func the_arity_of P -> Element of NAT means :Def6: :: QC_LANG1:def 6
P `1 = 7 + it;
existence
ex b1 being Element of NAT st P `1 = 7 + b1
proof end;
uniqueness
for b1, b2 being Element of NAT st P `1 = 7 + b1 & P `1 = 7 + b2 holds
b1 = b2 ;
end;

:: deftheorem Def6 defines the_arity_of QC_LANG1:def 6 :
for P being Element of QC-pred_symbols
for b2 being Element of NAT holds
( b2 = the_arity_of P iff P `1 = 7 + b2 );

definition
let k be Element of NAT ;
func k -ary_QC-pred_symbols -> Subset of QC-pred_symbols equals :: QC_LANG1:def 7
 { P where P is QC-pred_symbol : the_arity_of P = k } ;
coherence
{ P where P is QC-pred_symbol : the_arity_of P = k } is Subset of QC-pred_symbols
proof end;
end;

:: deftheorem defines -ary_QC-pred_symbols QC_LANG1:def 7 :
for k being Element of NAT holds k -ary_QC-pred_symbols = { P where P is QC-pred_symbol : the_arity_of P = k } ;

registration
let k be Element of NAT ;
cluster k -ary_QC-pred_symbols -> non empty ;
coherence
not k -ary_QC-pred_symbols is empty
proof end;
end;

definition
mode bound_QC-variable is Element of bound_QC-variables ;
mode fixed_QC-variable is Element of fixed_QC-variables ;
mode free_QC-variable is Element of free_QC-variables ;
let k be Element of NAT ;
mode QC-pred_symbol of k is Element of k -ary_QC-pred_symbols ;
end;

registration
let k be Element of NAT ;
cluster Relation-like QC-variables -valued Function-like V31() k -element FinSequence-like FinSubsequence-like FinSequence of QC-variables ;
existence
ex b1 being FinSequence of QC-variables st b1 is k -element
proof end;
end;

definition
let k be Element of NAT ;
mode QC-variable_list of k is k -element FinSequence of QC-variables ;
end;

definition
let D be set ;
canceled;
attr D is QC-closed means :Def9: :: QC_LANG1:def 9
( D is Subset of ([:NAT,NAT:] *) & ( for k being Element of NAT
for p being QC-pred_symbol of k
for ll being QC-variable_list of k holds <*p*> ^ ll in D ) & <*[0,0]*> in D & ( for p being FinSequence of [:NAT,NAT:] st p in D holds
<*[1,0]*> ^ p in D ) & ( for p, q being FinSequence of [:NAT,NAT:] st p in D & q in D holds
(<*[2,0]*> ^ p) ^ q in D ) & ( for x being bound_QC-variable
for p being FinSequence of [:NAT,NAT:] st p in D holds
(<*[3,0]*> ^ <*x*>) ^ p in D ) );
end;

:: deftheorem QC_LANG1:def 8 :
canceled;

:: deftheorem Def9 defines QC-closed QC_LANG1:def 9 :
for D being set holds
( D is QC-closed iff ( D is Subset of ([:NAT,NAT:] *) & ( for k being Element of NAT
for p being QC-pred_symbol of k
for ll being QC-variable_list of k holds <*p*> ^ ll in D ) & <*[0,0]*> in D & ( for p being FinSequence of [:NAT,NAT:] st p in D holds
<*[1,0]*> ^ p in D ) & ( for p, q being FinSequence of [:NAT,NAT:] st p in D & q in D holds
(<*[2,0]*> ^ p) ^ q in D ) & ( for x being bound_QC-variable
for p being FinSequence of [:NAT,NAT:] st p in D holds
(<*[3,0]*> ^ <*x*>) ^ p in D ) ) );

Lm1: for k, l being Element of NAT holds <*[k,l]*> is FinSequence of [:NAT,NAT:]
proof end;

Lm2: for k being Element of NAT
for p being QC-pred_symbol of k
for ll being QC-variable_list of k holds <*p*> ^ ll is FinSequence of [:NAT,NAT:]
proof end;

Lm3: for x being bound_QC-variable
for p being FinSequence of [:NAT,NAT:] holds (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,NAT:]
proof end;

definition
func QC-WFF -> non empty set means :Def10: :: QC_LANG1:def 10
( it is QC-closed & ( for D being non empty set st D is QC-closed holds
it c= D ) );
existence
ex b1 being non empty set st
( b1 is QC-closed & ( for D being non empty set st D is QC-closed holds
b1 c= D ) )
proof end;
uniqueness
for b1, b2 being non empty set st b1 is QC-closed & ( for D being non empty set st D is QC-closed holds
b1 c= D ) & b2 is QC-closed & ( for D being non empty set st D is QC-closed holds
b2 c= D ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines QC-WFF QC_LANG1:def 10 :
for b1 being non empty set holds
( b1 = QC-WFF iff ( b1 is QC-closed & ( for D being non empty set st D is QC-closed holds
b1 c= D ) ) );

theorem :: QC_LANG1:11
canceled;

theorem :: QC_LANG1:12
canceled;

theorem :: QC_LANG1:13
canceled;

theorem :: QC_LANG1:14
canceled;

theorem :: QC_LANG1:15
canceled;

theorem :: QC_LANG1:16
canceled;

theorem :: QC_LANG1:17
canceled;

theorem :: QC_LANG1:18
canceled;

theorem :: QC_LANG1:19
canceled;

theorem :: QC_LANG1:20
canceled;

theorem Th21: :: QC_LANG1:21
QC-WFF is QC-closed by Def10;

definition
mode QC-formula is Element of QC-WFF ;
end;

definition
let P be QC-pred_symbol;
let l be FinSequence of QC-variables ;
assume A1: the_arity_of P = len l ;
func P ! l -> Element of QC-WFF equals :Def11: :: QC_LANG1:def 11
<*P*> ^ l;
coherence
<*P*> ^ l is Element of QC-WFF
proof end;
end;

:: deftheorem Def11 defines ! QC_LANG1:def 11 :
for P being QC-pred_symbol
for l being FinSequence of QC-variables st the_arity_of P = len l holds
P ! l = <*P*> ^ l;

theorem :: QC_LANG1:22
canceled;

theorem Th23: :: QC_LANG1:23
for k being Element of NAT
for p being QC-pred_symbol of k
for ll being QC-variable_list of k holds p ! ll = <*p*> ^ ll
proof end;

definition
let p be Element of QC-WFF ;
func @ p -> FinSequence of [:NAT,NAT:] equals :: QC_LANG1:def 12
p;
coherence
p is FinSequence of [:NAT,NAT:]
proof end;
end;

:: deftheorem defines @ QC_LANG1:def 12 :
for p being Element of QC-WFF holds @ p = p;

definition
func VERUM -> QC-formula equals :: QC_LANG1:def 13
<*[0,0]*>;
correctness
coherence
<*[0,0]*> is QC-formula;
by Def9, Th21;
let p be Element of QC-WFF ;
func 'not' p -> QC-formula equals :: QC_LANG1:def 14
<*[1,0]*> ^ (@ p);
coherence
<*[1,0]*> ^ (@ p) is QC-formula by Def9, Th21;
correctness
;
let q be Element of QC-WFF ;
func p '&' q -> QC-formula equals :: QC_LANG1:def 15
(<*[2,0]*> ^ (@ p)) ^ (@ q);
correctness
coherence
(<*[2,0]*> ^ (@ p)) ^ (@ q) is QC-formula;
by Def9, Th21;
end;

:: deftheorem defines VERUM QC_LANG1:def 13 :
VERUM = <*[0,0]*>;

:: deftheorem defines 'not' QC_LANG1:def 14 :
for p being Element of QC-WFF holds 'not' p = <*[1,0]*> ^ (@ p);

:: deftheorem defines '&' QC_LANG1:def 15 :
for p, q being Element of QC-WFF holds p '&' q = (<*[2,0]*> ^ (@ p)) ^ (@ q);

definition
let x be bound_QC-variable;
let p be Element of QC-WFF ;
func All (x,p) -> QC-formula equals :: QC_LANG1:def 16
(<*[3,0]*> ^ <*x*>) ^ (@ p);
coherence
(<*[3,0]*> ^ <*x*>) ^ (@ p) is QC-formula by Def9, Th21;
end;

:: deftheorem defines All QC_LANG1:def 16 :
for x being bound_QC-variable
for p being Element of QC-WFF holds All (x,p) = (<*[3,0]*> ^ <*x*>) ^ (@ p);

scheme :: QC_LANG1:sch 1
QCInd{ P1[ Element of QC-WFF ] } :
for F being Element of QC-WFF holds P1[F]
provided
A1: for k being Element of NAT
for P being QC-pred_symbol of k
for ll being QC-variable_list of k holds P1[P ! ll] and
A2: P1[ VERUM ] and
A3: for p being Element of QC-WFF st P1[p] holds
P1[ 'not' p] and
A4: for p, q being Element of QC-WFF st P1[p] & P1[q] holds
P1[p '&' q] and
A5: for x being bound_QC-variable
for p being Element of QC-WFF st P1[p] holds
P1[ All (x,p)]
proof end;

definition
let F be Element of QC-WFF ;
attr F is atomic means :Def17: :: QC_LANG1:def 17
 ex k being Element of NAT ex p being QC-pred_symbol of k ex ll being QC-variable_list of k st F = p ! ll;
attr F is negative means :Def18: :: QC_LANG1:def 18
 ex p being Element of QC-WFF st F = 'not' p;
attr F is conjunctive means :Def19: :: QC_LANG1:def 19
 ex p, q being Element of QC-WFF st F = p '&' q;
attr F is universal means :Def20: :: QC_LANG1:def 20
 ex x being bound_QC-variable ex p being Element of QC-WFF st F = All (x,p);
end;

:: deftheorem Def17 defines atomic QC_LANG1:def 17 :
for F being Element of QC-WFF holds
( F is atomic iff ex k being Element of NAT ex p being QC-pred_symbol of k ex ll being QC-variable_list of k st F = p ! ll );

:: deftheorem Def18 defines negative QC_LANG1:def 18 :
for F being Element of QC-WFF holds
( F is negative iff ex p being Element of QC-WFF st F = 'not' p );

:: deftheorem Def19 defines conjunctive QC_LANG1:def 19 :
for F being Element of QC-WFF holds
( F is conjunctive iff ex p, q being Element of QC-WFF st F = p '&' q );

:: deftheorem Def20 defines universal QC_LANG1:def 20 :
for F being Element of QC-WFF holds
( F is universal iff ex x being bound_QC-variable ex p being Element of QC-WFF st F = All (x,p) );

theorem :: QC_LANG1:24
canceled;

theorem :: QC_LANG1:25
canceled;

theorem :: QC_LANG1:26
canceled;

theorem :: QC_LANG1:27
canceled;

theorem :: QC_LANG1:28
canceled;

theorem :: QC_LANG1:29
canceled;

theorem :: QC_LANG1:30
canceled;

theorem :: QC_LANG1:31
canceled;

theorem :: QC_LANG1:32
canceled;

theorem Th33: :: QC_LANG1:33
for F being Element of QC-WFF holds
( F = VERUM or F is atomic or F is negative or F is conjunctive or F is universal )
proof end;

theorem Th34: :: QC_LANG1:34
for F being Element of QC-WFF holds 1 <= len (@ F)
proof end;

theorem Th35: :: QC_LANG1:35
for k being Element of NAT
for P being QC-pred_symbol of k holds the_arity_of P = k
proof end;

theorem Th36: :: QC_LANG1:36
for F being Element of QC-WFF holds
( ( ((@ F) . 1) `1 = 0 implies F = VERUM ) & ( ((@ F) . 1) `1 = 1 implies F is negative ) & ( ((@ F) . 1) `1 = 2 implies F is conjunctive ) & ( ((@ F) . 1) `1 = 3 implies F is universal ) & ( ex k being Element of NAT st (@ F) . 1 is QC-pred_symbol of k implies F is atomic ) )
proof end;

theorem Th37: :: QC_LANG1:37
for F, G being Element of QC-WFF
for s being FinSequence st @ F = (@ G) ^ s holds
@ F = @ G
proof end;

definition
let F be Element of QC-WFF ;
assume A1: F is atomic ;
func the_pred_symbol_of F -> QC-pred_symbol means :Def21: :: QC_LANG1:def 21
 ex k being Element of NAT ex ll being QC-variable_list of k ex P being QC-pred_symbol of k st
( it = P & F = P ! ll );
existence
ex b1 being QC-pred_symbol ex k being Element of NAT ex ll being QC-variable_list of k ex P being QC-pred_symbol of k st
( b1 = P & F = P ! ll )
proof end;
uniqueness
for b1, b2 being QC-pred_symbol st ex k being Element of NAT ex ll being QC-variable_list of k ex P being QC-pred_symbol of k st
( b1 = P & F = P ! ll ) & ex k being Element of NAT ex ll being QC-variable_list of k ex P being QC-pred_symbol of k st
( b2 = P & F = P ! ll ) holds
b1 = b2
proof end;
end;

:: deftheorem Def21 defines the_pred_symbol_of QC_LANG1:def 21 :
for F being Element of QC-WFF st F is atomic holds
for b2 being QC-pred_symbol holds
( b2 = the_pred_symbol_of F iff ex k being Element of NAT ex ll being QC-variable_list of k ex P being QC-pred_symbol of k st
( b2 = P & F = P ! ll ) );

definition
let F be Element of QC-WFF ;
assume A1: F is atomic ;
func the_arguments_of F -> FinSequence of QC-variables means :Def22: :: QC_LANG1:def 22
 ex k being Element of NAT ex P being QC-pred_symbol of k ex ll being QC-variable_list of k st
( it = ll & F = P ! ll );
existence
ex b1 being FinSequence of QC-variables ex k being Element of NAT ex P being QC-pred_symbol of k ex ll being QC-variable_list of k st
( b1 = ll & F = P ! ll )
proof end;
uniqueness
for b1, b2 being FinSequence of QC-variables st ex k being Element of NAT ex P being QC-pred_symbol of k ex ll being QC-variable_list of k st
( b1 = ll & F = P ! ll ) & ex k being Element of NAT ex P being QC-pred_symbol of k ex ll being QC-variable_list of k st
( b2 = ll & F = P ! ll ) holds
b1 = b2
proof end;
end;

:: deftheorem Def22 defines the_arguments_of QC_LANG1:def 22 :
for F being Element of QC-WFF st F is atomic holds
for b2 being FinSequence of QC-variables holds
( b2 = the_arguments_of F iff ex k being Element of NAT ex P being QC-pred_symbol of k ex ll being QC-variable_list of k st
( b2 = ll & F = P ! ll ) );

definition
let F be Element of QC-WFF ;
assume A1: F is negative ;
func the_argument_of F -> QC-formula means :Def23: :: QC_LANG1:def 23
F = 'not' it;
existence
ex b1 being QC-formula st F = 'not' b1 by A1, Def18;
uniqueness
for b1, b2 being QC-formula st F = 'not' b1 & F = 'not' b2 holds
b1 = b2 by FINSEQ_1:46;
end;

:: deftheorem Def23 defines the_argument_of QC_LANG1:def 23 :
for F being Element of QC-WFF st F is negative holds
for b2 being QC-formula holds
( b2 = the_argument_of F iff F = 'not' b2 );

definition
let F be Element of QC-WFF ;
assume A1: F is conjunctive ;
func the_left_argument_of F -> QC-formula means :Def24: :: QC_LANG1:def 24
 ex q being Element of QC-WFF st F = it '&' q;
existence
ex b1 being QC-formula ex q being Element of QC-WFF st F = b1 '&' q by A1, Def19;
uniqueness
for b1, b2 being QC-formula st ex q being Element of QC-WFF st F = b1 '&' q & ex q being Element of QC-WFF st F = b2 '&' q holds
b1 = b2
proof end;
end;

:: deftheorem Def24 defines the_left_argument_of QC_LANG1:def 24 :
for F being Element of QC-WFF st F is conjunctive holds
for b2 being QC-formula holds
( b2 = the_left_argument_of F iff ex q being Element of QC-WFF st F = b2 '&' q );

definition
let F be Element of QC-WFF ;
assume A1: F is conjunctive ;
func the_right_argument_of F -> QC-formula means :Def25: :: QC_LANG1:def 25
 ex p being Element of QC-WFF st F = p '&' it;
existence
ex b1 being QC-formula ex p being Element of QC-WFF st F = p '&' b1
proof end;
uniqueness
for b1, b2 being QC-formula st ex p being Element of QC-WFF st F = p '&' b1 & ex p being Element of QC-WFF st F = p '&' b2 holds
b1 = b2
proof end;
end;

:: deftheorem Def25 defines the_right_argument_of QC_LANG1:def 25 :
for F being Element of QC-WFF st F is conjunctive holds
for b2 being QC-formula holds
( b2 = the_right_argument_of F iff ex p being Element of QC-WFF st F = p '&' b2 );

definition
let F be Element of QC-WFF ;
assume A1: F is universal ;
func bound_in F -> bound_QC-variable means :Def26: :: QC_LANG1:def 26
 ex p being Element of QC-WFF st F = All (it,p);
existence
ex b1 being bound_QC-variable ex p being Element of QC-WFF st F = All (b1,p) by A1, Def20;
uniqueness
for b1, b2 being bound_QC-variable st ex p being Element of QC-WFF st F = All (b1,p) & ex p being Element of QC-WFF st F = All (b2,p) holds
b1 = b2
proof end;
func the_scope_of F -> QC-formula means :Def27: :: QC_LANG1:def 27
 ex x being bound_QC-variable st F = All (x,it);
existence
ex b1 being QC-formula ex x being bound_QC-variable st F = All (x,b1)
proof end;
uniqueness
for b1, b2 being QC-formula st ex x being bound_QC-variable st F = All (x,b1) & ex x being bound_QC-variable st F = All (x,b2) holds
b1 = b2
proof end;
end;

:: deftheorem Def26 defines bound_in QC_LANG1:def 26 :
for F being Element of QC-WFF st F is universal holds
for b2 being bound_QC-variable holds
( b2 = bound_in F iff ex p being Element of QC-WFF st F = All (b2,p) );

:: deftheorem Def27 defines the_scope_of QC_LANG1:def 27 :
for F being Element of QC-WFF st F is universal holds
for b2 being QC-formula holds
( b2 = the_scope_of F iff ex x being bound_QC-variable st F = All (x,b2) );

theorem :: QC_LANG1:38
canceled;

theorem :: QC_LANG1:39
canceled;

theorem :: QC_LANG1:40
canceled;

theorem :: QC_LANG1:41
canceled;

theorem :: QC_LANG1:42
canceled;

theorem :: QC_LANG1:43
canceled;

theorem :: QC_LANG1:44
canceled;

theorem Th45: :: QC_LANG1:45
for p being Element of QC-WFF st p is negative holds
len (@ (the_argument_of p)) < len (@ p)
proof end;

theorem Th46: :: QC_LANG1:46
for p being Element of QC-WFF st p is conjunctive holds
( len (@ (the_left_argument_of p)) < len (@ p) & len (@ (the_right_argument_of p)) < len (@ p) )
proof end;

theorem Th47: :: QC_LANG1:47
for p being Element of QC-WFF st p is universal holds
len (@ (the_scope_of p)) < len (@ p)
proof end;

scheme :: QC_LANG1:sch 2
QCInd2{ P1[ Element of QC-WFF ] } :
for p being Element of QC-WFF holds P1[p]
provided
A1: for p being Element of QC-WFF holds
( ( p is atomic implies P1[p] ) & P1[ VERUM ] & ( p is negative & P1[ the_argument_of p] implies P1[p] ) & ( p is conjunctive & P1[ the_left_argument_of p] & P1[ the_right_argument_of p] implies P1[p] ) & ( p is universal & P1[ the_scope_of p] implies P1[p] ) )
proof end;

theorem Th48: :: QC_LANG1:48
for k being Element of NAT
for P being QC-pred_symbol of k holds
( P `1 <> 0 & P `1 <> 1 & P `1 <> 2 & P `1 <> 3 )
proof end;

theorem Th49: :: QC_LANG1:49
for F being Element of QC-WFF holds
( ((@ VERUM) . 1) `1 = 0 & ( F is atomic implies ex k being Element of NAT st (@ F) . 1 is QC-pred_symbol of k ) & ( F is negative implies ((@ F) . 1) `1 = 1 ) & ( F is conjunctive implies ((@ F) . 1) `1 = 2 ) & ( F is universal implies ((@ F) . 1) `1 = 3 ) )
proof end;

theorem Th50: :: QC_LANG1:50
for F being Element of QC-WFF st F is atomic holds
( ((@ F) . 1) `1 <> 0 & ((@ F) . 1) `1 <> 1 & ((@ F) . 1) `1 <> 2 & ((@ F) . 1) `1 <> 3 )
proof end;

theorem Th51: :: QC_LANG1:51
( not VERUM is atomic & not VERUM is negative & not VERUM is conjunctive & not VERUM is universal & ( for p being Element of QC-WFF holds
( not ( p is atomic & p is negative ) & not ( p is atomic & p is conjunctive ) & not ( p is atomic & p is universal ) & not ( p is negative & p is conjunctive ) & not ( p is negative & p is universal ) & not ( p is conjunctive & p is universal ) ) ) )
proof end;

scheme :: QC_LANG1:sch 3
QCFuncEx{ 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() } :
ex F being Function of QC-WFF,F1() st
( F . VERUM = F2() & ( for p being Element of QC-WFF holds
( ( p is atomic implies F . p = F3(p) ) & ( p is negative implies F . p = F4((F . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F5((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = F6(p,(F . (the_scope_of p))) ) ) ) )
proof end;

definition
let ll be FinSequence of QC-variables ;
func still_not-bound_in ll -> Subset of bound_QC-variables equals :: QC_LANG1:def 28
 { (ll . k) where k is Element of NAT : ( 1 <= k & k <= len ll & ll . k in bound_QC-variables ) } ;
coherence
{ (ll . k) where k is Element of NAT : ( 1 <= k & k <= len ll & ll . k in bound_QC-variables ) } is Subset of bound_QC-variables
proof end;
end;

:: deftheorem defines still_not-bound_in QC_LANG1:def 28 :
for ll being FinSequence of QC-variables holds still_not-bound_in ll = { (ll . k) where k is Element of NAT : ( 1 <= k & k <= len ll & ll . k in bound_QC-variables ) } ;

definition
let p be QC-formula;
func still_not-bound_in p -> Subset of bound_QC-variables means :: QC_LANG1:def 29
 ex F being Function of QC-WFF,(bool bound_QC-variables) st
( it = F . p & ( for p being Element of QC-WFF holds
( F . VERUM = {} & ( p is atomic implies F . p = { ((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 bound_QC-variables ) } ) & ( 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)} ) ) ) );
existence
ex b1 being Subset of bound_QC-variables ex F being Function of QC-WFF,(bool bound_QC-variables) st
( b1 = F . p & ( for p being Element of QC-WFF holds
( F . VERUM = {} & ( p is atomic implies F . p = { ((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 bound_QC-variables ) } ) & ( 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 end;
uniqueness
for b1, b2 being Subset of bound_QC-variables st ex F being Function of QC-WFF,(bool bound_QC-variables) st
( b1 = F . p & ( for p being Element of QC-WFF holds
( F . VERUM = {} & ( p is atomic implies F . p = { ((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 bound_QC-variables ) } ) & ( 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)} ) ) ) ) & ex F being Function of QC-WFF,(bool bound_QC-variables) st
( b2 = F . p & ( for p being Element of QC-WFF holds
( F . VERUM = {} & ( p is atomic implies F . p = { ((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 bound_QC-variables ) } ) & ( 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)} ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines still_not-bound_in QC_LANG1:def 29 :
for p being QC-formula
for b2 being Subset of bound_QC-variables holds
( b2 = still_not-bound_in p iff ex F being Function of QC-WFF,(bool bound_QC-variables) st
( b2 = F . p & ( for p being Element of QC-WFF holds
( F . VERUM = {} & ( p is atomic implies F . p = { ((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 bound_QC-variables ) } ) & ( 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)} ) ) ) ) );

definition
let p be QC-formula;
attr p is closed means :: QC_LANG1:def 30
 still_not-bound_in p = {} ;
end;

:: deftheorem defines closed QC_LANG1:def 30 :
for p being QC-formula holds
( p is closed iff still_not-bound_in p = {} );