:: QC_LANG1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem :: QC_LANG1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;
end;

theorem :: QC_LANG1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th4: :: QC_LANG1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Nat : 7 <= k } ;
coherence
{ [k,l] where k, l is 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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th10: :: QC_LANG1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 -> Nat means :Def6: :: QC_LANG1:def 6
P `1 = 7 + it;
existence
ex b1 being Nat st P `1 = 7 + b1
proof end;
uniqueness
for b1, b2 being Nat st P `1 = 7 + b1 & P `1 = 7 + b2 holds
b1 = b2 by XCMPLX_1:2;
end;

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

definition
let k be 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 Nat holds k -ary_QC-pred_symbols = { P where P is QC-pred_symbol : the_arity_of P = k } ;

registration
let k be 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 Nat;
mode QC-pred_symbol of k is Element of k -ary_QC-pred_symbols ;
end;

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

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

definition
let D be set ;
attr D is QC-closed means :Def9: :: QC_LANG1:def 9
( D is Subset of ([:NAT ,NAT :] * ) & ( for k being 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 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 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 Nat holds <*[k,l]*> is FinSequence of [:NAT ,NAT :]
proof end;

Lm2: for k being 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th21: :: QC_LANG1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th23: :: QC_LANG1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being 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 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 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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th33: :: QC_LANG1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF holds 1 <= len (@ F)
proof end;

theorem Th35: :: QC_LANG1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for P being QC-pred_symbol of k holds the_arity_of P = k
proof end;

theorem Th36: :: QC_LANG1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Nat st (@ F) . 1 is QC-pred_symbol of k implies F is atomic ) )
proof end;

theorem Th37: :: QC_LANG1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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 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 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 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 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 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 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 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 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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QC_LANG1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th45: :: QC_LANG1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF holds
( ((@ VERUM ) . 1) `1 = 0 & ( F is atomic implies ex k being 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( 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 Nat : ( 1 <= k & k <= len ll & ll . k in bound_QC-variables ) } ;
coherence
{ (ll . k) where k is 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 Nat : ( 1 <= k & k <= len ll & ll . k in bound_QC-variables ) } ;

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

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 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 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 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 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 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 = {} );