:: A First Order Language
:: by Piotr Rudnicki and Andrzej Trybulec
::
:: Copyright (c) 1990-2021 Association of Mizar Users

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 :: 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
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:] ) )
proof end;
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 )
proof end;
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 end;

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

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
\/ [:{4,5},():];
coherence
\/ [:{4,5},():] is set
;
end;

:: deftheorem defines QC-variables QC_LANG1:def 3 :
for A being QC-alphabet holds QC-variables A = \/ [:{4,5},():];

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},():] c= QC-variables A & [:{5},():] c= QC-variables A & c= QC-variables A )

proof end;

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

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

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

:: deftheorem defines free_QC-variables QC_LANG1:def 6 :
for A being QC-alphabet holds free_QC-variables A = ;

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

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

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

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

definition end;

definition
let A be QC-alphabet ;
let P be Element of QC-pred_symbols A;
func the_arity_of P -> Nat means :Def8: :: QC_LANG1:def 8
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
;
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 Nat holds
( b3 = the_arity_of P iff P 1 = 7 + b3 );

definition
let A be QC-alphabet ;
let k be Nat;
func k -ary_QC-pred_symbols A -> Subset of () 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 ()
proof end;
end;

:: deftheorem defines -ary_QC-pred_symbols QC_LANG1:def 9 :
for A being QC-alphabet
for k being 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 Nat;
let A be QC-alphabet ;
cluster k -ary_QC-pred_symbols A -> non empty ;
coherence
not k -ary_QC-pred_symbols A is empty
proof end;
end;

definition end;

registration
let k be Nat;
let A be QC-alphabet ;
existence
ex b1 being FinSequence of QC-variables A st b1 is k -element
proof end;
end;

definition
let k be 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 ;
attr D is A -closed means :Def10: :: QC_LANG1:def 10
( D is Subset of ([:NAT,():] *) & ( for k being Nat
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds <*p*> ^ ll in D ) & in D & ( for p being FinSequence of [:NAT,():] st p in D holds
<*[1,0]*> ^ p in D ) & ( for p, q being FinSequence of [:NAT,():] st p in D & q in D holds
(<*[2,0]*> ^ p) ^ q in D ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,():] 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,():] *) & ( for k being Nat
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds <*p*> ^ ll in D ) & in D & ( for p being FinSequence of [:NAT,():] st p in D holds
<*[1,0]*> ^ p in D ) & ( for p, q being FinSequence of [:NAT,():] st p in D & q in D holds
(<*[2,0]*> ^ p) ^ q in D ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,():] st p in D holds
(<*[3,0]*> ^ <*x*>) ^ p in D ) ) );

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

proof end;

Lm3: for A being QC-alphabet
for k being 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,():]

proof end;

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

proof end;

definition
let A be QC-alphabet ;
func QC-WFF A -> non empty set means :Def11: :: QC_LANG1:def 11
( it is A -closed & ( 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 & ( for D being non empty set st D is A -closed holds
b1 c= D ) )
proof end;
uniqueness
for b1, b2 being non empty set st b1 is A -closed & ( for D being non empty set st D is A -closed holds
b1 c= D ) & b2 is A -closed & ( for D being non empty set st D is A -closed holds
b2 c= D ) holds
b1 = b2
;
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 & ( 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 & not b1 is empty )
proof end;
end;

definition 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 ;
func P ! l -> Element of QC-WFF A equals :Def12: :: QC_LANG1:def 12
<*P*> ^ l;
coherence
<*P*> ^ l is Element of QC-WFF A
proof end;
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 Nat
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds p ! ll = <*p*> ^ ll
proof end;

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

definition
let A be QC-alphabet ;
let p be Element of QC-WFF A;
func @ p -> FinSequence of [:NAT,():] equals :: QC_LANG1:def 13
p;
coherence
p is FinSequence of [:NAT,():]
proof end;
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
;
coherence
is QC-formula of A
proof end;
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
proof end;
let q be Element of QC-WFF A;
func p '&' q -> QC-formula of A equals :: QC_LANG1:def 16
(<*[2,0]*> ^ (@ p)) ^ (@ q);
coherence
(<*[2,0]*> ^ (@ p)) ^ (@ q) is QC-formula of A
proof end;
end;

:: deftheorem defines VERUM QC_LANG1:def 14 :
for A being QC-alphabet holds VERUM A = ;

:: 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 '&' QC_LANG1:def 16 :
for A being QC-alphabet
for p, q being Element of QC-WFF A holds p '&' 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
proof end;
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 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] & P1[q] holds
P1[p '&' 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)]
proof end;

definition
let A be QC-alphabet ;
let F be Element of QC-WFF A;
attr F is atomic means :Def18: :: QC_LANG1:def 18
ex k being Nat ex p being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A st F = p ! ll;
attr F is negative means :Def19: :: QC_LANG1:def 19
ex p being Element of QC-WFF A st F = 'not' p;
attr F is conjunctive means :Def20: :: QC_LANG1:def 20
ex p, q being Element of QC-WFF A st F = p '&' q;
attr F 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 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 '&' 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 )
proof end;

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

theorem Th11: :: QC_LANG1:11
for A being QC-alphabet
for k being Nat
for P being QC-pred_symbol of k,A holds the_arity_of P = k
proof end;

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 ) & ( ((@ 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,A implies F is atomic ) )
proof end;

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
proof end;

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 Nat ex ll being QC-variable_list of k,A ex P being QC-pred_symbol of k,A st
( it = P & F = P ! ll );
existence
ex b1 being QC-pred_symbol of A ex k being Nat ex ll being QC-variable_list of k,A ex P being QC-pred_symbol of k,A st
( b1 = P & F = P ! ll )
by A1;
uniqueness
for b1, b2 being QC-pred_symbol of A st ex k being Nat ex ll being QC-variable_list of k,A ex P being QC-pred_symbol of k,A st
( b1 = P & F = P ! ll ) & ex k being Nat ex ll being QC-variable_list of k,A ex P being QC-pred_symbol of k,A st
( b2 = P & F = P ! ll ) holds
b1 = b2
proof end;
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 Nat ex ll being QC-variable_list of k,A ex P being QC-pred_symbol of k,A st
( b3 = P & F = P ! ll ) );

definition
let A be QC-alphabet ;
let F be Element of QC-WFF A;
assume A1: F is atomic ;
func the_arguments_of F -> FinSequence of QC-variables A means :Def23: :: QC_LANG1:def 23
ex k being Nat ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A st
( it = ll & F = P ! ll );
existence
ex b1 being FinSequence of QC-variables A ex k being Nat ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A st
( b1 = ll & F = P ! ll )
by A1;
uniqueness
for b1, b2 being FinSequence of QC-variables A st ex k being Nat ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A st
( b1 = ll & F = P ! ll ) & ex k being Nat ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A st
( b2 = ll & F = P ! ll ) holds
b1 = b2
proof end;
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 Nat ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A st
( b3 = ll & 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;
uniqueness
for b1, b2 being QC-formula of A st F = 'not' b1 & 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 '&' q;
existence
ex b1 being QC-formula of A ex q being Element of QC-WFF A st F = b1 '&' q
by A1;
uniqueness
for b1, b2 being QC-formula of A st ex q being Element of QC-WFF A st F = b1 '&' q & ex q being Element of QC-WFF A st F = b2 '&' q holds
b1 = b2
proof end;
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 '&' q );

definition
let A be QC-alphabet ;
let F be Element of QC-WFF A;
assume A1: 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 '&' it;
existence
ex b1 being QC-formula of A ex p being Element of QC-WFF A st F = p '&' b1
by A1;
uniqueness
for b1, b2 being QC-formula of A st ex p being Element of QC-WFF A st F = p '&' b1 & ex p being Element of QC-WFF A st F = p '&' b2 holds
b1 = b2
proof end;
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 '&' 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;
uniqueness
for b1, b2 being bound_QC-variable of A st ex p being Element of QC-WFF A st F = All (b1,p) & ex p being Element of QC-WFF A st F = All (b2,p) holds
b1 = b2
proof end;
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)
by A1;
uniqueness
for b1, b2 being QC-formula of A st ex x being bound_QC-variable of A st F = All (x,b1) & ex x being bound_QC-variable of A st F = All (x,b2) holds
b1 = b2
proof end;
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 (@ ()) < len (@ p)
proof end;

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

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

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] ) & P1[ VERUM F1()] & ( 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 Th17: :: QC_LANG1:17
for A being QC-alphabet
for k being Nat
for P being QC-pred_symbol of k,A holds
( P 1 <> 0 & P 1 <> 1 & P 1 <> 2 & P 1 <> 3 )
proof end;

theorem Th18: :: QC_LANG1:18
for A being QC-alphabet
for F being Element of QC-WFF A holds
( ((@ ()) . 1) 1 = 0 & ( F is atomic implies ex k being Nat st (@ F) . 1 is QC-pred_symbol of k,A ) & ( 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 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 & ((@ F) . 1) 1 <> 1 & ((@ F) . 1) 1 <> 2 & ((@ F) . 1) `1 <> 3 )
proof end;

theorem Th20: :: QC_LANG1:20
for A being QC-alphabet holds
( not VERUM A is atomic & not VERUM A is negative & not VERUM A is conjunctive & not VERUM A is universal & ( for p being Element of QC-WFF A 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() -> 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() & ( for p being Element of QC-WFF F1() holds
( ( p is atomic implies F . p = F4(p) ) & ( p is negative implies F . p = F5((F . ())) ) & ( p is conjunctive implies F . p = F6((),()) ) & ( p is universal implies F . p = F7(p,(F . ())) ) ) ) )
proof end;

definition
let A be QC-alphabet ;
let ll be FinSequence of QC-variables A;
func still_not-bound_in ll -> Subset of equals :: QC_LANG1:def 29
{ (ll . k) where k is Nat : ( 1 <= k & k <= len ll & ll . k in bound_QC-variables A ) } ;
coherence
{ (ll . k) where k is Nat : ( 1 <= k & k <= len ll & ll . k in bound_QC-variables A ) } is Subset of
proof end;
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 Nat : ( 1 <= k & k <= len ll & 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 means :: QC_LANG1:def 30
ex F being Function of (),() st
( it = F . p & ( for p being Element of QC-WFF A holds
( F . () = {} & ( p is atomic implies F . p = { (() . k) where k is Nat : ( 1 <= k & k <= len () & () . k in bound_QC-variables A ) } ) & ( p is negative implies F . p = F . () ) & ( p is conjunctive implies F . p = () \/ () ) & ( p is universal implies F . p = (F . ()) \ {()} ) ) ) );
existence
ex b1 being Subset of ex F being Function of (),() st
( b1 = F . p & ( for p being Element of QC-WFF A holds
( F . () = {} & ( p is atomic implies F . p = { (() . k) where k is Nat : ( 1 <= k & k <= len () & () . k in bound_QC-variables A ) } ) & ( p is negative implies F . p = F . () ) & ( p is conjunctive implies F . p = () \/ () ) & ( p is universal implies F . p = (F . ()) \ {()} ) ) ) )
proof end;
uniqueness
for b1, b2 being Subset of st ex F being Function of (),() st
( b1 = F . p & ( for p being Element of QC-WFF A holds
( F . () = {} & ( p is atomic implies F . p = { (() . k) where k is Nat : ( 1 <= k & k <= len () & () . k in bound_QC-variables A ) } ) & ( p is negative implies F . p = F . () ) & ( p is conjunctive implies F . p = () \/ () ) & ( p is universal implies F . p = (F . ()) \ {()} ) ) ) ) & ex F being Function of (),() st
( b2 = F . p & ( for p being Element of QC-WFF A holds
( F . () = {} & ( p is atomic implies F . p = { (() . k) where k is Nat : ( 1 <= k & k <= len () & () . k in bound_QC-variables A ) } ) & ( p is negative implies F . p = F . () ) & ( p is conjunctive implies F . p = () \/ () ) & ( p is universal implies F . p = (F . ()) \ {()} ) ) ) ) holds
b1 = b2
proof end;
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 holds
( b3 = still_not-bound_in p iff ex F being Function of (),() st
( b3 = F . p & ( for p being Element of QC-WFF A holds
( F . () = {} & ( p is atomic implies F . p = { (() . k) where k is Nat : ( 1 <= k & k <= len () & () . k in bound_QC-variables A ) } ) & ( p is negative implies F . p = F . () ) & ( p is conjunctive implies F . p = () \/ () ) & ( p is universal implies F . p = (F . ()) \ {()} ) ) ) ) );

definition
let A be QC-alphabet ;
let p be QC-formula of A;
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 () \ NAT;
existence
ex b1 being Relation st b1 well_orders () \ 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 () \ NAT );

definition
let A be QC-alphabet ;
let s, t be QC-symbol of A;
pred s <= t means :Def33: :: QC_LANG1:def 33
ex n, m being Nat st
( n = s & m = t & n <= m ) if ( s in NAT & t in NAT )
[s,t] in the Relation of A if ( not s in NAT & not t in NAT )
otherwise t in NAT ;
consistency
( s in NAT & t in NAT & not s in NAT & not t in NAT implies ( ex n, m being Nat st
( n = s & m = t & 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 & t in NAT implies ( s <= t iff ex n, m being Nat st
( n = s & m = t & n <= m ) ) ) & ( not s in NAT & not t in NAT implies ( s <= t iff [s,t] in the Relation of A ) ) & ( ( not s in NAT or not t in NAT ) & ( 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;
pred s < t means :: QC_LANG1:def 34
( s <= t & s <> t );
end;

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

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

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

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

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

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 ) by ;

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 ) by Th25;

definition
let A be QC-alphabet ;
let Y be non empty Subset of ();
func min Y -> QC-symbol of A means :Def35: :: QC_LANG1:def 35
( it in Y & ( 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 & ( for t being QC-symbol of A st t in Y holds
b1 <= t ) )
proof end;
uniqueness
for b1, b2 being QC-symbol of A st b1 in Y & ( for t being QC-symbol of A st t in Y holds
b1 <= t ) & b2 in Y & ( for t being QC-symbol of A st t in Y holds
b2 <= t ) holds
b1 = b2
proof end;
end;

:: deftheorem Def35 defines min QC_LANG1:def 35 :
for A being QC-alphabet
for Y being non empty Subset of ()
for b3 being QC-symbol of A holds
( b3 = min Y iff ( b3 in Y & ( 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
proof end;
uniqueness
for b1, b2 being QC-symbol of A st ( for t being QC-symbol of A holds b1 <= t ) & ( for t being QC-symbol of A holds b2 <= t ) holds
b1 = b2
proof end;
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 () 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 ()
proof end;
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;
func s ++ -> 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 ++
proof end;

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

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

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

definition
let A be QC-alphabet ;
let s be set ;
func s @ 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 ) & ( 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 ) & ( 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 Nat;
func t + n -> QC-symbol of A means :Def40: :: QC_LANG1:def 40
ex f being sequence of () st
( it = f . n & f . 0 = t & ( for k being Nat holds f . (k + 1) = (f . k) ++ ) );
existence
ex b1 being QC-symbol of A ex f being sequence of () st
( b1 = f . n & f . 0 = t & ( for k being Nat holds f . (k + 1) = (f . k) ++ ) )
proof end;
uniqueness
for b1, b2 being QC-symbol of A st ex f being sequence of () st
( b1 = f . n & f . 0 = t & ( for k being Nat holds f . (k + 1) = (f . k) ++ ) ) & ex f being sequence of () st
( b2 = f . n & f . 0 = t & ( for k being Nat holds f . (k + 1) = (f . k) ++ ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def40 defines + QC_LANG1:def 40 :
for A being QC-alphabet
for t being QC-symbol of A
for n being Nat
for b4 being QC-symbol of A holds
( b4 = t + n iff ex f being sequence of () st
( b4 = f . n & f . 0 = t & ( for k being Nat holds f . (k + 1) = (f . k) ++ ) ) );

theorem :: QC_LANG1:31
for A being QC-alphabet
for n being Nat
for t being QC-symbol of A holds t <= t + n
proof end;

definition
let A be QC-alphabet ;
let Y be set ;
func A -one_in Y -> QC-symbol of A equals :: QC_LANG1:def 41
the Element of Y if Y is non empty Subset of ()
otherwise 0 A;
coherence
( ( Y is non empty Subset of () implies the Element of Y is QC-symbol of A ) & ( Y is not non empty Subset of () implies 0 A is QC-symbol of A ) )
proof end;
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 () implies A -one_in Y = the Element of Y ) & ( Y is not non empty Subset of () implies A -one_in Y = 0 A ) );