:: QC_LANG1 semantic presentation

theorem Th1: :: QC_LANG1:1
for b1 being non empty set
for b2 being set
for b3 being Element of b1 holds [:{b3},b2:] c= [:b1,b2:]
proof end;

theorem Th2: :: QC_LANG1:2
for b1 being non empty set
for b2 being set
for b3, b4, b5 being Element of b1 holds [:{b3,b4,b5},b2:] c= [:b1,b2:]
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 Def1 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
proof end;
end;

theorem Th3: :: 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
{ [b1,b2] where B is Nat, B is Nat : 7 <= b1 } ;
coherence
{ [b1,b2] where B is Nat, B is Nat : 7 <= b1 } is set ;
end;

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

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

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

:: deftheorem Def5 defines QC-pred_symbols QC_LANG1:def 5 :
QC-pred_symbols = { [b1,b2] where B is Nat, B is Nat : 7 <= b1 } ;

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 Th5: :: QC_LANG1:5
canceled;

theorem Th6: :: QC_LANG1:6
canceled;

theorem Th7: :: QC_LANG1:7
canceled;

theorem Th8: :: QC_LANG1:8
canceled;

theorem Th9: :: 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 c1 be Element of QC-pred_symbols ;
func the_arity_of c1 -> Nat means :Def6: :: QC_LANG1:def 6
a1 `1 = 7 + a2;
existence
ex b1 being Nat st c1 `1 = 7 + b1
proof end;
uniqueness
for b1, b2 being Nat st c1 `1 = 7 + b1 & c1 `1 = 7 + b2 holds
b1 = b2 by XCMPLX_1:2;
end;

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

definition
let c1 be Nat;
func c1 -ary_QC-pred_symbols -> Subset of QC-pred_symbols equals :: QC_LANG1:def 7
{ b1 where B is QC-pred_symbol : the_arity_of b1 = a1 } ;
coherence
{ b1 where B is QC-pred_symbol : the_arity_of b1 = c1 } is Subset of QC-pred_symbols
proof end;
end;

:: deftheorem Def7 defines -ary_QC-pred_symbols QC_LANG1:def 7 :
for b1 being Nat holds b1 -ary_QC-pred_symbols = { b2 where B is QC-pred_symbol : the_arity_of b2 = b1 } ;

registration
let c1 be Nat;
cluster a1 -ary_QC-pred_symbols -> non empty ;
coherence
not c1 -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 c1 be Nat;
mode QC-pred_symbol of a1 is Element of a1 -ary_QC-pred_symbols ;
end;

definition
let c1 be Nat;
mode QC-variable_list of c1 -> FinSequence of QC-variables means :Def8: :: QC_LANG1:def 8
 len a2 = a1;
existence
ex b1 being FinSequence of QC-variables st len b1 = c1 by FINSEQ_1:24;
end;

:: deftheorem Def8 defines QC-variable_list QC_LANG1:def 8 :
for b1 being Nat
for b2 being FinSequence of QC-variables holds
( b2 is QC-variable_list of b1 iff len b2 = b1 );

definition
let c1 be set ;
attr a1 is QC-closed means :Def9: :: QC_LANG1:def 9
( a1 is Subset of ([:NAT ,NAT :] * ) & ( for b1 being Nat
for b2 being QC-pred_symbol of b1
for b3 being QC-variable_list of b1 holds <*b2*> ^ b3 in a1 ) & <*[0,0]*> in a1 & ( for b1 being FinSequence of [:NAT ,NAT :] st b1 in a1 holds
<*[1,0]*> ^ b1 in a1 ) & ( for b1, b2 being FinSequence of [:NAT ,NAT :] st b1 in a1 & b2 in a1 holds
(<*[2,0]*> ^ b1) ^ b2 in a1 ) & ( for b1 being bound_QC-variable
for b2 being FinSequence of [:NAT ,NAT :] st b2 in a1 holds
(<*[3,0]*> ^ <*b1*>) ^ b2 in a1 ) );
end;

:: deftheorem Def9 defines QC-closed QC_LANG1:def 9 :
for b1 being set holds
( b1 is QC-closed iff ( b1 is Subset of ([:NAT ,NAT :] * ) & ( for b2 being Nat
for b3 being QC-pred_symbol of b2
for b4 being QC-variable_list of b2 holds <*b3*> ^ b4 in b1 ) & <*[0,0]*> in b1 & ( for b2 being FinSequence of [:NAT ,NAT :] st b2 in b1 holds
<*[1,0]*> ^ b2 in b1 ) & ( for b2, b3 being FinSequence of [:NAT ,NAT :] st b2 in b1 & b3 in b1 holds
(<*[2,0]*> ^ b2) ^ b3 in b1 ) & ( for b2 being bound_QC-variable
for b3 being FinSequence of [:NAT ,NAT :] st b3 in b1 holds
(<*[3,0]*> ^ <*b2*>) ^ b3 in b1 ) ) );

Lemma7: for b1, b2 being Nat holds <*[b1,b2]*> is FinSequence of [:NAT ,NAT :]
proof end;

Lemma8: for b1 being Nat
for b2 being QC-pred_symbol of b1
for b3 being QC-variable_list of b1 holds <*b2*> ^ b3 is FinSequence of [:NAT ,NAT :]
proof end;

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

definition
func QC-WFF -> non empty set means :Def10: :: QC_LANG1:def 10
( a1 is QC-closed & ( for b1 being non empty set st b1 is QC-closed holds
a1 c= b1 ) );
existence
ex b1 being non empty set st
( b1 is QC-closed & ( for b2 being non empty set st b2 is QC-closed holds
b1 c= b2 ) )
proof end;
uniqueness
for b1, b2 being non empty set st b1 is QC-closed & ( for b3 being non empty set st b3 is QC-closed holds
b1 c= b3 ) & b2 is QC-closed & ( for b3 being non empty set st b3 is QC-closed holds
b2 c= b3 ) 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 b2 being non empty set st b2 is QC-closed holds
b1 c= b2 ) ) );

theorem Th11: :: QC_LANG1:11
canceled;

theorem Th12: :: QC_LANG1:12
canceled;

theorem Th13: :: QC_LANG1:13
canceled;

theorem Th14: :: QC_LANG1:14
canceled;

theorem Th15: :: QC_LANG1:15
canceled;

theorem Th16: :: QC_LANG1:16
canceled;

theorem Th17: :: QC_LANG1:17
canceled;

theorem Th18: :: QC_LANG1:18
canceled;

theorem Th19: :: QC_LANG1:19
canceled;

theorem Th20: :: 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 c1 be QC-pred_symbol;
let c2 be FinSequence of QC-variables ;
assume E12: the_arity_of c1 = len c2 ;
func c1 ! c2 -> Element of QC-WFF equals :Def11: :: QC_LANG1:def 11
<*a1*> ^ a2;
coherence
<*c1*> ^ c2 is Element of QC-WFF
proof end;
end;

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

theorem Th22: :: QC_LANG1:22
canceled;

theorem Th23: :: QC_LANG1:23
for b1 being Nat
for b2 being QC-pred_symbol of b1
for b3 being QC-variable_list of b1 holds b2 ! b3 = <*b2*> ^ b3
proof end;

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

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

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

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

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

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

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

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

scheme :: QC_LANG1:sch 1
s1{ P1[ Element of QC-WFF ] } :
for b1 being Element of QC-WFF holds P1[b1]
provided
E14: for b1 being Nat
for b2 being QC-pred_symbol of b1
for b3 being QC-variable_list of b1 holds P1[b2 ! b3] and
E15: P1[ VERUM ] and
E16: for b1 being Element of QC-WFF st P1[b1] holds
P1[ 'not' b1] and
E17: for b1, b2 being Element of QC-WFF st P1[b1] & P1[b2] holds
P1[b1 '&' b2] and
E18: for b1 being bound_QC-variable
for b2 being Element of QC-WFF st P1[b2] holds
P1[ All b1,b2]
proof end;

definition
let c1 be Element of QC-WFF ;
attr a1 is atomic means :Def17: :: QC_LANG1:def 17
ex b1 being Natex b2 being QC-pred_symbol of b1ex b3 being QC-variable_list of b1 st a1 = b2 ! b3;
attr a1 is negative means :Def18: :: QC_LANG1:def 18
ex b1 being Element of QC-WFF st a1 = 'not' b1;
attr a1 is conjunctive means :Def19: :: QC_LANG1:def 19
ex b1, b2 being Element of QC-WFF st a1 = b1 '&' b2;
attr a1 is universal means :Def20: :: QC_LANG1:def 20
ex b1 being bound_QC-variableex b2 being Element of QC-WFF st a1 = All b1,b2;
end;

:: deftheorem Def17 defines atomic QC_LANG1:def 17 :
for b1 being Element of QC-WFF holds
( b1 is atomic iff ex b2 being Natex b3 being QC-pred_symbol of b2ex b4 being QC-variable_list of b2 st b1 = b3 ! b4 );

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

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

:: deftheorem Def20 defines universal QC_LANG1:def 20 :
for b1 being Element of QC-WFF holds
( b1 is universal iff ex b2 being bound_QC-variableex b3 being Element of QC-WFF st b1 = All b2,b3 );

theorem Th24: :: QC_LANG1:24
canceled;

theorem Th25: :: QC_LANG1:25
canceled;

theorem Th26: :: QC_LANG1:26
canceled;

theorem Th27: :: QC_LANG1:27
canceled;

theorem Th28: :: QC_LANG1:28
canceled;

theorem Th29: :: QC_LANG1:29
canceled;

theorem Th30: :: QC_LANG1:30
canceled;

theorem Th31: :: QC_LANG1:31
canceled;

theorem Th32: :: QC_LANG1:32
canceled;

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

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

theorem Th35: :: QC_LANG1:35
for b1 being Nat
for b2 being QC-pred_symbol of b1 holds the_arity_of b2 = b1
proof end;

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

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

definition
let c1 be Element of QC-WFF ;
assume E23: c1 is atomic ;
func the_pred_symbol_of c1 -> QC-pred_symbol means :Def21: :: QC_LANG1:def 21
ex b1 being Natex b2 being QC-variable_list of b1ex b3 being QC-pred_symbol of b1 st
( a2 = b3 & a1 = b3 ! b2 );
existence
ex b1 being QC-pred_symbolex b2 being Natex b3 being QC-variable_list of b2ex b4 being QC-pred_symbol of b2 st
( b1 = b4 & c1 = b4 ! b3 )
proof end;
uniqueness
for b1, b2 being QC-pred_symbol st ex b3 being Natex b4 being QC-variable_list of b3ex b5 being QC-pred_symbol of b3 st
( b1 = b5 & c1 = b5 ! b4 ) & ex b3 being Natex b4 being QC-variable_list of b3ex b5 being QC-pred_symbol of b3 st
( b2 = b5 & c1 = b5 ! b4 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def21 defines the_pred_symbol_of QC_LANG1:def 21 :
for b1 being Element of QC-WFF st b1 is atomic holds
for b2 being QC-pred_symbol holds
( b2 = the_pred_symbol_of b1 iff ex b3 being Natex b4 being QC-variable_list of b3ex b5 being QC-pred_symbol of b3 st
( b2 = b5 & b1 = b5 ! b4 ) );

definition
let c1 be Element of QC-WFF ;
assume E24: c1 is atomic ;
func the_arguments_of c1 -> FinSequence of QC-variables means :Def22: :: QC_LANG1:def 22
ex b1 being Natex b2 being QC-pred_symbol of b1ex b3 being QC-variable_list of b1 st
( a2 = b3 & a1 = b2 ! b3 );
existence
ex b1 being FinSequence of QC-variables ex b2 being Natex b3 being QC-pred_symbol of b2ex b4 being QC-variable_list of b2 st
( b1 = b4 & c1 = b3 ! b4 )
proof end;
uniqueness
for b1, b2 being FinSequence of QC-variables st ex b3 being Natex b4 being QC-pred_symbol of b3ex b5 being QC-variable_list of b3 st
( b1 = b5 & c1 = b4 ! b5 ) & ex b3 being Natex b4 being QC-pred_symbol of b3ex b5 being QC-variable_list of b3 st
( b2 = b5 & c1 = b4 ! b5 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def22 defines the_arguments_of QC_LANG1:def 22 :
for b1 being Element of QC-WFF st b1 is atomic holds
for b2 being FinSequence of QC-variables holds
( b2 = the_arguments_of b1 iff ex b3 being Natex b4 being QC-pred_symbol of b3ex b5 being QC-variable_list of b3 st
( b2 = b5 & b1 = b4 ! b5 ) );

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

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

definition
let c1 be Element of QC-WFF ;
assume E26: c1 is conjunctive ;
func the_left_argument_of c1 -> QC-formula means :Def24: :: QC_LANG1:def 24
ex b1 being Element of QC-WFF st a1 = a2 '&' b1;
existence
ex b1 being QC-formulaex b2 being Element of QC-WFF st c1 = b1 '&' b2 by E26, Def19;
uniqueness
for b1, b2 being QC-formula st ex b3 being Element of QC-WFF st c1 = b1 '&' b3 & ex b3 being Element of QC-WFF st c1 = b2 '&' b3 holds
b1 = b2
proof end;
end;

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

definition
let c1 be Element of QC-WFF ;
assume E27: c1 is conjunctive ;
func the_right_argument_of c1 -> QC-formula means :Def25: :: QC_LANG1:def 25
ex b1 being Element of QC-WFF st a1 = b1 '&' a2;
existence
ex b1 being QC-formulaex b2 being Element of QC-WFF st c1 = b2 '&' b1
proof end;
uniqueness
for b1, b2 being QC-formula st ex b3 being Element of QC-WFF st c1 = b3 '&' b1 & ex b3 being Element of QC-WFF st c1 = b3 '&' b2 holds
b1 = b2
proof end;
end;

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

definition
let c1 be Element of QC-WFF ;
assume E28: c1 is universal ;
func bound_in c1 -> bound_QC-variable means :Def26: :: QC_LANG1:def 26
ex b1 being Element of QC-WFF st a1 = All a2,b1;
existence
ex b1 being bound_QC-variableex b2 being Element of QC-WFF st c1 = All b1,b2 by E28, Def20;
uniqueness
for b1, b2 being bound_QC-variable st ex b3 being Element of QC-WFF st c1 = All b1,b3 & ex b3 being Element of QC-WFF st c1 = All b2,b3 holds
b1 = b2
proof end;
func the_scope_of c1 -> QC-formula means :Def27: :: QC_LANG1:def 27
ex b1 being bound_QC-variable st a1 = All b1,a2;
existence
ex b1 being QC-formulaex b2 being bound_QC-variable st c1 = All b2,b1
proof end;
uniqueness
for b1, b2 being QC-formula st ex b3 being bound_QC-variable st c1 = All b3,b1 & ex b3 being bound_QC-variable st c1 = All b3,b2 holds
b1 = b2
proof end;
end;

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

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

theorem Th38: :: QC_LANG1:38
canceled;

theorem Th39: :: QC_LANG1:39
canceled;

theorem Th40: :: QC_LANG1:40
canceled;

theorem Th41: :: QC_LANG1:41
canceled;

theorem Th42: :: QC_LANG1:42
canceled;

theorem Th43: :: QC_LANG1:43
canceled;

theorem Th44: :: QC_LANG1:44
canceled;

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

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

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

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

theorem Th48: :: QC_LANG1:48
for b1 being Nat
for b2 being QC-pred_symbol of b1 holds
( b2 `1 <> 0 & b2 `1 <> 1 & b2 `1 <> 2 & b2 `1 <> 3 )
proof end;

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

theorem Th50: :: QC_LANG1:50
for b1 being Element of QC-WFF st b1 is atomic holds
( ((@ b1) . 1) `1 <> 0 & ((@ b1) . 1) `1 <> 1 & ((@ b1) . 1) `1 <> 2 & ((@ b1) . 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 b1 being Element of QC-WFF holds
( not ( b1 is atomic & b1 is negative ) & not ( b1 is atomic & b1 is conjunctive ) & not ( b1 is atomic & b1 is universal ) & not ( b1 is negative & b1 is conjunctive ) & not ( b1 is negative & b1 is universal ) & not ( b1 is conjunctive & b1 is universal ) ) ) )
proof end;

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

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

:: deftheorem Def28 defines still_not-bound_in QC_LANG1:def 28 :
for b1 being FinSequence of QC-variables holds still_not-bound_in b1 = { (b1 . b2) where B is Nat : ( 1 <= b2 & b2 <= len b1 & b1 . b2 in bound_QC-variables ) } ;

definition
let c1 be bound_QC-variable;
redefine func { as {c1} -> Subset of bound_QC-variables ;
coherence
{c1} is Subset of bound_QC-variables by SUBSET_1:63;
end;

definition
let c1 be QC-formula;
func still_not-bound_in c1 -> Subset of bound_QC-variables means :: QC_LANG1:def 29
ex b1 being Function of QC-WFF , bool bound_QC-variables st
( a2 = b1 . a1 & ( for b2 being Element of QC-WFF holds
( b1 . VERUM = {} & ( b2 is atomic implies b1 . b2 = { ((the_arguments_of b2) . b3) where B is Nat : ( 1 <= b3 & b3 <= len (the_arguments_of b2) & (the_arguments_of b2) . b3 in bound_QC-variables ) } ) & ( b2 is negative implies b1 . b2 = b1 . (the_argument_of b2) ) & ( b2 is conjunctive implies b1 . b2 = (b1 . (the_left_argument_of b2)) \/ (b1 . (the_right_argument_of b2)) ) & ( b2 is universal implies b1 . b2 = (b1 . (the_scope_of b2)) \ {(bound_in b2)} ) ) ) );
existence
ex b1 being Subset of bound_QC-variables ex b2 being Function of QC-WFF , bool bound_QC-variables st
( b1 = b2 . c1 & ( for b3 being Element of QC-WFF holds
( b2 . VERUM = {} & ( b3 is atomic implies b2 . b3 = { ((the_arguments_of b3) . b4) where B is Nat : ( 1 <= b4 & b4 <= len (the_arguments_of b3) & (the_arguments_of b3) . b4 in bound_QC-variables ) } ) & ( b3 is negative implies b2 . b3 = b2 . (the_argument_of b3) ) & ( b3 is conjunctive implies b2 . b3 = (b2 . (the_left_argument_of b3)) \/ (b2 . (the_right_argument_of b3)) ) & ( b3 is universal implies b2 . b3 = (b2 . (the_scope_of b3)) \ {(bound_in b3)} ) ) ) )
proof end;
uniqueness
for b1, b2 being Subset of bound_QC-variables st ex b3 being Function of QC-WFF , bool bound_QC-variables st
( b1 = b3 . c1 & ( for b4 being Element of QC-WFF holds
( b3 . VERUM = {} & ( b4 is atomic implies b3 . b4 = { ((the_arguments_of b4) . b5) where B is Nat : ( 1 <= b5 & b5 <= len (the_arguments_of b4) & (the_arguments_of b4) . b5 in bound_QC-variables ) } ) & ( b4 is negative implies b3 . b4 = b3 . (the_argument_of b4) ) & ( b4 is conjunctive implies b3 . b4 = (b3 . (the_left_argument_of b4)) \/ (b3 . (the_right_argument_of b4)) ) & ( b4 is universal implies b3 . b4 = (b3 . (the_scope_of b4)) \ {(bound_in b4)} ) ) ) ) & ex b3 being Function of QC-WFF , bool bound_QC-variables st
( b2 = b3 . c1 & ( for b4 being Element of QC-WFF holds
( b3 . VERUM = {} & ( b4 is atomic implies b3 . b4 = { ((the_arguments_of b4) . b5) where B is Nat : ( 1 <= b5 & b5 <= len (the_arguments_of b4) & (the_arguments_of b4) . b5 in bound_QC-variables ) } ) & ( b4 is negative implies b3 . b4 = b3 . (the_argument_of b4) ) & ( b4 is conjunctive implies b3 . b4 = (b3 . (the_left_argument_of b4)) \/ (b3 . (the_right_argument_of b4)) ) & ( b4 is universal implies b3 . b4 = (b3 . (the_scope_of b4)) \ {(bound_in b4)} ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def29 defines still_not-bound_in QC_LANG1:def 29 :
for b1 being QC-formula
for b2 being Subset of bound_QC-variables holds
( b2 = still_not-bound_in b1 iff ex b3 being Function of QC-WFF , bool bound_QC-variables st
( b2 = b3 . b1 & ( for b4 being Element of QC-WFF holds
( b3 . VERUM = {} & ( b4 is atomic implies b3 . b4 = { ((the_arguments_of b4) . b5) where B is Nat : ( 1 <= b5 & b5 <= len (the_arguments_of b4) & (the_arguments_of b4) . b5 in bound_QC-variables ) } ) & ( b4 is negative implies b3 . b4 = b3 . (the_argument_of b4) ) & ( b4 is conjunctive implies b3 . b4 = (b3 . (the_left_argument_of b4)) \/ (b3 . (the_right_argument_of b4)) ) & ( b4 is universal implies b3 . b4 = (b3 . (the_scope_of b4)) \ {(bound_in b4)} ) ) ) ) );

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

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