:: by Piotr Rudnicki and Andrzej Trybulec

::

:: Received August 8, 1989

:: Copyright (c) 1990-2019 Association of Mizar Users

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

for D2 being set

for k1, k2, k3 being Element of D1 holds [:{k1,k2,k3},D2:] c= [:D1,D2:]

proof end;

definition

ex b_{1} being set st

( b_{1} is non empty set & ex X being set st

( NAT c= X & b_{1} = [:NAT,X:] ) )
end;

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 ( it is non empty set & ex X being set st

( NAT c= X & it = [:NAT,X:] ) );

ex b

( b

( NAT c= X & b

proof end;

:: deftheorem Def1 defines QC-alphabet QC_LANG1:def 1 :

for b_{1} being set holds

( b_{1} is QC-alphabet iff ( b_{1} is non empty set & ex X being set st

( NAT c= X & b_{1} = [:NAT,X:] ) ) );

for b

( b

( NAT c= X & b

registration

coherence

for b_{1} being QC-alphabet holds

( not b_{1} is empty & b_{1} is Relation-like )

end;
for b

( not b

proof end;

:: deftheorem defines QC-symbols QC_LANG1:def 2 :

for A being QC-alphabet holds QC-symbols A = rng A;

for A being QC-alphabet holds QC-symbols A = rng A;

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

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

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;

definition

let A be QC-alphabet ;

mode QC-variable of A is Element of QC-variables A;

[:{4},(QC-symbols A):] is Subset of (QC-variables A) by Lm1;

[:{5},(QC-symbols A):] is Subset of (QC-variables A) by Lm1;

coherence

[:{6},NAT:] is Subset of (QC-variables A) by Lm1;

{ [n,x] where n is Nat, x is QC-symbol of A : 7 <= n } is set ;

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

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

[:{5},(QC-symbols A):] is Subset of (QC-variables A) by Lm1;

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 } ;

{ [n,x] where n is Nat, x is QC-symbol of A : 7 <= n } is set ;

:: deftheorem defines bound_QC-variables QC_LANG1:def 4 :

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

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

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

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 } ;

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 ;

coherence

not QC-pred_symbols A is empty

end;
coherence

not bound_QC-variables A is empty ;

coherence

not fixed_QC-variables A is empty ;

coherence

not free_QC-variables A is empty ;

coherence

not QC-pred_symbols A is empty

proof end;

definition

let A be QC-alphabet ;

let P be Element of QC-pred_symbols A;

existence

ex b_{1} being Nat st P `1 = 7 + b_{1}

for b_{1}, b_{2} being Nat st P `1 = 7 + b_{1} & P `1 = 7 + b_{2} holds

b_{1} = b_{2}
;

end;
let P be Element of QC-pred_symbols A;

existence

ex b

proof end;

uniqueness for b

b

:: 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_{3} being Nat holds

( b_{3} = the_arity_of P iff P `1 = 7 + b_{3} );

for A being QC-alphabet

for P being Element of QC-pred_symbols A

for b

( b

definition

let A be QC-alphabet ;

let k be Nat;

{ P where P is QC-pred_symbol of A : the_arity_of P = k } is Subset of (QC-pred_symbols A)

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

{ P where P is QC-pred_symbol of A : the_arity_of P = k } is Subset of (QC-pred_symbols A)

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

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

registration

let k be Nat;

let A be QC-alphabet ;

ex b_{1} being FinSequence of QC-variables A st b_{1} is k -element

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

proof 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;
let A be QC-alphabet ;

mode QC-variable_list of k,A is k -element FinSequence of QC-variables A;

definition

let A be QC-alphabet ;

let D be set ;

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

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

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

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 ;

ex b_{1} being non empty set st

( b_{1} is A -closed & ( for D being non empty set st D is A -closed holds

b_{1} c= D ) )

for b_{1}, b_{2} being non empty set st b_{1} is A -closed & ( for D being non empty set st D is A -closed holds

b_{1} c= D ) & b_{2} is A -closed & ( for D being non empty set st D is A -closed holds

b_{2} c= D ) holds

b_{1} = b_{2}
;

end;
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 ( it is A -closed & ( for D being non empty set st D is A -closed holds

it c= D ) );

ex b

( b

b

proof end;

uniqueness for b

b

b

b

:: deftheorem Def11 defines QC-WFF QC_LANG1:def 11 :

for A being QC-alphabet

for b_{2} being non empty set holds

( b_{2} = QC-WFF A iff ( b_{2} is A -closed & ( for D being non empty set st D is A -closed holds

b_{2} c= D ) ) );

for A being QC-alphabet

for b

( b

b

registration

let A be QC-alphabet ;

existence

ex b_{1} being set st

( b_{1} is A -closed & not b_{1} is empty )

end;
existence

ex b

( b

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

coherence

<*P*> ^ l is Element of QC-WFF A

end;
let P be QC-pred_symbol of A;

let l be FinSequence of QC-variables A;

assume A1: the_arity_of P = len l ;

coherence

<*P*> ^ l is Element of QC-WFF A

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

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

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;

coherence

p is FinSequence of [:NAT,(QC-symbols A):]

end;
let p be Element of QC-WFF A;

coherence

p is FinSequence of [:NAT,(QC-symbols A):]

proof end;

:: deftheorem defines @ QC_LANG1:def 13 :

for A being QC-alphabet

for p being Element of QC-WFF A holds @ p = p;

for A being QC-alphabet

for p being Element of QC-WFF A holds @ p = p;

definition

let A be QC-alphabet ;

coherence

<*[0,0]*> is QC-formula of A

coherence

<*[1,0]*> ^ (@ p) is QC-formula of A

coherence

(<*[2,0]*> ^ (@ p)) ^ (@ q) is QC-formula of A

end;
coherence

<*[0,0]*> is QC-formula of A

proof end;

let p be Element of QC-WFF A;coherence

<*[1,0]*> ^ (@ p) is QC-formula of A

proof end;

let q be Element of QC-WFF A;coherence

(<*[2,0]*> ^ (@ p)) ^ (@ q) is QC-formula of A

proof end;

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

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

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;

coherence

(<*[3,0]*> ^ <*x*>) ^ (@ p) is QC-formula of A

end;
let x be bound_QC-variable of A;

let p be Element of QC-WFF A;

coherence

(<*[3,0]*> ^ <*x*>) ^ (@ p) is QC-formula of A

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

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_{1}() -> QC-alphabet , P_{1}[ Element of QC-WFF F_{1}()] } :

provided

QCInd{ F

provided

A1:
for k being Nat

for P being QC-pred_symbol of k,F_{1}()

for ll being QC-variable_list of k,F_{1}() holds P_{1}[P ! ll]
and

A2: P_{1}[ VERUM F_{1}()]
and

A3: for p being Element of QC-WFF F_{1}() st P_{1}[p] holds

P_{1}[ 'not' p]
and

A4: for p, q being Element of QC-WFF F_{1}() st P_{1}[p] & P_{1}[q] holds

P_{1}[p '&' q]
and

A5: for x being bound_QC-variable of F_{1}()

for p being Element of QC-WFF F_{1}() st P_{1}[p] holds

P_{1}[ All (x,p)]

for P being QC-pred_symbol of k,F

for ll being QC-variable_list of k,F

A2: P

A3: for p being Element of QC-WFF F

P

A4: for p, q being Element of QC-WFF F

P

A5: for x being bound_QC-variable of F

for p being Element of QC-WFF F

P

proof end;

definition

let A be QC-alphabet ;

let F be Element of QC-WFF A;

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

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 conjunctive means :Def20: :: QC_LANG1:def 20

ex p, q being Element of QC-WFF A st F = p '&' q;

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

ex x being bound_QC-variable of A ex p being Element of QC-WFF A st F = All (x,p);

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

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

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

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

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 )

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

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

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 ;

ex b_{1} 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_{1} = P & F = P ! ll )
by A1;

uniqueness

for b_{1}, b_{2} 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_{1} = 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_{2} = P & F = P ! ll ) holds

b_{1} = b_{2}

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

ex b

( b

uniqueness

for b

( b

( b

b

proof 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_{3} being QC-pred_symbol of A holds

( b_{3} = 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_{3} = P & F = P ! ll ) );

for A being QC-alphabet

for F being Element of QC-WFF A st F is atomic holds

for b

( b

( b

definition

let A be QC-alphabet ;

let F be Element of QC-WFF A;

assume A1: F is atomic ;

ex b_{1} 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_{1} = ll & F = P ! ll )
by A1;

uniqueness

for b_{1}, b_{2} 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_{1} = 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_{2} = ll & F = P ! ll ) holds

b_{1} = b_{2}

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

ex b

( b

uniqueness

for b

( b

( b

b

proof 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_{3} being FinSequence of QC-variables A holds

( b_{3} = 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_{3} = ll & F = P ! ll ) );

for A being QC-alphabet

for F being Element of QC-WFF A st F is atomic holds

for b

( b

( b

definition

let A be QC-alphabet ;

let F be Element of QC-WFF A;

assume A1: F is negative ;

existence

ex b_{1} being QC-formula of A st F = 'not' b_{1}
by A1;

uniqueness

for b_{1}, b_{2} being QC-formula of A st F = 'not' b_{1} & F = 'not' b_{2} holds

b_{1} = b_{2}
by FINSEQ_1:33;

end;
let F be Element of QC-WFF A;

assume A1: F is negative ;

existence

ex b

uniqueness

for b

b

:: 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_{3} being QC-formula of A holds

( b_{3} = the_argument_of F iff F = 'not' b_{3} );

for A being QC-alphabet

for F being Element of QC-WFF A st F is negative holds

for b

( b

definition

let A be QC-alphabet ;

let F be Element of QC-WFF A;

assume A1: F is conjunctive ;

ex b_{1} being QC-formula of A ex q being Element of QC-WFF A st F = b_{1} '&' q
by A1;

uniqueness

for b_{1}, b_{2} being QC-formula of A st ex q being Element of QC-WFF A st F = b_{1} '&' q & ex q being Element of QC-WFF A st F = b_{2} '&' q holds

b_{1} = b_{2}

end;
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 q being Element of QC-WFF A st F = it '&' q;

ex b

uniqueness

for b

b

proof 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_{3} being QC-formula of A holds

( b_{3} = the_left_argument_of F iff ex q being Element of QC-WFF A st F = b_{3} '&' q );

for A being QC-alphabet

for F being Element of QC-WFF A st F is conjunctive holds

for b

( b

definition

let A be QC-alphabet ;

let F be Element of QC-WFF A;

assume A1: F is conjunctive ;

ex b_{1} being QC-formula of A ex p being Element of QC-WFF A st F = p '&' b_{1}
by A1;

uniqueness

for b_{1}, b_{2} being QC-formula of A st ex p being Element of QC-WFF A st F = p '&' b_{1} & ex p being Element of QC-WFF A st F = p '&' b_{2} holds

b_{1} = b_{2}

end;
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 p being Element of QC-WFF A st F = p '&' it;

ex b

uniqueness

for b

b

proof 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_{3} being QC-formula of A holds

( b_{3} = the_right_argument_of F iff ex p being Element of QC-WFF A st F = p '&' b_{3} );

for A being QC-alphabet

for F being Element of QC-WFF A st F is conjunctive holds

for b

( b

definition

let A be QC-alphabet ;

let F be Element of QC-WFF A;

assume A1: F is universal ;

ex b_{1} being bound_QC-variable of A ex p being Element of QC-WFF A st F = All (b_{1},p)
by A1;

uniqueness

for b_{1}, b_{2} being bound_QC-variable of A st ex p being Element of QC-WFF A st F = All (b_{1},p) & ex p being Element of QC-WFF A st F = All (b_{2},p) holds

b_{1} = b_{2}

ex b_{1} being QC-formula of A ex x being bound_QC-variable of A st F = All (x,b_{1})
by A1;

uniqueness

for b_{1}, b_{2} being QC-formula of A st ex x being bound_QC-variable of A st F = All (x,b_{1}) & ex x being bound_QC-variable of A st F = All (x,b_{2}) holds

b_{1} = b_{2}

end;
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 p being Element of QC-WFF A st F = All (it,p);

ex b

uniqueness

for 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 x being bound_QC-variable of A st F = All (x,it);

ex b

uniqueness

for b

b

proof 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_{3} being bound_QC-variable of A holds

( b_{3} = bound_in F iff ex p being Element of QC-WFF A st F = All (b_{3},p) );

for A being QC-alphabet

for F being Element of QC-WFF A st F is universal holds

for b

( b

:: 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_{3} being QC-formula of A holds

( b_{3} = the_scope_of F iff ex x being bound_QC-variable of A st F = All (x,b_{3}) );

for A being QC-alphabet

for F being Element of QC-WFF A st F is universal holds

for b

( 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)

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

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)

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_{1}() -> QC-alphabet , P_{1}[ Element of QC-WFF F_{1}()] } :

provided

QCInd2{ F

provided

A1:
for p being Element of QC-WFF F_{1}() holds

( ( p is atomic implies P_{1}[p] ) & P_{1}[ VERUM F_{1}()] & ( p is negative & P_{1}[ the_argument_of p] implies P_{1}[p] ) & ( p is conjunctive & P_{1}[ the_left_argument_of p] & P_{1}[ the_right_argument_of p] implies P_{1}[p] ) & ( p is universal & P_{1}[ the_scope_of p] implies P_{1}[p] ) )

( ( p is atomic implies 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 )

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

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 )

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

( 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_{1}() -> QC-alphabet , F_{2}() -> non empty set , F_{3}() -> Element of F_{2}(), F_{4}( Element of QC-WFF F_{1}()) -> Element of F_{2}(), F_{5}( Element of F_{2}()) -> Element of F_{2}(), F_{6}( Element of F_{2}(), Element of F_{2}()) -> Element of F_{2}(), F_{7}( Element of QC-WFF F_{1}(), Element of F_{2}()) -> Element of F_{2}() } :

QCFuncEx{ F

ex F being Function of (QC-WFF F_{1}()),F_{2}() st

( F . (VERUM F_{1}()) = F_{3}() & ( for p being Element of QC-WFF F_{1}() holds

( ( p is atomic implies F . p = F_{4}(p) ) & ( p is negative implies F . p = F_{5}((F . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F_{6}((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = F_{7}(p,(F . (the_scope_of p))) ) ) ) )

( F . (VERUM F

( ( p is atomic implies F . p = F

proof end;

definition

let A be QC-alphabet ;

let ll be FinSequence of QC-variables A;

{ (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)

end;
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 ) } ;

{ (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;

:: 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 ) } ;

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;

ex b_{1} being Subset of (bound_QC-variables A) ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st

( b_{1} = 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)} ) ) ) )

for b_{1}, b_{2} being Subset of (bound_QC-variables A) st ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st

( b_{1} = 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_{2} = 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_{1} = b_{2}

end;
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 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)} ) ) ) );

ex b

( b

( 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

( 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 . (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

proof 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_{3} being Subset of (bound_QC-variables A) holds

( b_{3} = still_not-bound_in p iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st

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

for A being QC-alphabet

for p being QC-formula of A

for b

( b

( b

( 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)} ) ) ) ) );

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

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 ;

existence

ex b_{1} being Relation st b_{1} well_orders (QC-symbols A) \ NAT
by WELLORD2:17;

end;
existence

ex b

:: deftheorem Def32 defines Relation QC_LANG1:def 32 :

for A being QC-alphabet

for b_{2} being Relation holds

( b_{2} is Relation of A iff b_{2} well_orders (QC-symbols A) \ NAT );

for A being QC-alphabet

for b

( b

definition

let A be QC-alphabet ;

let s, t be QC-symbol of A;

( 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;
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 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 ;

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

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

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

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

for A being QC-alphabet

for s, t being QC-symbol of A holds

( s < t iff ( s <= t & s <> t ) );

theorem :: QC_LANG1:26

definition

let A be QC-alphabet ;

let Y be non empty Subset of (QC-symbols A);

ex b_{1} being QC-symbol of A st

( b_{1} in Y & ( for t being QC-symbol of A st t in Y holds

b_{1} <= t ) )

for b_{1}, b_{2} being QC-symbol of A st b_{1} in Y & ( for t being QC-symbol of A st t in Y holds

b_{1} <= t ) & b_{2} in Y & ( for t being QC-symbol of A st t in Y holds

b_{2} <= t ) holds

b_{1} = b_{2}

end;
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 ( it in Y & ( for t being QC-symbol of A st t in Y holds

it <= t ) );

ex b

( b

b

proof end;

uniqueness for b

b

b

b

proof 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_{3} being QC-symbol of A holds

( b_{3} = min Y iff ( b_{3} in Y & ( for t being QC-symbol of A st t in Y holds

b_{3} <= t ) ) );

for A being QC-alphabet

for Y being non empty Subset of (QC-symbols A)

for b

( b

b

definition

let A be QC-alphabet ;

existence

ex b_{1} being QC-symbol of A st

for t being QC-symbol of A holds b_{1} <= t

for b_{1}, b_{2} being QC-symbol of A st ( for t being QC-symbol of A holds b_{1} <= t ) & ( for t being QC-symbol of A holds b_{2} <= t ) holds

b_{1} = b_{2}

end;
existence

ex b

for t being QC-symbol of A holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines 0 QC_LANG1:def 36 :

for A being QC-alphabet

for b_{2} being QC-symbol of A holds

( b_{2} = 0 A iff for t being QC-symbol of A holds b_{2} <= t );

for A being QC-alphabet

for b

( b

definition

let A be QC-alphabet ;

let s be QC-symbol of A;

{ t where t is QC-symbol of A : s < t } is non empty Subset of (QC-symbols A)

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

{ t where t is QC-symbol of A : s < t } is non empty Subset of (QC-symbols A)

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

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

:: deftheorem defines ++ QC_LANG1:def 38 :

for A being QC-alphabet

for s being QC-symbol of A holds s ++ = min (Seg s);

for A being QC-alphabet

for s being QC-symbol of A holds s ++ = min (Seg s);

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

for Y1, Y2 being non empty Subset of (QC-symbols A) st Y1 c= Y2 holds

min Y2 <= min Y1

proof end;

theorem :: QC_LANG1:30

definition

let A be QC-alphabet ;

let s be set ;

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_{1} being QC-symbol of A holds verum;

by Th3;

end;
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 s if s is QC-symbol of A

otherwise 0 ;

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

by Th3;

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

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;

ex b_{1} being QC-symbol of A ex f being sequence of (QC-symbols A) st

( b_{1} = f . n & f . 0 = t & ( for k being Nat holds f . (k + 1) = (f . k) ++ ) )

for b_{1}, b_{2} being QC-symbol of A st ex f being sequence of (QC-symbols A) st

( b_{1} = 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_{2} = f . n & f . 0 = t & ( for k being Nat holds f . (k + 1) = (f . k) ++ ) ) holds

b_{1} = b_{2}

end;
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 f being sequence of (QC-symbols A) st

( it = f . n & f . 0 = t & ( for k being Nat holds f . (k + 1) = (f . k) ++ ) );

ex b

( b

proof end;

uniqueness for b

( b

( b

b

proof 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_{4} being QC-symbol of A holds

( b_{4} = t + n iff ex f being sequence of (QC-symbols A) st

( b_{4} = f . n & f . 0 = t & ( for k being Nat holds f . (k + 1) = (f . k) ++ ) ) );

for A being QC-alphabet

for t being QC-symbol of A

for n being Nat

for b

( b

( b

definition

let A be QC-alphabet ;

let Y be set ;

( ( 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 ) )

for b_{1} being QC-symbol of A holds verum
;

end;
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 the Element of Y if Y is non empty Subset of (QC-symbols A)

otherwise 0 A;

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

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

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