:: A First Order Language
:: by Piotr Rudnicki and Andrzej Trybulec
::
:: Received August 8, 1989
:: Copyright (c) 1990-2012 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:]
proofend;

theorem :: 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:]
proofend;

definition
mode QC-alphabet  ->  set  means :Def1: :: QC_LANG1:def 1
( it is non empty set & ex X being set st
( NAT c= X & it = [:NAT,X:] ) );
existence
 ex b1 being set st
( b1 is non empty set & ex X being set st
( NAT c= X & b1 = [:NAT,X:] ) )
proofend;
end;

:: deftheorem Def1 defines QC-alphabet QC_LANG1:def_1_:_
 for b1 being set holds
( b1 is QC-alphabet iff ( b1 is non empty set & ex X being set st
( NAT c= X & b1 = [:NAT,X:] ) ) );

registration
cluster  ->  Relation-like non empty for QC-alphabet ;
coherence
 for b1 being QC-alphabet holds
( not b1 is empty & b1 is Relation-like )
proofend;
end;

definition
let A be QC-alphabet ;
func QC-symbols A ->  non empty set  equals :: QC_LANG1:def 2
 rng A;
coherence
 rng A is non empty set ;
end;

:: deftheorem  defines QC-symbols QC_LANG1:def_2_:_
 for A being QC-alphabet holds QC-symbols A = rng A;

definition
let A be QC-alphabet ;
mode QC-symbol of A is Element of QC-symbols A;
end;

theorem Th3: :: QC_LANG1:3
for A being QC-alphabet holds
( NAT c= QC-symbols A & 0 in QC-symbols A )
proofend;

registration
let A be QC-alphabet ;
cluster QC-symbols A ->  non empty ;
coherence
 not QC-symbols A is empty ;
end;

definition
let A be QC-alphabet ;
func QC-variables A ->  set  equals :: QC_LANG1:def 3
[:{6},NAT:] \/ [:{4,5},(QC-symbols A):];
coherence
 [:{6},NAT:] \/ [:{4,5},(QC-symbols A):] is set ;
end;

:: deftheorem  defines QC-variables QC_LANG1:def_3_:_
 for A being QC-alphabet holds QC-variables A = [:{6},NAT:] \/ [:{4,5},(QC-symbols A):];

registration
let A be QC-alphabet ;
cluster QC-variables A ->  non empty ;
coherence
 not QC-variables A is empty ;
end;

Lm1:  for A being QC-alphabet holds
( [:{4},(QC-symbols A):] c= QC-variables A & [:{5},(QC-symbols A):] c= QC-variables A & [:{6},NAT:] c= QC-variables A )
proofend;

theorem Th4: :: QC_LANG1:4
for A being QC-alphabet holds QC-variables A c= [:NAT,(QC-symbols A):]
proofend;

definition
let A be QC-alphabet ;
mode QC-variable of A is Element of QC-variables A;
func bound_QC-variables A ->  Subset of (QC-variables A) equals :: QC_LANG1:def 4
[:{4},(QC-symbols A):];
coherence
 [:{4},(QC-symbols A):] is Subset of (QC-variables A) by Lm1;
func fixed_QC-variables A ->  Subset of (QC-variables A) equals :: QC_LANG1:def 5
[:{5},(QC-symbols A):];
coherence
 [:{5},(QC-symbols A):] is Subset of (QC-variables A) by Lm1;
func free_QC-variables A ->  Subset of (QC-variables A) equals :: QC_LANG1:def 6
[:{6},NAT:];
coherence
 [:{6},NAT:] is Subset of (QC-variables A) by Lm1;
func QC-pred_symbols A ->  set  equals :: QC_LANG1:def 7
 {  [n,x] where n is Element of NAT , x is QC-symbol of A : 7 <= n  }  ;
coherence
  {  [n,x] where n is Element of NAT , x is QC-symbol of A : 7 <= n  }  is set ;
end;

:: deftheorem  defines bound_QC-variables QC_LANG1:def_4_:_
 for A being QC-alphabet holds bound_QC-variables A = [:{4},(QC-symbols A):];

:: deftheorem  defines fixed_QC-variables QC_LANG1:def_5_:_
 for A being QC-alphabet holds fixed_QC-variables A = [:{5},(QC-symbols A):];

:: deftheorem  defines free_QC-variables QC_LANG1:def_6_:_
 for A being QC-alphabet holds free_QC-variables A = [:{6},NAT:];

:: deftheorem  defines QC-pred_symbols QC_LANG1:def_7_:_
 for A being QC-alphabet holds QC-pred_symbols A =  {  [n,x] where n is Element of NAT , x is QC-symbol of A : 7 <= n  }  ;

registration
let A be QC-alphabet ;
cluster bound_QC-variables A ->  non empty ;
coherence
 not bound_QC-variables A is empty ;
cluster fixed_QC-variables A ->  non empty ;
coherence
 not fixed_QC-variables A is empty ;
cluster free_QC-variables A ->  non empty ;
coherence
 not free_QC-variables A is empty ;
cluster QC-pred_symbols A ->  non empty ;
coherence
 not QC-pred_symbols A is empty
proofend;
end;

theorem :: QC_LANG1:5
for A being QC-alphabet holds A = [:NAT,(QC-symbols A):]
proofend;

theorem Th6: :: QC_LANG1:6
for A being QC-alphabet holds QC-pred_symbols A c= [:NAT,(QC-symbols A):]
proofend;

definition
let A be QC-alphabet ;
mode QC-pred_symbol of A is Element of QC-pred_symbols A;
end;

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

:: deftheorem Def8 defines the_arity_of QC_LANG1:def_8_:_
 for A being QC-alphabet
for P being Element of QC-pred_symbols A
for b3 being Element of NAT holds
( b3 = the_arity_of P iff P `1 = 7 + b3 );

definition
let A be QC-alphabet ;
let k be Element of NAT ;
funck -ary_QC-pred_symbols A ->  Subset of (QC-pred_symbols A) equals :: QC_LANG1:def 9
 {  P where P is QC-pred_symbol of A : the_arity_of P = k  }  ;
coherence
  {  P where P is QC-pred_symbol of A : the_arity_of P = k  }  is Subset of (QC-pred_symbols A)
proofend;
end;

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

registration
let k be Element of NAT ;
let A be QC-alphabet ;
clusterk -ary_QC-pred_symbols A ->  non empty ;
coherence
 not k -ary_QC-pred_symbols A is empty
proofend;
end;

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

registration
let k be Element of NAT ;
let A be QC-alphabet ;
cluster Relation-like NAT -defined QC-variables A -valued Function-like V35() k -element FinSequence-like FinSubsequence-like for FinSequence of QC-variables A;
existence
 ex b1 being FinSequence of QC-variables A st b1 is k -element
proofend;
end;

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

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

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

Lm2:  for A being QC-alphabet
for k being Element of NAT
for x being QC-symbol of A holds <*[k,x]*> is FinSequence of [:NAT,(QC-symbols A):]
proofend;

Lm3:  for A being QC-alphabet
for k being Element of NAT
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds <*p*> ^ ll is FinSequence of [:NAT,(QC-symbols A):]
proofend;

Lm4:  for A being QC-alphabet
for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):] holds (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,(QC-symbols A):]
proofend;

definition
let A be QC-alphabet ;
func QC-WFF A ->  non empty set  means :Def11: :: QC_LANG1:def 11
( it is A -closed &amp; ( for D being non empty set st D is A -closed holds
it c= D ) );
existence
 ex b1 being non empty set st
( b1 is A -closed &amp; ( for D being non empty set st D is A -closed holds
b1 c= D ) )
proofend;
uniqueness
 for b1, b2 being non empty set st b1 is A -closed &amp; ( for D being non empty set st D is A -closed holds
b1 c= D ) &amp; b2 is A -closed &amp; ( for D being non empty set st D is A -closed holds
b2 c= D ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines QC-WFF QC_LANG1:def_11_:_
 for A being QC-alphabet
for b2 being non empty set holds
( b2 = QC-WFF A iff ( b2 is A -closed &amp; ( for D being non empty set st D is A -closed holds
b2 c= D ) ) );

theorem :: QC_LANG1:7
for A being QC-alphabet holds QC-WFF A is A -closed by Def11;

registration
let A be QC-alphabet ;
cluster non empty A -closed for set ;
existence
 ex b1 being set st
( b1 is A -closed &amp; not b1 is empty )
proofend;
end;

definition
let A be QC-alphabet ;
mode QC-formula of A is Element of QC-WFF A;
end;

definition
let A be QC-alphabet ;
let P be QC-pred_symbol of A;
let l be FinSequence of QC-variables A;
assume A1: the_arity_of P = len l ;
funcP ! l ->  Element of QC-WFF A equals :Def12: :: QC_LANG1:def 12
<*P*> ^ l;
coherence
 <*P*> ^ l is Element of QC-WFF A
proofend;
end;

:: deftheorem Def12 defines ! QC_LANG1:def_12_:_
 for A being QC-alphabet
for P being QC-pred_symbol of A
for l being FinSequence of QC-variables A st the_arity_of P = len l holds
P ! l = <*P*> ^ l;

theorem Th8: :: QC_LANG1:8
for A being QC-alphabet
for k being Element of NAT
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds p ! ll = <*p*> ^ ll
proofend;

Lm5:  for A being QC-alphabet holds QC-WFF A is Subset of ([:NAT,(QC-symbols A):] *)
proofend;

definition
let A be QC-alphabet ;
let p be Element of QC-WFF A;
func @ p ->  FinSequence of [:NAT,(QC-symbols A):] equals :: QC_LANG1:def 13
p;
coherence
 p is FinSequence of [:NAT,(QC-symbols A):]
proofend;
end;

:: deftheorem  defines @ QC_LANG1:def_13_:_
 for A being QC-alphabet
for p being Element of QC-WFF A holds @ p = p;

definition
let A be QC-alphabet ;
func VERUM A ->  QC-formula of A equals :: QC_LANG1:def 14
<*[0,0]*>;
coherence
 <*[0,0]*> is QC-formula of A
proofend;
let p be Element of QC-WFF A;
func 'not' p ->  QC-formula of A equals :: QC_LANG1:def 15
<*[1,0]*> ^ (@ p);
coherence
 <*[1,0]*> ^ (@ p) is QC-formula of A
proofend;
let q be Element of QC-WFF A;
funcp '&amp;' q ->  QC-formula of A equals :: QC_LANG1:def 16
(<*[2,0]*> ^ (@ p)) ^ (@ q);
coherence
 (<*[2,0]*> ^ (@ p)) ^ (@ q) is QC-formula of A
proofend;
end;

:: deftheorem  defines VERUM QC_LANG1:def_14_:_
 for A being QC-alphabet holds VERUM A = <*[0,0]*>;

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

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

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

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

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

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

:: deftheorem Def18 defines atomic QC_LANG1:def_18_:_
 for A being QC-alphabet
for F being Element of QC-WFF A holds
( F is atomic iff ex k being Element of NAT ex p being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A st F = p ! ll );

:: deftheorem Def19 defines negative QC_LANG1:def_19_:_
 for A being QC-alphabet
for F being Element of QC-WFF A holds
( F is negative iff ex p being Element of QC-WFF A st F = 'not' p );

:: deftheorem Def20 defines conjunctive QC_LANG1:def_20_:_
 for A being QC-alphabet
for F being Element of QC-WFF A holds
( F is conjunctive iff ex p, q being Element of QC-WFF A st F = p '&amp;' q );

:: deftheorem Def21 defines universal QC_LANG1:def_21_:_
 for A being QC-alphabet
for F being Element of QC-WFF A holds
( F is universal iff ex x being bound_QC-variable of A ex p being Element of QC-WFF A st F = All (x,p) );

theorem Th9: :: QC_LANG1:9
for A being QC-alphabet
for F being Element of QC-WFF A holds
( F = VERUM A or F is atomic or F is negative or F is conjunctive or F is universal )
proofend;

theorem Th10: :: QC_LANG1:10
for A being QC-alphabet
for F being Element of QC-WFF A holds 1 <= len (@ F)
proofend;

theorem Th11: :: QC_LANG1:11
for A being QC-alphabet
for k being Element of NAT
for P being QC-pred_symbol of k,A holds the_arity_of P = k
proofend;

theorem Th12: :: QC_LANG1:12
for A being QC-alphabet
for F being Element of QC-WFF A holds
( ( ((@ F) . 1) `1 = 0 implies F = VERUM A ) &amp; ( ((@ F) . 1) `1 = 1 implies F is negative ) &amp; ( ((@ F) . 1) `1 = 2 implies F is conjunctive ) &amp; ( ((@ F) . 1) `1 = 3 implies F is universal ) &amp; ( ex k being Element of NAT st (@ F) . 1 is QC-pred_symbol of k,A implies F is atomic ) )
proofend;

theorem Th13: :: QC_LANG1:13
for A being QC-alphabet
for F, G being Element of QC-WFF A
for s being FinSequence st @ F = (@ G) ^ s holds
@ F = @ G
proofend;

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

:: deftheorem Def22 defines the_pred_symbol_of QC_LANG1:def_22_:_
 for A being QC-alphabet
for F being Element of QC-WFF A st F is atomic holds
for b3 being QC-pred_symbol of A holds
( b3 = the_pred_symbol_of F iff ex k being Element of NAT ex ll being QC-variable_list of k,A ex P being QC-pred_symbol of k,A st
( b3 = P &amp; F = P ! ll ) );

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

:: deftheorem Def23 defines the_arguments_of QC_LANG1:def_23_:_
 for A being QC-alphabet
for F being Element of QC-WFF A st F is atomic holds
for b3 being FinSequence of QC-variables A holds
( b3 = the_arguments_of F iff ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A st
( b3 = ll &amp; F = P ! ll ) );

definition
let A be QC-alphabet ;
let F be Element of QC-WFF A;
assume A1: F is negative ;
func the_argument_of F ->  QC-formula of A means :Def24: :: QC_LANG1:def 24
F = 'not' it;
existence
 ex b1 being QC-formula of A st F = 'not' b1 by A1, Def19;
uniqueness
 for b1, b2 being QC-formula of A st F = 'not' b1 &amp; F = 'not' b2 holds
b1 = b2 by FINSEQ_1:33;
end;

:: deftheorem Def24 defines the_argument_of QC_LANG1:def_24_:_
 for A being QC-alphabet
for F being Element of QC-WFF A st F is negative holds
for b3 being QC-formula of A holds
( b3 = the_argument_of F iff F = 'not' b3 );

definition
let A be QC-alphabet ;
let F be Element of QC-WFF A;
assume A1: F is conjunctive ;
func the_left_argument_of F ->  QC-formula of A means :Def25: :: QC_LANG1:def 25
 ex q being Element of QC-WFF A st F = it '&amp;' q;
existence
 ex b1 being QC-formula of A ex q being Element of QC-WFF A st F = b1 '&amp;' q by A1, Def20;
uniqueness
 for b1, b2 being QC-formula of A st ex q being Element of QC-WFF A st F = b1 '&amp;' q &amp; ex q being Element of QC-WFF A st F = b2 '&amp;' q holds
b1 = b2
proofend;
end;

:: deftheorem Def25 defines the_left_argument_of QC_LANG1:def_25_:_
 for A being QC-alphabet
for F being Element of QC-WFF A st F is conjunctive holds
for b3 being QC-formula of A holds
( b3 = the_left_argument_of F iff ex q being Element of QC-WFF A st F = b3 '&amp;' q );

definition
let A be QC-alphabet ;
let F be Element of QC-WFF A;
assume B1: F is conjunctive ;
func the_right_argument_of F ->  QC-formula of A means :Def26: :: QC_LANG1:def 26
 ex p being Element of QC-WFF A st F = p '&amp;' it;
existence
 ex b1 being QC-formula of A ex p being Element of QC-WFF A st F = p '&amp;' b1
proofend;
uniqueness
 for b1, b2 being QC-formula of A st ex p being Element of QC-WFF A st F = p '&amp;' b1 &amp; ex p being Element of QC-WFF A st F = p '&amp;' b2 holds
b1 = b2
proofend;
end;

:: deftheorem Def26 defines the_right_argument_of QC_LANG1:def_26_:_
 for A being QC-alphabet
for F being Element of QC-WFF A st F is conjunctive holds
for b3 being QC-formula of A holds
( b3 = the_right_argument_of F iff ex p being Element of QC-WFF A st F = p '&amp;' b3 );

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

:: deftheorem Def27 defines bound_in QC_LANG1:def_27_:_
 for A being QC-alphabet
for F being Element of QC-WFF A st F is universal holds
for b3 being bound_QC-variable of A holds
( b3 = bound_in F iff ex p being Element of QC-WFF A st F = All (b3,p) );

:: deftheorem Def28 defines the_scope_of QC_LANG1:def_28_:_
 for A being QC-alphabet
for F being Element of QC-WFF A st F is universal holds
for b3 being QC-formula of A holds
( b3 = the_scope_of F iff ex x being bound_QC-variable of A st F = All (x,b3) );

theorem Th14: :: QC_LANG1:14
for A being QC-alphabet
for p being Element of QC-WFF A st p is negative holds
len (@ (the_argument_of p)) < len (@ p)
proofend;

theorem Th15: :: QC_LANG1:15
for A being QC-alphabet
for p being Element of QC-WFF A st p is conjunctive holds
( len (@ (the_left_argument_of p)) < len (@ p) &amp; len (@ (the_right_argument_of p)) < len (@ p) )
proofend;

theorem Th16: :: QC_LANG1:16
for A being QC-alphabet
for p being Element of QC-WFF A st p is universal holds
len (@ (the_scope_of p)) < len (@ p)
proofend;

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

theorem Th17: :: QC_LANG1:17
for A being QC-alphabet
for k being Element of NAT
for P being QC-pred_symbol of k,A holds
( P `1 <> 0 &amp; P `1 <> 1 &amp; P `1 <> 2 &amp; P `1 <> 3 )
proofend;

theorem Th18: :: QC_LANG1:18
for A being QC-alphabet
for F being Element of QC-WFF A holds
( ((@ (VERUM A)) . 1) `1 = 0 &amp; ( F is atomic implies ex k being Element of NAT st (@ F) . 1 is QC-pred_symbol of k,A ) &amp; ( F is negative implies ((@ F) . 1) `1 = 1 ) &amp; ( F is conjunctive implies ((@ F) . 1) `1 = 2 ) &amp; ( F is universal implies ((@ F) . 1) `1 = 3 ) )
proofend;

theorem Th19: :: QC_LANG1:19
for A being QC-alphabet
for F being Element of QC-WFF A st F is atomic holds
( ((@ F) . 1) `1 <> 0 &amp; ((@ F) . 1) `1 <> 1 &amp; ((@ F) . 1) `1 <> 2 &amp; ((@ F) . 1) `1 <> 3 )
proofend;

theorem Th20: :: QC_LANG1:20
for A being QC-alphabet holds
( not VERUM A is atomic &amp; not VERUM A is negative &amp; not VERUM A is conjunctive &amp; not VERUM A is universal &amp; ( for p being Element of QC-WFF A holds
( not ( p is atomic &amp; p is negative ) &amp; not ( p is atomic &amp; p is conjunctive ) &amp; not ( p is atomic &amp; p is universal ) &amp; not ( p is negative &amp; p is conjunctive ) &amp; not ( p is negative &amp; p is universal ) &amp; not ( p is conjunctive &amp; p is universal ) ) ) )
proofend;

scheme :: QC_LANG1:sch 3
QCFuncEx{ F1() ->  QC-alphabet , F2() ->  non empty set , F3() ->  Element of F2(), F4( Element of QC-WFF F1()) ->  Element of F2(), F5( Element of F2()) ->  Element of F2(), F6( Element of F2(), Element of F2()) ->  Element of F2(), F7( Element of QC-WFF F1(), Element of F2()) ->  Element of F2() } :
 ex F being Function of (QC-WFF F1()),F2() st
( F . (VERUM F1()) = F3() &amp; ( for p being Element of QC-WFF F1() holds
( ( p is atomic implies F . p = F4(p) ) &amp; ( p is negative implies F . p = F5((F . (the_argument_of p))) ) &amp; ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) &amp; ( p is universal implies F . p = F7(p,(F . (the_scope_of p))) ) ) ) )
proofend;

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

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

definition
let A be QC-alphabet ;
let p be QC-formula of A;
func still_not-bound_in p ->  Subset of (bound_QC-variables A) means :: QC_LANG1:def 30
 ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( it = F . p &amp; ( for p being Element of QC-WFF A holds
( F . (VERUM A) = {} &amp; ( p is atomic implies F . p =  {  ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k &amp; k <= len (the_arguments_of p) &amp; (the_arguments_of p) . k in bound_QC-variables A )  }  ) &amp; ( p is negative implies F . p = F . (the_argument_of p) ) &amp; ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) &amp; ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) ) ) );
existence
 ex b1 being Subset of (bound_QC-variables A) ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( b1 = F . p &amp; ( for p being Element of QC-WFF A holds
( F . (VERUM A) = {} &amp; ( p is atomic implies F . p =  {  ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k &amp; k <= len (the_arguments_of p) &amp; (the_arguments_of p) . k in bound_QC-variables A )  }  ) &amp; ( p is negative implies F . p = F . (the_argument_of p) ) &amp; ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) &amp; ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) ) ) )
proofend;
uniqueness
 for b1, b2 being Subset of (bound_QC-variables A) st ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( b1 = F . p &amp; ( for p being Element of QC-WFF A holds
( F . (VERUM A) = {} &amp; ( p is atomic implies F . p =  {  ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k &amp; k <= len (the_arguments_of p) &amp; (the_arguments_of p) . k in bound_QC-variables A )  }  ) &amp; ( p is negative implies F . p = F . (the_argument_of p) ) &amp; ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) &amp; ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) ) ) ) &amp; ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( b2 = F . p &amp; ( for p being Element of QC-WFF A holds
( F . (VERUM A) = {} &amp; ( p is atomic implies F . p =  {  ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k &amp; k <= len (the_arguments_of p) &amp; (the_arguments_of p) . k in bound_QC-variables A )  }  ) &amp; ( p is negative implies F . p = F . (the_argument_of p) ) &amp; ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) &amp; ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines still_not-bound_in QC_LANG1:def_30_:_
 for A being QC-alphabet
for p being QC-formula of A
for b3 being Subset of (bound_QC-variables A) holds
( b3 = still_not-bound_in p iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( b3 = F . p &amp; ( for p being Element of QC-WFF A holds
( F . (VERUM A) = {} &amp; ( p is atomic implies F . p =  {  ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k &amp; k <= len (the_arguments_of p) &amp; (the_arguments_of p) . k in bound_QC-variables A )  }  ) &amp; ( p is negative implies F . p = F . (the_argument_of p) ) &amp; ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) &amp; ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) ) ) ) );

definition
let A be QC-alphabet ;
let p be QC-formula of A;
attrp is closed  means :: QC_LANG1:def 31
 still_not-bound_in p = {} ;
end;

:: deftheorem  defines closed QC_LANG1:def_31_:_
 for A being QC-alphabet
for p being QC-formula of A holds
( p is closed iff still_not-bound_in p = {} );

definition
let A be QC-alphabet ;
mode Relation of A ->  Relation means :Def32: :: QC_LANG1:def 32
it well_orders (QC-symbols A) \ NAT;
existence
 ex b1 being Relation st b1 well_orders (QC-symbols A) \ NAT by WELLORD2:17;
end;

:: deftheorem Def32 defines Relation QC_LANG1:def_32_:_
 for A being QC-alphabet
for b2 being Relation holds
( b2 is Relation of A iff b2 well_orders (QC-symbols A) \ NAT );

definition
let A be QC-alphabet ;
let s, t be QC-symbol of A;
preds <= t means :Def33: :: QC_LANG1:def 33
 ex n, m being Element of NAT st
( n = s &amp; m = t &amp; n <= m ) if ( s in NAT &amp; t in NAT )
[s,t] in the Relation of A if ( not s in NAT &amp; not t in NAT )
otherwise t in NAT ;
consistency
 ( s in NAT &amp; t in NAT &amp; not s in NAT &amp; not t in NAT implies ( ex n, m being Element of NAT st
( n = s &amp; m = t &amp; n <= m ) iff [s,t] in the Relation of A ) ) ;
end;

:: deftheorem Def33 defines <= QC_LANG1:def_33_:_
 for A being QC-alphabet
for s, t being QC-symbol of A holds
( ( s in NAT &amp; t in NAT implies ( s <= t iff ex n, m being Element of NAT st
( n = s &amp; m = t &amp; n <= m ) ) ) &amp; ( not s in NAT &amp; not t in NAT implies ( s <= t iff [s,t] in the Relation of A ) ) &amp; ( ( not s in NAT or not t in NAT ) &amp; ( s in NAT or t in NAT ) implies ( s <= t iff t in NAT ) ) );

definition
let A be QC-alphabet ;
let s, t be QC-symbol of A;
preds < t means :Def34: :: QC_LANG1:def 34
( s <= t &amp; s <> t );
end;

:: deftheorem Def34 defines < QC_LANG1:def_34_:_
 for A being QC-alphabet
for s, t being QC-symbol of A holds
( s < t iff ( s <= t &amp; s <> t ) );

theorem Th21: :: QC_LANG1:21
for A being QC-alphabet
for s, t, u being QC-symbol of A st s <= t &amp; t <= u holds
s <= u
proofend;

theorem Th22: :: QC_LANG1:22
for A being QC-alphabet
for t being QC-symbol of A holds t <= t
proofend;

theorem Th23: :: QC_LANG1:23
for A being QC-alphabet
for t, u being QC-symbol of A st t <= u &amp; u <= t holds
u = t
proofend;

theorem Th24: :: QC_LANG1:24
for A being QC-alphabet
for t, u being QC-symbol of A holds
( t <= u or u <= t )
proofend;

theorem Th25: :: QC_LANG1:25
for A being QC-alphabet
for s, t being QC-symbol of A holds
( s < t iff not t <= s )
proofend;

theorem :: QC_LANG1:26
for A being QC-alphabet
for s, t being QC-symbol of A holds
( s < t or s = t or t < s )
proofend;

definition
let A be QC-alphabet ;
let Y be non empty Subset of (QC-symbols A);
func min Y ->  QC-symbol of A means :Def35: :: QC_LANG1:def 35
( it in Y &amp; ( for t being QC-symbol of A st t in Y holds
it <= t ) );
existence
 ex b1 being QC-symbol of A st
( b1 in Y &amp; ( for t being QC-symbol of A st t in Y holds
b1 <= t ) )
proofend;
uniqueness
 for b1, b2 being QC-symbol of A st b1 in Y &amp; ( for t being QC-symbol of A st t in Y holds
b1 <= t ) &amp; b2 in Y &amp; ( for t being QC-symbol of A st t in Y holds
b2 <= t ) holds
b1 = b2
proofend;
end;

:: deftheorem Def35 defines min QC_LANG1:def_35_:_
 for A being QC-alphabet
for Y being non empty Subset of (QC-symbols A)
for b3 being QC-symbol of A holds
( b3 = min Y iff ( b3 in Y &amp; ( for t being QC-symbol of A st t in Y holds
b3 <= t ) ) );

definition
let A be QC-alphabet ;
func 0 A ->  QC-symbol of A means :: QC_LANG1:def 36
 for t being QC-symbol of A holds it <= t;
existence
 ex b1 being QC-symbol of A st
for t being QC-symbol of A holds b1 <= t
proofend;
uniqueness
 for b1, b2 being QC-symbol of A st ( for t being QC-symbol of A holds b1 <= t ) &amp; ( for t being QC-symbol of A holds b2 <= t ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines 0 QC_LANG1:def_36_:_
 for A being QC-alphabet
for b2 being QC-symbol of A holds
( b2 = 0 A iff for t being QC-symbol of A holds b2 <= t );

definition
let A be QC-alphabet ;
let s be QC-symbol of A;
func Seg s ->  non empty Subset of (QC-symbols A) equals :: QC_LANG1:def 37
 {  t where t is QC-symbol of A : s < t  }  ;
coherence
  {  t where t is QC-symbol of A : s < t  }  is non empty Subset of (QC-symbols A)
proofend;
end;

:: deftheorem  defines Seg QC_LANG1:def_37_:_
 for A being QC-alphabet
for s being QC-symbol of A holds Seg s =  {  t where t is QC-symbol of A : s < t  }  ;

definition
let A be QC-alphabet ;
let s be QC-symbol of A;
funcs ++  ->  QC-symbol of A equals :: QC_LANG1:def 38
 min (Seg s);
coherence
 min (Seg s) is QC-symbol of A ;
end;

:: deftheorem  defines ++ QC_LANG1:def_38_:_
 for A being QC-alphabet
for s being QC-symbol of A holds s ++ = min (Seg s);

theorem Th27: :: QC_LANG1:27
for A being QC-alphabet
for s being QC-symbol of A holds s < s ++
proofend;

theorem :: QC_LANG1:28
for A being QC-alphabet
for Y1, Y2 being non empty Subset of (QC-symbols A) st Y1 c= Y2 holds
min Y2 <= min Y1
proofend;

theorem Th29: :: QC_LANG1:29
for A being QC-alphabet
for s, t, v being QC-symbol of A st s <= t &amp; t < v holds
s < v
proofend;

theorem :: QC_LANG1:30
for A being QC-alphabet
for s, t, v being QC-symbol of A st s < t &amp; t <= v holds
s < v
proofend;

definition
let A be QC-alphabet ;
let s be set ;
funcs @ A ->  QC-symbol of A equals :Def39: :: QC_LANG1:def 39
s if s is QC-symbol of A
otherwise  0 ;
correctness
coherence
( ( s is QC-symbol of A implies s is QC-symbol of A ) &amp; ( s is not QC-symbol of A implies 0 is QC-symbol of A ) );
consistency
for b1 being QC-symbol of A holds verum;
by Th3;
end;

:: deftheorem Def39 defines @ QC_LANG1:def_39_:_
 for A being QC-alphabet
for s being set holds
( ( s is QC-symbol of A implies s @ A = s ) &amp; ( s is not QC-symbol of A implies s @ A = 0 ) );

definition
let A be QC-alphabet ;
let t be QC-symbol of A;
let n be Element of NAT ;
funct + n ->  QC-symbol of A means :Def40: :: QC_LANG1:def 40
 ex f being Function of NAT,(QC-symbols A) st
( it = f . n &amp; f . 0 = t &amp; ( for k being Element of NAT holds f . (k + 1) = (f . k) ++ ) );
existence
 ex b1 being QC-symbol of A ex f being Function of NAT,(QC-symbols A) st
( b1 = f . n &amp; f . 0 = t &amp; ( for k being Element of NAT holds f . (k + 1) = (f . k) ++ ) )
proofend;
uniqueness
 for b1, b2 being QC-symbol of A st ex f being Function of NAT,(QC-symbols A) st
( b1 = f . n &amp; f . 0 = t &amp; ( for k being Element of NAT holds f . (k + 1) = (f . k) ++ ) ) &amp; ex f being Function of NAT,(QC-symbols A) st
( b2 = f . n &amp; f . 0 = t &amp; ( for k being Element of NAT holds f . (k + 1) = (f . k) ++ ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def40 defines + QC_LANG1:def_40_:_
 for A being QC-alphabet
for t being QC-symbol of A
for n being Element of NAT
for b4 being QC-symbol of A holds
( b4 = t + n iff ex f being Function of NAT,(QC-symbols A) st
( b4 = f . n &amp; f . 0 = t &amp; ( for k being Element of NAT holds f . (k + 1) = (f . k) ++ ) ) );

theorem :: QC_LANG1:31
for A being QC-alphabet
for n being Element of NAT
for t being QC-symbol of A holds t <= t + n
proofend;

definition
let A be QC-alphabet ;
let Y be set ;
funcA -one_in Y ->  QC-symbol of A equals :: QC_LANG1:def 41
 the Element of Y if Y is non empty Subset of (QC-symbols A)
otherwise  0 A;
coherence
 ( ( Y is non empty Subset of (QC-symbols A) implies the Element of Y is QC-symbol of A ) &amp; ( Y is not non empty Subset of (QC-symbols A) implies 0 A is QC-symbol of A ) )
proofend;
consistency
 for b1 being QC-symbol of A holds verum ;
end;

:: deftheorem  defines -one_in QC_LANG1:def_41_:_
 for A being QC-alphabet
for Y being set holds
( ( Y is non empty Subset of (QC-symbols A) implies A -one_in Y = the Element of Y ) &amp; ( Y is not non empty Subset of (QC-symbols A) implies A -one_in Y = 0 A ) );