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