:: A First Order Language
:: by Piotr Rudnicki and Andrzej Trybulec
::
:: Received August 8, 1989
:: 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 b₁ being set st
( b₁ is non empty set & ex X being set st
( NAT c= X & b₁ = [:NAT,X:] ) )

proof end;

end;

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

registration

cluster -> Relation-like non empty for QC-alphabet ;

coherence
for b₁ being QC-alphabet holds
( not b₁ is empty & b₁ 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

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 )

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
[:{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 )

proof end;

theorem Th4: :: QC_LANG1:4

for A being QC-alphabet holds QC-variables A c= [:NAT,(QC-symbols A):]

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 (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 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},(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 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

proof end;

end;

theorem :: QC_LANG1:5

for A being QC-alphabet holds A = [:NAT,(QC-symbols A):]

proof end;

theorem Th6: :: QC_LANG1:6

for A being QC-alphabet holds QC-pred_symbols A c= [:NAT,(QC-symbols A):]

proof end;

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 -> Nat means :Def8: :: QC_LANG1:def 8
P `1 = 7 + it;

existence
ex b₁ being Nat st P `1 = 7 + b₁

proof end;

uniqueness
for b₁, b₂ being Nat st P `1 = 7 + b<sub>1</sub> & P `1 = 7 + b₂ holds
b₁ = b₂ ;

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 b₃ being Nat holds
( b₃ = the_arity_of P iff P `1 = 7 + b₃ );

definition

let A be QC-alphabet ;
let k be Nat;

func k -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)

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

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 Nat;
mode QC-pred_symbol of k,A is Element of k -ary_QC-pred_symbols A;

end;

registration

let k be Nat;
let A be QC-alphabet ;

cluster Relation-like NAT -defined QC-variables A -valued Function-like V41() k -element FinSequence-like FinSubsequence-like for FinSequence of QC-variables A;

existence
ex b₁ being FinSequence of QC-variables A st b₁ 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,(QC-symbols A):] *) & ( 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 ) & <*[0,0]*> in D & ( for p being FinSequence of [:NAT,(QC-symbols A):] st p in D holds
<*[1,0]*> ^ p in D ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):] 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,(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):] *) & ( 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 ) & <*[0,0]*> in D & ( for p being FinSequence of [:NAT,(QC-symbols A):] st p in D holds
<*[1,0]*> ^ p in D ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):] 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,(QC-symbols A):] 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,(QC-symbols A):]

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,(QC-symbols A):]

proof end;

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):]

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 b₁ being non empty set st
( b₁ is A -closed & ( for D being non empty set st D is A -closed holds
b₁ c= D ) )

proof end;

uniqueness
for b₁, b₂ being non empty set st b₁ is A -closed & ( for D being non empty set st D is A -closed holds
b₁ c= D ) & b₂ is A -closed & ( for D being non empty set st D is A -closed holds
b₂ c= D ) holds
b₁ = b₂ ;

end;

:: deftheorem Def11 defines QC-WFF QC_LANG1:def 11 :
for A being QC-alphabet
for b₂ being non empty set holds
( b₂ = QC-WFF A iff ( b₂ is A -closed & ( for D being non empty set st D is A -closed holds
b₂ 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 b₁ being set st
( b₁ is A -closed & not b₁ is empty )

proof end;

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 ;

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,(QC-symbols A):] *)

proof end;

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):]

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
<*[0,0]*>;

coherence
<*[0,0]*> 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 = <*[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 '&' 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{ F₁() -> QC-alphabet , P₁[ Element of QC-WFF F₁()] } :

for F being Element of QC-WFF F₁() holds P₁[F]

provided

A1: for k being Nat
for P being QC-pred_symbol of k,F₁()
for ll being QC-variable_list of k,F₁() holds P₁[P ! ll] and
A2: P₁[ VERUM F₁()] and
A3: for p being Element of QC-WFF F₁() st P₁[p] holds
P₁[ 'not' p] and
A4: for p, q being Element of QC-WFF F₁() st P₁[p] & P₁[q] holds
P₁[p '&' q] and
A5: for x being bound_QC-variable of F₁()
for p being Element of QC-WFF F₁() st P₁[p] holds
P₁[ 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 b₁ 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
( b₁ = P & F = P ! ll ) by A1;
uniqueness
for b₁, b₂ 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
( b₁ = 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
( b₂ = P & F = P ! ll ) holds
b₁ = b₂

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 b₃ being QC-pred_symbol of A holds
( b₃ = 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
( b₃ = 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 b₁ 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
( b₁ = ll & F = P ! ll ) by A1;
uniqueness
for b₁, b₂ 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
( b₁ = 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
( b₂ = ll & F = P ! ll ) holds
b₁ = b₂

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 b₃ being FinSequence of QC-variables A holds
( b₃ = 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
( b₃ = 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 b₁ being QC-formula of A st F = 'not' b₁ by A1;
uniqueness
for b₁, b₂ being QC-formula of A st F = 'not' b₁ & F = 'not' b₂ holds
b₁ = b₂ 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 b₃ being QC-formula of A holds
( b₃ = the_argument_of F iff F = 'not' b₃ );

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 b₁ being QC-formula of A ex q being Element of QC-WFF A st F = b₁ '&' q by A1;
uniqueness
for b₁, b₂ being QC-formula of A st ex q being Element of QC-WFF A st F = b₁ '&' q & ex q being Element of QC-WFF A st F = b₂ '&' q holds
b₁ = b₂

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 b₃ being QC-formula of A holds
( b₃ = the_left_argument_of F iff ex q being Element of QC-WFF A st F = b₃ '&' 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 b₁ being QC-formula of A ex p being Element of QC-WFF A st F = p '&' b₁ by A1;
uniqueness
for b₁, b₂ being QC-formula of A st ex p being Element of QC-WFF A st F = p '&' b₁ & ex p being Element of QC-WFF A st F = p '&' b₂ holds
b₁ = b₂

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 b₃ being QC-formula of A holds
( b₃ = the_right_argument_of F iff ex p being Element of QC-WFF A st F = p '&' b₃ );

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 b₁ being bound_QC-variable of A ex p being Element of QC-WFF A st F = All (b₁,p) by A1;
uniqueness
for b₁, b₂ being bound_QC-variable of A st ex p being Element of QC-WFF A st F = All (b₁,p) & ex p being Element of QC-WFF A st F = All (b₂,p) holds
b₁ = b₂

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 b₁ being QC-formula of A ex x being bound_QC-variable of A st F = All (x,b₁) by A1;
uniqueness
for b₁, b₂ being QC-formula of A st ex x being bound_QC-variable of A st F = All (x,b₁) & ex x being bound_QC-variable of A st F = All (x,b₂) holds
b₁ = b₂

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 b₃ being bound_QC-variable of A holds
( b₃ = bound_in F iff ex p being Element of QC-WFF A st F = All (b₃,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 b₃ being QC-formula of A holds
( b₃ = the_scope_of F iff ex x being bound_QC-variable of A st F = All (x,b₃) );

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)

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 (@ (the_left_argument_of p)) < len (@ p) & len (@ (the_right_argument_of p)) < 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 (@ (the_scope_of p)) < len (@ p)

proof end;

scheme :: QC_LANG1:sch 2
QCInd2{ F₁() -> QC-alphabet , P₁[ Element of QC-WFF F₁()] } :

for p being Element of QC-WFF F₁() holds P₁[p]

provided

A1: for p being Element of QC-WFF F₁() holds
( ( p is atomic implies P₁[p] ) & P₁[ VERUM F₁()] & ( p is negative & P₁[ the_argument_of p] implies P₁[p] ) & ( p is conjunctive & P₁[ the_left_argument_of p] & P₁[ the_right_argument_of p] implies P₁[p] ) & ( p is universal & P₁[ the_scope_of p] implies P₁[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
( ((@ (VERUM A)) . 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{ F₁() -> QC-alphabet , F₂() -> non empty set , F₃() -> Element of F₂(), F₄( Element of QC-WFF F₁()) -> Element of F₂(), F₅( Element of F₂()) -> Element of F₂(), F₆( Element of F₂(), Element of F₂()) -> Element of F₂(), F₇( Element of QC-WFF F₁(), Element of F₂()) -> Element of F₂() } :

ex F being Function of (QC-WFF F₁()),F₂() st
( F . (VERUM F₁()) = F₃() & ( for p being Element of QC-WFF F₁() holds
( ( p is atomic implies F . p = F₄(p) ) & ( p is negative implies F . p = F₅((F . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F₆((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = F₇(p,(F . (the_scope_of p))) ) ) ) )

proof end;

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 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 (bound_QC-variables A)

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 (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 & ( for p being Element of QC-WFF A holds
( F . (VERUM A) = {} & ( 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 A ) } ) & ( 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 b₁ being Subset of (bound_QC-variables A) ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( b₁ = F . p & ( for p being Element of QC-WFF A holds
( F . (VERUM A) = {} & ( 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 A ) } ) & ( 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 b₁, b₂ being Subset of (bound_QC-variables A) st ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( b₁ = F . p & ( for p being Element of QC-WFF A holds
( F . (VERUM A) = {} & ( 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 A ) } ) & ( 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 A),(bool (bound_QC-variables A)) st
( b₂ = F . p & ( for p being Element of QC-WFF A holds
( F . (VERUM A) = {} & ( 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 A ) } ) & ( 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
b₁ = b₂

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 b₃ being Subset of (bound_QC-variables A) holds
( b₃ = still_not-bound_in p iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( b₃ = F . p & ( for p being Element of QC-WFF A holds
( F . (VERUM A) = {} & ( 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 A ) } ) & ( 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 A be QC-alphabet ;
let p be QC-formula of A;

attr p 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 b₁ being Relation st b₁ well_orders (QC-symbols A) \ NAT by WELLORD2:17;

end;

:: deftheorem Def32 defines Relation QC_LANG1:def 32 :
for A being QC-alphabet
for b₂ being Relation holds
( b₂ is Relation of A iff b₂ well_orders (QC-symbols A) \ 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 Th23, Th24;

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 (QC-symbols A);

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 b₁ being QC-symbol of A st
( b₁ in Y & ( for t being QC-symbol of A st t in Y holds
b₁ <= t ) )

proof end;

uniqueness
for b₁, b₂ being QC-symbol of A st b₁ in Y & ( for t being QC-symbol of A st t in Y holds
b₁ <= t ) & b₂ in Y & ( for t being QC-symbol of A st t in Y holds
b₂ <= t ) holds
b₁ = b₂

proof end;

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 b₃ being QC-symbol of A holds
( b₃ = min Y iff ( b₃ in Y & ( for t being QC-symbol of A st t in Y holds
b₃ <= 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 b₁ being QC-symbol of A st
for t being QC-symbol of A holds b₁ <= t

proof end;

uniqueness
for b₁, b₂ being QC-symbol of A st ( for t being QC-symbol of A holds b₁ <= t ) & ( for t being QC-symbol of A holds b₂ <= t ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines 0 QC_LANG1:def 36 :
for A being QC-alphabet
for b₂ being QC-symbol of A holds
( b₂ = 0 A iff for t being QC-symbol of A holds b₂ <= 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)

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 (QC-symbols A) 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 Th21, Th25;

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 Th21, Th25;

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 b₁ 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 (QC-symbols A) st
( it = f . n & f . 0 = t & ( for k being Nat holds f . (k + 1) = (f . k) ++ ) );

existence
ex b₁ being QC-symbol of A ex f being sequence of (QC-symbols A) st
( b₁ = f . n & f . 0 = t & ( for k being Nat holds f . (k + 1) = (f . k) ++ ) )

proof end;

uniqueness
for b₁, b₂ being QC-symbol of A st ex f being sequence of (QC-symbols A) st
( b₁ = f . n & f . 0 = t & ( for k being Nat holds f . (k + 1) = (f . k) ++ ) ) & ex f being sequence of (QC-symbols A) st
( b₂ = f . n & f . 0 = t & ( for k being Nat holds f . (k + 1) = (f . k) ++ ) ) holds
b₁ = b₂

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 b₄ being QC-symbol of A holds
( b₄ = t + n iff ex f being sequence of (QC-symbols A) st
( b₄ = 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 (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 ) & ( Y is not non empty Subset of (QC-symbols A) implies 0 A is QC-symbol of A ) )

proof end;

consistency
for b₁ 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 ) & ( Y is not non empty Subset of (QC-symbols A) implies A -one_in Y = 0 A ) );