:: QC_LANG1 semantic presentation
begin
theorem :: QC_LANG1:1
for D1 being non empty set
for D2 being set
for k being Element of D1 holds [:{k},D2:] c= [:D1,D2:]
proof
let D1 be non empty set ; ::_thesis: for D2 being set
for k being Element of D1 holds [:{k},D2:] c= [:D1,D2:]
let D2 be set ; ::_thesis: for k being Element of D1 holds [:{k},D2:] c= [:D1,D2:]
let k be Element of D1; ::_thesis: [:{k},D2:] c= [:D1,D2:]
{k} is Subset of D1 by SUBSET_1:41;
hence [:{k},D2:] c= [:D1,D2:] by ZFMISC_1:95; ::_thesis: verum
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
let D1 be non empty set ; ::_thesis: for D2 being set
for k1, k2, k3 being Element of D1 holds [:{k1,k2,k3},D2:] c= [:D1,D2:]
let D2 be set ; ::_thesis: for k1, k2, k3 being Element of D1 holds [:{k1,k2,k3},D2:] c= [:D1,D2:]
let k1, k2, k3 be Element of D1; ::_thesis: [:{k1,k2,k3},D2:] c= [:D1,D2:]
{k1,k2,k3} is Subset of D1 by SUBSET_1:35;
hence [:{k1,k2,k3},D2:] c= [:D1,D2:] by ZFMISC_1:95; ::_thesis: verum
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
[:NAT,NAT:] = [:NAT,NAT:] ;
hence ex b1 being set st
( b1 is non empty set & ex X being set st
( NAT c= X & b1 = [:NAT,X:] ) ) ; ::_thesis: verum
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
let A be QC-alphabet ; ::_thesis: ( not A is empty & A is Relation-like )
ex X being set st
( NAT c= X & A = [:NAT,X:] ) by Def1;
hence ( not A is empty & A is Relation-like ) by Def1; ::_thesis: verum
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
let A be QC-alphabet ; ::_thesis: ( NAT c= QC-symbols A & 0 in QC-symbols A )
consider X being set such that
A1: ( NAT c= X & A = [:NAT,X:] ) by Def1;
A2: X <> {} by A1;
thus A3: NAT c= QC-symbols A by A1, A2, RELAT_1:160; ::_thesis: 0 in QC-symbols A
0 in NAT ;
hence 0 in QC-symbols A by A3; ::_thesis: verum
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
let A be QC-alphabet ; ::_thesis: ( [:{4},(QC-symbols A):] c= QC-variables A & [:{5},(QC-symbols A):] c= QC-variables A & [:{6},NAT:] c= QC-variables A )
{5} c= {4,5} by ZFMISC_1:7;
then A1: [:{5},(QC-symbols A):] c= [:{4,5},(QC-symbols A):] by ZFMISC_1:96;
{4} c= {4,5} by ZFMISC_1:7;
then [:{4},(QC-symbols A):] c= [:{4,5},(QC-symbols A):] by ZFMISC_1:96;
hence ( [:{4},(QC-symbols A):] c= QC-variables A & [:{5},(QC-symbols A):] c= QC-variables A & [:{6},NAT:] c= QC-variables A ) by A1, XBOOLE_1:10; ::_thesis: verum
end;
theorem Th4: :: QC_LANG1:4
for A being QC-alphabet holds QC-variables A c= [:NAT,(QC-symbols A):]
proof
let A be QC-alphabet ; ::_thesis: QC-variables A c= [:NAT,(QC-symbols A):]
( {6} c= NAT & NAT c= QC-symbols A ) by Th3, ZFMISC_1:31;
then A1: [:{6},NAT:] c= [:NAT,(QC-symbols A):] by ZFMISC_1:96;
( {4,5} c= NAT & QC-symbols A c= QC-symbols A ) by ZFMISC_1:32;
then [:{4,5},(QC-symbols A):] c= [:NAT,(QC-symbols A):] by ZFMISC_1:96;
hence QC-variables A c= [:NAT,(QC-symbols A):] by A1, XBOOLE_1:8; ::_thesis: verum
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 Element of NAT , x is QC-symbol of A : 7 <= n } ;
coherence
{ [n,x] where n is Element of NAT , x is QC-symbol of A : 7 <= n } is set ;
end;
:: deftheorem defines bound_QC-variables QC_LANG1:def_4_:_
for A being QC-alphabet holds bound_QC-variables A = [:{4},(QC-symbols A):];
:: deftheorem defines fixed_QC-variables QC_LANG1:def_5_:_
for A being QC-alphabet holds fixed_QC-variables A = [:{5},(QC-symbols A):];
:: deftheorem defines free_QC-variables QC_LANG1:def_6_:_
for A being QC-alphabet holds free_QC-variables A = [:{6},NAT:];
:: deftheorem defines QC-pred_symbols QC_LANG1:def_7_:_
for A being QC-alphabet holds QC-pred_symbols A = { [n,x] where n is Element of NAT , x is QC-symbol of A : 7 <= n } ;
registration
let A be QC-alphabet ;
cluster bound_QC-variables A -> non empty ;
coherence
not bound_QC-variables A is empty ;
cluster fixed_QC-variables A -> non empty ;
coherence
not fixed_QC-variables A is empty ;
cluster free_QC-variables A -> non empty ;
coherence
not free_QC-variables A is empty ;
cluster QC-pred_symbols A -> non empty ;
coherence
not QC-pred_symbols A is empty
proof
0 is QC-symbol of A by Th3;
then [7,0] in { [n,x] where n is Element of NAT , x is QC-symbol of A : 7 <= n } ;
hence not QC-pred_symbols A is empty ; ::_thesis: verum
end;
end;
theorem :: QC_LANG1:5
for A being QC-alphabet holds A = [:NAT,(QC-symbols A):]
proof
let A be QC-alphabet ; ::_thesis: A = [:NAT,(QC-symbols A):]
consider X being set such that
A1: ( NAT c= X & A = [:NAT,X:] ) by Def1;
X <> {} by A1;
hence A = [:NAT,(QC-symbols A):] by A1, RELAT_1:160; ::_thesis: verum
end;
theorem Th6: :: QC_LANG1:6
for A being QC-alphabet holds QC-pred_symbols A c= [:NAT,(QC-symbols A):]
proof
let A be QC-alphabet ; ::_thesis: QC-pred_symbols A c= [:NAT,(QC-symbols A):]
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in QC-pred_symbols A or y in [:NAT,(QC-symbols A):] )
assume y in QC-pred_symbols A ; ::_thesis: y in [:NAT,(QC-symbols A):]
then ex k being Element of NAT ex x being QC-symbol of A st
( y = [k,x] & 7 <= k ) ;
hence y in [:NAT,(QC-symbols A):] by ZFMISC_1:def_2; ::_thesis: verum
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 -> Element of NAT means :Def8: :: QC_LANG1:def 8
P `1 = 7 + it;
existence
ex b1 being Element of NAT st P `1 = 7 + b1
proof
P in { [k,x] where k is Element of NAT , x is QC-symbol of A : 7 <= k } ;
then consider k being Element of NAT , x being QC-symbol of A such that
A1: P = [k,x] and
A2: 7 <= k ;
consider w being Nat such that
A3: k = 7 + w by A2, NAT_1:10;
w in NAT by ORDINAL1:def_12;
hence ex b1 being Element of NAT st P `1 = 7 + b1 by A1, A3, MCART_1:7; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of 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 Element of NAT holds
( b3 = the_arity_of P iff P `1 = 7 + b3 );
definition
let A be QC-alphabet ;
let k be Element of NAT ;
funck -ary_QC-pred_symbols A -> Subset of (QC-pred_symbols A) equals :: QC_LANG1:def 9
{ P where P is QC-pred_symbol of A : the_arity_of P = k } ;
coherence
{ P where P is QC-pred_symbol of A : the_arity_of P = k } is Subset of (QC-pred_symbols A)
proof
set Y = {(7 + k)};
[:{(7 + k)},(QC-symbols A):] c= QC-pred_symbols A
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in [:{(7 + k)},(QC-symbols A):] or y in QC-pred_symbols A )
assume A1: y in [:{(7 + k)},(QC-symbols A):] ; ::_thesis: y in QC-pred_symbols A
then reconsider y1 = y `1 as Element of NAT by MCART_1:12;
reconsider y2 = y `2 as QC-symbol of A by A1, MCART_1:12;
y `1 = 7 + k by A1, MCART_1:12;
then 7 <= y1 by NAT_1:12;
then [y1,y2] in { [m,x] where m is Element of NAT , x is QC-symbol of A : 7 <= m } ;
hence y in QC-pred_symbols A by A1, MCART_1:21; ::_thesis: verum
end;
then reconsider X = [:{(7 + k)},(QC-symbols A):] as Subset of (QC-pred_symbols A) ;
X = { P where P is QC-pred_symbol of A : the_arity_of P = k }
proof
thus X c= { P where P is QC-pred_symbol of A : the_arity_of P = k } :: according to XBOOLE_0:def_10 ::_thesis: { P where P is QC-pred_symbol of A : the_arity_of P = k } c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in { P where P is QC-pred_symbol of A : the_arity_of P = k } )
assume A2: x in X ; ::_thesis: x in { P where P is QC-pred_symbol of A : the_arity_of P = k }
then reconsider Q = x as QC-pred_symbol of A ;
x `1 in {(7 + k)} by A2, MCART_1:10;
then x `1 = 7 + k by TARSKI:def_1;
then the_arity_of Q = k by Def8;
hence x in { P where P is QC-pred_symbol of A : the_arity_of P = k } ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { P where P is QC-pred_symbol of A : the_arity_of P = k } or x in X )
assume x in { P where P is QC-pred_symbol of A : the_arity_of P = k } ; ::_thesis: x in X
then consider P being QC-pred_symbol of A such that
A3: x = P and
A4: the_arity_of P = k ;
P `1 = 7 + k by A4, Def8;
then A5: P `1 in {(7 + k)} by TARSKI:def_1;
A6: QC-pred_symbols A c= [:NAT,(QC-symbols A):] by Th6;
then P in [:NAT,(QC-symbols A):] by TARSKI:def_3;
then P `2 in QC-symbols A by MCART_1:10;
then [(P `1),(P `2)] in X by A5, ZFMISC_1:87;
hence x in X by A3, A6, MCART_1:21; ::_thesis: verum
end;
hence { P where P is QC-pred_symbol of A : the_arity_of P = k } is Subset of (QC-pred_symbols A) ; ::_thesis: verum
end;
end;
:: deftheorem defines -ary_QC-pred_symbols QC_LANG1:def_9_:_
for A being QC-alphabet
for k being Element of NAT holds k -ary_QC-pred_symbols A = { P where P is QC-pred_symbol of A : the_arity_of P = k } ;
registration
let k be Element of NAT ;
let A be QC-alphabet ;
clusterk -ary_QC-pred_symbols A -> non empty ;
coherence
not k -ary_QC-pred_symbols A is empty
proof
set Y = {(7 + k)};
[:{(7 + k)},(QC-symbols A):] c= QC-pred_symbols A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [:{(7 + k)},(QC-symbols A):] or x in QC-pred_symbols A )
assume A1: x in [:{(7 + k)},(QC-symbols A):] ; ::_thesis: x in QC-pred_symbols A
then reconsider x1 = x `1 as Element of NAT by MCART_1:12;
reconsider x2 = x `2 as QC-symbol of A by MCART_1:12, A1;
x `1 = 7 + k by A1, MCART_1:12;
then 7 <= x1 by NAT_1:12;
then [x1,x2] in { [m,y] where m is Element of NAT , y is QC-symbol of A : 7 <= m } ;
hence x in QC-pred_symbols A by A1, MCART_1:21; ::_thesis: verum
end;
then reconsider X = [:{(7 + k)},(QC-symbols A):] as non empty Subset of (QC-pred_symbols A) ;
X = { P where P is QC-pred_symbol of A : the_arity_of P = k }
proof
thus X c= { P where P is QC-pred_symbol of A : the_arity_of P = k } :: according to XBOOLE_0:def_10 ::_thesis: { P where P is QC-pred_symbol of A : the_arity_of P = k } c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in { P where P is QC-pred_symbol of A : the_arity_of P = k } )
assume A2: x in X ; ::_thesis: x in { P where P is QC-pred_symbol of A : the_arity_of P = k }
then reconsider Q = x as QC-pred_symbol of A ;
x `1 in {(7 + k)} by A2, MCART_1:10;
then x `1 = 7 + k by TARSKI:def_1;
then the_arity_of Q = k by Def8;
hence x in { P where P is QC-pred_symbol of A : the_arity_of P = k } ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { P where P is QC-pred_symbol of A : the_arity_of P = k } or x in X )
assume x in { P where P is QC-pred_symbol of A : the_arity_of P = k } ; ::_thesis: x in X
then consider P being QC-pred_symbol of A such that
A3: x = P and
A4: the_arity_of P = k ;
P `1 = 7 + k by A4, Def8;
then A5: P `1 in {(7 + k)} by TARSKI:def_1;
A6: QC-pred_symbols A c= [:NAT,(QC-symbols A):] by Th6;
then P in [:NAT,(QC-symbols A):] by TARSKI:def_3;
then P `2 in QC-symbols A by MCART_1:10;
then [(P `1),(P `2)] in X by A5, ZFMISC_1:87;
hence x in X by A3, A6, MCART_1:21; ::_thesis: verum
end;
hence not k -ary_QC-pred_symbols A is empty ; ::_thesis: verum
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 Element of NAT ;
mode QC-pred_symbol of k,A is Element of k -ary_QC-pred_symbols A;
end;
registration
let k be Element of NAT ;
let A be QC-alphabet ;
cluster Relation-like NAT -defined QC-variables A -valued Function-like V35() k -element FinSequence-like FinSubsequence-like for FinSequence of QC-variables A;
existence
ex b1 being FinSequence of QC-variables A st b1 is k -element
proof
consider p being FinSequence of QC-variables A such that
A1: len p = k by FINSEQ_1:19;
take p ; ::_thesis: p is k -element
thus len p = k by A1; :: according to CARD_1:def_7 ::_thesis: verum
end;
end;
definition
let k be Element of NAT ;
let A be QC-alphabet ;
mode QC-variable_list of k,A is k -element FinSequence of QC-variables A;
end;
definition
let A be QC-alphabet ;
let D be set ;
attrD is A -closed means :Def10: :: QC_LANG1:def 10
( D is Subset of ([:NAT,(QC-symbols A):] *) & ( for k being Element of NAT
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds <*p*> ^ ll in D ) & <*[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 Element of NAT
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds <*p*> ^ ll in D ) & <*[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 Element of NAT
for x being QC-symbol of A holds <*[k,x]*> is FinSequence of [:NAT,(QC-symbols A):]
proof
let A be QC-alphabet ; ::_thesis: for k being Element of NAT
for x being QC-symbol of A holds <*[k,x]*> is FinSequence of [:NAT,(QC-symbols A):]
let k be Element of NAT ; ::_thesis: for x being QC-symbol of A holds <*[k,x]*> is FinSequence of [:NAT,(QC-symbols A):]
let x be QC-symbol of A; ::_thesis: <*[k,x]*> is FinSequence of [:NAT,(QC-symbols A):]
[k,x] in [:NAT,(QC-symbols A):] by ZFMISC_1:def_2;
then ( rng <*[k,x]*> = {[k,x]} & {[k,x]} c= [:NAT,(QC-symbols A):] ) by FINSEQ_1:39, ZFMISC_1:31;
hence <*[k,x]*> is FinSequence of [:NAT,(QC-symbols A):] by FINSEQ_1:def_4; ::_thesis: verum
end;
Lm3: for A being QC-alphabet
for k being Element of NAT
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds <*p*> ^ ll is FinSequence of [:NAT,(QC-symbols A):]
proof
let A be QC-alphabet ; ::_thesis: for k being Element of NAT
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds <*p*> ^ ll is FinSequence of [:NAT,(QC-symbols A):]
let k be Element of NAT ; ::_thesis: 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):]
let p be QC-pred_symbol of k,A; ::_thesis: for ll being QC-variable_list of k,A holds <*p*> ^ ll is FinSequence of [:NAT,(QC-symbols A):]
let ll be QC-variable_list of k,A; ::_thesis: <*p*> ^ ll is FinSequence of [:NAT,(QC-symbols A):]
QC-variables A c= [:NAT,(QC-symbols A):] by Th4;
then A1: rng ll c= [:NAT,(QC-symbols A):] by XBOOLE_1:1;
QC-pred_symbols A c= [:NAT,(QC-symbols A):] by Th6;
then k -ary_QC-pred_symbols A c= [:NAT,(QC-symbols A):] by XBOOLE_1:1;
then rng <*p*> c= [:NAT,(QC-symbols A):] by XBOOLE_1:1;
then (rng <*p*>) \/ (rng ll) c= [:NAT,(QC-symbols A):] by A1, XBOOLE_1:8;
then rng (<*p*> ^ ll) c= [:NAT,(QC-symbols A):] by FINSEQ_1:31;
hence <*p*> ^ ll is FinSequence of [:NAT,(QC-symbols A):] by FINSEQ_1:def_4; ::_thesis: verum
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
let A be QC-alphabet ; ::_thesis: 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):]
A1: 0 is QC-symbol of A by Th3;
reconsider y = <*[3,0]*> as FinSequence of [:NAT,(QC-symbols A):] by A1, Lm2;
let x be bound_QC-variable of A; ::_thesis: for p being FinSequence of [:NAT,(QC-symbols A):] holds (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,(QC-symbols A):]
let p be FinSequence of [:NAT,(QC-symbols A):]; ::_thesis: (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,(QC-symbols A):]
QC-variables A c= [:NAT,(QC-symbols A):] by Th4;
then bound_QC-variables A c= [:NAT,(QC-symbols A):] by XBOOLE_1:1;
then rng <*x*> c= [:NAT,(QC-symbols A):] by XBOOLE_1:1;
then reconsider z = <*x*> as FinSequence of [:NAT,(QC-symbols A):] by FINSEQ_1:def_4;
(y ^ z) ^ p is FinSequence of [:NAT,(QC-symbols A):] ;
hence (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,(QC-symbols A):] ; ::_thesis: verum
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
0 is QC-symbol of A by Th3;
then <*[0,0]*> is FinSequence of [:NAT,(QC-symbols A):] by Lm2;
then A1: <*[0,0]*> in [:NAT,(QC-symbols A):] * by FINSEQ_1:def_11;
defpred S1[ set ] means for D being non empty set st D is A -closed holds
$1 in D;
consider D0 being set such that
A2: for x being set holds
( x in D0 iff ( x in [:NAT,(QC-symbols A):] * & S1[x] ) ) from XBOOLE_0:sch_1();
A3: for D being non empty set st D is A -closed holds
<*[0,0]*> in D by Def10;
then reconsider D0 = D0 as non empty set by A2, A1;
take D0 ; ::_thesis: ( D0 is A -closed & ( for D being non empty set st D is A -closed holds
D0 c= D ) )
D0 c= [:NAT,(QC-symbols A):] *
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D0 or x in [:NAT,(QC-symbols A):] * )
thus ( not x in D0 or x in [:NAT,(QC-symbols A):] * ) by A2; ::_thesis: verum
end;
hence D0 is Subset of ([:NAT,(QC-symbols A):] *) ; :: according to QC_LANG1:def_10 ::_thesis: ( ( for k being Element of NAT
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds <*p*> ^ ll in D0 ) & <*[0,0]*> in D0 & ( for p being FinSequence of [:NAT,(QC-symbols A):] st p in D0 holds
<*[1,0]*> ^ p in D0 ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):] st p in D0 & q in D0 holds
(<*[2,0]*> ^ p) ^ q in D0 ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):] st p in D0 holds
(<*[3,0]*> ^ <*x*>) ^ p in D0 ) & ( for D being non empty set st D is A -closed holds
D0 c= D ) )
thus for k being Element of NAT
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds <*p*> ^ ll in D0 ::_thesis: ( <*[0,0]*> in D0 & ( for p being FinSequence of [:NAT,(QC-symbols A):] st p in D0 holds
<*[1,0]*> ^ p in D0 ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):] st p in D0 & q in D0 holds
(<*[2,0]*> ^ p) ^ q in D0 ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):] st p in D0 holds
(<*[3,0]*> ^ <*x*>) ^ p in D0 ) & ( for D being non empty set st D is A -closed holds
D0 c= D ) )
proof
let k be Element of NAT ; ::_thesis: for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds <*p*> ^ ll in D0
let p be QC-pred_symbol of k,A; ::_thesis: for ll being QC-variable_list of k,A holds <*p*> ^ ll in D0
let ll be QC-variable_list of k,A; ::_thesis: <*p*> ^ ll in D0
<*p*> ^ ll is FinSequence of [:NAT,(QC-symbols A):] by Lm3;
then A4: <*p*> ^ ll in [:NAT,(QC-symbols A):] * by FINSEQ_1:def_11;
for D being non empty set st D is A -closed holds
<*p*> ^ ll in D by Def10;
hence <*p*> ^ ll in D0 by A2, A4; ::_thesis: verum
end;
thus <*[0,0]*> in D0 by A2, A1, A3; ::_thesis: ( ( for p being FinSequence of [:NAT,(QC-symbols A):] st p in D0 holds
<*[1,0]*> ^ p in D0 ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):] st p in D0 & q in D0 holds
(<*[2,0]*> ^ p) ^ q in D0 ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):] st p in D0 holds
(<*[3,0]*> ^ <*x*>) ^ p in D0 ) & ( for D being non empty set st D is A -closed holds
D0 c= D ) )
thus for p being FinSequence of [:NAT,(QC-symbols A):] st p in D0 holds
<*[1,0]*> ^ p in D0 ::_thesis: ( ( for p, q being FinSequence of [:NAT,(QC-symbols A):] st p in D0 & q in D0 holds
(<*[2,0]*> ^ p) ^ q in D0 ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):] st p in D0 holds
(<*[3,0]*> ^ <*x*>) ^ p in D0 ) & ( for D being non empty set st D is A -closed holds
D0 c= D ) )
proof
A5: 0 is QC-symbol of A by Th3;
reconsider h = <*[1,0]*> as FinSequence of [:NAT,(QC-symbols A):] by Lm2, A5;
let p be FinSequence of [:NAT,(QC-symbols A):]; ::_thesis: ( p in D0 implies <*[1,0]*> ^ p in D0 )
assume A6: p in D0 ; ::_thesis: <*[1,0]*> ^ p in D0
A7: for D being non empty set st D is A -closed holds
<*[1,0]*> ^ p in D
proof
let D be non empty set ; ::_thesis: ( D is A -closed implies <*[1,0]*> ^ p in D )
assume A8: D is A -closed ; ::_thesis: <*[1,0]*> ^ p in D
then p in D by A2, A6;
hence <*[1,0]*> ^ p in D by A8, Def10; ::_thesis: verum
end;
h ^ p is FinSequence of [:NAT,(QC-symbols A):] ;
then <*[1,0]*> ^ p in [:NAT,(QC-symbols A):] * by FINSEQ_1:def_11;
hence <*[1,0]*> ^ p in D0 by A2, A7; ::_thesis: verum
end;
thus for p, q being FinSequence of [:NAT,(QC-symbols A):] st p in D0 & q in D0 holds
(<*[2,0]*> ^ p) ^ q in D0 ::_thesis: ( ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):] st p in D0 holds
(<*[3,0]*> ^ <*x*>) ^ p in D0 ) & ( for D being non empty set st D is A -closed holds
D0 c= D ) )
proof
A9: 0 is QC-symbol of A by Th3;
reconsider h = <*[2,0]*> as FinSequence of [:NAT,(QC-symbols A):] by A9, Lm2;
let p, q be FinSequence of [:NAT,(QC-symbols A):]; ::_thesis: ( p in D0 & q in D0 implies (<*[2,0]*> ^ p) ^ q in D0 )
assume A10: ( p in D0 & q in D0 ) ; ::_thesis: (<*[2,0]*> ^ p) ^ q in D0
A11: for D being non empty set st D is A -closed holds
(<*[2,0]*> ^ p) ^ q in D
proof
let D be non empty set ; ::_thesis: ( D is A -closed implies (<*[2,0]*> ^ p) ^ q in D )
assume A12: D is A -closed ; ::_thesis: (<*[2,0]*> ^ p) ^ q in D
then ( p in D & q in D ) by A2, A10;
hence (<*[2,0]*> ^ p) ^ q in D by A12, Def10; ::_thesis: verum
end;
(h ^ p) ^ q is FinSequence of [:NAT,(QC-symbols A):] ;
then (<*[2,0]*> ^ p) ^ q in [:NAT,(QC-symbols A):] * by FINSEQ_1:def_11;
hence (<*[2,0]*> ^ p) ^ q in D0 by A2, A11; ::_thesis: verum
end;
thus for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):] st p in D0 holds
(<*[3,0]*> ^ <*x*>) ^ p in D0 ::_thesis: for D being non empty set st D is A -closed holds
D0 c= D
proof
let x be bound_QC-variable of A; ::_thesis: for p being FinSequence of [:NAT,(QC-symbols A):] st p in D0 holds
(<*[3,0]*> ^ <*x*>) ^ p in D0
let p be FinSequence of [:NAT,(QC-symbols A):]; ::_thesis: ( p in D0 implies (<*[3,0]*> ^ <*x*>) ^ p in D0 )
assume A13: p in D0 ; ::_thesis: (<*[3,0]*> ^ <*x*>) ^ p in D0
A14: for D being non empty set st D is A -closed holds
(<*[3,0]*> ^ <*x*>) ^ p in D
proof
let D be non empty set ; ::_thesis: ( D is A -closed implies (<*[3,0]*> ^ <*x*>) ^ p in D )
assume A15: D is A -closed ; ::_thesis: (<*[3,0]*> ^ <*x*>) ^ p in D
then p in D by A2, A13;
hence (<*[3,0]*> ^ <*x*>) ^ p in D by A15, Def10; ::_thesis: verum
end;
(<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,(QC-symbols A):] by Lm4;
then (<*[3,0]*> ^ <*x*>) ^ p in [:NAT,(QC-symbols A):] * by FINSEQ_1:def_11;
hence (<*[3,0]*> ^ <*x*>) ^ p in D0 by A2, A14; ::_thesis: verum
end;
let D be non empty set ; ::_thesis: ( D is A -closed implies D0 c= D )
assume A16: D is A -closed ; ::_thesis: D0 c= D
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D0 or x in D )
assume x in D0 ; ::_thesis: x in D
hence x in D by A2, A16; ::_thesis: verum
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
proof
let D1, D2 be non empty set ; ::_thesis: ( D1 is A -closed & ( for D being non empty set st D is A -closed holds
D1 c= D ) & D2 is A -closed & ( for D being non empty set st D is A -closed holds
D2 c= D ) implies D1 = D2 )
assume ( D1 is A -closed & ( for D being non empty set st D is A -closed holds
D1 c= D ) & D2 is A -closed & ( for D being non empty set st D is A -closed holds
D2 c= D ) ) ; ::_thesis: D1 = D2
then ( D1 c= D2 & D2 c= D1 ) ;
hence D1 = D2 by XBOOLE_0:def_10; ::_thesis: verum
end;
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
QC-WFF A is A -closed by Def11;
hence ex b1 being set st
( b1 is A -closed & not b1 is empty ) ; ::_thesis: verum
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 ;
funcP ! l -> Element of QC-WFF A equals :Def12: :: QC_LANG1:def 12
<*P*> ^ l;
coherence
<*P*> ^ l is Element of QC-WFF A
proof
set k = len l;
set QCP = { Q where Q is QC-pred_symbol of A : the_arity_of Q = len l } ;
P in { Q where Q is QC-pred_symbol of A : the_arity_of Q = len l } by A1;
then reconsider P = P as QC-pred_symbol of (len l),A ;
reconsider l = l as QC-variable_list of len l,A by CARD_1:def_7;
A2: QC-WFF A is non empty A -closed set by Def11;
for D being non empty A -closed set holds <*P*> ^ l in D by Def10;
hence <*P*> ^ l is Element of QC-WFF A by A2; ::_thesis: verum
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 Element of NAT
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds p ! ll = <*p*> ^ ll
proof
let A be QC-alphabet ; ::_thesis: for k being Element of NAT
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds p ! ll = <*p*> ^ ll
let k be Element of NAT ; ::_thesis: for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds p ! ll = <*p*> ^ ll
let p be QC-pred_symbol of k,A; ::_thesis: for ll being QC-variable_list of k,A holds p ! ll = <*p*> ^ ll
let ll be QC-variable_list of k,A; ::_thesis: p ! ll = <*p*> ^ ll
set QCP = { Q where Q is QC-pred_symbol of A : the_arity_of Q = k } ;
p in { Q where Q is QC-pred_symbol of A : the_arity_of Q = k } ;
then A1: ex Q being QC-pred_symbol of A st
( p = Q & the_arity_of Q = k ) ;
len ll = k by CARD_1:def_7;
hence p ! ll = <*p*> ^ ll by A1, Def12; ::_thesis: verum
end;
Lm5: for A being QC-alphabet holds QC-WFF A is Subset of ([:NAT,(QC-symbols A):] *)
proof
let A be QC-alphabet ; ::_thesis: QC-WFF A is Subset of ([:NAT,(QC-symbols A):] *)
A1: QC-WFF A is non empty A -closed set by Def11;
thus QC-WFF A is Subset of ([:NAT,(QC-symbols A):] *) by A1, Def10; ::_thesis: verum
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
( QC-WFF A is Subset of ([:NAT,(QC-symbols A):] *) & p in QC-WFF A ) by Lm5;
hence p is FinSequence of [:NAT,(QC-symbols A):] by FINSEQ_1:def_11; ::_thesis: verum
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
QC-WFF A is non empty A -closed set by Def11;
hence <*[0,0]*> is QC-formula of A by Def10; ::_thesis: verum
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
QC-WFF A is non empty A -closed set by Def11;
hence <*[1,0]*> ^ (@ p) is QC-formula of A by Def10; ::_thesis: verum
end;
let q be Element of QC-WFF A;
funcp '&' 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
QC-WFF A is non empty A -closed set by Def11;
hence (<*[2,0]*> ^ (@ p)) ^ (@ q) is QC-formula of A by Def10; ::_thesis: verum
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
QC-WFF A is non empty A -closed set by Def11;
hence (<*[3,0]*> ^ <*x*>) ^ (@ p) is QC-formula of A by Def10; ::_thesis: verum
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 Element of NAT
for P being QC-pred_symbol of k,F1()
for ll being QC-variable_list of k,F1() holds P1[P ! ll] and
A2: P1[ VERUM F1()] and
A3: for p being Element of QC-WFF F1() st P1[p] holds
P1[ 'not' p] and
A4: for p, q being Element of QC-WFF F1() st P1[p] & 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
VERUM F1() in { F where F is Element of QC-WFF F1() : P1[F] } by A2;
then reconsider X = { F where F is Element of QC-WFF F1() : P1[F] } as non empty set ;
A6: for k being Element of NAT
for P being QC-pred_symbol of k,F1()
for ll being QC-variable_list of k,F1() holds <*P*> ^ ll in X
proof
let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,F1()
for ll being QC-variable_list of k,F1() holds <*P*> ^ ll in X
let P be QC-pred_symbol of k,F1(); ::_thesis: for ll being QC-variable_list of k,F1() holds <*P*> ^ ll in X
let ll be QC-variable_list of k,F1(); ::_thesis: <*P*> ^ ll in X
P1[P ! ll] by A1;
then P ! ll in X ;
hence <*P*> ^ ll in X by Th8; ::_thesis: verum
end;
A7: for x being bound_QC-variable of F1()
for p being FinSequence of [:NAT,(QC-symbols F1()):] st p in X holds
(<*[3,0]*> ^ <*x*>) ^ p in X
proof
let x be bound_QC-variable of F1(); ::_thesis: for p being FinSequence of [:NAT,(QC-symbols F1()):] st p in X holds
(<*[3,0]*> ^ <*x*>) ^ p in X
let p be FinSequence of [:NAT,(QC-symbols F1()):]; ::_thesis: ( p in X implies (<*[3,0]*> ^ <*x*>) ^ p in X )
assume p in X ; ::_thesis: (<*[3,0]*> ^ <*x*>) ^ p in X
then consider p9 being Element of QC-WFF F1() such that
A8: p = p9 and
A9: P1[p9] ;
P1[ All (x,p9)] by A5, A9;
hence (<*[3,0]*> ^ <*x*>) ^ p in X by A8; ::_thesis: verum
end;
A10: for p, q being FinSequence of [:NAT,(QC-symbols F1()):] st p in X & q in X holds
(<*[2,0]*> ^ p) ^ q in X
proof
let p, q be FinSequence of [:NAT,(QC-symbols F1()):]; ::_thesis: ( p in X & q in X implies (<*[2,0]*> ^ p) ^ q in X )
assume p in X ; ::_thesis: ( not q in X or (<*[2,0]*> ^ p) ^ q in X )
then consider p9 being Element of QC-WFF F1() such that
A11: p = p9 and
A12: P1[p9] ;
assume q in X ; ::_thesis: (<*[2,0]*> ^ p) ^ q in X
then consider q9 being Element of QC-WFF F1() such that
A13: q = q9 and
A14: P1[q9] ;
P1[p9 '&' q9] by A4, A12, A14;
hence (<*[2,0]*> ^ p) ^ q in X by A11, A13; ::_thesis: verum
end;
A15: for p being FinSequence of [:NAT,(QC-symbols F1()):] st p in X holds
<*[1,0]*> ^ p in X
proof
let p be FinSequence of [:NAT,(QC-symbols F1()):]; ::_thesis: ( p in X implies <*[1,0]*> ^ p in X )
assume p in X ; ::_thesis: <*[1,0]*> ^ p in X
then consider p9 being Element of QC-WFF F1() such that
A16: p = p9 and
A17: P1[p9] ;
P1[ 'not' p9] by A3, A17;
hence <*[1,0]*> ^ p in X by A16; ::_thesis: verum
end;
let F9 be Element of QC-WFF F1(); ::_thesis: P1[F9]
A18: X c= [:NAT,(QC-symbols F1()):] *
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in [:NAT,(QC-symbols F1()):] * )
assume x in X ; ::_thesis: x in [:NAT,(QC-symbols F1()):] *
then consider p being Element of QC-WFF F1() such that
A19: x = p and
P1[p] ;
p = @ p ;
hence x in [:NAT,(QC-symbols F1()):] * by A19, FINSEQ_1:def_11; ::_thesis: verum
end;
A20: <*[0,0]*> in X by A2;
X is F1() -closed by A6, A18, A20, A15, A10, A7, Def10;
then QC-WFF F1() c= X by Def11;
then F9 in X by TARSKI:def_3;
then ex F99 being Element of QC-WFF F1() st
( F9 = F99 & P1[F99] ) ;
hence P1[F9] ; ::_thesis: verum
end;
definition
let A be QC-alphabet ;
let F be Element of QC-WFF A;
attrF is atomic means :Def18: :: QC_LANG1:def 18
ex k being Element of NAT ex p being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A st F = p ! ll;
attrF is negative means :Def19: :: QC_LANG1:def 19
ex p being Element of QC-WFF A st F = 'not' p;
attrF is conjunctive means :Def20: :: QC_LANG1:def 20
ex p, q being Element of QC-WFF A st F = p '&' q;
attrF is universal means :Def21: :: QC_LANG1:def 21
ex x being bound_QC-variable of A ex p being Element of QC-WFF A st F = All (x,p);
end;
:: deftheorem Def18 defines atomic QC_LANG1:def_18_:_
for A being QC-alphabet
for F being Element of QC-WFF A holds
( F is atomic iff ex k being Element of NAT ex p being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A st F = p ! ll );
:: deftheorem Def19 defines negative QC_LANG1:def_19_:_
for A being QC-alphabet
for F being Element of QC-WFF A holds
( F is negative iff ex p being Element of QC-WFF A st F = 'not' p );
:: deftheorem Def20 defines conjunctive QC_LANG1:def_20_:_
for A being QC-alphabet
for F being Element of QC-WFF A holds
( F is conjunctive iff ex p, q being Element of QC-WFF A st F = p '&' 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
let A be QC-alphabet ; ::_thesis: 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 )
defpred S1[ Element of QC-WFF A] means ( $1 = VERUM A or $1 is atomic or $1 is negative or $1 is conjunctive or $1 is universal );
A1: S1[ VERUM A] ;
A2: for p being Element of QC-WFF A st S1[p] holds
S1[ 'not' p] by Def19;
A3: for x being bound_QC-variable of A
for p being Element of QC-WFF A st S1[p] holds
S1[ All (x,p)] by Def21;
A4: for p, q being Element of QC-WFF A st S1[p] & S1[q] holds
S1[p '&' q] by Def20;
A5: for k being Element of NAT
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds S1[p ! ll] by Def18;
thus for F being Element of QC-WFF A holds S1[F] from QC_LANG1:sch_1(A5, A1, A2, A4, A3); ::_thesis: verum
end;
theorem Th10: :: QC_LANG1:10
for A being QC-alphabet
for F being Element of QC-WFF A holds 1 <= len (@ F)
proof
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A holds 1 <= len (@ F)
let F be Element of QC-WFF A; ::_thesis: 1 <= len (@ F)
now__::_thesis:_1_<=_len_(@_F)
percases ( F = VERUM A or F is atomic or F is negative or F is conjunctive or F is universal ) by Th9;
suppose F = VERUM A ; ::_thesis: 1 <= len (@ F)
hence 1 <= len (@ F) by FINSEQ_1:39; ::_thesis: verum
end;
suppose F is atomic ; ::_thesis: 1 <= len (@ F)
then consider k being Element of NAT , p being QC-pred_symbol of k,A, ll being QC-variable_list of k,A such that
A1: F = p ! ll by Def18;
@ F = <*p*> ^ ll by A1, Th8;
then len (@ F) = (len <*p*>) + (len ll) by FINSEQ_1:22
.= 1 + (len ll) by FINSEQ_1:39 ;
hence 1 <= len (@ F) by NAT_1:11; ::_thesis: verum
end;
suppose F is negative ; ::_thesis: 1 <= len (@ F)
then consider p being Element of QC-WFF A such that
A2: F = 'not' p by Def19;
len (@ F) = (len <*[1,0]*>) + (len (@ p)) by A2, FINSEQ_1:22
.= 1 + (len (@ p)) by FINSEQ_1:39 ;
hence 1 <= len (@ F) by NAT_1:11; ::_thesis: verum
end;
suppose F is conjunctive ; ::_thesis: 1 <= len (@ F)
then consider p, q being Element of QC-WFF A such that
A3: F = p '&' q by Def20;
@ F = <*[2,0]*> ^ ((@ p) ^ (@ q)) by A3, FINSEQ_1:32;
then len (@ F) = (len <*[2,0]*>) + (len ((@ p) ^ (@ q))) by FINSEQ_1:22
.= 1 + (len ((@ p) ^ (@ q))) by FINSEQ_1:39 ;
hence 1 <= len (@ F) by NAT_1:11; ::_thesis: verum
end;
suppose F is universal ; ::_thesis: 1 <= len (@ F)
then consider x being bound_QC-variable of A, p being Element of QC-WFF A such that
A4: F = All (x,p) by Def21;
@ F = <*[3,0]*> ^ (<*x*> ^ (@ p)) by A4, FINSEQ_1:32;
then len (@ F) = (len <*[3,0]*>) + (len (<*x*> ^ (@ p))) by FINSEQ_1:22
.= 1 + (len (<*x*> ^ (@ p))) by FINSEQ_1:39 ;
hence 1 <= len (@ F) by NAT_1:11; ::_thesis: verum
end;
end;
end;
hence 1 <= len (@ F) ; ::_thesis: verum
end;
theorem Th11: :: QC_LANG1:11
for A being QC-alphabet
for k being Element of NAT
for P being QC-pred_symbol of k,A holds the_arity_of P = k
proof
let A be QC-alphabet ; ::_thesis: for k being Element of NAT
for P being QC-pred_symbol of k,A holds the_arity_of P = k
let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,A holds the_arity_of P = k
let P be QC-pred_symbol of k,A; ::_thesis: the_arity_of P = k
reconsider P = P as Element of k -ary_QC-pred_symbols A ;
P in { Q where Q is QC-pred_symbol of A : the_arity_of Q = k } ;
then ex Q being QC-pred_symbol of A st
( P = Q & the_arity_of Q = k ) ;
hence the_arity_of P = k ; ::_thesis: verum
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 Element of NAT st (@ F) . 1 is QC-pred_symbol of k,A implies F is atomic ) )
proof
let A be QC-alphabet ; ::_thesis: 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 Element of NAT st (@ F) . 1 is QC-pred_symbol of k,A implies F is atomic ) )
let F be Element of QC-WFF A; ::_thesis: ( ( ((@ 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 Element of NAT st (@ F) . 1 is QC-pred_symbol of k,A implies F is atomic ) )
A1: now__::_thesis:_(_(_F_is_atomic_&_ex_k_being_Element_of_NAT_st_(@_F)_._1_is_QC-pred_symbol_of_k,A_)_or_(_F_=_VERUM_A_&_((@_F)_._1)_`1_=_0_)_or_(_F_is_negative_&_((@_F)_._1)_`1_=_1_)_or_(_F_is_conjunctive_&_((@_F)_._1)_`1_=_2_)_or_(_F_is_universal_&_((@_F)_._1)_`1_=_3_)_)
percases ( F is atomic or F = VERUM A or F is negative or F is conjunctive or F is universal ) by Th9;
case F is atomic ; ::_thesis: ex k being Element of NAT st (@ F) . 1 is QC-pred_symbol of k,A
then consider k being Element of NAT , P being QC-pred_symbol of k,A, ll being QC-variable_list of k,A such that
A2: F = P ! ll by Def18;
@ F = <*P*> ^ ll by A2, Th8;
then (@ F) . 1 = P by FINSEQ_1:41;
hence ex k being Element of NAT st (@ F) . 1 is QC-pred_symbol of k,A ; ::_thesis: verum
end;
case F = VERUM A ; ::_thesis: ((@ F) . 1) `1 = 0
hence ((@ F) . 1) `1 = [0,0] `1 by FINSEQ_1:def_8
.= 0 ;
::_thesis: verum
end;
case F is negative ; ::_thesis: ((@ F) . 1) `1 = 1
then ex p being Element of QC-WFF A st F = 'not' p by Def19;
then (@ F) . 1 = [1,0] by FINSEQ_1:41;
hence ((@ F) . 1) `1 = 1 by MCART_1:7; ::_thesis: verum
end;
case F is conjunctive ; ::_thesis: ((@ F) . 1) `1 = 2
then consider p, q being Element of QC-WFF A such that
A3: F = p '&' q by Def20;
@ F = <*[2,0]*> ^ ((@ p) ^ (@ q)) by A3, FINSEQ_1:32;
then (@ F) . 1 = [2,0] by FINSEQ_1:41;
hence ((@ F) . 1) `1 = 2 by MCART_1:7; ::_thesis: verum
end;
case F is universal ; ::_thesis: ((@ F) . 1) `1 = 3
then consider x being bound_QC-variable of A, p being Element of QC-WFF A such that
A4: F = All (x,p) by Def21;
@ F = <*[3,0]*> ^ (<*x*> ^ (@ p)) by A4, FINSEQ_1:32;
then (@ F) . 1 = [3,0] by FINSEQ_1:41;
hence ((@ F) . 1) `1 = 3 by MCART_1:7; ::_thesis: verum
end;
end;
end;
now__::_thesis:_for_k_being_Element_of_NAT_
for_P_being_QC-pred_symbol_of_k,A_holds_
(_P_`1_<>_0_&_P_`1_<>_1_&_P_`1_<>_2_&_P_`1_<>_3_)
let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,A holds
( P `1 <> 0 & P `1 <> 1 & P `1 <> 2 & P `1 <> 3 )
let P be QC-pred_symbol of k,A; ::_thesis: ( P `1 <> 0 & P `1 <> 1 & P `1 <> 2 & P `1 <> 3 )
reconsider P9 = P as QC-pred_symbol of A ;
P9 `1 = 7 + (the_arity_of P9) by Def8;
hence ( P `1 <> 0 & P `1 <> 1 & P `1 <> 2 & P `1 <> 3 ) by NAT_1:11; ::_thesis: verum
end;
hence ( ( ((@ 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 Element of NAT st (@ F) . 1 is QC-pred_symbol of k,A implies F is atomic ) ) by A1; ::_thesis: verum
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
let A be QC-alphabet ; ::_thesis: for F, G being Element of QC-WFF A
for s being FinSequence st @ F = (@ G) ^ s holds
@ F = @ G
let F, G be Element of QC-WFF A; ::_thesis: for s being FinSequence st @ F = (@ G) ^ s holds
@ F = @ G
let s be FinSequence; ::_thesis: ( @ F = (@ G) ^ s implies @ F = @ G )
defpred S1[ set ] means for F, G being Element of QC-WFF A
for s being FinSequence st len (@ F) = $1 & @ F = (@ G) ^ s holds
@ F = @ G;
A1: for n being Nat st ( for k being Nat st k < n holds
S1[k] ) holds
S1[n]
proof
let n be Nat; ::_thesis: ( ( for k being Nat st k < n holds
S1[k] ) implies S1[n] )
assume A2: for k being Nat st k < n holds
for F, G being Element of QC-WFF A
for s being FinSequence st len (@ F) = k & @ F = (@ G) ^ s holds
@ F = @ G ; ::_thesis: S1[n]
let F, G be Element of QC-WFF A; ::_thesis: for s being FinSequence st len (@ F) = n & @ F = (@ G) ^ s holds
@ F = @ G
let s be FinSequence; ::_thesis: ( len (@ F) = n & @ F = (@ G) ^ s implies @ F = @ G )
assume that
A3: len (@ F) = n and
A4: @ F = (@ G) ^ s ; ::_thesis: @ F = @ G
( dom (@ G) = Seg (len (@ G)) & 1 <= len (@ G) ) by Th10, FINSEQ_1:def_3;
then 1 in dom (@ G) ;
then A5: (@ F) . 1 = (@ G) . 1 by A4, FINSEQ_1:def_7;
A6: len ((@ G) ^ s) = (len (@ G)) + (len s) by FINSEQ_1:22;
now__::_thesis:_@_F_=_@_G
percases ( F = VERUM A or F is atomic or F is negative or F is conjunctive or F is universal ) by Th9;
supposeA7: F = VERUM A ; ::_thesis: @ F = @ G
A8: 1 <= len (@ G) by Th10;
A9: len (@ F) = 1 by A7, FINSEQ_1:39;
then len (@ G) <= 1 by A4, A6, NAT_1:11;
then 1 + 0 = 1 + (len s) by A4, A6, A9, A8, XXREAL_0:1;
then s = {} ;
hence @ F = @ G by A4, FINSEQ_1:34; ::_thesis: verum
end;
suppose F is atomic ; ::_thesis: @ F = @ G
then consider k being Element of NAT , P being QC-pred_symbol of k,A, ll being QC-variable_list of k,A such that
A10: F = P ! ll by Def18;
A11: @ F = <*P*> ^ ll by A10, Th8;
then A12: (@ G) . 1 = P by A5, FINSEQ_1:41;
then G is atomic by Th12;
then consider k9 being Element of NAT , P9 being QC-pred_symbol of k9,A, ll9 being QC-variable_list of k9,A such that
A13: G = P9 ! ll9 by Def18;
A14: @ G = <*P9*> ^ ll9 by A13, Th8;
then A15: (@ G) . 1 = P9 by FINSEQ_1:41;
then <*P*> ^ ll = <*P*> ^ (ll9 ^ s) by A4, A11, A12, A14, FINSEQ_1:32;
then ll = ll9 ^ s by FINSEQ_1:33;
then A16: (len ll) + 0 = (len ll9) + (len s) by FINSEQ_1:22;
len ll9 = k9 by CARD_1:def_7
.= the_arity_of P by A12, A15, Th11
.= k by Th11
.= len ll by CARD_1:def_7 ;
then s = {} by A16;
hence @ F = @ G by A4, FINSEQ_1:34; ::_thesis: verum
end;
suppose F is negative ; ::_thesis: @ F = @ G
then consider p being Element of QC-WFF A such that
A17: F = 'not' p by Def19;
(@ F) . 1 = [1,0] by A17, FINSEQ_1:41;
then ((@ G) . 1) `1 = 1 by A5, MCART_1:7;
then G is negative by Th12;
then consider p9 being Element of QC-WFF A such that
A18: G = 'not' p9 by Def19;
<*[1,0]*> ^ (@ p) = <*[1,0]*> ^ ((@ p9) ^ s) by A4, A17, A18, FINSEQ_1:32;
then A19: @ p = (@ p9) ^ s by FINSEQ_1:33;
len (@ F) = (len (@ p)) + (len <*[1,0]*>) by A17, FINSEQ_1:22
.= (len (@ p)) + 1 by FINSEQ_1:40 ;
then len (@ p) < len (@ F) by NAT_1:13;
then @ p = @ p9 by A2, A3, A19;
then (@ p9) ^ {} = (@ p9) ^ s by A19, FINSEQ_1:34;
then s = {} by FINSEQ_1:33;
hence @ F = @ G by A4, FINSEQ_1:34; ::_thesis: verum
end;
suppose F is conjunctive ; ::_thesis: @ F = @ G
then consider p, q being Element of QC-WFF A such that
A20: F = p '&' q by Def20;
A21: @ F = <*[2,0]*> ^ ((@ p) ^ (@ q)) by A20, FINSEQ_1:32;
then A22: len (@ F) = (len ((@ p) ^ (@ q))) + (len <*[2,0]*>) by FINSEQ_1:22
.= (len ((@ p) ^ (@ q))) + 1 by FINSEQ_1:40 ;
then A23: len (@ F) = ((len (@ p)) + (len (@ q))) + 1 by FINSEQ_1:22;
(@ F) . 1 = [2,0] by A21, FINSEQ_1:41;
then ((@ G) . 1) `1 = 2 by A5, MCART_1:7;
then G is conjunctive by Th12;
then consider p9, q9 being Element of QC-WFF A such that
A24: G = p9 '&' q9 by Def20;
A25: len (@ p9) <= (len (@ p9)) + (len ((@ q9) ^ s)) by NAT_1:11;
A26: @ G = <*[2,0]*> ^ ((@ p9) ^ (@ q9)) by A24, FINSEQ_1:32;
then <*[2,0]*> ^ ((@ p) ^ (@ q)) = <*[2,0]*> ^ (((@ p9) ^ (@ q9)) ^ s) by A4, A21, FINSEQ_1:32;
then A27: (@ p) ^ (@ q) = ((@ p9) ^ (@ q9)) ^ s by FINSEQ_1:33
.= (@ p9) ^ ((@ q9) ^ s) by FINSEQ_1:32 ;
then len (@ F) = ((len (@ p9)) + (len ((@ q9) ^ s))) + 1 by A22, FINSEQ_1:22;
then A28: len (@ p9) < len (@ F) by A25, NAT_1:13;
len (@ q) <= (len (@ p)) + (len (@ q)) by NAT_1:11;
then A29: len (@ q) < len (@ F) by A23, NAT_1:13;
len (@ p) <= (len (@ p)) + (len (@ q)) by NAT_1:11;
then A30: len (@ p) < len (@ F) by A23, NAT_1:13;
( len (@ p) <= len (@ p9) or len (@ p9) <= len (@ p) ) ;
then consider a, b, c, d being FinSequence such that
A31: ( ( a = @ p & b = @ p9 ) or ( a = @ p9 & b = @ p ) ) and
A32: ( len a <= len b & a ^ c = b ^ d ) by A27;
ex t being FinSequence st a ^ t = b by A32, FINSEQ_1:47;
then A33: @ p = @ p9 by A2, A3, A31, A30, A28;
then @ q = (@ q9) ^ s by A27, FINSEQ_1:33;
hence @ F = @ G by A2, A3, A21, A26, A33, A29; ::_thesis: verum
end;
suppose F is universal ; ::_thesis: @ F = @ G
then consider x being bound_QC-variable of A, p being Element of QC-WFF A such that
A34: F = All (x,p) by Def21;
A35: @ F = <*[3,0]*> ^ (<*x*> ^ (@ p)) by A34, FINSEQ_1:32;
then len (@ F) = (len (<*x*> ^ (@ p))) + (len <*[3,0]*>) by FINSEQ_1:22
.= (len (<*x*> ^ (@ p))) + 1 by FINSEQ_1:40
.= ((len <*x*>) + (len (@ p))) + 1 by FINSEQ_1:22
.= (1 + (len (@ p))) + 1 by FINSEQ_1:40 ;
then (len (@ p)) + 1 <= len (@ F) by NAT_1:13;
then A36: len (@ p) < len (@ F) by NAT_1:13;
(@ F) . 1 = [3,0] by A35, FINSEQ_1:41;
then ((@ G) . 1) `1 = 3 by A5, MCART_1:7;
then G is universal by Th12;
then consider x9 being bound_QC-variable of A, p9 being Element of QC-WFF A such that
A37: G = All (x9,p9) by Def21;
(<*[3,0]*> ^ <*x*>) ^ (@ p) = (<*[3,0]*> ^ (<*x9*> ^ (@ p9))) ^ s by A4, A34, A37, FINSEQ_1:32
.= <*[3,0]*> ^ ((<*x9*> ^ (@ p9)) ^ s) by FINSEQ_1:32 ;
then A38: <*x*> ^ (@ p) = (<*x9*> ^ (@ p9)) ^ s by A34, A35, FINSEQ_1:33
.= <*x9*> ^ ((@ p9) ^ s) by FINSEQ_1:32 ;
then A39: x = (<*x9*> ^ ((@ p9) ^ s)) . 1 by FINSEQ_1:41
.= x9 by FINSEQ_1:41 ;
then @ p = (@ p9) ^ s by A38, FINSEQ_1:33;
hence @ F = @ G by A2, A3, A34, A37, A39, A36; ::_thesis: verum
end;
end;
end;
hence @ F = @ G ; ::_thesis: verum
end;
A40: for n being Nat holds S1[n] from NAT_1:sch_4(A1);
len (@ F) = len (@ F) ;
hence ( @ F = (@ G) ^ s implies @ F = @ G ) by A40; ::_thesis: verum
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 Element of 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 Element of 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 )
proof
ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A st F = P ! ll by A1, Def18;
hence ex b1 being QC-pred_symbol of A ex k being Element of NAT ex ll being QC-variable_list of k,A ex P being QC-pred_symbol of k,A st
( b1 = P & F = P ! ll ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being QC-pred_symbol of A st ex k being Element of NAT ex ll being QC-variable_list of k,A ex P being QC-pred_symbol of k,A st
( b1 = P & F = P ! ll ) & ex k being Element of NAT ex ll being QC-variable_list of k,A ex P being QC-pred_symbol of k,A st
( b2 = P & F = P ! ll ) holds
b1 = b2
proof
let P1, P2 be QC-pred_symbol of A; ::_thesis: ( ex k being Element of NAT ex ll being QC-variable_list of k,A ex P being QC-pred_symbol of k,A st
( P1 = P & F = P ! ll ) & ex k being Element of NAT ex ll being QC-variable_list of k,A ex P being QC-pred_symbol of k,A st
( P2 = P & F = P ! ll ) implies P1 = P2 )
given k1 being Element of NAT , ll1 being QC-variable_list of k1,A, P19 being QC-pred_symbol of k1,A such that A1: ( P1 = P19 & F = P19 ! ll1 ) ; ::_thesis: ( for k being Element of NAT
for ll being QC-variable_list of k,A
for P being QC-pred_symbol of k,A holds
( not P2 = P or not F = P ! ll ) or P1 = P2 )
given k2 being Element of NAT , ll2 being QC-variable_list of k2,A, P29 being QC-pred_symbol of k2,A such that A2: ( P2 = P29 & F = P29 ! ll2 ) ; ::_thesis: P1 = P2
A3: <*P1*> ^ ll1 = F by A1, Th8
.= <*P2*> ^ ll2 by A2, Th8 ;
thus P1 = (<*P1*> ^ ll1) . 1 by FINSEQ_1:41
.= P2 by A3, FINSEQ_1:41 ; ::_thesis: verum
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 Element of 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 B1: F is atomic ;
func the_arguments_of F -> FinSequence of QC-variables A means :Def23: :: QC_LANG1:def 23
ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A st
( it = ll & F = P ! ll );
existence
ex b1 being FinSequence of QC-variables A ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A st
( b1 = ll & F = P ! ll )
proof
consider k being Element of NAT , P being QC-pred_symbol of k,A, ll being QC-variable_list of k,A such that
A1: F = P ! ll by B1, Def18;
reconsider ll = ll as FinSequence of QC-variables A ;
take ll ; ::_thesis: ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A st
( ll = ll & F = P ! ll )
thus ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A st
( ll = ll & F = P ! ll ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of QC-variables A st ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A st
( b1 = ll & F = P ! ll ) & ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A st
( b2 = ll & F = P ! ll ) holds
b1 = b2
proof
let ll1, ll2 be FinSequence of QC-variables A; ::_thesis: ( ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A st
( ll1 = ll & F = P ! ll ) & ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A st
( ll2 = ll & F = P ! ll ) implies ll1 = ll2 )
given k1 being Element of NAT , P1 being QC-pred_symbol of k1,A, ll19 being QC-variable_list of k1,A such that A2: ll1 = ll19 and
A3: F = P1 ! ll19 ; ::_thesis: ( for k being Element of NAT
for P being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds
( not ll2 = ll or not F = P ! ll ) or ll1 = ll2 )
A4: F = <*P1*> ^ ll19 by A3, Th8;
given k2 being Element of NAT , P2 being QC-pred_symbol of k2,A, ll29 being QC-variable_list of k2,A such that A5: ll2 = ll29 and
A6: F = P2 ! ll29 ; ::_thesis: ll1 = ll2
A7: F = <*P2*> ^ ll29 by A6, Th8;
P1 = the_pred_symbol_of F by B1, A3, Def22
.= P2 by B1, A6, Def22 ;
hence ll1 = ll2 by A2, A5, A4, A7, FINSEQ_1:33; ::_thesis: verum
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 Element of 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, Def19;
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, Def20;
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
let p1, p2 be QC-formula of A; ::_thesis: ( ex q being Element of QC-WFF A st F = p1 '&' q & ex q being Element of QC-WFF A st F = p2 '&' q implies p1 = p2 )
given q1 being Element of QC-WFF A such that A1: F = p1 '&' q1 ; ::_thesis: ( for q being Element of QC-WFF A holds not F = p2 '&' q or p1 = p2 )
given q2 being Element of QC-WFF A such that A2: F = p2 '&' q2 ; ::_thesis: p1 = p2
<*[2,0]*> ^ ((@ p1) ^ (@ q1)) = p2 '&' q2 by A1, A2, FINSEQ_1:32
.= <*[2,0]*> ^ ((@ p2) ^ (@ q2)) by FINSEQ_1:32 ;
then A3: (@ p1) ^ (@ q1) = (@ p2) ^ (@ q2) by FINSEQ_1:33;
( len (@ p1) <= len (@ p2) or len (@ p2) <= len (@ p1) ) ;
then consider a, b, c, d being FinSequence such that
A4: ( ( a = @ p1 & b = @ p2 ) or ( a = @ p2 & b = @ p1 ) ) and
A5: ( len a <= len b & a ^ c = b ^ d ) by A3;
ex t being FinSequence st a ^ t = b by A5, FINSEQ_1:47;
hence p1 = p2 by A4, Th13; ::_thesis: verum
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 B1: F is conjunctive ;
func the_right_argument_of F -> QC-formula of A means :Def26: :: QC_LANG1:def 26
ex p being Element of QC-WFF A st F = p '&' it;
existence
ex b1 being QC-formula of A ex p being Element of QC-WFF A st F = p '&' b1
proof
ex p, q being Element of QC-WFF A st F = p '&' q by B1, Def20;
hence ex b1 being QC-formula of A ex p being Element of QC-WFF A st F = p '&' b1 ; ::_thesis: verum
end;
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
let q1, q2 be QC-formula of A; ::_thesis: ( ex p being Element of QC-WFF A st F = p '&' q1 & ex p being Element of QC-WFF A st F = p '&' q2 implies q1 = q2 )
given p1 being Element of QC-WFF A such that A1: F = p1 '&' q1 ; ::_thesis: ( for p being Element of QC-WFF A holds not F = p '&' q2 or q1 = q2 )
given p2 being Element of QC-WFF A such that A2: F = p2 '&' q2 ; ::_thesis: q1 = q2
<*[2,0]*> ^ ((@ p1) ^ (@ q1)) = p2 '&' q2 by A1, A2, FINSEQ_1:32
.= <*[2,0]*> ^ ((@ p2) ^ (@ q2)) by FINSEQ_1:32 ;
then A3: (@ p1) ^ (@ q1) = (@ p2) ^ (@ q2) by FINSEQ_1:33;
p1 = the_left_argument_of F by B1, A1, Def25
.= p2 by B1, A2, Def25 ;
hence q1 = q2 by A3, FINSEQ_1:33; ::_thesis: verum
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, Def21;
uniqueness
for b1, b2 being bound_QC-variable of A st ex p being Element of QC-WFF A st F = All (b1,p) & ex p being Element of QC-WFF A st F = All (b2,p) holds
b1 = b2
proof
let x1, x2 be bound_QC-variable of A; ::_thesis: ( ex p being Element of QC-WFF A st F = All (x1,p) & ex p being Element of QC-WFF A st F = All (x2,p) implies x1 = x2 )
given p1 being Element of QC-WFF A such that A1: F = All (x1,p1) ; ::_thesis: ( for p being Element of QC-WFF A holds not F = All (x2,p) or x1 = x2 )
given p2 being Element of QC-WFF A such that A2: F = All (x2,p2) ; ::_thesis: x1 = x2
<*[3,0]*> ^ (<*x1*> ^ (@ p1)) = All (x2,p2) by A1, A2, FINSEQ_1:32
.= <*[3,0]*> ^ (<*x2*> ^ (@ p2)) by FINSEQ_1:32 ;
then A3: <*x1*> ^ (@ p1) = <*x2*> ^ (@ p2) by FINSEQ_1:33;
thus x1 = (<*x1*> ^ (@ p1)) . 1 by FINSEQ_1:41
.= x2 by A3, FINSEQ_1:41 ; ::_thesis: verum
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)
proof
ex x being bound_QC-variable of A ex p being Element of QC-WFF A st F = All (x,p) by A1, Def21;
hence ex b1 being QC-formula of A ex x being bound_QC-variable of A st F = All (x,b1) ; ::_thesis: verum
end;
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
let p1, p2 be QC-formula of A; ::_thesis: ( ex x being bound_QC-variable of A st F = All (x,p1) & ex x being bound_QC-variable of A st F = All (x,p2) implies p1 = p2 )
given x1 being bound_QC-variable of A such that A4: F = All (x1,p1) ; ::_thesis: ( for x being bound_QC-variable of A holds not F = All (x,p2) or p1 = p2 )
given x2 being bound_QC-variable of A such that A5: F = All (x2,p2) ; ::_thesis: p1 = p2
<*[3,0]*> ^ (<*x1*> ^ (@ p1)) = All (x2,p2) by A4, A5, FINSEQ_1:32
.= <*[3,0]*> ^ (<*x2*> ^ (@ p2)) by FINSEQ_1:32 ;
then A6: <*x1*> ^ (@ p1) = <*x2*> ^ (@ p2) by FINSEQ_1:33;
x1 = (<*x1*> ^ (@ p1)) . 1 by FINSEQ_1:41
.= x2 by A6, FINSEQ_1:41 ;
hence p1 = p2 by A6, FINSEQ_1:33; ::_thesis: verum
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 (@ (the_argument_of p)) < len (@ p)
proof
let A be QC-alphabet ; ::_thesis: for p being Element of QC-WFF A st p is negative holds
len (@ (the_argument_of p)) < len (@ p)
let p be Element of QC-WFF A; ::_thesis: ( p is negative implies len (@ (the_argument_of p)) < len (@ p) )
assume A1: p is negative ; ::_thesis: len (@ (the_argument_of p)) < len (@ p)
then consider q being Element of QC-WFF A such that
A2: p = 'not' q by Def19;
len (@ p) = (len <*[1,0]*>) + (len (@ q)) by A2, FINSEQ_1:22
.= (len (@ q)) + 1 by FINSEQ_1:40 ;
then len (@ q) < len (@ p) by NAT_1:13;
hence len (@ (the_argument_of p)) < len (@ p) by A1, A2, Def24; ::_thesis: verum
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
let A be QC-alphabet ; ::_thesis: 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) )
let p be Element of QC-WFF A; ::_thesis: ( p is conjunctive implies ( len (@ (the_left_argument_of p)) < len (@ p) & len (@ (the_right_argument_of p)) < len (@ p) ) )
assume A1: p is conjunctive ; ::_thesis: ( len (@ (the_left_argument_of p)) < len (@ p) & len (@ (the_right_argument_of p)) < len (@ p) )
then consider l, q being Element of QC-WFF A such that
A2: p = l '&' q by Def20;
p = <*[2,0]*> ^ ((@ l) ^ (@ q)) by A2, FINSEQ_1:32;
then A3: len (@ p) = (len <*[2,0]*>) + (len ((@ l) ^ (@ q))) by FINSEQ_1:22
.= (len ((@ l) ^ (@ q))) + 1 by FINSEQ_1:40 ;
A4: (len (@ q)) + (len (@ l)) = len ((@ l) ^ (@ q)) by FINSEQ_1:22;
then len (@ q) <= len ((@ l) ^ (@ q)) by NAT_1:11;
then A5: len (@ q) < len (@ p) by A3, NAT_1:13;
len (@ l) <= len ((@ l) ^ (@ q)) by A4, NAT_1:11;
then len (@ l) < len (@ p) by A3, NAT_1:13;
hence ( len (@ (the_left_argument_of p)) < len (@ p) & len (@ (the_right_argument_of p)) < len (@ p) ) by A1, A2, A5, Def25, Def26; ::_thesis: verum
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
let A be QC-alphabet ; ::_thesis: for p being Element of QC-WFF A st p is universal holds
len (@ (the_scope_of p)) < len (@ p)
let p be Element of QC-WFF A; ::_thesis: ( p is universal implies len (@ (the_scope_of p)) < len (@ p) )
assume A1: p is universal ; ::_thesis: len (@ (the_scope_of p)) < len (@ p)
then consider x being bound_QC-variable of A, q being Element of QC-WFF A such that
A2: p = All (x,q) by Def21;
(len (@ q)) + (len <*x*>) = len (<*x*> ^ (@ q)) by FINSEQ_1:22;
then A3: len (@ q) <= len (<*x*> ^ (@ q)) by NAT_1:11;
p = <*[3,0]*> ^ (<*x*> ^ (@ q)) by A2, FINSEQ_1:32;
then len (@ p) = (len <*[3,0]*>) + (len (<*x*> ^ (@ q))) by FINSEQ_1:22
.= (len (<*x*> ^ (@ q))) + 1 by FINSEQ_1:40 ;
then len (@ q) < len (@ p) by A3, NAT_1:13;
hence len (@ (the_scope_of p)) < len (@ p) by A1, A2, Def28; ::_thesis: verum
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
A2: now__::_thesis:_for_x_being_bound_QC-variable_of_F1()
for_p_being_Element_of_QC-WFF_F1()_st_P1[p]_holds_
P1[_All_(x,p)]
let x be bound_QC-variable of F1(); ::_thesis: for p being Element of QC-WFF F1() st P1[p] holds
P1[ All (x,p)]
let p be Element of QC-WFF F1(); ::_thesis: ( P1[p] implies P1[ All (x,p)] )
assume A3: P1[p] ; ::_thesis: P1[ All (x,p)]
A4: All (x,p) is universal by Def21;
then p = the_scope_of (All (x,p)) by Def28;
hence P1[ All (x,p)] by A1, A3, A4; ::_thesis: verum
end;
A5: now__::_thesis:_for_p_being_Element_of_QC-WFF_F1()_st_P1[p]_holds_
P1[_'not'_p]
let p be Element of QC-WFF F1(); ::_thesis: ( P1[p] implies P1[ 'not' p] )
assume A6: P1[p] ; ::_thesis: P1[ 'not' p]
A7: 'not' p is negative by Def19;
then p = the_argument_of ('not' p) by Def24;
hence P1[ 'not' p] by A1, A6, A7; ::_thesis: verum
end;
A8: now__::_thesis:_for_p,_q_being_Element_of_QC-WFF_F1()_st_P1[p]_&_P1[q]_holds_
P1[p_'&'_q]
let p, q be Element of QC-WFF F1(); ::_thesis: ( P1[p] & P1[q] implies P1[p '&' q] )
assume A9: ( P1[p] & P1[q] ) ; ::_thesis: P1[p '&' q]
A10: p '&' q is conjunctive by Def20;
then ( p = the_left_argument_of (p '&' q) & q = the_right_argument_of (p '&' q) ) by Def25, Def26;
hence P1[p '&' q] by A1, A9, A10; ::_thesis: verum
end;
A11: now__::_thesis:_for_k_being_Element_of_NAT_
for_P_being_QC-pred_symbol_of_k,F1()
for_ll_being_QC-variable_list_of_k,F1()_holds_P1[P_!_ll]
let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,F1()
for ll being QC-variable_list of k,F1() holds P1[P ! ll]
let P be QC-pred_symbol of k,F1(); ::_thesis: for ll being QC-variable_list of k,F1() holds P1[P ! ll]
let ll be QC-variable_list of k,F1(); ::_thesis: P1[P ! ll]
P ! ll is atomic by Def18;
hence P1[P ! ll] by A1; ::_thesis: verum
end;
A12: P1[ VERUM F1()] by A1;
thus for p being Element of QC-WFF F1() holds P1[p] from QC_LANG1:sch_1(A11, A12, A5, A8, A2); ::_thesis: verum
end;
theorem Th17: :: QC_LANG1:17
for A being QC-alphabet
for k being Element of NAT
for P being QC-pred_symbol of k,A holds
( P `1 <> 0 & P `1 <> 1 & P `1 <> 2 & P `1 <> 3 )
proof
let A be QC-alphabet ; ::_thesis: for k being Element of NAT
for P being QC-pred_symbol of k,A holds
( P `1 <> 0 & P `1 <> 1 & P `1 <> 2 & P `1 <> 3 )
let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,A holds
( P `1 <> 0 & P `1 <> 1 & P `1 <> 2 & P `1 <> 3 )
let P be QC-pred_symbol of k,A; ::_thesis: ( P `1 <> 0 & P `1 <> 1 & P `1 <> 2 & P `1 <> 3 )
reconsider P9 = P as QC-pred_symbol of A ;
P9 `1 = 7 + (the_arity_of P9) by Def8;
hence ( P `1 <> 0 & P `1 <> 1 & P `1 <> 2 & P `1 <> 3 ) by NAT_1:11; ::_thesis: verum
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 Element of 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
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A holds
( ((@ (VERUM A)) . 1) `1 = 0 & ( F is atomic implies ex k being Element of 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 ) )
let F be Element of QC-WFF A; ::_thesis: ( ((@ (VERUM A)) . 1) `1 = 0 & ( F is atomic implies ex k being Element of 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 ) )
thus ((@ (VERUM A)) . 1) `1 = [0,0] `1 by FINSEQ_1:def_8
.= 0 ; ::_thesis: ( ( F is atomic implies ex k being Element of 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 ) )
thus ( F is atomic implies ex k being Element of NAT st (@ F) . 1 is QC-pred_symbol of k,A ) ::_thesis: ( ( 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
assume F is atomic ; ::_thesis: ex k being Element of NAT st (@ F) . 1 is QC-pred_symbol of k,A
then consider k being Element of NAT , P being QC-pred_symbol of k,A, ll being QC-variable_list of k,A such that
A1: F = P ! ll by Def18;
@ F = <*P*> ^ ll by A1, Th8;
then (@ F) . 1 = P by FINSEQ_1:41;
hence ex k being Element of NAT st (@ F) . 1 is QC-pred_symbol of k,A ; ::_thesis: verum
end;
thus ( F is negative implies ((@ F) . 1) `1 = 1 ) ::_thesis: ( ( F is conjunctive implies ((@ F) . 1) `1 = 2 ) & ( F is universal implies ((@ F) . 1) `1 = 3 ) )
proof
assume F is negative ; ::_thesis: ((@ F) . 1) `1 = 1
then ex p being Element of QC-WFF A st F = 'not' p by Def19;
then (@ F) . 1 = [1,0] by FINSEQ_1:41;
hence ((@ F) . 1) `1 = 1 by MCART_1:7; ::_thesis: verum
end;
thus ( F is conjunctive implies ((@ F) . 1) `1 = 2 ) ::_thesis: ( F is universal implies ((@ F) . 1) `1 = 3 )
proof
assume F is conjunctive ; ::_thesis: ((@ F) . 1) `1 = 2
then consider p, q being Element of QC-WFF A such that
A2: F = p '&' q by Def20;
@ F = <*[2,0]*> ^ ((@ p) ^ (@ q)) by A2, FINSEQ_1:32;
then (@ F) . 1 = [2,0] by FINSEQ_1:41;
hence ((@ F) . 1) `1 = 2 by MCART_1:7; ::_thesis: verum
end;
thus ( F is universal implies ((@ F) . 1) `1 = 3 ) ::_thesis: verum
proof
assume F is universal ; ::_thesis: ((@ F) . 1) `1 = 3
then consider x being bound_QC-variable of A, p being Element of QC-WFF A such that
A3: F = All (x,p) by Def21;
@ F = <*[3,0]*> ^ (<*x*> ^ (@ p)) by A3, FINSEQ_1:32;
then (@ F) . 1 = [3,0] by FINSEQ_1:41;
hence ((@ F) . 1) `1 = 3 by MCART_1:7; ::_thesis: verum
end;
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
let A be QC-alphabet ; ::_thesis: 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 )
let F be Element of QC-WFF A; ::_thesis: ( F is atomic implies ( ((@ F) . 1) `1 <> 0 & ((@ F) . 1) `1 <> 1 & ((@ F) . 1) `1 <> 2 & ((@ F) . 1) `1 <> 3 ) )
assume F is atomic ; ::_thesis: ( ((@ F) . 1) `1 <> 0 & ((@ F) . 1) `1 <> 1 & ((@ F) . 1) `1 <> 2 & ((@ F) . 1) `1 <> 3 )
then ex k being Element of NAT st (@ F) . 1 is QC-pred_symbol of k,A by Th18;
hence ( ((@ F) . 1) `1 <> 0 & ((@ F) . 1) `1 <> 1 & ((@ F) . 1) `1 <> 2 & ((@ F) . 1) `1 <> 3 ) by Th17; ::_thesis: verum
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
let A be QC-alphabet ; ::_thesis: ( 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 ) ) ) )
((@ (VERUM A)) . 1) `1 = 0 by Th18;
hence ( not VERUM A is atomic & not VERUM A is negative & not VERUM A is conjunctive & not VERUM A is universal ) by Th18, Th19; ::_thesis: 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 ) )
let p be Element of QC-WFF A; ::_thesis: ( 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 ) )
A1: ( p is conjunctive implies ((@ p) . 1) `1 = 2 ) by Th18;
A2: ( p is universal implies ((@ p) . 1) `1 = 3 ) by Th18;
( p is negative implies ((@ p) . 1) `1 = 1 ) by Th18;
hence ( 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 ) ) by A1, A2, Th19; ::_thesis: verum
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 . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = F7(p,(F . (the_scope_of p))) ) ) ) )
proof
defpred S1[ Function of (QC-WFF F1()),F2(), Element of NAT ] means ( $1 . (VERUM F1()) = F3() & ( for p being Element of QC-WFF F1() st len (@ p) <= $2 holds
( ( p is atomic implies $1 . p = F4(p) ) & ( p is negative implies $1 . p = F5(($1 . (the_argument_of p))) ) & ( p is conjunctive implies $1 . p = F6(($1 . (the_left_argument_of p)),($1 . (the_right_argument_of p))) ) & ( p is universal implies $1 . p = F7(p,($1 . (the_scope_of p))) ) ) ) );
defpred S2[ Element of F2(), Function of (QC-WFF F1()),F2(), Element of QC-WFF F1()] means ( ( $3 = VERUM F1() implies $1 = F3() ) & ( $3 is atomic implies $1 = F4($3) ) & ( $3 is negative implies $1 = F5(($2 . (the_argument_of $3))) ) & ( $3 is conjunctive implies $1 = F6(($2 . (the_left_argument_of $3)),($2 . (the_right_argument_of $3))) ) & ( $3 is universal implies $1 = F7($3,($2 . (the_scope_of $3))) ) );
defpred S3[ Element of NAT ] means ex F being Function of (QC-WFF F1()),F2() st S1[F,$1];
defpred S4[ set , set ] means ex p being Element of QC-WFF F1() st
( p = $1 & ( for g being Function of (QC-WFF F1()),F2() st S1[g, len (@ p)] holds
$2 = g . p ) );
A1: for n being Element of NAT st S3[n] holds
S3[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S3[n] implies S3[n + 1] )
given F being Function of (QC-WFF F1()),F2() such that A2: S1[F,n] ; ::_thesis: S3[n + 1]
defpred S5[ Element of QC-WFF F1(), Element of F2()] means ( ( len (@ $1) <> n + 1 implies $2 = F . $1 ) & ( len (@ $1) = n + 1 implies S2[$2,F,$1] ) );
A3: for p being Element of QC-WFF F1() ex y being Element of F2() st S5[p,y]
proof
let p be Element of QC-WFF F1(); ::_thesis: ex y being Element of F2() st S5[p,y]
now__::_thesis:_(_(_len_(@_p)_<>_n_+_1_&_ex_y_being_Element_of_F2()_st_y_=_F_._p_)_or_(_len_(@_p)_=_n_+_1_&_p_=_VERUM_F1()_&_ex_y_being_Element_of_F2()_st_S2[y,F,p]_)_or_(_len_(@_p)_=_n_+_1_&_p_is_atomic_&_ex_y_being_Element_of_F2()_st_S2[y,F,p]_)_or_(_len_(@_p)_=_n_+_1_&_p_is_negative_&_ex_y_being_Element_of_F2()_st_S2[y,F,p]_)_or_(_len_(@_p)_=_n_+_1_&_p_is_conjunctive_&_ex_y_being_Element_of_F2()_st_S2[y,F,p]_)_or_(_len_(@_p)_=_n_+_1_&_p_is_universal_&_ex_y_being_Element_of_F2()_st_S2[y,F,p]_)_)
percases ( len (@ p) <> n + 1 or ( len (@ p) = n + 1 & p = VERUM F1() ) or ( len (@ p) = n + 1 & p is atomic ) or ( len (@ p) = n + 1 & p is negative ) or ( len (@ p) = n + 1 & p is conjunctive ) or ( len (@ p) = n + 1 & p is universal ) ) by Th9;
case len (@ p) <> n + 1 ; ::_thesis: ex y being Element of F2() st y = F . p
take y = F . p; ::_thesis: y = F . p
thus y = F . p ; ::_thesis: verum
end;
caseA4: ( len (@ p) = n + 1 & p = VERUM F1() ) ; ::_thesis: ex y being Element of F2() st S2[y,F,p]
take y = F3(); ::_thesis: S2[y,F,p]
thus S2[y,F,p] by A4, Th20; ::_thesis: verum
end;
caseA5: ( len (@ p) = n + 1 & p is atomic ) ; ::_thesis: ex y being Element of F2() st S2[y,F,p]
take y = F4(p); ::_thesis: S2[y,F,p]
thus S2[y,F,p] by A5, Th20; ::_thesis: verum
end;
caseA6: ( len (@ p) = n + 1 & p is negative ) ; ::_thesis: ex y being Element of F2() st S2[y,F,p]
take y = F5((F . (the_argument_of p))); ::_thesis: S2[y,F,p]
thus S2[y,F,p] by A6, Th20; ::_thesis: verum
end;
caseA7: ( len (@ p) = n + 1 & p is conjunctive ) ; ::_thesis: ex y being Element of F2() st S2[y,F,p]
take y = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))); ::_thesis: S2[y,F,p]
thus S2[y,F,p] by A7, Th20; ::_thesis: verum
end;
caseA8: ( len (@ p) = n + 1 & p is universal ) ; ::_thesis: ex y being Element of F2() st S2[y,F,p]
take y = F7(p,(F . (the_scope_of p))); ::_thesis: S2[y,F,p]
thus S2[y,F,p] by A8, Th20; ::_thesis: verum
end;
end;
end;
hence ex y being Element of F2() st S5[p,y] ; ::_thesis: verum
end;
consider G being Function of (QC-WFF F1()),F2() such that
A9: for p being Element of QC-WFF F1() holds S5[p,G . p] from FUNCT_2:sch_3(A3);
take H = G; ::_thesis: S1[H,n + 1]
thus S1[H,n + 1] ::_thesis: verum
proof
thus H . (VERUM F1()) = F3() ::_thesis: for p being Element of QC-WFF F1() st len (@ p) <= n + 1 holds
( ( p is atomic implies H . p = F4(p) ) & ( p is negative implies H . p = F5((H . (the_argument_of p))) ) & ( p is conjunctive implies H . p = F6((H . (the_left_argument_of p)),(H . (the_right_argument_of p))) ) & ( p is universal implies H . p = F7(p,(H . (the_scope_of p))) ) )
proof
percases ( len (@ (VERUM F1())) <> n + 1 or len (@ (VERUM F1())) = n + 1 ) ;
suppose len (@ (VERUM F1())) <> n + 1 ; ::_thesis: H . (VERUM F1()) = F3()
hence H . (VERUM F1()) = F3() by A2, A9; ::_thesis: verum
end;
suppose len (@ (VERUM F1())) = n + 1 ; ::_thesis: H . (VERUM F1()) = F3()
hence H . (VERUM F1()) = F3() by A9; ::_thesis: verum
end;
end;
end;
let p be Element of QC-WFF F1(); ::_thesis: ( len (@ p) <= n + 1 implies ( ( p is atomic implies H . p = F4(p) ) & ( p is negative implies H . p = F5((H . (the_argument_of p))) ) & ( p is conjunctive implies H . p = F6((H . (the_left_argument_of p)),(H . (the_right_argument_of p))) ) & ( p is universal implies H . p = F7(p,(H . (the_scope_of p))) ) ) )
assume A10: len (@ p) <= n + 1 ; ::_thesis: ( ( p is atomic implies H . p = F4(p) ) & ( p is negative implies H . p = F5((H . (the_argument_of p))) ) & ( p is conjunctive implies H . p = F6((H . (the_left_argument_of p)),(H . (the_right_argument_of p))) ) & ( p is universal implies H . p = F7(p,(H . (the_scope_of p))) ) )
thus ( p is atomic implies H . p = F4(p) ) ::_thesis: ( ( p is negative implies H . p = F5((H . (the_argument_of p))) ) & ( p is conjunctive implies H . p = F6((H . (the_left_argument_of p)),(H . (the_right_argument_of p))) ) & ( p is universal implies H . p = F7(p,(H . (the_scope_of p))) ) )
proof
now__::_thesis:_(_p_is_atomic_implies_H_._p_=_F4(p)_)
percases ( len (@ p) <> n + 1 or len (@ p) = n + 1 ) ;
suppose len (@ p) <> n + 1 ; ::_thesis: ( p is atomic implies H . p = F4(p) )
then ( len (@ p) <= n & H . p = F . p ) by A9, A10, NAT_1:8;
hence ( p is atomic implies H . p = F4(p) ) by A2; ::_thesis: verum
end;
suppose len (@ p) = n + 1 ; ::_thesis: ( p is atomic implies H . p = F4(p) )
hence ( p is atomic implies H . p = F4(p) ) by A9; ::_thesis: verum
end;
end;
end;
hence ( p is atomic implies H . p = F4(p) ) ; ::_thesis: verum
end;
thus ( p is negative implies H . p = F5((H . (the_argument_of p))) ) ::_thesis: ( ( p is conjunctive implies H . p = F6((H . (the_left_argument_of p)),(H . (the_right_argument_of p))) ) & ( p is universal implies H . p = F7(p,(H . (the_scope_of p))) ) )
proof
assume A11: p is negative ; ::_thesis: H . p = F5((H . (the_argument_of p)))
then len (@ (the_argument_of p)) <> n + 1 by A10, Th14;
then A12: H . (the_argument_of p) = F . (the_argument_of p) by A9;
now__::_thesis:_H_._p_=_F5((H_._(the_argument_of_p)))
percases ( len (@ p) <> n + 1 or len (@ p) = n + 1 ) ;
suppose len (@ p) <> n + 1 ; ::_thesis: H . p = F5((H . (the_argument_of p)))
then ( len (@ p) <= n & H . p = F . p ) by A9, A10, NAT_1:8;
hence H . p = F5((H . (the_argument_of p))) by A2, A11, A12; ::_thesis: verum
end;
suppose len (@ p) = n + 1 ; ::_thesis: H . p = F5((H . (the_argument_of p)))
hence H . p = F5((H . (the_argument_of p))) by A9, A11, A12; ::_thesis: verum
end;
end;
end;
hence H . p = F5((H . (the_argument_of p))) ; ::_thesis: verum
end;
thus ( p is conjunctive implies H . p = F6((H . (the_left_argument_of p)),(H . (the_right_argument_of p))) ) ::_thesis: ( p is universal implies H . p = F7(p,(H . (the_scope_of p))) )
proof
assume A13: p is conjunctive ; ::_thesis: H . p = F6((H . (the_left_argument_of p)),(H . (the_right_argument_of p)))
then len (@ (the_right_argument_of p)) <> n + 1 by A10, Th15;
then A14: H . (the_right_argument_of p) = F . (the_right_argument_of p) by A9;
len (@ (the_left_argument_of p)) <> n + 1 by A10, A13, Th15;
then A15: H . (the_left_argument_of p) = F . (the_left_argument_of p) by A9;
now__::_thesis:_H_._p_=_F6((H_._(the_left_argument_of_p)),(H_._(the_right_argument_of_p)))
percases ( len (@ p) <> n + 1 or len (@ p) = n + 1 ) ;
suppose len (@ p) <> n + 1 ; ::_thesis: H . p = F6((H . (the_left_argument_of p)),(H . (the_right_argument_of p)))
then ( len (@ p) <= n & H . p = F . p ) by A9, A10, NAT_1:8;
hence H . p = F6((H . (the_left_argument_of p)),(H . (the_right_argument_of p))) by A2, A13, A15, A14; ::_thesis: verum
end;
suppose len (@ p) = n + 1 ; ::_thesis: H . p = F6((H . (the_left_argument_of p)),(H . (the_right_argument_of p)))
hence H . p = F6((H . (the_left_argument_of p)),(H . (the_right_argument_of p))) by A9, A13, A15, A14; ::_thesis: verum
end;
end;
end;
hence H . p = F6((H . (the_left_argument_of p)),(H . (the_right_argument_of p))) ; ::_thesis: verum
end;
thus ( p is universal implies H . p = F7(p,(H . (the_scope_of p))) ) ::_thesis: verum
proof
assume A16: p is universal ; ::_thesis: H . p = F7(p,(H . (the_scope_of p)))
then len (@ (the_scope_of p)) <> n + 1 by A10, Th16;
then A17: H . (the_scope_of p) = F . (the_scope_of p) by A9;
now__::_thesis:_H_._p_=_F7(p,(H_._(the_scope_of_p)))
percases ( len (@ p) <> n + 1 or len (@ p) = n + 1 ) ;
suppose len (@ p) <> n + 1 ; ::_thesis: H . p = F7(p,(H . (the_scope_of p)))
then ( len (@ p) <= n & H . p = F . p ) by A9, A10, NAT_1:8;
hence H . p = F7(p,(H . (the_scope_of p))) by A2, A16, A17; ::_thesis: verum
end;
suppose len (@ p) = n + 1 ; ::_thesis: H . p = F7(p,(H . (the_scope_of p)))
hence H . p = F7(p,(H . (the_scope_of p))) by A9, A16, A17; ::_thesis: verum
end;
end;
end;
hence H . p = F7(p,(H . (the_scope_of p))) ; ::_thesis: verum
end;
end;
end;
A18: S3[ 0 ]
proof
reconsider F = (QC-WFF F1()) --> F3() as Function of (QC-WFF F1()),F2() ;
take F ; ::_thesis: S1[F, 0 ]
thus F . (VERUM F1()) = F3() by FUNCOP_1:7; ::_thesis: for p being Element of QC-WFF F1() st len (@ p) <= 0 holds
( ( p is atomic implies F . p = F4(p) ) & ( p is negative implies F . p = F5((F . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = F7(p,(F . (the_scope_of p))) ) )
let p be Element of QC-WFF F1(); ::_thesis: ( len (@ p) <= 0 implies ( ( p is atomic implies F . p = F4(p) ) & ( p is negative implies F . p = F5((F . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = F7(p,(F . (the_scope_of p))) ) ) )
assume A19: len (@ p) <= 0 ; ::_thesis: ( ( p is atomic implies F . p = F4(p) ) & ( p is negative implies F . p = F5((F . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = F7(p,(F . (the_scope_of p))) ) )
1 <= len (@ p) by Th10;
hence ( ( p is atomic implies F . p = F4(p) ) & ( p is negative implies F . p = F5((F . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = F7(p,(F . (the_scope_of p))) ) ) by A19, XXREAL_0:2; ::_thesis: verum
end;
A20: for n being Element of NAT holds S3[n] from NAT_1:sch_1(A18, A1);
then A21: ex G being Function of (QC-WFF F1()),F2() st S1[G, len (@ (VERUM F1()))] ;
A22: for x being set st x in QC-WFF F1() holds
ex y being set st S4[x,y]
proof
let x be set ; ::_thesis: ( x in QC-WFF F1() implies ex y being set st S4[x,y] )
assume x in QC-WFF F1() ; ::_thesis: ex y being set st S4[x,y]
then reconsider x9 = x as Element of QC-WFF F1() ;
consider F being Function of (QC-WFF F1()),F2() such that
A23: S1[F, len (@ x9)] by A20;
take F . x ; ::_thesis: S4[x,F . x]
take x9 ; ::_thesis: ( x9 = x & ( for g being Function of (QC-WFF F1()),F2() st S1[g, len (@ x9)] holds
F . x = g . x9 ) )
thus x = x9 ; ::_thesis: for g being Function of (QC-WFF F1()),F2() st S1[g, len (@ x9)] holds
F . x = g . x9
let G be Function of (QC-WFF F1()),F2(); ::_thesis: ( S1[G, len (@ x9)] implies F . x = G . x9 )
assume A24: S1[G, len (@ x9)] ; ::_thesis: F . x = G . x9
defpred S5[ Element of QC-WFF F1()] means ( len (@ $1) <= len (@ x9) implies F . $1 = G . $1 );
A25: now__::_thesis:_for_p_being_Element_of_QC-WFF_F1()_holds_
(_(_p_is_atomic_implies_S5[p]_)_&_S5[_VERUM_F1()]_&_(_p_is_negative_&_S5[_the_argument_of_p]_implies_S5[p]_)_&_(_p_is_conjunctive_&_S5[_the_left_argument_of_p]_&_S5[_the_right_argument_of_p]_implies_S5[p]_)_&_(_p_is_universal_&_S5[_the_scope_of_p]_implies_S5[p]_)_)
let p be Element of QC-WFF F1(); ::_thesis: ( ( p is atomic implies S5[p] ) & S5[ VERUM F1()] & ( p is negative & S5[ the_argument_of p] implies S5[p] ) & ( p is conjunctive & S5[ the_left_argument_of p] & S5[ the_right_argument_of p] implies S5[p] ) & ( p is universal & S5[ the_scope_of p] implies S5[p] ) )
thus ( p is atomic implies S5[p] ) ::_thesis: ( S5[ VERUM F1()] & ( p is negative & S5[ the_argument_of p] implies S5[p] ) & ( p is conjunctive & S5[ the_left_argument_of p] & S5[ the_right_argument_of p] implies S5[p] ) & ( p is universal & S5[ the_scope_of p] implies S5[p] ) )
proof
assume A26: ( p is atomic & len (@ p) <= len (@ x9) ) ; ::_thesis: F . p = G . p
hence F . p = F4(p) by A23
.= G . p by A24, A26 ;
::_thesis: verum
end;
thus S5[ VERUM F1()] by A23, A24; ::_thesis: ( ( p is negative & S5[ the_argument_of p] implies S5[p] ) & ( p is conjunctive & S5[ the_left_argument_of p] & S5[ the_right_argument_of p] implies S5[p] ) & ( p is universal & S5[ the_scope_of p] implies S5[p] ) )
thus ( p is negative & S5[ the_argument_of p] implies S5[p] ) ::_thesis: ( ( p is conjunctive & S5[ the_left_argument_of p] & S5[ the_right_argument_of p] implies S5[p] ) & ( p is universal & S5[ the_scope_of p] implies S5[p] ) )
proof
assume that
A27: p is negative and
A28: S5[ the_argument_of p] and
A29: len (@ p) <= len (@ x9) ; ::_thesis: F . p = G . p
len (@ (the_argument_of p)) < len (@ p) by A27, Th14;
hence F . p = F5((G . (the_argument_of p))) by A23, A27, A28, A29, XXREAL_0:2
.= G . p by A24, A27, A29 ;
::_thesis: verum
end;
thus ( p is conjunctive & S5[ the_left_argument_of p] & S5[ the_right_argument_of p] implies S5[p] ) ::_thesis: ( p is universal & S5[ the_scope_of p] implies S5[p] )
proof
assume that
A30: p is conjunctive and
A31: ( S5[ the_left_argument_of p] & S5[ the_right_argument_of p] ) and
A32: len (@ p) <= len (@ x9) ; ::_thesis: F . p = G . p
( len (@ (the_left_argument_of p)) < len (@ p) & len (@ (the_right_argument_of p)) < len (@ p) ) by A30, Th15;
hence F . p = F6((G . (the_left_argument_of p)),(G . (the_right_argument_of p))) by A23, A30, A31, A32, XXREAL_0:2
.= G . p by A24, A30, A32 ;
::_thesis: verum
end;
thus ( p is universal & S5[ the_scope_of p] implies S5[p] ) ::_thesis: verum
proof
assume that
A33: p is universal and
A34: S5[ the_scope_of p] and
A35: len (@ p) <= len (@ x9) ; ::_thesis: F . p = G . p
len (@ (the_scope_of p)) < len (@ p) by A33, Th16;
hence F . p = F7(p,(G . (the_scope_of p))) by A23, A33, A34, A35, XXREAL_0:2
.= G . p by A24, A33, A35 ;
::_thesis: verum
end;
end;
for p being Element of QC-WFF F1() holds S5[p] from QC_LANG1:sch_2(A25);
hence F . x = G . x9 ; ::_thesis: verum
end;
consider F being Function such that
A36: dom F = QC-WFF F1() and
A37: for x being set st x in QC-WFF F1() holds
S4[x,F . x] from CLASSES1:sch_1(A22);
rng F c= F2()
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F or y in F2() )
assume y in rng F ; ::_thesis: y in F2()
then consider x being set such that
A38: ( x in QC-WFF F1() & y = F . x ) by A36, FUNCT_1:def_3;
consider p being Element of QC-WFF F1() such that
p = x and
A39: for g being Function of (QC-WFF F1()),F2() st S1[g, len (@ p)] holds
y = g . p by A37, A38;
consider G being Function of (QC-WFF F1()),F2() such that
A40: S1[G, len (@ p)] by A20;
y = G . p by A39, A40;
hence y in F2() ; ::_thesis: verum
end;
then reconsider F = F as Function of (QC-WFF F1()),F2() by A36, FUNCT_2:def_1, RELSET_1:4;
take F ; ::_thesis: ( 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 . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = F7(p,(F . (the_scope_of p))) ) ) ) )
S4[ VERUM F1(),F . (VERUM F1())] by A37;
hence F . (VERUM F1()) = F3() by A21; ::_thesis: 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 . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = F7(p,(F . (the_scope_of p))) ) )
let p be Element of QC-WFF F1(); ::_thesis: ( ( p is atomic implies F . p = F4(p) ) & ( p is negative implies F . p = F5((F . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = F7(p,(F . (the_scope_of p))) ) )
consider p1 being Element of QC-WFF F1() such that
A41: p1 = p and
A42: for g being Function of (QC-WFF F1()),F2() st S1[g, len (@ p1)] holds
F . p = g . p1 by A37;
consider G being Function of (QC-WFF F1()),F2() such that
A43: S1[G, len (@ p1)] by A20;
set p9 = the_scope_of p;
A44: ex p1 being Element of QC-WFF F1() st
( p1 = the_scope_of p & ( for g being Function of (QC-WFF F1()),F2() st S1[g, len (@ p1)] holds
F . (the_scope_of p) = g . p1 ) ) by A37;
A45: F . p = G . p by A41, A42, A43;
hence ( p is atomic implies F . p = F4(p) ) by A41, A43; ::_thesis: ( ( p is negative implies F . p = F5((F . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = F7(p,(F . (the_scope_of p))) ) )
A46: for k being Element of NAT st k < len (@ p) holds
S1[G,k]
proof
let k be Element of NAT ; ::_thesis: ( k < len (@ p) implies S1[G,k] )
assume A47: k < len (@ p) ; ::_thesis: S1[G,k]
thus G . (VERUM F1()) = F3() by A43; ::_thesis: for p being Element of QC-WFF F1() st len (@ p) <= k holds
( ( p is atomic implies G . p = F4(p) ) & ( p is negative implies G . p = F5((G . (the_argument_of p))) ) & ( p is conjunctive implies G . p = F6((G . (the_left_argument_of p)),(G . (the_right_argument_of p))) ) & ( p is universal implies G . p = F7(p,(G . (the_scope_of p))) ) )
let p9 be Element of QC-WFF F1(); ::_thesis: ( len (@ p9) <= k implies ( ( p9 is atomic implies G . p9 = F4(p9) ) & ( p9 is negative implies G . p9 = F5((G . (the_argument_of p9))) ) & ( p9 is conjunctive implies G . p9 = F6((G . (the_left_argument_of p9)),(G . (the_right_argument_of p9))) ) & ( p9 is universal implies G . p9 = F7(p9,(G . (the_scope_of p9))) ) ) )
assume len (@ p9) <= k ; ::_thesis: ( ( p9 is atomic implies G . p9 = F4(p9) ) & ( p9 is negative implies G . p9 = F5((G . (the_argument_of p9))) ) & ( p9 is conjunctive implies G . p9 = F6((G . (the_left_argument_of p9)),(G . (the_right_argument_of p9))) ) & ( p9 is universal implies G . p9 = F7(p9,(G . (the_scope_of p9))) ) )
then len (@ p9) <= len (@ p) by A47, XXREAL_0:2;
hence ( ( p9 is atomic implies G . p9 = F4(p9) ) & ( p9 is negative implies G . p9 = F5((G . (the_argument_of p9))) ) & ( p9 is conjunctive implies G . p9 = F6((G . (the_left_argument_of p9)),(G . (the_right_argument_of p9))) ) & ( p9 is universal implies G . p9 = F7(p9,(G . (the_scope_of p9))) ) ) by A41, A43; ::_thesis: verum
end;
thus ( p is negative implies F . p = F5((F . (the_argument_of p))) ) ::_thesis: ( ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = F7(p,(F . (the_scope_of p))) ) )
proof
set p9 = the_argument_of p;
set k = len (@ (the_argument_of p));
A48: ex p1 being Element of QC-WFF F1() st
( p1 = the_argument_of p & ( for g being Function of (QC-WFF F1()),F2() st S1[g, len (@ p1)] holds
F . (the_argument_of p) = g . p1 ) ) by A37;
assume A49: p is negative ; ::_thesis: F . p = F5((F . (the_argument_of p)))
then len (@ (the_argument_of p)) < len (@ p) by Th14;
then S1[G, len (@ (the_argument_of p))] by A46;
then F . (the_argument_of p) = G . (the_argument_of p) by A48;
hence F . p = F5((F . (the_argument_of p))) by A41, A43, A45, A49; ::_thesis: verum
end;
thus ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) ::_thesis: ( p is universal implies F . p = F7(p,(F . (the_scope_of p))) )
proof
set p99 = the_right_argument_of p;
set p9 = the_left_argument_of p;
set k9 = len (@ (the_left_argument_of p));
set k99 = len (@ (the_right_argument_of p));
A50: ex p2 being Element of QC-WFF F1() st
( p2 = the_right_argument_of p & ( for g being Function of (QC-WFF F1()),F2() st S1[g, len (@ p2)] holds
F . (the_right_argument_of p) = g . p2 ) ) by A37;
assume A51: p is conjunctive ; ::_thesis: F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p)))
then len (@ (the_left_argument_of p)) < len (@ p) by Th15;
then A52: S1[G, len (@ (the_left_argument_of p))] by A46;
len (@ (the_right_argument_of p)) < len (@ p) by A51, Th15;
then S1[G, len (@ (the_right_argument_of p))] by A46;
then A53: F . (the_right_argument_of p) = G . (the_right_argument_of p) by A50;
ex p1 being Element of QC-WFF F1() st
( p1 = the_left_argument_of p & ( for g being Function of (QC-WFF F1()),F2() st S1[g, len (@ p1)] holds
F . (the_left_argument_of p) = g . p1 ) ) by A37;
then F . (the_left_argument_of p) = G . (the_left_argument_of p) by A52;
hence F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) by A41, A43, A45, A51, A53; ::_thesis: verum
end;
set k = len (@ (the_scope_of p));
assume A54: p is universal ; ::_thesis: F . p = F7(p,(F . (the_scope_of p)))
then len (@ (the_scope_of p)) < len (@ p) by Th16;
then S1[G, len (@ (the_scope_of p))] by A46;
then F . (the_scope_of p) = G . (the_scope_of p) by A44;
hence F . p = F7(p,(F . (the_scope_of p))) by A41, A43, A45, A54; ::_thesis: verum
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 Element of NAT : ( 1 <= k & k <= len ll & ll . k in bound_QC-variables A ) } ;
coherence
{ (ll . k) where k is Element of NAT : ( 1 <= k & k <= len ll & ll . k in bound_QC-variables A ) } is Subset of (bound_QC-variables A)
proof
set IT = { (ll . k) where k is Element of NAT : ( 1 <= k & k <= len ll & ll . k in bound_QC-variables A ) } ;
now__::_thesis:_for_x_being_set_st_x_in__{__(ll_._k)_where_k_is_Element_of_NAT_:_(_1_<=_k_&_k_<=_len_ll_&_ll_._k_in_bound_QC-variables_A_)__}__holds_
x_in_bound_QC-variables_A
let x be set ; ::_thesis: ( x in { (ll . k) where k is Element of NAT : ( 1 <= k & k <= len ll & ll . k in bound_QC-variables A ) } implies x in bound_QC-variables A )
assume x in { (ll . k) where k is Element of NAT : ( 1 <= k & k <= len ll & ll . k in bound_QC-variables A ) } ; ::_thesis: x in bound_QC-variables A
then ex k being Element of NAT st
( x = ll . k & 1 <= k & k <= len ll & ll . k in bound_QC-variables A ) ;
hence x in bound_QC-variables A ; ::_thesis: verum
end;
hence { (ll . k) where k is Element of NAT : ( 1 <= k & k <= len ll & ll . k in bound_QC-variables A ) } is Subset of (bound_QC-variables A) by TARSKI:def_3; ::_thesis: verum
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 Element of 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 Element of 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 b1 being Subset of (bound_QC-variables A) ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( b1 = F . p & ( 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 Element of 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
deffunc H1( Element of QC-WFF A, Subset of (bound_QC-variables A)) -> Element of bool (bound_QC-variables A) = $2 \ {(bound_in $1)};
deffunc H2( Subset of (bound_QC-variables A), Subset of (bound_QC-variables A)) -> Element of bool (bound_QC-variables A) = $1 \/ $2;
deffunc H3( Subset of (bound_QC-variables A)) -> Subset of (bound_QC-variables A) = $1;
deffunc H4( Element of QC-WFF A) -> Subset of (bound_QC-variables A) = still_not-bound_in (the_arguments_of $1);
reconsider Emp = {} as Subset of (bound_QC-variables A) by XBOOLE_1:2;
consider F being Function of (QC-WFF A),(bool (bound_QC-variables A)) such that
A1: ( F . (VERUM A) = Emp & ( for p being Element of QC-WFF A holds
( ( p is atomic implies F . p = H4(p) ) & ( p is negative implies F . p = H3(F . (the_argument_of p)) ) & ( p is conjunctive implies F . p = H2(F . (the_left_argument_of p),F . (the_right_argument_of p)) ) & ( p is universal implies F . p = H1(p,F . (the_scope_of p)) ) ) ) ) from QC_LANG1:sch_3();
take F . p ; ::_thesis: ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( F . p = 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 Element of 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)} ) ) ) )
take F ; ::_thesis: ( F . p = 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 Element of 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)} ) ) ) )
thus F . p = F . p ; ::_thesis: 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 Element of 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)} ) )
let p be Element of QC-WFF A; ::_thesis: ( F . (VERUM A) = {} & ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Element of 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)} ) )
thus F . (VERUM A) = {} by A1; ::_thesis: ( ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Element of 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)} ) )
thus ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ) ::_thesis: ( ( 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
assume p is atomic ; ::_thesis: F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) }
then F . p = still_not-bound_in (the_arguments_of p) by A1;
hence F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ; ::_thesis: verum
end;
thus ( p is negative implies F . p = F . (the_argument_of p) ) by A1; ::_thesis: ( ( 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)} ) )
thus ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) by A1; ::_thesis: ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} )
assume p is universal ; ::_thesis: F . p = (F . (the_scope_of p)) \ {(bound_in p)}
hence F . p = (F . (the_scope_of p)) \ {(bound_in p)} by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of (bound_QC-variables A) st ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( b1 = F . p & ( 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 Element of 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
( b2 = 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 Element of 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
b1 = b2
proof
let IT, IT9 be Subset of (bound_QC-variables A); ::_thesis: ( 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 Element of 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
( IT9 = 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 Element of 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)} ) ) ) ) implies IT = IT9 )
given F1 being Function of (QC-WFF A),(bool (bound_QC-variables A)) such that A2: IT = F1 . p and
A3: for p being Element of QC-WFF A holds
( F1 . (VERUM A) = {} & ( p is atomic implies F1 . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ) & ( p is negative implies F1 . p = F1 . (the_argument_of p) ) & ( p is conjunctive implies F1 . p = (F1 . (the_left_argument_of p)) \/ (F1 . (the_right_argument_of p)) ) & ( p is universal implies F1 . p = (F1 . (the_scope_of p)) \ {(bound_in p)} ) ) ; ::_thesis: ( for F being Function of (QC-WFF A),(bool (bound_QC-variables A)) holds
( not IT9 = F . p or ex p being Element of QC-WFF A st
( F . (VERUM A) = {} & ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Element of 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)) ) implies ( p is universal & not F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) ) ) or IT = IT9 )
given F2 being Function of (QC-WFF A),(bool (bound_QC-variables A)) such that A4: IT9 = F2 . p and
A5: for p being Element of QC-WFF A holds
( F2 . (VERUM A) = {} & ( p is atomic implies F2 . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ) & ( p is negative implies F2 . p = F2 . (the_argument_of p) ) & ( p is conjunctive implies F2 . p = (F2 . (the_left_argument_of p)) \/ (F2 . (the_right_argument_of p)) ) & ( p is universal implies F2 . p = (F2 . (the_scope_of p)) \ {(bound_in p)} ) ) ; ::_thesis: IT = IT9
defpred S1[ Element of QC-WFF A] means F1 . $1 = F2 . $1;
A6: for k being Element of NAT
for P being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds S1[P ! ll]
proof
let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds S1[P ! ll]
let P be QC-pred_symbol of k,A; ::_thesis: for ll being QC-variable_list of k,A holds S1[P ! ll]
let ll be QC-variable_list of k,A; ::_thesis: S1[P ! ll]
A7: P ! ll is atomic by Def18;
then A8: the_arguments_of (P ! ll) = ll by Def23;
hence F1 . (P ! ll) = { (ll . j) where j is Element of NAT : ( 1 <= j & j <= len ll & ll . j in bound_QC-variables A ) } by A3, A7
.= F2 . (P ! ll) by A5, A7, A8 ;
::_thesis: verum
end;
A9: for p being Element of QC-WFF A st S1[p] holds
S1[ 'not' p]
proof
let p be Element of QC-WFF A; ::_thesis: ( S1[p] implies S1[ 'not' p] )
assume A10: F1 . p = F2 . p ; ::_thesis: S1[ 'not' p]
A11: 'not' p is negative by Def19;
then A12: the_argument_of ('not' p) = p by Def24;
hence F1 . ('not' p) = F2 . p by A3, A10, A11
.= F2 . ('not' p) by A5, A11, A12 ;
::_thesis: verum
end;
A13: for x being bound_QC-variable of A
for p being Element of QC-WFF A st S1[p] holds
S1[ All (x,p)]
proof
let x be bound_QC-variable of A; ::_thesis: for p being Element of QC-WFF A st S1[p] holds
S1[ All (x,p)]
let p be Element of QC-WFF A; ::_thesis: ( S1[p] implies S1[ All (x,p)] )
assume A14: F1 . p = F2 . p ; ::_thesis: S1[ All (x,p)]
A15: All (x,p) is universal by Def21;
then A16: ( the_scope_of (All (x,p)) = p & bound_in (All (x,p)) = x ) by Def27, Def28;
hence F1 . (All (x,p)) = (F2 . p) \ {x} by A3, A14, A15
.= F2 . (All (x,p)) by A5, A15, A16 ;
::_thesis: verum
end;
A17: for p, q being Element of QC-WFF A st S1[p] & S1[q] holds
S1[p '&' q]
proof
let p, q be Element of QC-WFF A; ::_thesis: ( S1[p] & S1[q] implies S1[p '&' q] )
assume A18: ( F1 . p = F2 . p & F1 . q = F2 . q ) ; ::_thesis: S1[p '&' q]
A19: p '&' q is conjunctive by Def20;
then A20: ( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q ) by Def25, Def26;
hence F1 . (p '&' q) = (F2 . p) \/ (F2 . q) by A3, A18, A19
.= F2 . (p '&' q) by A5, A19, A20 ;
::_thesis: verum
end;
A21: S1[ VERUM A] by A3, A5;
for p being Element of QC-WFF A holds S1[p] from QC_LANG1:sch_1(A6, A21, A9, A17, A13);
hence IT = IT9 by A2, A4; ::_thesis: verum
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 (bound_QC-variables A) holds
( b3 = still_not-bound_in p iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( b3 = F . p & ( 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 Element of 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;
attrp is closed means :: QC_LANG1:def 31
still_not-bound_in p = {} ;
end;
:: deftheorem defines closed QC_LANG1:def_31_:_
for A being QC-alphabet
for p being QC-formula of A holds
( p is closed iff still_not-bound_in p = {} );
definition
let A be QC-alphabet ;
mode Relation of A -> Relation means :Def32: :: QC_LANG1:def 32
it well_orders (QC-symbols A) \ NAT;
existence
ex b1 being Relation st b1 well_orders (QC-symbols A) \ NAT by WELLORD2:17;
end;
:: deftheorem Def32 defines Relation QC_LANG1:def_32_:_
for A being QC-alphabet
for b2 being Relation holds
( b2 is Relation of A iff b2 well_orders (QC-symbols A) \ NAT );
definition
let A be QC-alphabet ;
let s, t be QC-symbol of A;
preds <= t means :Def33: :: QC_LANG1:def 33
ex n, m being Element of NAT st
( n = s & 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 Element of 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 Element of 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;
preds < t means :Def34: :: QC_LANG1:def 34
( s <= t & s <> t );
end;
:: deftheorem Def34 defines < QC_LANG1:def_34_:_
for A being QC-alphabet
for s, t being QC-symbol of A holds
( s < t iff ( s <= t & 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
let A be QC-alphabet ; ::_thesis: for s, t, u being QC-symbol of A st s <= t & t <= u holds
s <= u
let s, t, u be QC-symbol of A; ::_thesis: ( s <= t & t <= u implies s <= u )
set R = the Relation of A;
the Relation of A well_orders (QC-symbols A) \ NAT by Def32;
then A1: the Relation of A is_transitive_in (QC-symbols A) \ NAT by WELLORD1:def_5;
assume A2: ( s <= t & t <= u ) ; ::_thesis: s <= u
percases ( s in NAT or not s in NAT ) ;
supposeA3: s in NAT ; ::_thesis: s <= u
then A4: t in NAT by A2, Def33;
then A5: u in NAT by A2, Def33;
consider m, n being Element of NAT such that
A6: ( s = m & t = n & m <= n ) by A2, A3, A4, Def33;
consider k, j being Element of NAT such that
A7: ( t = k & u = j & k <= j ) by A2, A4, A5, Def33;
m <= j by A6, A7, XXREAL_0:2;
hence s <= u by A6, A7, Def33; ::_thesis: verum
end;
supposeA8: not s in NAT ; ::_thesis: s <= u
percases ( t in NAT or not t in NAT ) ;
suppose t in NAT ; ::_thesis: s <= u
then u in NAT by A2, Def33;
hence s <= u by A8, Def33; ::_thesis: verum
end;
supposeA9: not t in NAT ; ::_thesis: s <= u
percases ( u in NAT or not u in NAT ) ;
suppose u in NAT ; ::_thesis: s <= u
hence s <= u by A8, Def33; ::_thesis: verum
end;
supposeA10: not u in NAT ; ::_thesis: s <= u
then A11: ( s in (QC-symbols A) \ NAT & t in (QC-symbols A) \ NAT & u in (QC-symbols A) \ NAT ) by A8, A9, XBOOLE_0:def_5;
( [s,t] in the Relation of A & [t,u] in the Relation of A ) by A2, A8, A9, A10, Def33;
then [s,u] in the Relation of A by A1, A11, RELAT_2:def_8;
hence s <= u by A8, A10, Def33; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
theorem Th22: :: QC_LANG1:22
for A being QC-alphabet
for t being QC-symbol of A holds t <= t
proof
let A be QC-alphabet ; ::_thesis: for t being QC-symbol of A holds t <= t
let t be QC-symbol of A; ::_thesis: t <= t
set R = the Relation of A;
the Relation of A well_orders (QC-symbols A) \ NAT by Def32;
then A1: the Relation of A is_reflexive_in (QC-symbols A) \ NAT by WELLORD1:def_5;
percases ( t in NAT or not t in NAT ) ;
suppose t in NAT ; ::_thesis: t <= t
hence t <= t by Def33; ::_thesis: verum
end;
supposeA2: not t in NAT ; ::_thesis: t <= t
then t in (QC-symbols A) \ NAT by XBOOLE_0:def_5;
then [t,t] in the Relation of A by A1, RELAT_2:def_1;
hence t <= t by A2, Def33; ::_thesis: verum
end;
end;
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
let A be QC-alphabet ; ::_thesis: for t, u being QC-symbol of A st t <= u & u <= t holds
u = t
let t, u be QC-symbol of A; ::_thesis: ( t <= u & u <= t implies u = t )
set R = the Relation of A;
the Relation of A well_orders (QC-symbols A) \ NAT by Def32;
then A1: the Relation of A is_antisymmetric_in (QC-symbols A) \ NAT by WELLORD1:def_5;
assume A2: ( t <= u & u <= t ) ; ::_thesis: u = t
percases ( ( t in NAT & u in NAT ) or not t in NAT or not u in NAT ) ;
supposeA3: ( t in NAT & u in NAT ) ; ::_thesis: u = t
then consider n, m being Element of NAT such that
A4: ( t = n & u = m & n <= m ) by A2, Def33;
consider k, j being Element of NAT such that
A5: ( u = k & t = j & k <= j ) by A2, A3, Def33;
thus u = t by A4, A5, XXREAL_0:1; ::_thesis: verum
end;
suppose ( not t in NAT or not u in NAT ) ; ::_thesis: u = t
percasesthen ( not t in NAT or not u in NAT ) ;
suppose not t in NAT ; ::_thesis: u = t
then A6: ( not t in NAT & not u in NAT ) by A2, Def33;
then A7: ( t in (QC-symbols A) \ NAT & u in (QC-symbols A) \ NAT ) by XBOOLE_0:def_5;
( [t,u] in the Relation of A & [u,t] in the Relation of A ) by A2, A6, Def33;
hence u = t by A1, A7, RELAT_2:def_4; ::_thesis: verum
end;
suppose not u in NAT ; ::_thesis: u = t
then A8: ( not t in NAT & not u in NAT ) by A2, Def33;
then A9: ( t in (QC-symbols A) \ NAT & u in (QC-symbols A) \ NAT ) by XBOOLE_0:def_5;
( [t,u] in the Relation of A & [u,t] in the Relation of A ) by A2, A8, Def33;
hence u = t by A1, A9, RELAT_2:def_4; ::_thesis: verum
end;
end;
end;
end;
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
let A be QC-alphabet ; ::_thesis: for t, u being QC-symbol of A holds
( t <= u or u <= t )
let t, u be QC-symbol of A; ::_thesis: ( t <= u or u <= t )
set R = the Relation of A;
the Relation of A well_orders (QC-symbols A) \ NAT by Def32;
then ( the Relation of A is_connected_in (QC-symbols A) \ NAT & the Relation of A is_reflexive_in (QC-symbols A) \ NAT ) by WELLORD1:def_5;
then A1: the Relation of A is_strongly_connected_in (QC-symbols A) \ NAT by ORDERS_1:7;
percases ( ( t in NAT & u in NAT ) or not t in NAT or not u in NAT ) ;
suppose ( t in NAT & u in NAT ) ; ::_thesis: ( t <= u or u <= t )
then consider n, m being Element of NAT such that
A2: ( n = t & m = u ) ;
( n <= m or m <= n ) ;
hence ( t <= u or u <= t ) by A2, Def33; ::_thesis: verum
end;
suppose ( not t in NAT or not u in NAT ) ; ::_thesis: ( t <= u or u <= t )
percasesthen ( not t in NAT or not u in NAT ) ;
supposeA3: not t in NAT ; ::_thesis: ( t <= u or u <= t )
percases ( u in NAT or not u in NAT ) ;
suppose u in NAT ; ::_thesis: ( t <= u or u <= t )
hence ( t <= u or u <= t ) by A3, Def33; ::_thesis: verum
end;
supposeA4: not u in NAT ; ::_thesis: ( t <= u or u <= t )
then ( t in (QC-symbols A) \ NAT & u in (QC-symbols A) \ NAT ) by A3, XBOOLE_0:def_5;
then ( [t,u] in the Relation of A or [u,t] in the Relation of A ) by A1, RELAT_2:def_7;
hence ( t <= u or u <= t ) by A3, A4, Def33; ::_thesis: verum
end;
end;
end;
supposeA5: not u in NAT ; ::_thesis: ( t <= u or u <= t )
percases ( t in NAT or not t in NAT ) ;
suppose t in NAT ; ::_thesis: ( t <= u or u <= t )
hence ( t <= u or u <= t ) by A5, Def33; ::_thesis: verum
end;
supposeA6: not t in NAT ; ::_thesis: ( t <= u or u <= t )
then ( t in (QC-symbols A) \ NAT & u in (QC-symbols A) \ NAT ) by A5, XBOOLE_0:def_5;
then ( [u,t] in the Relation of A or [t,u] in the Relation of A ) by A1, RELAT_2:def_7;
hence ( t <= u or u <= t ) by A5, A6, Def33; ::_thesis: verum
end;
end;
end;
end;
end;
end;
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 )
proof
let A be QC-alphabet ; ::_thesis: for s, t being QC-symbol of A holds
( s < t iff not t <= s )
let s, t be QC-symbol of A; ::_thesis: ( s < t iff not t <= s )
thus ( s < t implies not t <= s ) ::_thesis: ( not t <= s implies s < t )
proof
assume s < t ; ::_thesis: not t <= s
then A1: ( s <= t & not s = t ) by Def34;
assume t <= s ; ::_thesis: contradiction
hence contradiction by A1, Th23; ::_thesis: verum
end;
assume not t <= s ; ::_thesis: s < t
then ( s <= t & not t = s ) by Th24;
hence s < t by Def34; ::_thesis: verum
end;
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 )
proof
let A be QC-alphabet ; ::_thesis: for s, t being QC-symbol of A holds
( s < t or s = t or t < s )
let s, t be QC-symbol of A; ::_thesis: ( s < t or s = t or t < s )
assume ( not s < t & not s = t ) ; ::_thesis: t < s
then ( t <= s & not s = t ) by Th25;
hence t < s by Def34; ::_thesis: verum
end;
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 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
percases ( Y c= NAT or not Y c= NAT ) ;
suppose Y c= NAT ; ::_thesis: 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 ) )
then reconsider Y = Y as non empty Subset of NAT ;
set y = min* Y;
NAT c= QC-symbols A by Th3;
then reconsider yp = min* Y as QC-symbol of A by TARSKI:def_3;
take yp ; ::_thesis: ( yp in Y & ( for t being QC-symbol of A st t in Y holds
yp <= t ) )
for t being QC-symbol of A st t in Y holds
yp <= t
proof
let t be QC-symbol of A; ::_thesis: ( t in Y implies yp <= t )
assume A1: t in Y ; ::_thesis: yp <= t
reconsider t = t as Nat by A1;
min* Y <= t by A1, NAT_1:def_1;
hence yp <= t by A1, Def33; ::_thesis: verum
end;
hence ( yp in Y & ( for t being QC-symbol of A st t in Y holds
yp <= t ) ) by NAT_1:def_1; ::_thesis: verum
end;
suppose not Y c= NAT ; ::_thesis: 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 ) )
then consider a being set such that
A2: ( a in Y & not a in NAT ) by TARSKI:def_3;
set R = the Relation of A;
( the Relation of A well_orders (QC-symbols A) \ NAT & Y \ NAT <> {} ) by A2, XBOOLE_0:def_5, Def32;
then consider y being set such that
A3: ( y in Y \ NAT & ( for b being set st b in Y \ NAT holds
[y,b] in the Relation of A ) ) by XBOOLE_1:33, WELLORD1:5;
reconsider y = y as QC-symbol of A by A3;
A4: ( not y in NAT & y in Y ) by A3, XBOOLE_0:def_5;
for s being QC-symbol of A st s in Y holds
y <= s
proof
let s be QC-symbol of A; ::_thesis: ( s in Y implies y <= s )
assume A5: s in Y ; ::_thesis: y <= s
percases ( s in NAT or not s in NAT ) ;
suppose s in NAT ; ::_thesis: y <= s
hence y <= s by A4, Def33; ::_thesis: verum
end;
supposeA6: not s in NAT ; ::_thesis: y <= s
then s in Y \ NAT by A5, XBOOLE_0:def_5;
then [y,s] in the Relation of A by A3;
hence y <= s by A4, A6, Def33; ::_thesis: verum
end;
end;
end;
hence 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 ) ) by A4; ::_thesis: verum
end;
end;
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
let t, u be QC-symbol of A; ::_thesis: ( t in Y & ( for t being QC-symbol of A st t in Y holds
t <= t ) & u in Y & ( for t being QC-symbol of A st t in Y holds
u <= t ) implies t = u )
assume A7: ( t in Y & ( for s being QC-symbol of A st s in Y holds
t <= s ) & u in Y & ( for s being QC-symbol of A st s in Y holds
u <= s ) ) ; ::_thesis: t = u
( t <= u & u <= t ) by A7;
hence t = u by Th23; ::_thesis: verum
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 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
QC-symbols A c= QC-symbols A ;
then reconsider symb = QC-symbols A as non empty Subset of (QC-symbols A) ;
set z = min symb;
take min symb ; ::_thesis: for t being QC-symbol of A holds min symb <= t
thus for t being QC-symbol of A holds min symb <= t by Def35; ::_thesis: verum
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
let s, t be QC-symbol of A; ::_thesis: ( ( for t being QC-symbol of A holds s <= t ) & ( for t being QC-symbol of A holds t <= t ) implies s = t )
assume A1: ( ( for u being QC-symbol of A holds s <= u ) & ( for u being QC-symbol of A holds t <= u ) ) ; ::_thesis: s = t
( s <= t & t <= s ) by A1;
hence s = t by Th23; ::_thesis: verum
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 (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
set e = { t where t is QC-symbol of A : s < t } ;
A1: { t where t is QC-symbol of A : s < t } c= QC-symbols A
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { t where t is QC-symbol of A : s < t } or a in QC-symbols A )
assume a in { t where t is QC-symbol of A : s < t } ; ::_thesis: a in QC-symbols A
then consider t being QC-symbol of A such that
A2: ( a = t & s < t ) ;
thus a in QC-symbols A by A2; ::_thesis: verum
end;
ex a being set st a in { t where t is QC-symbol of A : s < t }
proof
percases ( s in NAT or not s in NAT ) ;
suppose s in NAT ; ::_thesis: ex a being set st a in { t where t is QC-symbol of A : s < t }
then consider n being Element of NAT such that
A3: s = n ;
reconsider a = n + 1 as Element of NAT ;
NAT c= QC-symbols A by Th3;
then reconsider b = a as QC-symbol of A by TARSKI:def_3;
( not n = a & n <= a ) by NAT_1:19;
then ( s <= b & not s = b ) by A3, Def33;
then s < b by Def34;
then b in { t where t is QC-symbol of A : s < t } ;
hence ex a being set st a in { t where t is QC-symbol of A : s < t } ; ::_thesis: verum
end;
supposeA4: not s in NAT ; ::_thesis: ex a being set st a in { t where t is QC-symbol of A : s < t }
reconsider a = 0 as QC-symbol of A by Th3;
( not s = a & s <= a ) by A4, Def33;
then s < a by Def34;
then a in { t where t is QC-symbol of A : s < t } ;
hence ex a being set st a in { t where t is QC-symbol of A : s < t } ; ::_thesis: verum
end;
end;
end;
hence { t where t is QC-symbol of A : s < t } is non empty Subset of (QC-symbols A) by A1; ::_thesis: verum
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;
funcs ++ -> QC-symbol of A equals :: QC_LANG1:def 38
min (Seg s);
coherence
min (Seg s) is QC-symbol of A ;
end;
:: deftheorem defines ++ QC_LANG1:def_38_:_
for A being QC-alphabet
for s being QC-symbol of A holds s ++ = min (Seg s);
theorem Th27: :: QC_LANG1:27
for A being QC-alphabet
for s being QC-symbol of A holds s < s ++
proof
let A be QC-alphabet ; ::_thesis: for s being QC-symbol of A holds s < s ++
let s be QC-symbol of A; ::_thesis: s < s ++
s ++ in Seg s by Def35;
then consider t being QC-symbol of A such that
A1: ( t = s ++ & s < t ) ;
thus s < s ++ by A1; ::_thesis: verum
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
let A be QC-alphabet ; ::_thesis: for Y1, Y2 being non empty Subset of (QC-symbols A) st Y1 c= Y2 holds
min Y2 <= min Y1
let Y1, Y2 be non empty Subset of (QC-symbols A); ::_thesis: ( Y1 c= Y2 implies min Y2 <= min Y1 )
assume A1: Y1 c= Y2 ; ::_thesis: min Y2 <= min Y1
min Y1 in Y1 by Def35;
hence min Y2 <= min Y1 by A1, Def35; ::_thesis: verum
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
proof
let A be QC-alphabet ; ::_thesis: for s, t, v being QC-symbol of A st s <= t & t < v holds
s < v
let s, t, v be QC-symbol of A; ::_thesis: ( s <= t & t < v implies s < v )
assume A1: ( s <= t & t < v ) ; ::_thesis: s < v
then ( s <= t & t <= v ) by Def34;
then A2: s <= v by Th21;
not s = v by A1, Th25;
hence s < v by A2, Def34; ::_thesis: verum
end;
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
proof
let A be QC-alphabet ; ::_thesis: for s, t, v being QC-symbol of A st s < t & t <= v holds
s < v
let s, t, v be QC-symbol of A; ::_thesis: ( s < t & t <= v implies s < v )
assume A1: ( s < t & t <= v ) ; ::_thesis: s < v
then ( s <= t & t <= v ) by Def34;
then A2: s <= v by Th21;
not s = v by A1, Th25;
hence s < v by A2, Def34; ::_thesis: verum
end;
definition
let A be QC-alphabet ;
let s be set ;
funcs @ A -> QC-symbol of A equals :Def39: :: QC_LANG1:def 39
s if s is QC-symbol of A
otherwise 0 ;
correctness
coherence
( ( s is QC-symbol of A implies s is QC-symbol of A ) & ( 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 Element of NAT ;
funct + n -> QC-symbol of A means :Def40: :: QC_LANG1:def 40
ex f being Function of NAT,(QC-symbols A) st
( it = f . n & f . 0 = t & ( for k being Element of NAT holds f . (k + 1) = (f . k) ++ ) );
existence
ex b1 being QC-symbol of A ex f being Function of NAT,(QC-symbols A) st
( b1 = f . n & f . 0 = t & ( for k being Element of NAT holds f . (k + 1) = (f . k) ++ ) )
proof
deffunc H1( set , set ) -> QC-symbol of A = ($2 @ A) ++ ;
consider f being Function of NAT,(QC-symbols A) such that
A1: ( f . 0 = t & ( for k being Nat holds f . (k + 1) = H1(k,f . k) ) ) from NAT_1:sch_12();
take f . n ; ::_thesis: ex f being Function of NAT,(QC-symbols A) st
( f . n = f . n & f . 0 = t & ( for k being Element of NAT holds f . (k + 1) = (f . k) ++ ) )
for k being Element of NAT holds f . (k + 1) = (f . k) ++
proof
let k be Element of NAT ; ::_thesis: f . (k + 1) = (f . k) ++
( (f . k) ++ = H1(k,f . k) & H1(k,f . k) = f . (k + 1) ) by A1, Def39;
hence f . (k + 1) = (f . k) ++ ; ::_thesis: verum
end;
hence ex f being Function of NAT,(QC-symbols A) st
( f . n = f . n & f . 0 = t & ( for k being Element of NAT holds f . (k + 1) = (f . k) ++ ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being QC-symbol of A st ex f being Function of NAT,(QC-symbols A) st
( b1 = f . n & f . 0 = t & ( for k being Element of NAT holds f . (k + 1) = (f . k) ++ ) ) & ex f being Function of NAT,(QC-symbols A) st
( b2 = f . n & f . 0 = t & ( for k being Element of NAT holds f . (k + 1) = (f . k) ++ ) ) holds
b1 = b2
proof
let u, v be QC-symbol of A; ::_thesis: ( ex f being Function of NAT,(QC-symbols A) st
( u = f . n & f . 0 = t & ( for k being Element of NAT holds f . (k + 1) = (f . k) ++ ) ) & ex f being Function of NAT,(QC-symbols A) st
( v = f . n & f . 0 = t & ( for k being Element of NAT holds f . (k + 1) = (f . k) ++ ) ) implies u = v )
assume A2: ( ex f being Function of NAT,(QC-symbols A) st
( f . n = u & f . 0 = t & ( for k being Element of NAT holds f . (k + 1) = (f . k) ++ ) ) & ex g being Function of NAT,(QC-symbols A) st
( g . n = v & g . 0 = t & ( for k being Element of NAT holds g . (k + 1) = (g . k) ++ ) ) ) ; ::_thesis: u = v
consider f being Function of NAT,(QC-symbols A) such that
A3: ( f . n = u & f . 0 = t & ( for k being Element of NAT holds f . (k + 1) = (f . k) ++ ) ) by A2;
consider g being Function of NAT,(QC-symbols A) such that
A4: ( g . n = v & g . 0 = t & ( for k being Element of NAT holds g . (k + 1) = (g . k) ++ ) ) by A2;
defpred S1[ Element of NAT ] means f . $1 = g . $1;
A5: S1[ 0 ] by A3, A4;
A6: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A7: S1[k] ; ::_thesis: S1[k + 1]
thus f . (k + 1) = (f . k) ++ by A3
.= g . (k + 1) by A4, A7 ; ::_thesis: verum
end;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A5, A6);
hence u = v by A3, A4; ::_thesis: verum
end;
end;
:: deftheorem Def40 defines + QC_LANG1:def_40_:_
for A being QC-alphabet
for t being QC-symbol of A
for n being Element of NAT
for b4 being QC-symbol of A holds
( b4 = t + n iff ex f being Function of NAT,(QC-symbols A) st
( b4 = f . n & f . 0 = t & ( for k being Element of NAT holds f . (k + 1) = (f . k) ++ ) ) );
theorem :: QC_LANG1:31
for A being QC-alphabet
for n being Element of NAT
for t being QC-symbol of A holds t <= t + n
proof
let A be QC-alphabet ; ::_thesis: for n being Element of NAT
for t being QC-symbol of A holds t <= t + n
let n be Element of NAT ; ::_thesis: for t being QC-symbol of A holds t <= t + n
let t be QC-symbol of A; ::_thesis: t <= t + n
defpred S1[ Element of NAT ] means t <= t + $1;
A1: S1[ 0 ]
proof
consider f being Function of NAT,(QC-symbols A) such that
A2: ( t + 0 = f . 0 & f . 0 = t & ( for k being Element of NAT holds f . (k + 1) = (f . k) ++ ) ) by Def40;
thus S1[ 0 ] by A2, Th22; ::_thesis: verum
end;
A3: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: t <= t + k ; ::_thesis: S1[k + 1]
consider f being Function of NAT,(QC-symbols A) such that
A5: ( t + (k + 1) = f . (k + 1) & f . 0 = t & ( for k being Element of NAT holds f . (k + 1) = (f . k) ++ ) ) by Def40;
f . k = t + k by A5, Def40;
then f . (k + 1) = (t + k) ++ by A5;
then t < t + (k + 1) by A5, A4, Th27, Th29;
hence S1[k + 1] by Def34; ::_thesis: verum
end;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A1, A3);
hence t <= t + n ; ::_thesis: verum
end;
definition
let A be QC-alphabet ;
let Y be set ;
funcA -one_in Y -> QC-symbol of A equals :: QC_LANG1:def 41
the Element of Y if Y is non empty Subset of (QC-symbols A)
otherwise 0 A;
coherence
( ( Y is non empty Subset of (QC-symbols A) implies the Element of Y is QC-symbol of A ) & ( Y is not non empty Subset of (QC-symbols A) implies 0 A is QC-symbol of A ) )
proof
thus ( Y is non empty Subset of (QC-symbols A) implies the Element of Y is QC-symbol of A ) ::_thesis: ( Y is not non empty Subset of (QC-symbols A) implies 0 A is QC-symbol of A )
proof
assume A1: Y is non empty Subset of (QC-symbols A) ; ::_thesis: the Element of Y is QC-symbol of A
consider a being set such that
A2: a = the Element of Y ;
A3: a in Y by A1, A2;
a is QC-symbol of A by A1, A3;
hence the Element of Y is QC-symbol of A by A2; ::_thesis: verum
end;
thus ( Y is not non empty Subset of (QC-symbols A) implies 0 A is QC-symbol of A ) ; ::_thesis: verum
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 (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 ) );