:: ABCMIZ_A semantic presentation begin theorem Th1: :: ABCMIZ_A:1 for x being pair set holds x = [(x `1),(x `2)] ; scheme :: ABCMIZ_A:sch 1 MinimalElement{ F1() -> non empty finite set , P1[ set , set ] } : ex x being set st ( x in F1() & ( for y being set st y in F1() holds not P1[y,x] ) ) provided A1: for x, y being set st x in F1() & y in F1() & P1[x,y] holds not P1[y,x] and A2: for x, y, z being set st x in F1() & y in F1() & z in F1() & P1[x,y] & P1[y,z] holds P1[x,z] proof assume A3: for x being set st x in F1() holds ex y being set st ( y in F1() & P1[y,x] ) ; ::_thesis: contradiction set n = card F1(); set x0 = the Element of F1(); defpred S1[ Nat, set , set ] means ( $2 in F1() implies ( $3 in F1() & P1[$3,$2] ) ); A4: for m being Element of NAT st 1 <= m & m < (card F1()) + 1 holds for x being set ex y being set st S1[m,x,y] proof let m be Element of NAT ; ::_thesis: ( 1 <= m & m < (card F1()) + 1 implies for x being set ex y being set st S1[m,x,y] ) assume ( 1 <= m & m < (card F1()) + 1 ) ; ::_thesis: for x being set ex y being set st S1[m,x,y] let x be set ; ::_thesis: ex y being set st S1[m,x,y] percases ( x nin F1() or x in F1() ) ; supposeA5: x nin F1() ; ::_thesis: ex y being set st S1[m,x,y] set y = the set ; take the set ; ::_thesis: S1[m,x, the set ] thus S1[m,x, the set ] by A5; ::_thesis: verum end; suppose x in F1() ; ::_thesis: ex y being set st S1[m,x,y] then consider y being set such that A6: ( y in F1() & P1[y,x] ) by A3; take y ; ::_thesis: S1[m,x,y] thus S1[m,x,y] by A6; ::_thesis: verum end; end; end; consider p being FinSequence such that A7: len p = (card F1()) + 1 and A8: ( p . 1 = the Element of F1() or (card F1()) + 1 = 0 ) and A9: for i being Element of NAT st 1 <= i & i < (card F1()) + 1 holds S1[i,p . i,p . (i + 1)] from RECDEF_1:sch_3(A4); defpred S2[ Nat] means ( $1 in dom p implies p . $1 in F1() ); A10: S2[ 0 ] by FINSEQ_3:25; A11: now__::_thesis:_for_i_being_Nat_st_S2[i]_holds_ S2[i_+_1] let i be Nat; ::_thesis: ( S2[i] implies S2[i + 1] ) assume A12: S2[i] ; ::_thesis: S2[i + 1] thus S2[i + 1] ::_thesis: verum proof assume i + 1 in dom p ; ::_thesis: p . (i + 1) in F1() then i + 1 <= (card F1()) + 1 by A7, FINSEQ_3:25; then A13: i < (card F1()) + 1 by NAT_1:13; percases ( i = 0 or i > 0 ) by NAT_1:3; suppose i = 0 ; ::_thesis: p . (i + 1) in F1() hence p . (i + 1) in F1() by A8; ::_thesis: verum end; suppose i > 0 ; ::_thesis: p . (i + 1) in F1() then ( i >= 0 + 1 & i is Element of NAT ) by NAT_1:13, ORDINAL1:def_12; hence p . (i + 1) in F1() by A12, A7, A9, A13, FINSEQ_3:25; ::_thesis: verum end; end; end; end; A14: for i being Nat holds S2[i] from NAT_1:sch_2(A10, A11); A15: rng p c= F1() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in F1() ) assume x in rng p ; ::_thesis: x in F1() then ex i being set st ( i in dom p & x = p . i ) by FUNCT_1:def_3; hence x in F1() by A14; ::_thesis: verum end; A16: for i, j being Nat st 1 <= i & i < j & j <= (card F1()) + 1 holds P1[p . j,p . i] proof let i, j be Nat; ::_thesis: ( 1 <= i & i < j & j <= (card F1()) + 1 implies P1[p . j,p . i] ) assume A17: 1 <= i ; ::_thesis: ( not i < j or not j <= (card F1()) + 1 or P1[p . j,p . i] ) assume A18: i < j ; ::_thesis: ( not j <= (card F1()) + 1 or P1[p . j,p . i] ) then i + 1 <= j by NAT_1:13; then consider k being Nat such that A19: j = (i + 1) + k by NAT_1:10; assume A20: j <= (card F1()) + 1 ; ::_thesis: P1[p . j,p . i] then i <= (card F1()) + 1 by A18, XXREAL_0:2; then A21: i in dom p by A17, A7, FINSEQ_3:25; defpred S3[ Nat] means ( (i + 1) + $1 <= (card F1()) + 1 implies P1[p . ((i + 1) + $1),p . i] ); A22: S3[ 0 ] proof assume (i + 1) + 0 <= (card F1()) + 1 ; ::_thesis: P1[p . ((i + 1) + 0),p . i] then A23: i < (card F1()) + 1 by NAT_1:13; ( p . i in F1() & i is Element of NAT ) by A14, A21; hence P1[p . ((i + 1) + 0),p . i] by A9, A17, A23; ::_thesis: verum end; A24: now__::_thesis:_for_k_being_Nat_st_S3[k]_holds_ S3[k_+_1] let k be Nat; ::_thesis: ( S3[k] implies S3[k + 1] ) assume A25: S3[k] ; ::_thesis: S3[k + 1] thus S3[k + 1] ::_thesis: verum proof assume A26: (i + 1) + (k + 1) <= (card F1()) + 1 ; ::_thesis: P1[p . ((i + 1) + (k + 1)),p . i] A27: (i + 1) + (k + 1) = ((i + 1) + k) + 1 ; then A28: (i + 1) + k < (card F1()) + 1 by A26, NAT_1:13; A29: p . i in F1() by A14, A21; (i + 1) + k = 1 + (i + k) ; then A30: 1 <= (i + 1) + k by NAT_1:11; then (i + 1) + k in dom p by A7, A28, FINSEQ_3:25; then A31: ( p . ((i + 1) + k) in F1() & (i + 1) + k is Element of NAT ) by A14; then ( p . ((i + 1) + (k + 1)) in F1() & P1[p . ((i + 1) + (k + 1)),p . ((i + 1) + k)] ) by A9, A28, A27, A30; hence P1[p . ((i + 1) + (k + 1)),p . i] by A2, A28, A25, A31, A29; ::_thesis: verum end; end; for k being Nat holds S3[k] from NAT_1:sch_2(A22, A24); hence P1[p . j,p . i] by A19, A20; ::_thesis: verum end; A32: ( dom p = Seg ((card F1()) + 1) & card (Seg ((card F1()) + 1)) = (card F1()) + 1 ) by A7, FINSEQ_1:57, FINSEQ_1:def_3; card (rng p) c= card F1() by A15, CARD_1:11; then ( card (rng p) <= card F1() & card F1() < (card F1()) + 1 ) by NAT_1:19, NAT_1:39; then not dom p, rng p are_equipotent by A32, CARD_1:5; then not p is one-to-one by WELLORD2:def_4; then consider i, j being set such that A33: ( i in dom p & j in dom p & p . i = p . j & i <> j ) by FUNCT_1:def_4; reconsider i = i, j = j as Nat by A33; A34: ( 1 <= i & 1 <= j & i <= (card F1()) + 1 & j <= (card F1()) + 1 ) by A7, A33, FINSEQ_3:25; p . i in rng p by A33, FUNCT_1:def_3; then A35: p . i in F1() by A15; ( i < j or j < i ) by A33, XXREAL_0:1; then P1[p . i,p . i] by A16, A33, A34; hence contradiction by A1, A35; ::_thesis: verum end; scheme :: ABCMIZ_A:sch 2 FiniteC{ F1() -> finite set , P1[ set ] } : P1[F1()] provided A1: for A being Subset of F1() st ( for B being set st B c< A holds P1[B] ) holds P1[A] proof defpred S1[ Nat] means for A being Subset of F1() st card A = $1 holds P1[A]; A2: for n being Nat st ( for i being Nat st i < n holds S1[i] ) holds S1[n] proof let n be Nat; ::_thesis: ( ( for i being Nat st i < n holds S1[i] ) implies S1[n] ) assume A3: for i being Nat st i < n holds S1[i] ; ::_thesis: S1[n] let A be Subset of F1(); ::_thesis: ( card A = n implies P1[A] ) assume A4: card A = n ; ::_thesis: P1[A] now__::_thesis:_for_B_being_set_st_B_c<_A_holds_ P1[B] let B be set ; ::_thesis: ( B c< A implies P1[B] ) assume A5: B c< A ; ::_thesis: P1[B] B c= A by A5, XBOOLE_0:def_8; then reconsider B9 = B as Subset of F1() by XBOOLE_1:1; card B9 < n by A4, A5, TREES_1:6; hence P1[B] by A3; ::_thesis: verum end; hence P1[A] by A1; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_4(A2); then ( S1[ card F1()] & [#] F1() = F1() ) ; hence P1[F1()] ; ::_thesis: verum end; scheme :: ABCMIZ_A:sch 3 Numeration{ F1() -> finite set , P1[ set , set ] } : ex s being one-to-one FinSequence st ( rng s = F1() & ( for i, j being Nat st i in dom s & j in dom s & P1[s . i,s . j] holds i < j ) ) provided A1: for x, y being set st x in F1() & y in F1() & P1[x,y] holds not P1[y,x] and A2: for x, y, z being set st x in F1() & y in F1() & z in F1() & P1[x,y] & P1[y,z] holds P1[x,z] proof defpred S1[ set ] means ex s being one-to-one FinSequence st ( rng s = $1 & ( for i, j being Nat st i in dom s & j in dom s & P1[s . i,s . j] holds i < j ) ); A3: S1[ {} ] proof reconsider s = {} as one-to-one FinSequence ; take s ; ::_thesis: ( rng s = {} & ( for i, j being Nat st i in dom s & j in dom s & P1[s . i,s . j] holds i < j ) ) thus ( rng s = {} & ( for i, j being Nat st i in dom s & j in dom s & P1[s . i,s . j] holds i < j ) ) ; ::_thesis: verum end; A4: for A being Subset of F1() st ( for B being set st B c< A holds S1[B] ) holds S1[A] proof let A be Subset of F1(); ::_thesis: ( ( for B being set st B c< A holds S1[B] ) implies S1[A] ) assume A5: for B being set st B c< A holds S1[B] ; ::_thesis: S1[A] percases ( A is empty or not A is empty ) ; suppose A is empty ; ::_thesis: S1[A] hence S1[A] by A3; ::_thesis: verum end; suppose not A is empty ; ::_thesis: S1[A] then reconsider A9 = A as non empty finite set ; A6: for x, y being set st x in A9 & y in A9 & P1[x,y] holds not P1[y,x] by A1; A7: for x, y, z being set st x in A9 & y in A9 & z in A9 & P1[x,y] & P1[y,z] holds P1[x,z] by A2; consider x being set such that A8: ( x in A9 & ( for y being set st y in A9 holds not P1[y,x] ) ) from ABCMIZ_A:sch_1(A6, A7); set B = A \ {x}; A9: ( x nin A \ {x} & A \ {x} c= A ) by XBOOLE_1:36, ZFMISC_1:56; then A \ {x} c< A by A8, XBOOLE_0:def_8; then consider s being one-to-one FinSequence such that A10: rng s = A \ {x} and A11: for i, j being Nat st i in dom s & j in dom s & P1[s . i,s . j] holds i < j by A5; ( <*x*> is one-to-one & rng <*x*> = {x} & {x} misses A \ {x} ) by FINSEQ_1:39, FINSEQ_3:93, XBOOLE_1:79; then reconsider s9 = <*x*> ^ s as one-to-one FinSequence by A10, FINSEQ_3:91; A12: {x} c= A by A8, ZFMISC_1:31; A13: len <*x*> = 1 by FINSEQ_1:40; thus S1[A] ::_thesis: verum proof take s9 ; ::_thesis: ( rng s9 = A & ( for i, j being Nat st i in dom s9 & j in dom s9 & P1[s9 . i,s9 . j] holds i < j ) ) thus rng s9 = (rng <*x*>) \/ (rng s) by FINSEQ_1:31 .= {x} \/ (A \ {x}) by A10, FINSEQ_1:38 .= A by A12, XBOOLE_1:45 ; ::_thesis: for i, j being Nat st i in dom s9 & j in dom s9 & P1[s9 . i,s9 . j] holds i < j let i, j be Nat; ::_thesis: ( i in dom s9 & j in dom s9 & P1[s9 . i,s9 . j] implies i < j ) assume A14: ( i in dom s9 & j in dom s9 & P1[s9 . i,s9 . j] ) ; ::_thesis: i < j A15: dom <*x*> = Seg 1 by FINSEQ_1:38; percases ( ( i in dom <*x*> & j in dom <*x*> ) or ( i in dom <*x*> & ex n being Nat st ( n in dom s & j = 1 + n ) ) or ( j in dom <*x*> & ex n being Nat st ( n in dom s & i = 1 + n ) ) or ( ex n being Nat st ( n in dom s & i = 1 + n ) & ex n being Nat st ( n in dom s & j = 1 + n ) ) ) by A13, A14, FINSEQ_1:25; suppose ( i in dom <*x*> & j in dom <*x*> ) ; ::_thesis: i < j then ( i = 1 & j = 1 ) by A15, FINSEQ_1:2, TARSKI:def_1; then ( s9 . i = x & s9 . j = x ) by FINSEQ_1:41; hence i < j by A8, A14; ::_thesis: verum end; supposeA16: ( i in dom <*x*> & ex n being Nat st ( n in dom s & j = 1 + n ) ) ; ::_thesis: i < j then A17: i = 1 by A15, FINSEQ_1:2, TARSKI:def_1; consider n being Nat such that A18: ( n in dom s & j = 1 + n ) by A16; 1 <= n by A18, FINSEQ_3:25; hence i < j by A17, A18, NAT_1:13; ::_thesis: verum end; supposeA19: ( j in dom <*x*> & ex n being Nat st ( n in dom s & i = 1 + n ) ) ; ::_thesis: i < j then j = 1 by A15, FINSEQ_1:2, TARSKI:def_1; then A20: s9 . j = x by FINSEQ_1:41; consider n being Nat such that A21: ( n in dom s & i = 1 + n ) by A19; s9 . i = s . n by A13, A21, FINSEQ_1:def_7; then s9 . i in rng s by A21, FUNCT_1:def_3; hence i < j by A8, A14, A20, A9, A10; ::_thesis: verum end; suppose ( ex n being Nat st ( n in dom s & i = 1 + n ) & ex n being Nat st ( n in dom s & j = 1 + n ) ) ; ::_thesis: i < j then consider ni, nj being Nat such that A22: ( ni in dom s & i = 1 + ni & nj in dom s & j = 1 + nj ) ; ( s9 . i = s . ni & s9 . j = s . nj ) by A13, A22, FINSEQ_1:def_7; then ni < nj by A11, A14, A22; hence i < j by A22, XREAL_1:6; ::_thesis: verum end; end; end; end; end; end; thus S1[F1()] from ABCMIZ_A:sch_2(A4); ::_thesis: verum end; theorem Th2: :: ABCMIZ_A:2 for x being variable holds varcl (vars x) = vars x proof let x be variable; ::_thesis: varcl (vars x) = vars x x in Vars ; then consider A being Subset of Vars, j being Element of NAT such that A1: ( x = [(varcl A),j] & A is finite ) by ABCMIZ_1:18; vars x = varcl A by A1, MCART_1:7; hence varcl (vars x) = vars x ; ::_thesis: verum end; theorem Th3: :: ABCMIZ_A:3 for C being initialized ConstructorSignature for e being expression of C holds ( e is compound iff for x being Element of Vars holds not e = x -term C ) proof let C be initialized ConstructorSignature; ::_thesis: for e being expression of C holds ( e is compound iff for x being Element of Vars holds not e = x -term C ) let e be expression of C; ::_thesis: ( e is compound iff for x being Element of Vars holds not e = x -term C ) ( ex x being variable st e = x -term C or ex c being constructor OperSymbol of C ex p being FinSequence of QuasiTerms C st ( len p = len (the_arity_of c) & e = c -trm p ) or ex a being expression of C, an_Adj C st e = (non_op C) term a or ex a being expression of C, an_Adj C ex t being expression of C, a_Type C st e = (ast C) term (a,t) ) by ABCMIZ_1:53; hence ( e is compound iff for x being Element of Vars holds not e = x -term C ) ; ::_thesis: verum end; begin registration cluster empty Relation-like NAT -defined Vars -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like for Element of QuasiLoci ; existence ex b1 being quasi-loci st b1 is empty by ABCMIZ_1:29; end; definition let C be ConstructorSignature; attrC is standardized means :Def1: :: ABCMIZ_A:def 1 for o being OperSymbol of C st o is constructor holds ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) ); end; :: deftheorem Def1 defines standardized ABCMIZ_A:def_1_:_ for C being ConstructorSignature holds ( C is standardized iff for o being OperSymbol of C st o is constructor holds ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) ) ); theorem Th4: :: ABCMIZ_A:4 for C being ConstructorSignature st C is standardized holds for o being OperSymbol of C holds ( o is constructor iff o in Constructors ) proof let C be ConstructorSignature; ::_thesis: ( C is standardized implies for o being OperSymbol of C holds ( o is constructor iff o in Constructors ) ) assume A1: C is standardized ; ::_thesis: for o being OperSymbol of C holds ( o is constructor iff o in Constructors ) let o be OperSymbol of C; ::_thesis: ( o is constructor iff o in Constructors ) thus ( o is constructor implies o in Constructors ) by A1, Def1; ::_thesis: ( o in Constructors implies o is constructor ) assume o in Constructors ; ::_thesis: o is constructor then not o in {*,non_op} by ABCMIZ_1:39, XBOOLE_0:3; hence ( o <> * & o <> non_op ) by TARSKI:def_2; :: according to ABCMIZ_1:def_11 ::_thesis: verum end; registration cluster MaxConstrSign -> standardized ; coherence MaxConstrSign is standardized proof let o be OperSymbol of MaxConstrSign; :: according to ABCMIZ_A:def_1 ::_thesis: ( o is constructor implies ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) ) ) A1: the carrier' of MaxConstrSign = {*,non_op} \/ Constructors by ABCMIZ_1:def_24; assume A2: o is constructor ; ::_thesis: ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) ) then A3: ( the ResultSort of MaxConstrSign . o = o `1 & card ( the Arity of MaxConstrSign . o) = card ((o `2) `1) ) by ABCMIZ_1:def_24; ( o <> * & o <> non_op ) by A2, ABCMIZ_1:def_11; then not o in {*,non_op} by TARSKI:def_2; hence ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) ) by A3, A1, XBOOLE_0:def_3; ::_thesis: verum end; end; registration cluster non empty non void V68() strict V146() constructor initialized standardized for ManySortedSign ; existence ex b1 being ConstructorSignature st ( b1 is initialized & b1 is standardized & b1 is strict ) proof take MaxConstrSign ; ::_thesis: ( MaxConstrSign is initialized & MaxConstrSign is standardized & MaxConstrSign is strict ) thus ( MaxConstrSign is initialized & MaxConstrSign is standardized & MaxConstrSign is strict ) ; ::_thesis: verum end; end; definition let C be initialized standardized ConstructorSignature; let c be constructor OperSymbol of C; func loci_of c -> quasi-loci equals :: ABCMIZ_A:def 2 (c `2) `1 ; coherence (c `2) `1 is quasi-loci proof reconsider c = c as Element of Constructors by Th4; loci_of c is quasi-loci ; hence (c `2) `1 is quasi-loci ; ::_thesis: verum end; end; :: deftheorem defines loci_of ABCMIZ_A:def_2_:_ for C being initialized standardized ConstructorSignature for c being constructor OperSymbol of C holds loci_of c = (c `2) `1 ; registration let C be ConstructorSignature; clusterV146() constructor for Subsignature of C; existence ex b1 being Subsignature of C st b1 is constructor proof reconsider S = C as Subsignature of C by INSTALG1:15; take S ; ::_thesis: S is constructor thus S is constructor ; ::_thesis: verum end; end; registration let C be initialized ConstructorSignature; cluster non empty non void V68() V146() constructor initialized for Subsignature of C; existence ex b1 being constructor Subsignature of C st b1 is initialized proof reconsider S = C as constructor Subsignature of C by INSTALG1:15; take S ; ::_thesis: S is initialized thus S is initialized ; ::_thesis: verum end; end; registration let C be standardized ConstructorSignature; cluster constructor -> constructor standardized for Subsignature of C; coherence for b1 being constructor Subsignature of C holds b1 is standardized proof let S be constructor Subsignature of C; ::_thesis: S is standardized let o be OperSymbol of S; :: according to ABCMIZ_A:def_1 ::_thesis: ( o is constructor implies ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) ) ) assume A1: ( o <> * & o <> non_op ) ; :: according to ABCMIZ_1:def_11 ::_thesis: ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) ) A2: the carrier' of S c= the carrier' of C by INSTALG1:10; o in the carrier' of S ; then reconsider c = o as OperSymbol of C by A2; A3: c is constructor by A1, ABCMIZ_1:def_11; ( the Arity of S = the Arity of C | the carrier' of S & the ResultSort of S = the ResultSort of C | the carrier' of S ) by INSTALG1:12; then ( the_result_sort_of c = the_result_sort_of o & the_arity_of c = the_arity_of o ) by FUNCT_1:49; hence ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) ) by A3, Def1; ::_thesis: verum end; end; theorem :: ABCMIZ_A:5 for S1, S2 being standardized ConstructorSignature st the carrier' of S1 = the carrier' of S2 holds ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #) proof let S1, S2 be standardized ConstructorSignature; ::_thesis: ( the carrier' of S1 = the carrier' of S2 implies ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #) ) assume A1: the carrier' of S1 = the carrier' of S2 ; ::_thesis: ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #) A2: ( the carrier of S1 = 3 & the carrier of S2 = 3 ) by ABCMIZ_1:def_9, YELLOW11:1; now__::_thesis:_for_o_being_OperSymbol_of_S1_holds_the_Arity_of_S1_._o_=_the_Arity_of_S2_._o let o be OperSymbol of S1; ::_thesis: the Arity of S1 . b1 = the Arity of S2 . b1 reconsider o2 = o as OperSymbol of S2 by A1; percases ( o = * or o = non_op or ( o is constructor & o2 is constructor ) ) by ABCMIZ_1:def_11; suppose ( o = * or o = non_op ) ; ::_thesis: the Arity of S1 . b1 = the Arity of S2 . b1 then ( ( the Arity of S1 . o = <*an_Adj*> & the Arity of S2 . o = <*an_Adj*> ) or ( the Arity of S1 . o = <*an_Adj,a_Type*> & the Arity of S2 . o = <*an_Adj,a_Type*> ) ) by ABCMIZ_1:def_9; hence the Arity of S1 . o = the Arity of S2 . o ; ::_thesis: verum end; suppose ( o is constructor & o2 is constructor ) ; ::_thesis: the Arity of S1 . b1 = the Arity of S2 . b1 then ( card ((o `2) `1) = len (the_arity_of o) & card ((o `2) `1) = len (the_arity_of o2) & the_arity_of o = (len (the_arity_of o)) |-> a_Term & the_arity_of o2 = (len (the_arity_of o2)) |-> a_Term ) by Def1, ABCMIZ_1:37; hence the Arity of S1 . o = the_arity_of o2 .= the Arity of S2 . o ; ::_thesis: verum end; end; end; then A3: the Arity of S1 = the Arity of S2 by A1, A2, FUNCT_2:63; now__::_thesis:_for_o_being_OperSymbol_of_S1_holds_the_ResultSort_of_S1_._o_=_the_ResultSort_of_S2_._o let o be OperSymbol of S1; ::_thesis: the ResultSort of S1 . b1 = the ResultSort of S2 . b1 reconsider o2 = o as OperSymbol of S2 by A1; percases ( o = * or o = non_op or ( o is constructor & o2 is constructor ) ) by ABCMIZ_1:def_11; suppose ( o = * or o = non_op ) ; ::_thesis: the ResultSort of S1 . b1 = the ResultSort of S2 . b1 then ( ( the ResultSort of S1 . o = a_Type & the ResultSort of S2 . o = a_Type ) or ( the ResultSort of S1 . o = an_Adj & the ResultSort of S2 . o = an_Adj ) ) by ABCMIZ_1:def_9; hence the ResultSort of S1 . o = the ResultSort of S2 . o ; ::_thesis: verum end; suppose ( o is constructor & o2 is constructor ) ; ::_thesis: the ResultSort of S1 . b1 = the ResultSort of S2 . b1 then ( the_result_sort_of o = o `1 & the_result_sort_of o2 = o `1 ) by Def1; hence the ResultSort of S1 . o = the_result_sort_of o2 .= the ResultSort of S2 . o ; ::_thesis: verum end; end; end; hence ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #) by A1, A2, A3, FUNCT_2:63; ::_thesis: verum end; theorem :: ABCMIZ_A:6 for C being ConstructorSignature holds ( C is standardized iff C is Subsignature of MaxConstrSign ) proof let C be ConstructorSignature; ::_thesis: ( C is standardized iff C is Subsignature of MaxConstrSign ) A1: the carrier' of MaxConstrSign = {*,non_op} \/ Constructors by ABCMIZ_1:def_24; A2: dom the Arity of MaxConstrSign = the carrier' of MaxConstrSign by FUNCT_2:def_1; A3: dom the ResultSort of MaxConstrSign = the carrier' of MaxConstrSign by FUNCT_2:def_1; thus ( C is standardized implies C is Subsignature of MaxConstrSign ) ::_thesis: ( C is Subsignature of MaxConstrSign implies C is standardized ) proof assume A4: for o being OperSymbol of C st o is constructor holds ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) ) ; :: according to ABCMIZ_A:def_1 ::_thesis: C is Subsignature of MaxConstrSign A5: ( the carrier of C = 3 & the carrier of MaxConstrSign = 3 ) by ABCMIZ_1:def_9, YELLOW11:1; A6: the Arity of C c= the Arity of MaxConstrSign proof let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in the Arity of C or [x,y] in the Arity of MaxConstrSign ) assume A7: [x,y] in the Arity of C ; ::_thesis: [x,y] in the Arity of MaxConstrSign then reconsider x = x as OperSymbol of C by ZFMISC_1:87; ( x = * or x = non_op or x is constructor ) by ABCMIZ_1:def_11; then ( x in {*,non_op} or x in Constructors ) by A4, TARSKI:def_2; then reconsider c = x as OperSymbol of MaxConstrSign by A1, XBOOLE_0:def_3; A8: y = the Arity of C . x by A7, FUNCT_1:1; percases ( x = * or x = non_op or x is constructor ) by ABCMIZ_1:def_11; suppose ( x = * or x = non_op ) ; ::_thesis: [x,y] in the Arity of MaxConstrSign then ( ( c = * & y = <*an_Adj,a_Type*> ) or ( c = non_op & y = <*an_Adj*> ) ) by A8, ABCMIZ_1:def_9; then y = the Arity of MaxConstrSign . c by ABCMIZ_1:def_9; hence [x,y] in the Arity of MaxConstrSign by A2, FUNCT_1:def_2; ::_thesis: verum end; supposeA9: x is constructor ; ::_thesis: [x,y] in the Arity of MaxConstrSign then A10: ( x <> * & x <> non_op ) by ABCMIZ_1:def_11; then A11: c is constructor by ABCMIZ_1:def_11; card ((x `2) `1) = len (the_arity_of x) by A4, A9 .= card y by A7, FUNCT_1:1 ; then A12: card y = card ( the Arity of MaxConstrSign . c) by A11, ABCMIZ_1:def_24; ( y in {a_Term} * & the Arity of MaxConstrSign . c in {a_Term} * ) by A8, A10, ABCMIZ_1:def_9; then y = the Arity of MaxConstrSign . c by A12, ABCMIZ_1:6; hence [x,y] in the Arity of MaxConstrSign by A2, FUNCT_1:def_2; ::_thesis: verum end; end; end; the ResultSort of C c= the ResultSort of MaxConstrSign proof let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in the ResultSort of C or [x,y] in the ResultSort of MaxConstrSign ) assume A13: [x,y] in the ResultSort of C ; ::_thesis: [x,y] in the ResultSort of MaxConstrSign then reconsider x = x as OperSymbol of C by ZFMISC_1:87; ( x is constructor or x = * or x = non_op ) by ABCMIZ_1:def_11; then ( x in {*,non_op} or x in Constructors ) by A4, TARSKI:def_2; then reconsider c = x as OperSymbol of MaxConstrSign by A1, XBOOLE_0:def_3; A14: y = the ResultSort of C . x by A13, FUNCT_1:1; percases ( x = * or x = non_op or ( x is constructor & c is constructor ) ) by ABCMIZ_1:def_11; suppose ( x = * or x = non_op ) ; ::_thesis: [x,y] in the ResultSort of MaxConstrSign then ( ( c = * & y = a_Type ) or ( c = non_op & y = an_Adj ) ) by A14, ABCMIZ_1:def_9; then y = the ResultSort of MaxConstrSign . c by ABCMIZ_1:def_9; hence [x,y] in the ResultSort of MaxConstrSign by A3, FUNCT_1:def_2; ::_thesis: verum end; supposeA15: ( x is constructor & c is constructor ) ; ::_thesis: [x,y] in the ResultSort of MaxConstrSign then x `1 = the_result_sort_of x by A4 .= y by A13, FUNCT_1:1 ; then y = the_result_sort_of c by A15, Def1 .= the ResultSort of MaxConstrSign . c ; hence [x,y] in the ResultSort of MaxConstrSign by A3, FUNCT_1:def_2; ::_thesis: verum end; end; end; hence C is Subsignature of MaxConstrSign by A5, A6, INSTALG1:13; ::_thesis: verum end; assume A16: C is Subsignature of MaxConstrSign ; ::_thesis: C is standardized let o be OperSymbol of C; :: according to ABCMIZ_A:def_1 ::_thesis: ( o is constructor implies ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) ) ) assume A17: ( o <> * & o <> non_op ) ; :: according to ABCMIZ_1:def_11 ::_thesis: ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) ) ( the carrier' of C c= the carrier' of MaxConstrSign & o in the carrier' of C ) by A16, INSTALG1:10; then reconsider c = o as OperSymbol of MaxConstrSign ; A18: c is constructor by A17, ABCMIZ_1:def_11; not c in {*,non_op} by A17, TARSKI:def_2; hence o in Constructors by A1, XBOOLE_0:def_3; ::_thesis: ( o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) ) thus o `1 = the ResultSort of MaxConstrSign . c by A18, ABCMIZ_1:def_24 .= ( the ResultSort of MaxConstrSign | the carrier' of C) . o by FUNCT_1:49 .= the ResultSort of C . o by A16, INSTALG1:12 .= the_result_sort_of o ; ::_thesis: card ((o `2) `1) = len (the_arity_of o) thus card ((o `2) `1) = card ( the Arity of MaxConstrSign . c) by A18, ABCMIZ_1:def_24 .= card (( the Arity of MaxConstrSign | the carrier' of C) . o) by FUNCT_1:49 .= card ( the Arity of C . o) by A16, INSTALG1:12 .= len (the_arity_of o) ; ::_thesis: verum end; registration let C be initialized ConstructorSignature; cluster non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching non compound for expression of C, a_Term C; existence not for b1 being quasi-term of C holds b1 is compound proof set x = the Element of Vars ; take the Element of Vars -term C ; ::_thesis: not the Element of Vars -term C is compound thus not the Element of Vars -term C is compound ; ::_thesis: verum end; end; registration cluster -> pair for Element of Vars ; coherence for b1 being Element of Vars holds b1 is pair proof let x be Element of Vars ; ::_thesis: x is pair ( Vars = { [(varcl A),j] where A is Subset of Vars, j is Element of NAT : A is finite } & x in Vars ) by ABCMIZ_1:18; then ex A being Subset of Vars ex j being Element of NAT st ( x = [(varcl A),j] & A is finite ) ; hence x is pair ; ::_thesis: verum end; end; theorem Th7: :: ABCMIZ_A:7 for x being Element of Vars st vars x is natural holds vars x = 0 proof let x be Element of Vars ; ::_thesis: ( vars x is natural implies vars x = 0 ) assume x `1 is natural ; ::_thesis: vars x = 0 then reconsider n = x `1 as Element of NAT by ORDINAL1:def_12; ( Vars = { [(varcl A),j] where A is Subset of Vars, j is Element of NAT : A is finite } & x in Vars ) by ABCMIZ_1:18; then consider A being Subset of Vars, j being Element of NAT such that A1: ( x = [(varcl A),j] & A is finite ) ; set i = the Element of n; assume A2: x `1 <> 0 ; ::_thesis: contradiction then A3: the Element of n in n ; reconsider i = the Element of n as Element of NAT by A2, ORDINAL1:10; ( n = varcl A & vars x c= Vars ) by A1, MCART_1:7; then i in Vars by A3; hence contradiction ; ::_thesis: verum end; theorem Th8: :: ABCMIZ_A:8 Vars misses Constructors proof assume Vars meets Constructors ; ::_thesis: contradiction then consider x being set such that A1: ( x in Vars & x in Constructors ) by XBOOLE_0:3; reconsider x = x as Element of Vars by A1; consider A being Subset of Vars, j being Element of NAT such that A2: ( x = [(varcl A),j] & A is finite ) by A1, ABCMIZ_1:18; ( x in Modes \/ Attrs or x in Funcs ) by A1, XBOOLE_0:def_3; then ( x in Modes or x in Attrs or x in Funcs ) by XBOOLE_0:def_3; then ( x `2 in [:QuasiLoci,NAT:] & x `2 = j ) by A2, MCART_1:7, MCART_1:10; then ex a, b being set st ( a in QuasiLoci & b in NAT & [a,b] = j ) by ZFMISC_1:def_2; hence contradiction ; ::_thesis: verum end; theorem :: ABCMIZ_A:9 for x being Element of Vars holds ( x <> * & x <> non_op ) ; theorem Th10: :: ABCMIZ_A:10 for C being standardized ConstructorSignature holds Vars misses the carrier' of C proof let C be standardized ConstructorSignature; ::_thesis: Vars misses the carrier' of C assume Vars meets the carrier' of C ; ::_thesis: contradiction then consider x being set such that A1: ( x in Vars & x in the carrier' of C ) by XBOOLE_0:3; reconsider x = x as Element of Vars by A1; reconsider c = x as OperSymbol of C by A1; ( x = * or x = non_op or c is constructor ) by ABCMIZ_1:def_11; then ( x = * or x = non_op or ( x in Constructors & Vars misses Constructors ) ) by Th8, Def1; hence contradiction by XBOOLE_0:3; ::_thesis: verum end; theorem Th11: :: ABCMIZ_A:11 for C being initialized standardized ConstructorSignature for e being expression of C holds ( ex x being Element of Vars st ( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st ( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ) proof let C be initialized standardized ConstructorSignature; ::_thesis: for e being expression of C holds ( ex x being Element of Vars st ( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st ( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ) let e be expression of C; ::_thesis: ( ex x being Element of Vars st ( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st ( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ) set X = MSVars C; set Y = (MSVars C) \/ ( the carrier of C --> {0}); reconsider q = e as Term of C,((MSVars C) \/ ( the carrier of C --> {0})) by MSAFREE3:8; percases ( ex s being SortSymbol of C ex v being Element of ((MSVars C) \/ ( the carrier of C --> {0})) . s st q . {} = [v,s] or q . {} in [: the carrier' of C,{ the carrier of C}:] ) by MSATERM:2; suppose ex s being SortSymbol of C ex v being Element of ((MSVars C) \/ ( the carrier of C --> {0})) . s st q . {} = [v,s] ; ::_thesis: ( ex x being Element of Vars st ( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st ( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ) then consider s being SortSymbol of C, v being Element of ((MSVars C) \/ ( the carrier of C --> {0})) . s such that A1: q . {} = [v,s] ; consider z being set such that A2: ( z in dom the Sorts of (Free (C,(MSVars C))) & e in the Sorts of (Free (C,(MSVars C))) . z ) by CARD_5:2; reconsider z = z as SortSymbol of C by A2; the carrier of C = {a_Type,an_Adj,a_Term} by ABCMIZ_1:def_9; then A3: ( z = a_Type or z = an_Adj or z = a_Term ) by ENUMSET1:def_1; A4: q = root-tree [v,s] by A1, MSATERM:5; then A5: the_sort_of q = s by MSATERM:14; A6: the Sorts of (Free (C,(MSVars C))) = C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0}))) by MSAFREE3:24; then the Sorts of (Free (C,(MSVars C))) c= the Sorts of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) by PBOOLE:def_18; then ( the Sorts of (Free (C,(MSVars C))) . z c= the Sorts of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) . z & FreeMSA ((MSVars C) \/ ( the carrier of C --> {0})) = MSAlgebra(# (FreeSort ((MSVars C) \/ ( the carrier of C --> {0}))),(FreeOper ((MSVars C) \/ ( the carrier of C --> {0}))) #) ) by PBOOLE:def_2; then ( q in the Sorts of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) . z & the Sorts of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) . z = FreeSort (((MSVars C) \/ ( the carrier of C --> {0})),z) ) by A2, MSAFREE:def_11; then A7: s = z by A5, MSATERM:def_5; then v in (MSVars C) . z by A4, A2, A6, MSAFREE3:18; then A8: ( v in Vars & z = a_Term ) by A3, ABCMIZ_1:def_25; then reconsider x = v as Element of Vars ; e = x -term C by A1, A7, A8, MSATERM:5; hence ( ex x being Element of Vars st ( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st ( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ) by A1, A7, A8; ::_thesis: verum end; suppose q . {} in [: the carrier' of C,{ the carrier of C}:] ; ::_thesis: ( ex x being Element of Vars st ( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st ( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ) then consider o, s being set such that A9: ( o in the carrier' of C & s in { the carrier of C} & q . {} = [o,s] ) by ZFMISC_1:def_2; reconsider o = o as OperSymbol of C by A9; ( o is constructor iff ( o <> * & o <> non_op ) ) by ABCMIZ_1:def_11; then ( s = the carrier of C & ( o in Constructors or o = * or o = non_op ) ) by A9, Def1, TARSKI:def_1; hence ( ex x being Element of Vars st ( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st ( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ) by A9; ::_thesis: verum end; end; end; registration let C be initialized standardized ConstructorSignature; let e be expression of C; clustere . {} -> pair ; coherence e . {} is pair proof ( ex x being Element of Vars st ( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st ( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ) by Th11; hence e . {} is pair ; ::_thesis: verum end; end; theorem Th12: :: ABCMIZ_A:12 for C being initialized ConstructorSignature for e being expression of C for o being OperSymbol of C st e . {} = [o, the carrier of C] holds e is expression of C, the_result_sort_of o proof let C be initialized ConstructorSignature; ::_thesis: for e being expression of C for o being OperSymbol of C st e . {} = [o, the carrier of C] holds e is expression of C, the_result_sort_of o let e be expression of C; ::_thesis: for o being OperSymbol of C st e . {} = [o, the carrier of C] holds e is expression of C, the_result_sort_of o let o be OperSymbol of C; ::_thesis: ( e . {} = [o, the carrier of C] implies e is expression of C, the_result_sort_of o ) assume A1: e . {} = [o, the carrier of C] ; ::_thesis: e is expression of C, the_result_sort_of o set X = MSVars C; set Y = (MSVars C) \/ ( the carrier of C --> {0}); reconsider t = e as Term of C,((MSVars C) \/ ( the carrier of C --> {0})) by MSAFREE3:8; variables_in t c= MSVars C by MSAFREE3:27; then e in { t1 where t1 is Term of C,((MSVars C) \/ ( the carrier of C --> {0})) : ( the_sort_of t1 = the_sort_of t & variables_in t1 c= MSVars C ) } ; then e in (C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0})))) . (the_sort_of t) by MSAFREE3:def_5; then A2: e in the Sorts of (Free (C,(MSVars C))) . (the_sort_of t) by MSAFREE3:24; the_sort_of t = the_result_sort_of o by A1, MSATERM:17; hence e is expression of C, the_result_sort_of o by A2, ABCMIZ_1:def_28; ::_thesis: verum end; theorem Th13: :: ABCMIZ_A:13 for C being initialized standardized ConstructorSignature for e being expression of C holds ( ( (e . {}) `1 = * implies e is expression of C, a_Type C ) & ( (e . {}) `1 = non_op implies e is expression of C, an_Adj C ) ) proof let C be initialized standardized ConstructorSignature; ::_thesis: for e being expression of C holds ( ( (e . {}) `1 = * implies e is expression of C, a_Type C ) & ( (e . {}) `1 = non_op implies e is expression of C, an_Adj C ) ) let e be expression of C; ::_thesis: ( ( (e . {}) `1 = * implies e is expression of C, a_Type C ) & ( (e . {}) `1 = non_op implies e is expression of C, an_Adj C ) ) percases ( ex x being Element of Vars st ( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st ( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ) by Th11; suppose ex x being Element of Vars st ( e = x -term C & e . {} = [x,a_Term] ) ; ::_thesis: ( ( (e . {}) `1 = * implies e is expression of C, a_Type C ) & ( (e . {}) `1 = non_op implies e is expression of C, an_Adj C ) ) then consider x being Element of Vars such that A1: ( e = x -term C & e . {} = [x,a_Term] ) ; thus ( ( (e . {}) `1 = * implies e is expression of C, a_Type C ) & ( (e . {}) `1 = non_op implies e is expression of C, an_Adj C ) ) by A1, MCART_1:7; ::_thesis: verum end; suppose ex o being OperSymbol of C st ( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ; ::_thesis: ( ( (e . {}) `1 = * implies e is expression of C, a_Type C ) & ( (e . {}) `1 = non_op implies e is expression of C, an_Adj C ) ) then consider o being OperSymbol of C such that A2: e . {} = [o, the carrier of C] ; set X = MSVars C; set Y = (MSVars C) \/ ( the carrier of C --> {0}); reconsider t = e as Term of C,((MSVars C) \/ ( the carrier of C --> {0})) by MSAFREE3:8; variables_in t c= MSVars C by MSAFREE3:27; then e in { t1 where t1 is Term of C,((MSVars C) \/ ( the carrier of C --> {0})) : ( the_sort_of t1 = the_sort_of t & variables_in t1 c= MSVars C ) } ; then e in (C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0})))) . (the_sort_of t) by MSAFREE3:def_5; then A3: e in the Sorts of (Free (C,(MSVars C))) . (the_sort_of t) by MSAFREE3:24; A4: ( the_result_sort_of (non_op C) = an_Adj C & the_result_sort_of (ast C) = a_Type C ) by ABCMIZ_1:38; A5: ( (e . {}) `1 = o & non_op C = non_op & ast C = * ) by A2, MCART_1:7; the_sort_of t = the_result_sort_of o by A2, MSATERM:17; hence ( ( (e . {}) `1 = * implies e is expression of C, a_Type C ) & ( (e . {}) `1 = non_op implies e is expression of C, an_Adj C ) ) by A3, A4, A5, ABCMIZ_1:def_28; ::_thesis: verum end; end; end; theorem Th14: :: ABCMIZ_A:14 for C being initialized standardized ConstructorSignature for e being expression of C holds ( ( (e . {}) `1 in Vars & (e . {}) `2 = a_Term & e is quasi-term of C ) or ( (e . {}) `2 = the carrier of C & ( ( (e . {}) `1 in Constructors & (e . {}) `1 in the carrier' of C ) or (e . {}) `1 = * or (e . {}) `1 = non_op ) ) ) proof let C be initialized standardized ConstructorSignature; ::_thesis: for e being expression of C holds ( ( (e . {}) `1 in Vars & (e . {}) `2 = a_Term & e is quasi-term of C ) or ( (e . {}) `2 = the carrier of C & ( ( (e . {}) `1 in Constructors & (e . {}) `1 in the carrier' of C ) or (e . {}) `1 = * or (e . {}) `1 = non_op ) ) ) let e be expression of C; ::_thesis: ( ( (e . {}) `1 in Vars & (e . {}) `2 = a_Term & e is quasi-term of C ) or ( (e . {}) `2 = the carrier of C & ( ( (e . {}) `1 in Constructors & (e . {}) `1 in the carrier' of C ) or (e . {}) `1 = * or (e . {}) `1 = non_op ) ) ) percases ( ex x being Element of Vars st ( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st ( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ) by Th11; suppose ex x being Element of Vars st ( e = x -term C & e . {} = [x,a_Term] ) ; ::_thesis: ( ( (e . {}) `1 in Vars & (e . {}) `2 = a_Term & e is quasi-term of C ) or ( (e . {}) `2 = the carrier of C & ( ( (e . {}) `1 in Constructors & (e . {}) `1 in the carrier' of C ) or (e . {}) `1 = * or (e . {}) `1 = non_op ) ) ) then consider x being Element of Vars such that A1: ( e = x -term C & e . {} = [x,a_Term] ) ; ( (e . {}) `1 = x & (e . {}) `2 = a_Term ) by A1, MCART_1:7; hence ( ( (e . {}) `1 in Vars & (e . {}) `2 = a_Term & e is quasi-term of C ) or ( (e . {}) `2 = the carrier of C & ( ( (e . {}) `1 in Constructors & (e . {}) `1 in the carrier' of C ) or (e . {}) `1 = * or (e . {}) `1 = non_op ) ) ) by A1; ::_thesis: verum end; suppose ex o being OperSymbol of C st ( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ; ::_thesis: ( ( (e . {}) `1 in Vars & (e . {}) `2 = a_Term & e is quasi-term of C ) or ( (e . {}) `2 = the carrier of C & ( ( (e . {}) `1 in Constructors & (e . {}) `1 in the carrier' of C ) or (e . {}) `1 = * or (e . {}) `1 = non_op ) ) ) then consider o being OperSymbol of C such that A2: ( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ; ( (e . {}) `1 = o & (e . {}) `2 = the carrier of C ) by A2, MCART_1:7; hence ( ( (e . {}) `1 in Vars & (e . {}) `2 = a_Term & e is quasi-term of C ) or ( (e . {}) `2 = the carrier of C & ( ( (e . {}) `1 in Constructors & (e . {}) `1 in the carrier' of C ) or (e . {}) `1 = * or (e . {}) `1 = non_op ) ) ) by A2; ::_thesis: verum end; end; end; theorem :: ABCMIZ_A:15 for C being initialized standardized ConstructorSignature for e being expression of C st (e . {}) `1 in Constructors holds e in the Sorts of (Free (C,(MSVars C))) . (((e . {}) `1) `1) proof let C be initialized standardized ConstructorSignature; ::_thesis: for e being expression of C st (e . {}) `1 in Constructors holds e in the Sorts of (Free (C,(MSVars C))) . (((e . {}) `1) `1) let e be expression of C; ::_thesis: ( (e . {}) `1 in Constructors implies e in the Sorts of (Free (C,(MSVars C))) . (((e . {}) `1) `1) ) assume A1: (e . {}) `1 in Constructors ; ::_thesis: e in the Sorts of (Free (C,(MSVars C))) . (((e . {}) `1) `1) percases ( ex x being Element of Vars st ( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st ( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ) by Th11; suppose ex x being Element of Vars st ( e = x -term C & e . {} = [x,a_Term] ) ; ::_thesis: e in the Sorts of (Free (C,(MSVars C))) . (((e . {}) `1) `1) then consider x being Element of Vars such that A2: ( e = x -term C & e . {} = [x,a_Term] ) ; (e . {}) `1 = x by A2, MCART_1:7; hence e in the Sorts of (Free (C,(MSVars C))) . (((e . {}) `1) `1) by A1, Th8, XBOOLE_0:3; ::_thesis: verum end; suppose ex o being OperSymbol of C st ( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ; ::_thesis: e in the Sorts of (Free (C,(MSVars C))) . (((e . {}) `1) `1) then consider o being OperSymbol of C such that A3: e . {} = [o, the carrier of C] ; A4: (e . {}) `1 = o by A3, MCART_1:7; ( * in {*,non_op} & non_op in {*,non_op} ) by TARSKI:def_2; then ( o <> * & o <> non_op ) by A1, A4, ABCMIZ_1:39, XBOOLE_0:3; then A5: o is constructor by ABCMIZ_1:def_11; set X = MSVars C; reconsider t = e as Term of C,((MSVars C) \/ ( the carrier of C --> {0})) by MSAFREE3:8; A6: the_sort_of t = the_result_sort_of o by A3, MSATERM:17 .= o `1 by A5, Def1 ; variables_in t c= MSVars C by MSAFREE3:27; then e in { t1 where t1 is Term of C,((MSVars C) \/ ( the carrier of C --> {0})) : ( the_sort_of t1 = the_sort_of t & variables_in t1 c= MSVars C ) } ; then e in (C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0})))) . (the_sort_of t) by MSAFREE3:def_5; hence e in the Sorts of (Free (C,(MSVars C))) . (((e . {}) `1) `1) by A4, A6, MSAFREE3:23; ::_thesis: verum end; end; end; theorem :: ABCMIZ_A:16 for C being initialized standardized ConstructorSignature for e being expression of C holds ( not (e . {}) `1 in Vars iff (e . {}) `1 is OperSymbol of C ) proof let C be initialized standardized ConstructorSignature; ::_thesis: for e being expression of C holds ( not (e . {}) `1 in Vars iff (e . {}) `1 is OperSymbol of C ) let e be expression of C; ::_thesis: ( not (e . {}) `1 in Vars iff (e . {}) `1 is OperSymbol of C ) A1: ( (e . {}) `1 in Vars or (e . {}) `1 in the carrier' of C or (e . {}) `1 = ast C or (e . {}) `1 = non_op C ) by Th14; Vars misses the carrier' of C by Th10; hence ( not (e . {}) `1 in Vars iff (e . {}) `1 is OperSymbol of C ) by A1, XBOOLE_0:3; ::_thesis: verum end; theorem Th17: :: ABCMIZ_A:17 for C being initialized standardized ConstructorSignature for e being expression of C st (e . {}) `1 in Vars holds ex x being Element of Vars st ( x = (e . {}) `1 & e = x -term C ) proof let C be initialized standardized ConstructorSignature; ::_thesis: for e being expression of C st (e . {}) `1 in Vars holds ex x being Element of Vars st ( x = (e . {}) `1 & e = x -term C ) let t be expression of C; ::_thesis: ( (t . {}) `1 in Vars implies ex x being Element of Vars st ( x = (t . {}) `1 & t = x -term C ) ) assume A1: (t . {}) `1 in Vars ; ::_thesis: ex x being Element of Vars st ( x = (t . {}) `1 & t = x -term C ) set X = MSVars C; set V = (MSVars C) \/ ( the carrier of C --> {0}); reconsider q = t as Term of C,((MSVars C) \/ ( the carrier of C --> {0})) by MSAFREE3:8; percases ( q . {} in [: the carrier' of C,{ the carrier of C}:] or ex s being SortSymbol of C ex v being Element of ((MSVars C) \/ ( the carrier of C --> {0})) . s st q . {} = [v,s] ) by MSATERM:2; suppose q . {} in [: the carrier' of C,{ the carrier of C}:] ; ::_thesis: ex x being Element of Vars st ( x = (t . {}) `1 & t = x -term C ) then ( (q . {}) `1 in the carrier' of C & the carrier' of C misses Vars ) by Th10, MCART_1:10; hence ex x being Element of Vars st ( x = (t . {}) `1 & t = x -term C ) by A1, XBOOLE_0:3; ::_thesis: verum end; suppose ex s being SortSymbol of C ex v being Element of ((MSVars C) \/ ( the carrier of C --> {0})) . s st q . {} = [v,s] ; ::_thesis: ex x being Element of Vars st ( x = (t . {}) `1 & t = x -term C ) then consider s being SortSymbol of C, v being Element of ((MSVars C) \/ ( the carrier of C --> {0})) . s such that A2: t . {} = [v,s] ; A3: q = root-tree [v,s] by A2, MSATERM:5; reconsider x = v as Element of Vars by A1, A2, MCART_1:7; take x ; ::_thesis: ( x = (t . {}) `1 & t = x -term C ) the carrier of C = {a_Type,an_Adj,a_Term} by ABCMIZ_1:def_9; then A4: ( s = a_Term or s = a_Type or s = an_Adj ) by ENUMSET1:def_1; ( the carrier of C --> {0}) . s = {0} by FUNCOP_1:7; then ((MSVars C) \/ ( the carrier of C --> {0})) . s = ((MSVars C) . s) \/ {0} by PBOOLE:def_4; then A5: ( s = a_Term or ((MSVars C) \/ ( the carrier of C --> {0})) . s = {} \/ {0} ) by A4, ABCMIZ_1:def_25; ( v in ((MSVars C) \/ ( the carrier of C --> {0})) . s & x <> 0 ) ; hence ( x = (t . {}) `1 & t = x -term C ) by A2, A3, A5, MCART_1:7; ::_thesis: verum end; end; end; theorem Th18: :: ABCMIZ_A:18 for C being initialized standardized ConstructorSignature for e being expression of C st (e . {}) `1 = * holds ex a being expression of C, an_Adj C ex q being expression of C, a_Type C st e = [*,3] -tree (a,q) proof let C be initialized standardized ConstructorSignature; ::_thesis: for e being expression of C st (e . {}) `1 = * holds ex a being expression of C, an_Adj C ex q being expression of C, a_Type C st e = [*,3] -tree (a,q) let e be expression of C; ::_thesis: ( (e . {}) `1 = * implies ex a being expression of C, an_Adj C ex q being expression of C, a_Type C st e = [*,3] -tree (a,q) ) assume A1: (e . {}) `1 = * ; ::_thesis: ex a being expression of C, an_Adj C ex q being expression of C, a_Type C st e = [*,3] -tree (a,q) for x being Element of Vars holds ( not e = x -term C or not e . {} = [x,a_Term] ) by A1, MCART_1:7; then consider o being OperSymbol of C such that A2: e . {} = [o, the carrier of C] and ( o in Constructors or o = * or o = non_op ) by Th11; set Y = (MSVars C) \/ ( the carrier of C --> {0}); reconsider t = e as Term of C,((MSVars C) \/ ( the carrier of C --> {0})) by MSAFREE3:8; consider aa being ArgumentSeq of Sym (o,((MSVars C) \/ ( the carrier of C --> {0}))) such that A3: t = [o, the carrier of C] -tree aa by A2, MSATERM:10; A4: * = [o, the carrier of C] `1 by A1, A3, TREES_4:def_4 .= o ; A5: the_arity_of (ast C) = <*(an_Adj C),(a_Type C)*> by ABCMIZ_1:38; A6: len aa = len (the_arity_of o) by MSATERM:22 .= 2 by A4, A5, FINSEQ_1:44 ; then dom aa = Seg 2 by FINSEQ_1:def_3; then A7: ( 1 in dom aa & 2 in dom aa ) ; then reconsider t1 = aa . 1, t2 = aa . 2 as Term of C,((MSVars C) \/ ( the carrier of C --> {0})) by MSATERM:22; A8: len (doms aa) = len aa by TREES_3:38; ( (doms aa) . 1 = dom t1 & (doms aa) . 2 = dom t2 ) by A7, FUNCT_6:22; then A9: ( 0 < 2 & 0 + 1 = 1 & 1 < 2 & 1 + 1 = 2 & {} in (doms aa) . 1 & {} in (doms aa) . 2 & <*0*> ^ (<*> NAT) = <*0*> & <*1*> ^ (<*> NAT) = <*1*> ) by FINSEQ_1:34, TREES_1:22; dom t = tree (doms aa) by A3, TREES_4:10; then reconsider 00 = <*0*>, 01 = <*1*> as Element of dom t by A6, A8, A9, TREES_3:def_15; ( 0 < 2 & 1 = 0 + 1 & 1 < 2 & 2 = 1 + 1 & aa is DTree-yielding ) ; then ( t1 = t | 00 & t2 = t | 01 ) by A3, A6, TREES_4:def_4; then A10: ( t1 is expression of C & t2 is expression of C & variables_in t1 c= variables_in t & variables_in t2 c= variables_in t ) by MSAFREE3:32, MSAFREE3:33; then A11: ( variables_in t1 c= MSVars C & variables_in t2 c= MSVars C ) by MSAFREE3:27; the_sort_of t1 = (the_arity_of o) . 1 by A7, MSATERM:23 .= an_Adj C by A4, A5, FINSEQ_1:44 ; then t1 in { s where s is Term of C,((MSVars C) \/ ( the carrier of C --> {0})) : ( the_sort_of s = an_Adj C & variables_in s c= MSVars C ) } by A11; then t1 in (C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0})))) . (an_Adj C) by MSAFREE3:def_5; then t1 in the Sorts of (Free (C,(MSVars C))) . (an_Adj C) by MSAFREE3:24; then reconsider a = t1 as expression of C, an_Adj C by A10, ABCMIZ_1:def_28; the_sort_of t2 = (the_arity_of o) . 2 by A7, MSATERM:23 .= a_Type C by A4, A5, FINSEQ_1:44 ; then t2 in { s where s is Term of C,((MSVars C) \/ ( the carrier of C --> {0})) : ( the_sort_of s = a_Type C & variables_in s c= MSVars C ) } by A11; then t2 in (C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0})))) . (a_Type C) by MSAFREE3:def_5; then t2 in the Sorts of (Free (C,(MSVars C))) . (a_Type C) by MSAFREE3:24; then reconsider q = t2 as expression of C, a_Type C by A10, ABCMIZ_1:def_28; take a ; ::_thesis: ex q being expression of C, a_Type C st e = [*,3] -tree (a,q) take q ; ::_thesis: e = [*,3] -tree (a,q) A12: the carrier of C = 3 by ABCMIZ_1:def_9, YELLOW11:1; aa = <*a,q*> by A6, FINSEQ_1:44; hence e = [*,3] -tree (a,q) by A3, A4, A12, TREES_4:def_6; ::_thesis: verum end; theorem Th19: :: ABCMIZ_A:19 for C being initialized standardized ConstructorSignature for e being expression of C st (e . {}) `1 = non_op holds ex a being expression of C, an_Adj C st e = [non_op,3] -tree a proof let C be initialized standardized ConstructorSignature; ::_thesis: for e being expression of C st (e . {}) `1 = non_op holds ex a being expression of C, an_Adj C st e = [non_op,3] -tree a let e be expression of C; ::_thesis: ( (e . {}) `1 = non_op implies ex a being expression of C, an_Adj C st e = [non_op,3] -tree a ) assume A1: (e . {}) `1 = non_op ; ::_thesis: ex a being expression of C, an_Adj C st e = [non_op,3] -tree a for x being Element of Vars holds ( not e = x -term C or not e . {} = [x,a_Term] ) by A1, MCART_1:7; then consider o being OperSymbol of C such that A2: e . {} = [o, the carrier of C] and ( o in Constructors or o = * or o = non_op ) by Th11; set Y = (MSVars C) \/ ( the carrier of C --> {0}); reconsider t = e as Term of C,((MSVars C) \/ ( the carrier of C --> {0})) by MSAFREE3:8; consider aa being ArgumentSeq of Sym (o,((MSVars C) \/ ( the carrier of C --> {0}))) such that A3: t = [o, the carrier of C] -tree aa by A2, MSATERM:10; A4: non_op = [o, the carrier of C] `1 by A1, A3, TREES_4:def_4 .= o ; A5: the_arity_of (non_op C) = <*(an_Adj C)*> by ABCMIZ_1:38; A6: len aa = len (the_arity_of o) by MSATERM:22 .= 1 by A4, A5, FINSEQ_1:40 ; then dom aa = Seg 1 by FINSEQ_1:def_3; then A7: 1 in dom aa ; then reconsider t1 = aa . 1 as Term of C,((MSVars C) \/ ( the carrier of C --> {0})) by MSATERM:22; A8: len (doms aa) = len aa by TREES_3:38; (doms aa) . 1 = dom t1 by A7, FUNCT_6:22; then A9: ( 0 < 1 & 0 + 1 = 1 & {} in (doms aa) . 1 & <*0*> ^ (<*> NAT) = <*0*> ) by FINSEQ_1:34, TREES_1:22; dom t = tree (doms aa) by A3, TREES_4:10; then reconsider 00 = <*0*> as Element of dom t by A6, A8, A9, TREES_3:def_15; t1 = t | 00 by A3, A6, A9, TREES_4:def_4; then A10: ( t1 is expression of C & variables_in t1 c= variables_in t ) by MSAFREE3:32, MSAFREE3:33; then A11: variables_in t1 c= MSVars C by MSAFREE3:27; the_sort_of t1 = (the_arity_of o) . 1 by A7, MSATERM:23 .= an_Adj C by A4, A5, FINSEQ_1:40 ; then t1 in { s where s is Term of C,((MSVars C) \/ ( the carrier of C --> {0})) : ( the_sort_of s = an_Adj C & variables_in s c= MSVars C ) } by A11; then t1 in (C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0})))) . (an_Adj C) by MSAFREE3:def_5; then t1 in the Sorts of (Free (C,(MSVars C))) . (an_Adj C) by MSAFREE3:24; then reconsider a = t1 as expression of C, an_Adj C by A10, ABCMIZ_1:def_28; take a ; ::_thesis: e = [non_op,3] -tree a A12: the carrier of C = 3 by ABCMIZ_1:def_9, YELLOW11:1; aa = <*a*> by A6, FINSEQ_1:40; hence e = [non_op,3] -tree a by A3, A4, A12, TREES_4:def_5; ::_thesis: verum end; theorem Th20: :: ABCMIZ_A:20 for C being initialized standardized ConstructorSignature for e being expression of C st (e . {}) `1 in Constructors holds ex o being OperSymbol of C st ( o = (e . {}) `1 & the_result_sort_of o = o `1 & e is expression of C, the_result_sort_of o ) proof let C be initialized standardized ConstructorSignature; ::_thesis: for e being expression of C st (e . {}) `1 in Constructors holds ex o being OperSymbol of C st ( o = (e . {}) `1 & the_result_sort_of o = o `1 & e is expression of C, the_result_sort_of o ) let e be expression of C; ::_thesis: ( (e . {}) `1 in Constructors implies ex o being OperSymbol of C st ( o = (e . {}) `1 & the_result_sort_of o = o `1 & e is expression of C, the_result_sort_of o ) ) assume A1: (e . {}) `1 in Constructors ; ::_thesis: ex o being OperSymbol of C st ( o = (e . {}) `1 & the_result_sort_of o = o `1 & e is expression of C, the_result_sort_of o ) percases ( ex x being Element of Vars st ( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st ( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ) by Th11; suppose ex x being Element of Vars st ( e = x -term C & e . {} = [x,a_Term] ) ; ::_thesis: ex o being OperSymbol of C st ( o = (e . {}) `1 & the_result_sort_of o = o `1 & e is expression of C, the_result_sort_of o ) then consider x being Element of Vars such that A2: ( e = x -term C & e . {} = [x,a_Term] ) ; ( (e . {}) `1 = x & x in Vars ) by A2, MCART_1:7; hence ex o being OperSymbol of C st ( o = (e . {}) `1 & the_result_sort_of o = o `1 & e is expression of C, the_result_sort_of o ) by A1, Th8, XBOOLE_0:3; ::_thesis: verum end; suppose ex o being OperSymbol of C st ( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ; ::_thesis: ex o being OperSymbol of C st ( o = (e . {}) `1 & the_result_sort_of o = o `1 & e is expression of C, the_result_sort_of o ) then consider o being OperSymbol of C such that A3: ( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ; take o ; ::_thesis: ( o = (e . {}) `1 & the_result_sort_of o = o `1 & e is expression of C, the_result_sort_of o ) A4: ( (e . {}) `1 = o & (e . {}) `2 = the carrier of C ) by A3, MCART_1:7; ( * in {*,non_op} & non_op in {*,non_op} ) by TARSKI:def_2; then ( o <> * & o <> non_op ) by A1, A4, ABCMIZ_1:39, XBOOLE_0:3; then o is constructor by ABCMIZ_1:def_11; hence ( o = (e . {}) `1 & the_result_sort_of o = o `1 ) by A3, Def1, MCART_1:7; ::_thesis: e is expression of C, the_result_sort_of o set X = MSVars C; set V = (MSVars C) \/ ( the carrier of C --> {0}); reconsider q = e as Term of C,((MSVars C) \/ ( the carrier of C --> {0})) by MSAFREE3:8; A5: variables_in q c= MSVars C by MSAFREE3:27; A6: the_sort_of q = the_result_sort_of o by A3, MSATERM:17; the Sorts of (Free (C,(MSVars C))) . (the_result_sort_of o) = (C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0})))) . (the_result_sort_of o) by MSAFREE3:24 .= { a where a is Term of C,((MSVars C) \/ ( the carrier of C --> {0})) : ( the_sort_of a = the_result_sort_of o & variables_in a c= MSVars C ) } by MSAFREE3:def_5 ; hence e in the Sorts of (Free (C,(MSVars C))) . (the_result_sort_of o) by A5, A6; :: according to ABCMIZ_1:def_28 ::_thesis: verum end; end; end; theorem Th21: :: ABCMIZ_A:21 for C being initialized standardized ConstructorSignature for t being quasi-term of C holds ( t is compound iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) ) proof let C be initialized standardized ConstructorSignature; ::_thesis: for t being quasi-term of C holds ( t is compound iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) ) set X = MSVars C; set V = (MSVars C) \/ ( the carrier of C --> {0}); let t be quasi-term of C; ::_thesis: ( t is compound iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) ) ( C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0}))) c= the Sorts of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) & the Sorts of (Free (C,(MSVars C))) = C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0}))) ) by MSAFREE3:24, PBOOLE:def_18; then A1: ( FreeMSA ((MSVars C) \/ ( the carrier of C --> {0})) = MSAlgebra(# (FreeSort ((MSVars C) \/ ( the carrier of C --> {0}))),(FreeOper ((MSVars C) \/ ( the carrier of C --> {0}))) #) & (C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0})))) . (a_Term C) c= the Sorts of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) . (a_Term C) & t in (C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0})))) . (a_Term C) ) by ABCMIZ_1:def_28, PBOOLE:def_2; then t in (FreeSort ((MSVars C) \/ ( the carrier of C --> {0}))) . (a_Term C) ; then A2: t in FreeSort (((MSVars C) \/ ( the carrier of C --> {0})),(a_Term C)) by MSAFREE:def_11; A3: ( (MSVars C) . a_Term = Vars & a_Term C = a_Term & a_Term = 2 ) by ABCMIZ_1:def_25; reconsider q = t as Term of C,((MSVars C) \/ ( the carrier of C --> {0})) by MSAFREE3:8; percases ( ex s being SortSymbol of C ex v being Element of ((MSVars C) \/ ( the carrier of C --> {0})) . s st q . {} = [v,s] or q . {} in [: the carrier' of C,{ the carrier of C}:] ) by MSATERM:2; suppose ex s being SortSymbol of C ex v being Element of ((MSVars C) \/ ( the carrier of C --> {0})) . s st q . {} = [v,s] ; ::_thesis: ( t is compound iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) ) then consider s being SortSymbol of C, v being Element of ((MSVars C) \/ ( the carrier of C --> {0})) . s such that A4: t . {} = [v,s] ; A5: ( q = root-tree [v,s] & the_sort_of q = a_Term C ) by A2, A4, MSATERM:5, MSATERM:def_5; then A6: ( a_Term C = s & (t . {}) `1 = v ) by A4, MCART_1:7, MSATERM:14; then reconsider x = v as Element of Vars by A3, A5, A1, MSAFREE3:18; ( q = x -term C & vars x <> 2 ) by A5, A6, Th7; hence ( t is compound iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) ) by A6; ::_thesis: verum end; suppose q . {} in [: the carrier' of C,{ the carrier of C}:] ; ::_thesis: ( t is compound iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) ) then consider o, k being set such that A7: ( o in the carrier' of C & k in { the carrier of C} & q . {} = [o,k] ) by ZFMISC_1:def_2; reconsider o = o as OperSymbol of C by A7; k = the carrier of C by A7, TARSKI:def_1; then A8: the_result_sort_of o = the_sort_of q by A7, MSATERM:17 .= a_Term C by A1, MSAFREE3:17 ; then ( o <> ast C & o <> non_op C ) by ABCMIZ_1:38; then A9: o is constructor by ABCMIZ_1:def_11; then A10: a_Term C = o `1 by A8, Def1 .= ((q . {}) `1) `1 by A7, MCART_1:7 ; A11: (q . {}) `1 = o by A7, MCART_1:7; now__::_thesis:_for_x_being_Element_of_Vars_holds_not_q_=_x_-term_C given x being Element of Vars such that A12: q = x -term C ; ::_thesis: contradiction q . {} = [x,a_Term] by A12, TREES_4:3; then k = a_Term by A7, XTUPLE_0:1; then 2 = the carrier of C by A7, TARSKI:def_1; hence contradiction by ABCMIZ_1:def_9, YELLOW11:1; ::_thesis: verum end; hence ( t is compound iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) ) by A9, A10, A11, Th3, Def1; ::_thesis: verum end; end; end; theorem Th22: :: ABCMIZ_A:22 for C being initialized standardized ConstructorSignature for t being expression of C holds ( t is non compound quasi-term of C iff (t . {}) `1 in Vars ) proof let C be initialized standardized ConstructorSignature; ::_thesis: for t being expression of C holds ( t is non compound quasi-term of C iff (t . {}) `1 in Vars ) let t be expression of C; ::_thesis: ( t is non compound quasi-term of C iff (t . {}) `1 in Vars ) hereby ::_thesis: ( (t . {}) `1 in Vars implies t is non compound quasi-term of C ) assume t is non compound quasi-term of C ; ::_thesis: (t . {}) `1 in Vars then consider x being Element of Vars such that A1: t = x -term C by Th3; ( t . {} = [x,a_Term] & x in Vars ) by A1, TREES_4:3; hence (t . {}) `1 in Vars by MCART_1:7; ::_thesis: verum end; assume (t . {}) `1 in Vars ; ::_thesis: t is non compound quasi-term of C then ex x being Element of Vars st ( x = (t . {}) `1 & t = x -term C ) by Th17; hence t is non compound quasi-term of C ; ::_thesis: verum end; theorem :: ABCMIZ_A:23 for C being initialized standardized ConstructorSignature for t being expression of C holds ( t is quasi-term of C iff ( ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) or (t . {}) `1 in Vars ) ) proof let C be initialized standardized ConstructorSignature; ::_thesis: for t being expression of C holds ( t is quasi-term of C iff ( ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) or (t . {}) `1 in Vars ) ) let t be expression of C; ::_thesis: ( t is quasi-term of C iff ( ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) or (t . {}) `1 in Vars ) ) hereby ::_thesis: ( ( ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) or (t . {}) `1 in Vars ) implies t is quasi-term of C ) assume t is quasi-term of C ; ::_thesis: ( ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) or (t . {}) `1 in Vars ) then reconsider tr = t as quasi-term of C ; ( tr is compound or not tr is compound ) ; hence ( ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) or (t . {}) `1 in Vars ) by Th21, Th22; ::_thesis: verum end; assume that A1: ( ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) or (t . {}) `1 in Vars ) and A2: t is not quasi-term of C ; ::_thesis: contradiction A3: ( (t . {}) `1 in Vars implies ex x being Element of Vars st ( x = (t . {}) `1 & t = x -term C ) ) by Th17; then ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) by A1, A2; then ex o being OperSymbol of C st ( o = (t . {}) `1 & the_result_sort_of o = o `1 & t is expression of C, the_result_sort_of o ) by Th20; hence contradiction by A2, A3, A1; ::_thesis: verum end; theorem Th24: :: ABCMIZ_A:24 for C being initialized standardized ConstructorSignature for a being expression of C holds ( a is positive quasi-adjective of C iff ( (a . {}) `1 in Constructors & ((a . {}) `1) `1 = an_Adj ) ) proof let C be initialized standardized ConstructorSignature; ::_thesis: for a being expression of C holds ( a is positive quasi-adjective of C iff ( (a . {}) `1 in Constructors & ((a . {}) `1) `1 = an_Adj ) ) set X = MSVars C; set V = (MSVars C) \/ ( the carrier of C --> {0}); let t be expression of C; ::_thesis: ( t is positive quasi-adjective of C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = an_Adj ) ) consider A being MSSubset of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) such that A1: ( Free (C,(MSVars C)) = GenMSAlg A & A = (Reverse ((MSVars C) \/ ( the carrier of C --> {0}))) "" (MSVars C) ) by MSAFREE3:def_1; the Sorts of (Free (C,(MSVars C))) is MSSubset of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) by A1, MSUALG_2:def_9; then the Sorts of (Free (C,(MSVars C))) c= the Sorts of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) by PBOOLE:def_18; then A2: the Sorts of (Free (C,(MSVars C))) . (an_Adj C) c= the Sorts of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) . (an_Adj C) by PBOOLE:def_2; percases ( ( (t . {}) `1 in Vars & (t . {}) `2 = a_Term & t is quasi-term of C ) or ( (t . {}) `2 = the carrier of C & (t . {}) `1 in Constructors & (t . {}) `1 in the carrier' of C ) or (t . {}) `1 = * or (t . {}) `1 = non_op ) by Th14; suppose ( (t . {}) `1 in Vars & (t . {}) `2 = a_Term & t is quasi-term of C ) ; ::_thesis: ( t is positive quasi-adjective of C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = an_Adj ) ) hence ( t is positive quasi-adjective of C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = an_Adj ) ) by Th8, ABCMIZ_1:77, XBOOLE_0:3; ::_thesis: verum end; supposethat A3: (t . {}) `2 = the carrier of C and A4: (t . {}) `1 in Constructors and A5: (t . {}) `1 in the carrier' of C ; ::_thesis: ( t is positive quasi-adjective of C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = an_Adj ) ) reconsider o = (t . {}) `1 as OperSymbol of C by A5; reconsider tt = t as Term of C,((MSVars C) \/ ( the carrier of C --> {0})) by MSAFREE3:8; not o in {*,non_op} by A4, ABCMIZ_1:39, XBOOLE_0:3; then ( o <> * & o <> non_op ) by TARSKI:def_2; then o is constructor by ABCMIZ_1:def_11; then A6: o `1 = the_result_sort_of o by Def1; A7: t . {} = [o,((t . {}) `2)] by Th1; then A8: the_sort_of tt = the_result_sort_of o by A3, MSATERM:17; hereby ::_thesis: ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = an_Adj implies t is positive quasi-adjective of C ) assume t is positive quasi-adjective of C ; ::_thesis: ( (t . {}) `1 in Constructors & not ((t . {}) `1) `1 <> an_Adj ) then A9: t in the Sorts of (Free (C,(MSVars C))) . (an_Adj C) by ABCMIZ_1:def_28; thus (t . {}) `1 in Constructors by A4; ::_thesis: not ((t . {}) `1) `1 <> an_Adj assume ((t . {}) `1) `1 <> an_Adj ; ::_thesis: contradiction hence contradiction by A2, A9, A6, A8, MSAFREE3:7; ::_thesis: verum end; assume (t . {}) `1 in Constructors ; ::_thesis: ( not ((t . {}) `1) `1 = an_Adj or t is positive quasi-adjective of C ) assume ((t . {}) `1) `1 = an_Adj ; ::_thesis: t is positive quasi-adjective of C then reconsider t = t as expression of C, an_Adj C by A3, A6, A7, Th12; t is positive proof given a being expression of C, an_Adj C such that A10: t = (non_op C) term a ; :: according to ABCMIZ_1:def_37 ::_thesis: contradiction t = [non_op, the carrier of C] -tree <*a*> by A10, ABCMIZ_1:43; then t . {} = [non_op, the carrier of C] by TREES_4:def_4; then (t . {}) `1 = non_op by MCART_1:7; then (t . {}) `1 in {*,non_op} by TARSKI:def_2; hence contradiction by A4, ABCMIZ_1:39, XBOOLE_0:3; ::_thesis: verum end; hence t is positive quasi-adjective of C ; ::_thesis: verum end; supposeA11: (t . {}) `1 = * ; ::_thesis: ( t is positive quasi-adjective of C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = an_Adj ) ) then (t . {}) `1 in {*,non_op} by TARSKI:def_2; then A12: not (t . {}) `1 in Constructors by ABCMIZ_1:39, XBOOLE_0:3; consider a being expression of C, an_Adj C, q being expression of C, a_Type C such that A13: t = [*,3] -tree (a,q) by A11, Th18; t = [*,3] -tree <*a,q*> by A13, TREES_4:def_6; then t . {} = [*,3] by TREES_4:def_4; then (t . {}) `1 = * by MCART_1:7; then ( t is expression of C, a_Type C & a_Type C = a_Type & a_Type = 0 & an_Adj C = an_Adj & an_Adj = 1 ) by Th13; hence ( t is positive quasi-adjective of C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = an_Adj ) ) by A12, ABCMIZ_1:48; ::_thesis: verum end; supposeA14: (t . {}) `1 = non_op ; ::_thesis: ( t is positive quasi-adjective of C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = an_Adj ) ) then (t . {}) `1 in {*,non_op} by TARSKI:def_2; then A15: not (t . {}) `1 in Constructors by ABCMIZ_1:39, XBOOLE_0:3; consider a being expression of C, an_Adj C such that A16: t = [non_op,3] -tree a by A14, Th19; t = [non_op,3] -tree <*a*> by A16, TREES_4:def_5 .= [non_op, the carrier of C] -tree <*a*> by ABCMIZ_1:def_9, YELLOW11:1 .= (non_op C) term a by ABCMIZ_1:43 ; hence ( t is positive quasi-adjective of C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = an_Adj ) ) by A15, ABCMIZ_1:def_37; ::_thesis: verum end; end; end; theorem :: ABCMIZ_A:25 for C being initialized standardized ConstructorSignature for a being quasi-adjective of C holds ( a is negative iff (a . {}) `1 = non_op ) proof let C be initialized standardized ConstructorSignature; ::_thesis: for a being quasi-adjective of C holds ( a is negative iff (a . {}) `1 = non_op ) let t be quasi-adjective of C; ::_thesis: ( t is negative iff (t . {}) `1 = non_op ) percases ( t is positive expression of C, an_Adj C or t is negative expression of C, an_Adj C ) ; supposeA1: t is positive expression of C, an_Adj C ; ::_thesis: ( t is negative iff (t . {}) `1 = non_op ) then ( (t . {}) `1 in Constructors & non_op in {*,non_op} ) by Th24, TARSKI:def_2; hence ( t is negative iff (t . {}) `1 = non_op ) by A1, ABCMIZ_1:39, XBOOLE_0:3; ::_thesis: verum end; supposeA2: t is negative expression of C, an_Adj C ; ::_thesis: ( t is negative iff (t . {}) `1 = non_op ) then consider a being expression of C, an_Adj C such that A3: ( a is positive & t = (non_op C) term a ) by ABCMIZ_1:def_38; t = [non_op, the carrier of C] -tree <*a*> by A3, ABCMIZ_1:43; then t . {} = [non_op, the carrier of C] by TREES_4:def_4; hence ( t is negative iff (t . {}) `1 = non_op ) by A2, MCART_1:7; ::_thesis: verum end; end; end; theorem :: ABCMIZ_A:26 for C being initialized standardized ConstructorSignature for t being expression of C holds ( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) ) proof let C be initialized standardized ConstructorSignature; ::_thesis: for t being expression of C holds ( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) ) set X = MSVars C; set V = (MSVars C) \/ ( the carrier of C --> {0}); let t be expression of C; ::_thesis: ( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) ) consider A being MSSubset of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) such that A1: ( Free (C,(MSVars C)) = GenMSAlg A & A = (Reverse ((MSVars C) \/ ( the carrier of C --> {0}))) "" (MSVars C) ) by MSAFREE3:def_1; the Sorts of (Free (C,(MSVars C))) is MSSubset of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) by A1, MSUALG_2:def_9; then the Sorts of (Free (C,(MSVars C))) c= the Sorts of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) by PBOOLE:def_18; then A2: the Sorts of (Free (C,(MSVars C))) . (a_Type C) c= the Sorts of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) . (a_Type C) by PBOOLE:def_2; percases ( ( (t . {}) `1 in Vars & (t . {}) `2 = a_Term & t is quasi-term of C ) or ( (t . {}) `2 = the carrier of C & (t . {}) `1 in Constructors & (t . {}) `1 in the carrier' of C ) or (t . {}) `1 = * or (t . {}) `1 = non_op ) by Th14; suppose ( (t . {}) `1 in Vars & (t . {}) `2 = a_Term & t is quasi-term of C ) ; ::_thesis: ( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) ) hence ( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) ) by Th8, ABCMIZ_1:48, XBOOLE_0:3; ::_thesis: verum end; supposethat A3: (t . {}) `2 = the carrier of C and A4: (t . {}) `1 in Constructors and A5: (t . {}) `1 in the carrier' of C ; ::_thesis: ( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) ) reconsider o = (t . {}) `1 as OperSymbol of C by A5; reconsider tt = t as Term of C,((MSVars C) \/ ( the carrier of C --> {0})) by MSAFREE3:8; not o in {*,non_op} by A4, ABCMIZ_1:39, XBOOLE_0:3; then ( o <> * & o <> non_op ) by TARSKI:def_2; then o is constructor by ABCMIZ_1:def_11; then A6: o `1 = the_result_sort_of o by Def1; A7: t . {} = [o,((t . {}) `2)] by Th1; then A8: the_sort_of tt = the_result_sort_of o by A3, MSATERM:17; hereby ::_thesis: ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type implies t is pure expression of C, a_Type C ) assume t is pure expression of C, a_Type C ; ::_thesis: ( (t . {}) `1 in Constructors & not ((t . {}) `1) `1 <> a_Type ) then A9: t in the Sorts of (Free (C,(MSVars C))) . (a_Type C) by ABCMIZ_1:def_28; thus (t . {}) `1 in Constructors by A4; ::_thesis: not ((t . {}) `1) `1 <> a_Type assume ((t . {}) `1) `1 <> a_Type ; ::_thesis: contradiction hence contradiction by A2, A9, A6, A8, MSAFREE3:7; ::_thesis: verum end; assume (t . {}) `1 in Constructors ; ::_thesis: ( not ((t . {}) `1) `1 = a_Type or t is pure expression of C, a_Type C ) assume ((t . {}) `1) `1 = a_Type ; ::_thesis: t is pure expression of C, a_Type C then reconsider t = t as expression of C, a_Type C by A3, A7, Th12, A6; t is pure proof given a being expression of C, an_Adj C, q being expression of C, a_Type C such that A10: t = (ast C) term (a,q) ; :: according to ABCMIZ_1:def_41 ::_thesis: contradiction t = [*, the carrier of C] -tree <*a,q*> by A10, ABCMIZ_1:46; then t . {} = [*, the carrier of C] by TREES_4:def_4; then (t . {}) `1 = * by MCART_1:7; then (t . {}) `1 in {*,non_op} by TARSKI:def_2; hence contradiction by A4, ABCMIZ_1:39, XBOOLE_0:3; ::_thesis: verum end; hence t is pure expression of C, a_Type C ; ::_thesis: verum end; supposeA11: (t . {}) `1 = * ; ::_thesis: ( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) ) then (t . {}) `1 in {*,non_op} by TARSKI:def_2; then A12: not (t . {}) `1 in Constructors by ABCMIZ_1:39, XBOOLE_0:3; consider a being expression of C, an_Adj C, q being expression of C, a_Type C such that A13: t = [*,3] -tree (a,q) by A11, Th18; t = [*,3] -tree <*a,q*> by A13, TREES_4:def_6 .= [*, the carrier of C] -tree <*a,q*> by ABCMIZ_1:def_9, YELLOW11:1 .= (ast C) term (a,q) by ABCMIZ_1:46 ; hence ( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) ) by A12, ABCMIZ_1:def_41; ::_thesis: verum end; supposeA14: (t . {}) `1 = non_op ; ::_thesis: ( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) ) then (t . {}) `1 in {*,non_op} by TARSKI:def_2; then A15: not (t . {}) `1 in Constructors by ABCMIZ_1:39, XBOOLE_0:3; consider a being expression of C, an_Adj C such that A16: t = [non_op,3] -tree a by A14, Th19; t = [non_op,3] -tree <*a*> by A16, TREES_4:def_5; then t . {} = [non_op,3] by TREES_4:def_4; then (t . {}) `1 = non_op by MCART_1:7; then t is expression of C, an_Adj C by Th13; hence ( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) ) by A15, ABCMIZ_1:48; ::_thesis: verum end; end; end; begin set MC = MaxConstrSign ; definition mode expression is expression of MaxConstrSign; mode valuation is valuation of MaxConstrSign; mode quasi-adjective is quasi-adjective of MaxConstrSign; func QuasiAdjs -> Subset of (Free (MaxConstrSign,(MSVars MaxConstrSign))) equals :: ABCMIZ_A:def 3 QuasiAdjs MaxConstrSign; coherence QuasiAdjs MaxConstrSign is Subset of (Free (MaxConstrSign,(MSVars MaxConstrSign))) ; mode quasi-term is quasi-term of MaxConstrSign; func QuasiTerms -> Subset of (Free (MaxConstrSign,(MSVars MaxConstrSign))) equals :: ABCMIZ_A:def 4 QuasiTerms MaxConstrSign; coherence QuasiTerms MaxConstrSign is Subset of (Free (MaxConstrSign,(MSVars MaxConstrSign))) ; mode quasi-type is quasi-type of MaxConstrSign ; func QuasiTypes -> set equals :: ABCMIZ_A:def 5 QuasiTypes MaxConstrSign; coherence QuasiTypes MaxConstrSign is set ; end; :: deftheorem defines QuasiAdjs ABCMIZ_A:def_3_:_ QuasiAdjs = QuasiAdjs MaxConstrSign; :: deftheorem defines QuasiTerms ABCMIZ_A:def_4_:_ QuasiTerms = QuasiTerms MaxConstrSign; :: deftheorem defines QuasiTypes ABCMIZ_A:def_5_:_ QuasiTypes = QuasiTypes MaxConstrSign; registration cluster QuasiAdjs -> non empty ; coherence not QuasiAdjs is empty ; cluster QuasiTerms -> non empty ; coherence not QuasiTerms is empty ; cluster QuasiTypes -> non empty ; coherence not QuasiTypes is empty ; end; definition :: original: Modes redefine func Modes -> non empty Subset of Constructors; coherence Modes is non empty Subset of Constructors proof ( Modes c= Modes \/ Attrs & Modes \/ Attrs c= Constructors ) by XBOOLE_1:7; hence Modes is non empty Subset of Constructors by XBOOLE_1:1; ::_thesis: verum end; :: original: Attrs redefine func Attrs -> non empty Subset of Constructors; coherence Attrs is non empty Subset of Constructors proof ( Attrs c= Modes \/ Attrs & Modes \/ Attrs c= Constructors ) by XBOOLE_1:7; hence Attrs is non empty Subset of Constructors by XBOOLE_1:1; ::_thesis: verum end; :: original: Funcs redefine func Funcs -> non empty Subset of Constructors; coherence Funcs is non empty Subset of Constructors by XBOOLE_1:7; end; definition func set-constr -> Element of Modes equals :: ABCMIZ_A:def 6 [a_Type,[{},0]]; coherence [a_Type,[{},0]] is Element of Modes proof ( a_Type in {a_Type} & [{},0] in [:QuasiLoci,NAT:] ) by ABCMIZ_1:29, TARSKI:def_1, ZFMISC_1:def_2; hence [a_Type,[{},0]] is Element of Modes by ZFMISC_1:def_2; ::_thesis: verum end; end; :: deftheorem defines set-constr ABCMIZ_A:def_6_:_ set-constr = [a_Type,[{},0]]; theorem :: ABCMIZ_A:27 ( kind_of set-constr = a_Type & loci_of set-constr = {} & index_of set-constr = 0 ) proof set-constr `2 = [{},0] by MCART_1:7; hence ( kind_of set-constr = a_Type & loci_of set-constr = {} & index_of set-constr = 0 ) by MCART_1:7; ::_thesis: verum end; theorem Th28: :: ABCMIZ_A:28 Constructors = [:{a_Type,an_Adj,a_Term},[:QuasiLoci,NAT:]:] proof thus Constructors = ([:{a_Type},[:QuasiLoci,NAT:]:] \/ [:{an_Adj},[:QuasiLoci,NAT:]:]) \/ Funcs .= [:({a_Type} \/ {an_Adj}),[:QuasiLoci,NAT:]:] \/ Funcs by ZFMISC_1:97 .= [:{a_Type,an_Adj},[:QuasiLoci,NAT:]:] \/ Funcs by ENUMSET1:1 .= [:({a_Type,an_Adj} \/ {a_Term}),[:QuasiLoci,NAT:]:] by ZFMISC_1:97 .= [:{a_Type,an_Adj,a_Term},[:QuasiLoci,NAT:]:] by ENUMSET1:3 ; ::_thesis: verum end; theorem Th29: :: ABCMIZ_A:29 for i being Nat for l being quasi-loci holds ( [(rng l),i] in Vars & l ^ <*[(rng l),i]*> is quasi-loci ) proof let i be Nat; ::_thesis: for l being quasi-loci holds ( [(rng l),i] in Vars & l ^ <*[(rng l),i]*> is quasi-loci ) let l be quasi-loci; ::_thesis: ( [(rng l),i] in Vars & l ^ <*[(rng l),i]*> is quasi-loci ) varcl (rng l) = rng l by ABCMIZ_1:33; hence [(rng l),i] in Vars by ABCMIZ_1:17; ::_thesis: l ^ <*[(rng l),i]*> is quasi-loci then reconsider x = [(rng l),i] as variable ; ( rng l in {(rng l),i} & {(rng l),i} in x ) by TARSKI:def_2; then ( vars x = rng l & x nin rng l ) by MCART_1:7, XREGULAR:7; hence l ^ <*[(rng l),i]*> is quasi-loci by ABCMIZ_1:31; ::_thesis: verum end; theorem Th30: :: ABCMIZ_A:30 for i being Nat ex l being quasi-loci st len l = i proof let i be Nat; ::_thesis: ex l being quasi-loci st len l = i defpred S1[ Nat] means ex l being quasi-loci st len l = $1; ( <*> Vars is quasi-loci & len (<*> Vars) = 0 ) by ABCMIZ_1:29; then A1: S1[ 0 ] ; A2: for j being Nat st S1[j] holds S1[j + 1] proof let j be Nat; ::_thesis: ( S1[j] implies S1[j + 1] ) given l being quasi-loci such that A3: len l = j ; ::_thesis: S1[j + 1] reconsider l1 = l ^ <*[(rng l),1]*> as quasi-loci by Th29; take l1 ; ::_thesis: len l1 = j + 1 thus len l1 = j + 1 by A3, FINSEQ_2:16; ::_thesis: verum end; for j being Nat holds S1[j] from NAT_1:sch_2(A1, A2); hence ex l being quasi-loci st len l = i ; ::_thesis: verum end; theorem Th31: :: ABCMIZ_A:31 for X being finite Subset of Vars ex l being quasi-loci st rng l = varcl X proof let X be finite Subset of Vars; ::_thesis: ex l being quasi-loci st rng l = varcl X reconsider Y = varcl X as finite Subset of Vars by ABCMIZ_1:24; defpred S1[ set , set ] means $1 in $2 `1 ; A1: for x, y being set st x in Y & y in Y & S1[x,y] holds not S1[y,x] proof let x, y be set ; ::_thesis: ( x in Y & y in Y & S1[x,y] implies not S1[y,x] ) assume A2: ( x in Y & y in Y & S1[x,y] & S1[y,x] ) ; ::_thesis: contradiction x in Vars by A2; then consider A being Subset of Vars, j being Element of NAT such that A3: ( x = [(varcl A),j] & A is finite ) by ABCMIZ_1:18; y in Vars by A2; then consider B being Subset of Vars, k being Element of NAT such that A4: ( y = [(varcl B),k] & B is finite ) by ABCMIZ_1:18; A5: ( y in varcl A & x in varcl B ) by A2, A3, A4, MCART_1:7; A6: ( varcl A in {(varcl A)} & varcl B in {(varcl B)} ) by TARSKI:def_1; ( {(varcl A)} in x & {(varcl B)} in y ) by A4, A3, TARSKI:def_2; hence contradiction by A5, A6, XREGULAR:10; ::_thesis: verum end; A7: for x, y, z being set st x in Y & y in Y & z in Y & S1[x,y] & S1[y,z] holds S1[x,z] proof let x, y, z be set ; ::_thesis: ( x in Y & y in Y & z in Y & S1[x,y] & S1[y,z] implies S1[x,z] ) assume A8: ( x in Y & y in Y & z in Y & S1[x,y] & S1[y,z] ) ; ::_thesis: S1[x,z] y in Vars by A8; then consider B being Subset of Vars, k being Element of NAT such that A9: ( y = [(varcl B),k] & B is finite ) by ABCMIZ_1:18; z in Vars by A8; then consider C being Subset of Vars, j being Element of NAT such that A10: ( z = [(varcl C),j] & C is finite ) by ABCMIZ_1:18; A11: ( z `1 = varcl C & y `1 = varcl B ) by A10, A9, MCART_1:7; then varcl B c= varcl C by A8, A9, ABCMIZ_1:def_1; hence S1[x,z] by A11, A8; ::_thesis: verum end; consider l being one-to-one FinSequence such that A12: rng l = Y and A13: for i, j being Nat st i in dom l & j in dom l & S1[l . i,l . j] holds i < j from ABCMIZ_A:sch_3(A1, A7); reconsider l = l as one-to-one FinSequence of Vars by A12, FINSEQ_1:def_4; now__::_thesis:_for_i_being_Nat for_x_being_variable_st_i_in_dom_l_&_x_=_l_._i_holds_ for_y_being_variable_st_y_in_vars_x_holds_ ex_a_being_Nat_st_ (_a_in_dom_l_&_a_<_i_&_y_=_l_._a_) let i be Nat; ::_thesis: for x being variable st i in dom l & x = l . i holds for y being variable st y in vars x holds ex a being Nat st ( a in dom l & a < i & y = l . a ) let x be variable; ::_thesis: ( i in dom l & x = l . i implies for y being variable st y in vars x holds ex a being Nat st ( a in dom l & a < i & y = l . a ) ) assume A14: ( i in dom l & x = l . i ) ; ::_thesis: for y being variable st y in vars x holds ex a being Nat st ( a in dom l & a < i & y = l . a ) let y be variable; ::_thesis: ( y in vars x implies ex a being Nat st ( a in dom l & a < i & y = l . a ) ) assume A15: y in vars x ; ::_thesis: ex a being Nat st ( a in dom l & a < i & y = l . a ) x in Vars ; then consider A being Subset of Vars, j being Element of NAT such that A16: ( x = [(varcl A),j] & A is finite ) by ABCMIZ_1:18; ( x in rng l & vars x = varcl A ) by A14, A16, FUNCT_1:def_3, MCART_1:7; then vars x c= Y by A12, A16, ABCMIZ_1:def_1; then consider a being set such that A17: ( a in dom l & y = l . a ) by A12, A15, FUNCT_1:def_3; reconsider a = a as Nat by A17; take a = a; ::_thesis: ( a in dom l & a < i & y = l . a ) thus ( a in dom l & a < i & y = l . a ) by A13, A14, A15, A17; ::_thesis: verum end; then reconsider l = l as quasi-loci by ABCMIZ_1:30; take l ; ::_thesis: rng l = varcl X thus rng l = varcl X by A12; ::_thesis: verum end; theorem Th32: :: ABCMIZ_A:32 for X, o being set for p being DTree-yielding FinSequence st ex C being initialized ConstructorSignature st X = Union the Sorts of (Free (C,(MSVars C))) & o -tree p in X holds p is FinSequence of X proof let X, o be set ; ::_thesis: for p being DTree-yielding FinSequence st ex C being initialized ConstructorSignature st X = Union the Sorts of (Free (C,(MSVars C))) & o -tree p in X holds p is FinSequence of X let p be DTree-yielding FinSequence; ::_thesis: ( ex C being initialized ConstructorSignature st X = Union the Sorts of (Free (C,(MSVars C))) & o -tree p in X implies p is FinSequence of X ) given C being initialized ConstructorSignature such that A1: X = Union the Sorts of (Free (C,(MSVars C))) ; ::_thesis: ( not o -tree p in X or p is FinSequence of X ) assume o -tree p in X ; ::_thesis: p is FinSequence of X then reconsider e = o -tree p as expression of C by A1; rng p c= X proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng p or z in X ) assume z in rng p ; ::_thesis: z in X then consider i being set such that A2: ( i in dom p & z = p . i ) by FUNCT_1:def_3; reconsider i = i as Nat by A2; reconsider ppi = p . i as DecoratedTree by A2, TREES_3:24; A3: ( 1 <= i & i <= len p ) by A2, FINSEQ_3:25; then A4: (i -' 1) + 1 = i by XREAL_1:235; then A5: i -' 1 < len p by A3, NAT_1:13; A6: len (doms p) = len p by TREES_3:38; A7: (doms p) . i = dom ppi by A2, FUNCT_6:22; A8: dom e = tree (doms p) by TREES_4:10; ( <*(i -' 1)*> ^ (<*> NAT) = <*(i -' 1)*> & <*> NAT in dom ppi ) by FINSEQ_1:34, TREES_1:22; then reconsider q = <*(i -' 1)*> as Element of dom e by A4, A5, A6, A7, A8, TREES_3:def_15; e | q = z by A2, A4, A5, TREES_4:def_4; then z is Element of (Free (C,(MSVars C))) by MSAFREE3:33; hence z in X by A1; ::_thesis: verum end; hence p is FinSequence of X by FINSEQ_1:def_4; ::_thesis: verum end; definition let C be initialized ConstructorSignature; let e be expression of C; mode subexpression of e -> expression of C means :: ABCMIZ_A:def 7 it in Subtrees e; existence ex b1 being expression of C st b1 in Subtrees e by TREES_9:11; func constrs e -> set equals :: ABCMIZ_A:def 8 (proj1 (rng e)) /\ { o where o is constructor OperSymbol of C : verum } ; coherence (proj1 (rng e)) /\ { o where o is constructor OperSymbol of C : verum } is set ; func main-constr e -> set equals :Def9: :: ABCMIZ_A:def 9 (e . {}) `1 if e is compound otherwise {} ; correctness coherence ( ( e is compound implies (e . {}) `1 is set ) & ( not e is compound implies {} is set ) ); consistency for b1 being set holds verum; ; func args e -> FinSequence of (Free (C,(MSVars C))) means :: ABCMIZ_A:def 10 e = (e . {}) -tree it; existence ex b1 being FinSequence of (Free (C,(MSVars C))) st e = (e . {}) -tree b1 proof consider v being set , p being DTree-yielding FinSequence such that A1: e = v -tree p by TREES_9:8; A2: v = e . {} by A1, TREES_4:def_4; p is FinSequence of (Free (C,(MSVars C))) by A1, Th32; hence ex b1 being FinSequence of (Free (C,(MSVars C))) st e = (e . {}) -tree b1 by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence of (Free (C,(MSVars C))) st e = (e . {}) -tree b1 & e = (e . {}) -tree b2 holds b1 = b2 by TREES_4:15; end; :: deftheorem defines subexpression ABCMIZ_A:def_7_:_ for C being initialized ConstructorSignature for e, b3 being expression of C holds ( b3 is subexpression of e iff b3 in Subtrees e ); :: deftheorem defines constrs ABCMIZ_A:def_8_:_ for C being initialized ConstructorSignature for e being expression of C holds constrs e = (proj1 (rng e)) /\ { o where o is constructor OperSymbol of C : verum } ; :: deftheorem Def9 defines main-constr ABCMIZ_A:def_9_:_ for C being initialized ConstructorSignature for e being expression of C holds ( ( e is compound implies main-constr e = (e . {}) `1 ) & ( not e is compound implies main-constr e = {} ) ); :: deftheorem defines args ABCMIZ_A:def_10_:_ for C being initialized ConstructorSignature for e being expression of C for b3 being FinSequence of (Free (C,(MSVars C))) holds ( b3 = args e iff e = (e . {}) -tree b3 ); theorem Th33: :: ABCMIZ_A:33 for C being initialized ConstructorSignature for e being expression of C holds e is subexpression of e proof let C be initialized ConstructorSignature; ::_thesis: for e being expression of C holds e is subexpression of e let e be expression of C; ::_thesis: e is subexpression of e thus e in Subtrees e by TREES_9:11; :: according to ABCMIZ_A:def_7 ::_thesis: verum end; theorem :: ABCMIZ_A:34 for x being variable for C being initialized ConstructorSignature holds main-constr (x -term C) = {} by Def9; theorem Th35: :: ABCMIZ_A:35 for C being initialized ConstructorSignature for c being constructor OperSymbol of C for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds main-constr (c -trm p) = c proof let C be initialized ConstructorSignature; ::_thesis: for c being constructor OperSymbol of C for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds main-constr (c -trm p) = c let c be constructor OperSymbol of C; ::_thesis: for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds main-constr (c -trm p) = c let p be FinSequence of QuasiTerms C; ::_thesis: ( len p = len (the_arity_of c) implies main-constr (c -trm p) = c ) assume len p = len (the_arity_of c) ; ::_thesis: main-constr (c -trm p) = c then c -trm p = [c, the carrier of C] -tree p by ABCMIZ_1:def_35; then (c -trm p) . {} = [c, the carrier of C] by TREES_4:def_4; hence main-constr (c -trm p) = [c, the carrier of C] `1 by Def9 .= c ; ::_thesis: verum end; definition let C be initialized ConstructorSignature; let e be expression of C; attre is constructor means :Def11: :: ABCMIZ_A:def 11 ( e is compound & main-constr e is constructor OperSymbol of C ); end; :: deftheorem Def11 defines constructor ABCMIZ_A:def_11_:_ for C being initialized ConstructorSignature for e being expression of C holds ( e is constructor iff ( e is compound & main-constr e is constructor OperSymbol of C ) ); registration let C be initialized ConstructorSignature; cluster constructor -> compound for Element of Union the Sorts of (Free (C,(MSVars C))); coherence for b1 being expression of C st b1 is constructor holds b1 is compound by Def11; end; registration let C be initialized ConstructorSignature; cluster non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching constructor for Element of Union the Sorts of (Free (C,(MSVars C))); existence ex b1 being expression of C st b1 is constructor proof consider m, a being OperSymbol of C such that A1: ( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} ) by ABCMIZ_1:def_12; ( the_arity_of (ast C) = <*(an_Adj C),(a_Type C)*> & the_arity_of (non_op C) = <*(an_Adj C)*> ) by ABCMIZ_1:38; then reconsider m = m as constructor OperSymbol of C by A1, ABCMIZ_1:def_11; set p = <*> (QuasiTerms C); take e = m -trm (<*> (QuasiTerms C)); ::_thesis: e is constructor thus e is compound ; :: according to ABCMIZ_A:def_11 ::_thesis: main-constr e is constructor OperSymbol of C len (<*> (QuasiTerms C)) = len (the_arity_of m) by A1; hence main-constr e is constructor OperSymbol of C by Th35; ::_thesis: verum end; end; registration let C be initialized ConstructorSignature; let e be constructor expression of C; cluster non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching constructor for subexpression of e; existence ex b1 being subexpression of e st b1 is constructor proof e is subexpression of e by Th33; hence ex b1 being subexpression of e st b1 is constructor ; ::_thesis: verum end; end; registration let S be non void Signature; let X be V6() ManySortedSet of S; let t be Element of (Free (S,X)); cluster proj2 t -> Relation-like ; coherence rng t is Relation-like proof set Z = the carrier of S --> {0}; set Y = X \/ ( the carrier of S --> {0}); t is Term of S,(X \/ ( the carrier of S --> {0})) by MSAFREE3:8; then rng t c= the carrier of (DTConMSA (X \/ ( the carrier of S --> {0}))) by RELAT_1:def_19; hence rng t is Relation-like ; ::_thesis: verum end; end; theorem :: ABCMIZ_A:36 for C being initialized ConstructorSignature for e being constructor expression of C holds main-constr e in constrs e proof let C be initialized ConstructorSignature; ::_thesis: for e being constructor expression of C holds main-constr e in constrs e let e be constructor expression of C; ::_thesis: main-constr e in constrs e A1: main-constr e = (e . {}) `1 by Def9; {} in dom e by TREES_1:22; then e . {} in rng e by FUNCT_1:def_3; then A2: main-constr e in proj1 (rng e) by A1, MCART_1:86; main-constr e is constructor OperSymbol of C by Def11; then main-constr e in { c where c is constructor OperSymbol of C : verum } ; hence main-constr e in constrs e by A2, XBOOLE_0:def_4; ::_thesis: verum end; begin definition let C be non void Signature; attrC is arity-rich means :Def12: :: ABCMIZ_A:def 12 for n being Nat for s being SortSymbol of C holds { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } is infinite ; let o be OperSymbol of C; attro is nullary means :Def13: :: ABCMIZ_A:def 13 the_arity_of o = {} ; attro is unary means :Def14: :: ABCMIZ_A:def 14 len (the_arity_of o) = 1; attro is binary means :Def15: :: ABCMIZ_A:def 15 len (the_arity_of o) = 2; end; :: deftheorem Def12 defines arity-rich ABCMIZ_A:def_12_:_ for C being non void Signature holds ( C is arity-rich iff for n being Nat for s being SortSymbol of C holds { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } is infinite ); :: deftheorem Def13 defines nullary ABCMIZ_A:def_13_:_ for C being non void Signature for o being OperSymbol of C holds ( o is nullary iff the_arity_of o = {} ); :: deftheorem Def14 defines unary ABCMIZ_A:def_14_:_ for C being non void Signature for o being OperSymbol of C holds ( o is unary iff len (the_arity_of o) = 1 ); :: deftheorem Def15 defines binary ABCMIZ_A:def_15_:_ for C being non void Signature for o being OperSymbol of C holds ( o is binary iff len (the_arity_of o) = 2 ); theorem Th37: :: ABCMIZ_A:37 for C being non void Signature for o being OperSymbol of C holds ( ( o is nullary implies not o is unary ) & ( o is nullary implies not o is binary ) & ( o is unary implies not o is binary ) ) proof let C be non void Signature; ::_thesis: for o being OperSymbol of C holds ( ( o is nullary implies not o is unary ) & ( o is nullary implies not o is binary ) & ( o is unary implies not o is binary ) ) let o be OperSymbol of C; ::_thesis: ( ( o is nullary implies not o is unary ) & ( o is nullary implies not o is binary ) & ( o is unary implies not o is binary ) ) thus ( o is nullary implies not o is unary ) ::_thesis: ( ( o is nullary implies not o is binary ) & ( o is unary implies not o is binary ) ) proof assume the_arity_of o = {} ; :: according to ABCMIZ_A:def_13 ::_thesis: not o is unary hence len (the_arity_of o) <> 1 ; :: according to ABCMIZ_A:def_14 ::_thesis: verum end; thus ( o is nullary implies not o is binary ) ::_thesis: ( o is unary implies not o is binary ) proof assume the_arity_of o = {} ; :: according to ABCMIZ_A:def_13 ::_thesis: not o is binary hence len (the_arity_of o) <> 2 ; :: according to ABCMIZ_A:def_15 ::_thesis: verum end; assume len (the_arity_of o) = 1 ; :: according to ABCMIZ_A:def_14 ::_thesis: not o is binary hence len (the_arity_of o) <> 2 ; :: according to ABCMIZ_A:def_15 ::_thesis: verum end; registration let C be ConstructorSignature; cluster non_op C -> unary ; coherence non_op C is unary proof the_arity_of (non_op C) = <*(an_Adj C)*> by ABCMIZ_1:38; hence len (the_arity_of (non_op C)) = 1 by FINSEQ_1:39; :: according to ABCMIZ_A:def_14 ::_thesis: verum end; cluster ast C -> binary ; coherence ast C is binary proof the_arity_of (ast C) = <*(an_Adj C),(a_Type C)*> by ABCMIZ_1:38; hence len (the_arity_of (ast C)) = 2 by FINSEQ_1:44; :: according to ABCMIZ_A:def_15 ::_thesis: verum end; end; registration let C be ConstructorSignature; cluster nullary -> constructor for Element of the carrier' of C; coherence for b1 being OperSymbol of C st b1 is nullary holds b1 is constructor proof let o be OperSymbol of C; ::_thesis: ( o is nullary implies o is constructor ) assume A1: the_arity_of o = {} ; :: according to ABCMIZ_A:def_13 ::_thesis: o is constructor ( the_arity_of (ast C) = <*(an_Adj C),(a_Type C)*> & the_arity_of (non_op C) = <*(an_Adj C)*> ) by ABCMIZ_1:38; hence ( o <> * & o <> non_op ) by A1; :: according to ABCMIZ_1:def_11 ::_thesis: verum end; end; theorem Th38: :: ABCMIZ_A:38 for C being ConstructorSignature holds ( C is initialized iff ex m being OperSymbol of a_Type C ex a being OperSymbol of an_Adj C st ( m is nullary & a is nullary ) ) proof let C be ConstructorSignature; ::_thesis: ( C is initialized iff ex m being OperSymbol of a_Type C ex a being OperSymbol of an_Adj C st ( m is nullary & a is nullary ) ) hereby ::_thesis: ( ex m being OperSymbol of a_Type C ex a being OperSymbol of an_Adj C st ( m is nullary & a is nullary ) implies C is initialized ) assume C is initialized ; ::_thesis: ex m being OperSymbol of a_Type C ex a being OperSymbol of an_Adj C st ( m is nullary & a is nullary ) then consider m, a being OperSymbol of C such that A1: ( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} ) by ABCMIZ_1:def_12; reconsider m = m as OperSymbol of a_Type C by A1, ABCMIZ_1:def_32; reconsider a = a as OperSymbol of an_Adj C by A1, ABCMIZ_1:def_32; take m = m; ::_thesis: ex a being OperSymbol of an_Adj C st ( m is nullary & a is nullary ) take a = a; ::_thesis: ( m is nullary & a is nullary ) thus m is nullary ::_thesis: a is nullary proof thus the_arity_of m = {} by A1; :: according to ABCMIZ_A:def_13 ::_thesis: verum end; thus a is nullary ::_thesis: verum proof thus the_arity_of a = {} by A1; :: according to ABCMIZ_A:def_13 ::_thesis: verum end; end; given m being OperSymbol of a_Type C, a being OperSymbol of an_Adj C such that A2: ( m is nullary & a is nullary ) ; ::_thesis: C is initialized take m ; :: according to ABCMIZ_1:def_12 ::_thesis: ex b1 being Element of the carrier' of C st ( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of b1 = an_Adj & the_arity_of b1 = {} ) take a ; ::_thesis: ( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} ) ( the_result_sort_of (non_op C) = an_Adj C & the_result_sort_of (ast C) = a_Type C ) by ABCMIZ_1:38; hence ( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} ) by A2, Def13, ABCMIZ_1:def_32; ::_thesis: verum end; registration let C be initialized ConstructorSignature; cluster constructor nullary for OperSymbol of a_Type C; existence ex b1 being OperSymbol of a_Type C st ( b1 is nullary & b1 is constructor ) proof consider m being OperSymbol of a_Type C, a being OperSymbol of an_Adj C such that A1: ( m is nullary & a is nullary ) by Th38; take m ; ::_thesis: ( m is nullary & m is constructor ) thus ( m is nullary & m is constructor ) by A1; ::_thesis: verum end; cluster constructor nullary for OperSymbol of an_Adj C; existence ex b1 being OperSymbol of an_Adj C st ( b1 is nullary & b1 is constructor ) proof consider m being OperSymbol of a_Type C, a being OperSymbol of an_Adj C such that A2: ( m is nullary & a is nullary ) by Th38; take a ; ::_thesis: ( a is nullary & a is constructor ) thus ( a is nullary & a is constructor ) by A2; ::_thesis: verum end; end; registration let C be initialized ConstructorSignature; cluster constructor nullary for Element of the carrier' of C; existence ex b1 being OperSymbol of C st ( b1 is nullary & b1 is constructor ) proof set o = the constructor nullary OperSymbol of a_Type C; take the constructor nullary OperSymbol of a_Type C ; ::_thesis: ( the constructor nullary OperSymbol of a_Type C is nullary & the constructor nullary OperSymbol of a_Type C is constructor ) thus ( the constructor nullary OperSymbol of a_Type C is nullary & the constructor nullary OperSymbol of a_Type C is constructor ) ; ::_thesis: verum end; end; registration cluster non void V146() arity-rich -> non void with_an_operation_for_each_sort for ManySortedSign ; coherence for b1 being non void Signature st b1 is arity-rich holds b1 is with_an_operation_for_each_sort proof let S be non void Signature; ::_thesis: ( S is arity-rich implies S is with_an_operation_for_each_sort ) assume A1: for n being Nat for s being SortSymbol of S holds { o where o is OperSymbol of S : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } is infinite ; :: according to ABCMIZ_A:def_12 ::_thesis: S is with_an_operation_for_each_sort let v be set ; :: according to TARSKI:def_3,ABCMIZ_1:def_54 ::_thesis: ( not v in the carrier of S or v in rng the ResultSort of S ) assume v in the carrier of S ; ::_thesis: v in rng the ResultSort of S then reconsider v = v as SortSymbol of S ; set A = { o where o is OperSymbol of S : ( the_result_sort_of o = v & len (the_arity_of o) = 0 ) } ; reconsider A = { o where o is OperSymbol of S : ( the_result_sort_of o = v & len (the_arity_of o) = 0 ) } as infinite set by A1; set a = the Element of A; the Element of A in A ; then consider o being OperSymbol of S such that A2: ( the Element of A = o & the_result_sort_of o = v & len (the_arity_of o) = 0 ) ; thus v in rng the ResultSort of S by A2, FUNCT_2:4; ::_thesis: verum end; clusterV146() constructor arity-rich -> initialized for ManySortedSign ; coherence for b1 being ConstructorSignature st b1 is arity-rich holds b1 is initialized proof let C be ConstructorSignature; ::_thesis: ( C is arity-rich implies C is initialized ) assume A3: C is arity-rich ; ::_thesis: C is initialized set Xt = { o where o is OperSymbol of C : ( the_result_sort_of o = a_Type C & len (the_arity_of o) = 0 ) } ; set x = the Element of { o where o is OperSymbol of C : ( the_result_sort_of o = a_Type C & len (the_arity_of o) = 0 ) } ; { o where o is OperSymbol of C : ( the_result_sort_of o = a_Type C & len (the_arity_of o) = 0 ) } is infinite set by A3, Def12; then the Element of { o where o is OperSymbol of C : ( the_result_sort_of o = a_Type C & len (the_arity_of o) = 0 ) } in { o where o is OperSymbol of C : ( the_result_sort_of o = a_Type C & len (the_arity_of o) = 0 ) } ; then consider m being OperSymbol of C such that A4: ( the Element of { o where o is OperSymbol of C : ( the_result_sort_of o = a_Type C & len (the_arity_of o) = 0 ) } = m & the_result_sort_of m = a_Type C & len (the_arity_of m) = 0 ) ; set Xa = { o where o is OperSymbol of C : ( the_result_sort_of o = an_Adj C & len (the_arity_of o) = 0 ) } ; set x = the Element of { o where o is OperSymbol of C : ( the_result_sort_of o = an_Adj C & len (the_arity_of o) = 0 ) } ; { o where o is OperSymbol of C : ( the_result_sort_of o = an_Adj C & len (the_arity_of o) = 0 ) } is infinite set by A3, Def12; then the Element of { o where o is OperSymbol of C : ( the_result_sort_of o = an_Adj C & len (the_arity_of o) = 0 ) } in { o where o is OperSymbol of C : ( the_result_sort_of o = an_Adj C & len (the_arity_of o) = 0 ) } ; then consider a being OperSymbol of C such that A5: ( the Element of { o where o is OperSymbol of C : ( the_result_sort_of o = an_Adj C & len (the_arity_of o) = 0 ) } = a & the_result_sort_of a = an_Adj C & len (the_arity_of a) = 0 ) ; take m ; :: according to ABCMIZ_1:def_12 ::_thesis: ex b1 being Element of the carrier' of C st ( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of b1 = an_Adj & the_arity_of b1 = {} ) take a ; ::_thesis: ( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} ) thus ( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} ) by A4, A5; ::_thesis: verum end; end; registration cluster MaxConstrSign -> arity-rich ; coherence MaxConstrSign is arity-rich proof set C = MaxConstrSign ; let n be Nat; :: according to ABCMIZ_A:def_12 ::_thesis: for s being SortSymbol of MaxConstrSign holds { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } is infinite let s be SortSymbol of MaxConstrSign; ::_thesis: { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } is infinite A1: the carrier of MaxConstrSign = {0,1,2} by ABCMIZ_1:def_9; set X = { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } ; consider l being quasi-loci such that A2: len l = n by Th30; deffunc H1( set ) -> set = [s,[l,c1]]; consider f being Function such that A3: ( dom f = NAT & ( for i being set st i in NAT holds f . i = H1(i) ) ) from FUNCT_1:sch_3(); f is one-to-one proof let i, j be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not i in proj1 f or not j in proj1 f or not f . i = f . j or i = j ) assume ( i in dom f & j in dom f ) ; ::_thesis: ( not f . i = f . j or i = j ) then reconsider i = i, j = j as Element of NAT by A3; ( f . i = H1(i) & f . j = H1(j) ) by A3; then ( f . i = f . j implies [l,i] = [l,j] ) by XTUPLE_0:1; hence ( not f . i = f . j or i = j ) by XTUPLE_0:1; ::_thesis: verum end; then A4: rng f is infinite by A3, CARD_1:59; rng f c= { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } ) assume y in rng f ; ::_thesis: y in { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } then consider x being set such that A5: ( x in dom f & y = f . x ) by FUNCT_1:def_3; reconsider x = x as Element of NAT by A3, A5; A6: ( [l,x] in [:QuasiLoci,NAT:] & y = H1(x) ) by A3, A5; then y in Constructors by A1, Th28, ZFMISC_1:def_2; then y in {*,non_op} \/ Constructors by XBOOLE_0:def_3; then reconsider y = y as OperSymbol of MaxConstrSign by ABCMIZ_1:def_24; A7: y is constructor by A6, ABCMIZ_1:def_11; then A8: the_result_sort_of y = y `1 by ABCMIZ_1:def_24 .= s by A6, MCART_1:7 ; len (the_arity_of y) = card ((y `2) `1) by A7, ABCMIZ_1:def_24 .= card ([l,x] `1) by A6, MCART_1:7 .= len l ; hence y in { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } by A2, A8; ::_thesis: verum end; hence { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } is infinite by A4; ::_thesis: verum end; end; registration cluster non empty non void V68() V146() constructor initialized arity-rich for ManySortedSign ; existence ex b1 being ConstructorSignature st ( b1 is arity-rich & b1 is initialized ) proof take MaxConstrSign ; ::_thesis: ( MaxConstrSign is arity-rich & MaxConstrSign is initialized ) thus ( MaxConstrSign is arity-rich & MaxConstrSign is initialized ) ; ::_thesis: verum end; end; registration let C be arity-rich ConstructorSignature; let s be SortSymbol of C; cluster constructor nullary for OperSymbol of s; existence ex b1 being OperSymbol of s st ( b1 is nullary & b1 is constructor ) proof set X = { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 0 ) } ; { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 0 ) } is infinite by Def12; then consider m1, m2 being set such that A1: ( m1 in { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 0 ) } & m2 in { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 0 ) } & m1 <> m2 ) by ZFMISC_1:def_10; consider o1 being OperSymbol of C such that A2: ( m1 = o1 & the_result_sort_of o1 = s & len (the_arity_of o1) = 0 ) by A1; reconsider m1 = m1 as OperSymbol of s by A2, ABCMIZ_1:def_32; the_arity_of m1 = {} by A2; then m1 is nullary by Def13; hence ex b1 being OperSymbol of s st ( b1 is nullary & b1 is constructor ) ; ::_thesis: verum end; cluster constructor unary for OperSymbol of s; existence ex b1 being OperSymbol of s st ( b1 is unary & b1 is constructor ) proof set X = { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 1 ) } ; { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 1 ) } is infinite by Def12; then consider m1, m2 being set such that A3: ( m1 in { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 1 ) } & m2 in { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 1 ) } & m1 <> m2 ) by ZFMISC_1:def_10; consider o1 being OperSymbol of C such that A4: ( m1 = o1 & the_result_sort_of o1 = s & len (the_arity_of o1) = 1 ) by A3; consider o2 being OperSymbol of C such that A5: ( m2 = o2 & the_result_sort_of o2 = s & len (the_arity_of o2) = 1 ) by A3; reconsider m1 = m1, m2 = m2 as OperSymbol of s by A4, A5, ABCMIZ_1:def_32; A6: ( m1 is unary & m2 is unary ) by A4, A5, Def14; then A7: ( m1 <> ast C & m2 <> ast C ) by Th37; ( m1 <> non_op or m2 <> non_op ) by A3; then ( m1 is constructor or m2 is constructor ) by A7, ABCMIZ_1:def_11; hence ex b1 being OperSymbol of s st ( b1 is unary & b1 is constructor ) by A6; ::_thesis: verum end; cluster constructor binary for OperSymbol of s; existence ex b1 being OperSymbol of s st ( b1 is binary & b1 is constructor ) proof set X = { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 2 ) } ; { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 2 ) } is infinite by Def12; then consider m1, m2 being set such that A8: ( m1 in { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 2 ) } & m2 in { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 2 ) } & m1 <> m2 ) by ZFMISC_1:def_10; consider o1 being OperSymbol of C such that A9: ( m1 = o1 & the_result_sort_of o1 = s & len (the_arity_of o1) = 2 ) by A8; consider o2 being OperSymbol of C such that A10: ( m2 = o2 & the_result_sort_of o2 = s & len (the_arity_of o2) = 2 ) by A8; reconsider m1 = m1, m2 = m2 as OperSymbol of s by A9, A10, ABCMIZ_1:def_32; A11: ( m1 is binary & m2 is binary ) by A9, A10, Def15; then A12: ( m1 <> non_op C & m2 <> non_op C ) by Th37; ( m1 <> * or m2 <> * ) by A8; then ( m1 is constructor or m2 is constructor ) by A12, ABCMIZ_1:def_11; hence ex b1 being OperSymbol of s st ( b1 is binary & b1 is constructor ) by A11; ::_thesis: verum end; end; registration let C be arity-rich ConstructorSignature; cluster constructor unary for Element of the carrier' of C; existence ex b1 being OperSymbol of C st ( b1 is unary & b1 is constructor ) proof set o = the constructor unary OperSymbol of a_Type C; take the constructor unary OperSymbol of a_Type C ; ::_thesis: ( the constructor unary OperSymbol of a_Type C is unary & the constructor unary OperSymbol of a_Type C is constructor ) thus ( the constructor unary OperSymbol of a_Type C is unary & the constructor unary OperSymbol of a_Type C is constructor ) ; ::_thesis: verum end; cluster constructor binary for Element of the carrier' of C; existence ex b1 being OperSymbol of C st ( b1 is binary & b1 is constructor ) proof set o = the constructor binary OperSymbol of a_Type C; take the constructor binary OperSymbol of a_Type C ; ::_thesis: ( the constructor binary OperSymbol of a_Type C is binary & the constructor binary OperSymbol of a_Type C is constructor ) thus ( the constructor binary OperSymbol of a_Type C is binary & the constructor binary OperSymbol of a_Type C is constructor ) ; ::_thesis: verum end; end; theorem Th39: :: ABCMIZ_A:39 for C being initialized ConstructorSignature for o being nullary OperSymbol of C holds [o, the carrier of C] -tree {} is expression of C, the_result_sort_of o proof let C be initialized ConstructorSignature; ::_thesis: for o being nullary OperSymbol of C holds [o, the carrier of C] -tree {} is expression of C, the_result_sort_of o let o be nullary OperSymbol of C; ::_thesis: [o, the carrier of C] -tree {} is expression of C, the_result_sort_of o set X = MSVars C; set Z = the carrier of C --> {0}; set Y = (MSVars C) \/ ( the carrier of C --> {0}); A1: the_arity_of o = {} by Def13; A2: the Sorts of (Free (C,(MSVars C))) = C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0}))) by MSAFREE3:24; for i being Nat st i in dom {} holds ex t being Term of C,((MSVars C) \/ ( the carrier of C --> {0})) st ( t = {} . i & the_sort_of t = (the_arity_of o) . i ) ; then reconsider p = {} as ArgumentSeq of Sym (o,((MSVars C) \/ ( the carrier of C --> {0}))) by A1, MSATERM:24; A3: variables_in ((Sym (o,((MSVars C) \/ ( the carrier of C --> {0})))) -tree p) c= MSVars C proof let s be set ; :: according to PBOOLE:def_2 ::_thesis: ( not s in the carrier of C or (variables_in ((Sym (o,((MSVars C) \/ ( the carrier of C --> {0})))) -tree p)) . s c= (MSVars C) . s ) assume s in the carrier of C ; ::_thesis: (variables_in ((Sym (o,((MSVars C) \/ ( the carrier of C --> {0})))) -tree p)) . s c= (MSVars C) . s then reconsider s9 = s as SortSymbol of C ; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (variables_in ((Sym (o,((MSVars C) \/ ( the carrier of C --> {0})))) -tree p)) . s or x in (MSVars C) . s ) assume x in (variables_in ((Sym (o,((MSVars C) \/ ( the carrier of C --> {0})))) -tree p)) . s ; ::_thesis: x in (MSVars C) . s then ex t being DecoratedTree st ( t in rng p & x in (C variables_in t) . s9 ) by MSAFREE3:11; hence x in (MSVars C) . s ; ::_thesis: verum end; set s9 = the_result_sort_of o; A4: the_sort_of ((Sym (o,((MSVars C) \/ ( the carrier of C --> {0})))) -tree p) = the_result_sort_of o by MSATERM:20; the Sorts of (Free (C,(MSVars C))) . (the_result_sort_of o) = { t where t is Term of C,((MSVars C) \/ ( the carrier of C --> {0})) : ( the_sort_of t = the_result_sort_of o & variables_in t c= MSVars C ) } by A2, MSAFREE3:def_5; then [o, the carrier of C] -tree {} in the Sorts of (Free (C,(MSVars C))) . (the_result_sort_of o) by A3, A4; hence [o, the carrier of C] -tree {} is expression of C, the_result_sort_of o by ABCMIZ_1:41; ::_thesis: verum end; definition let C be initialized ConstructorSignature; let m be constructor nullary OperSymbol of a_Type C; :: original: term redefine funcm term -> pure expression of C, a_Type C; coherence m term is pure expression of C, a_Type C proof set T = m term ; the_arity_of m = 0 by Def13; then len (the_arity_of m) = 0 ; then A1: m term = [m, the carrier of C] -tree {} by ABCMIZ_1:def_29; ex m, a being OperSymbol of C st ( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} ) by ABCMIZ_1:def_12; then the_result_sort_of m = a_Type C by ABCMIZ_1:def_32; then reconsider T = m term as expression of C, a_Type C by A1, Th39; T is pure proof given a being expression of C, an_Adj C, t being expression of C, a_Type C such that A2: T = (ast C) term (a,t) ; :: according to ABCMIZ_1:def_41 ::_thesis: contradiction T = [*, the carrier of C] -tree <*a,t*> by A2, ABCMIZ_1:46; hence contradiction by A1, TREES_4:15; ::_thesis: verum end; hence m term is pure expression of C, a_Type C ; ::_thesis: verum end; end; definition let c be Element of Constructors ; func @ c -> constructor OperSymbol of MaxConstrSign equals :: ABCMIZ_A:def 16 c; coherence c is constructor OperSymbol of MaxConstrSign proof ( * in {*,non_op} & non_op in {*,non_op} & the carrier' of MaxConstrSign = {*,non_op} \/ Constructors ) by ABCMIZ_1:def_24, TARSKI:def_2; then ( c <> * & c <> non_op & c in the carrier' of MaxConstrSign ) by ABCMIZ_1:39, XBOOLE_0:3, XBOOLE_0:def_3; hence c is constructor OperSymbol of MaxConstrSign by ABCMIZ_1:def_11; ::_thesis: verum end; end; :: deftheorem defines @ ABCMIZ_A:def_16_:_ for c being Element of Constructors holds @ c = c; definition let m be Element of Modes ; :: original: @ redefine func @ m -> constructor OperSymbol of a_Type MaxConstrSign; coherence @ m is constructor OperSymbol of a_Type MaxConstrSign proof A1: m `1 in {a_Type} by MCART_1:10; the_result_sort_of (@ m) = m `1 by ABCMIZ_1:def_24 .= a_Type by A1, TARSKI:def_1 ; hence @ m is constructor OperSymbol of a_Type MaxConstrSign by ABCMIZ_1:def_32; ::_thesis: verum end; end; registration cluster @ set-constr -> constructor nullary ; coherence @ set-constr is nullary proof len (the_arity_of (@ set-constr)) = card ((set-constr `2) `1) by ABCMIZ_1:def_24 .= card ([{},0] `1) by MCART_1:7 .= card 0 ; hence the_arity_of (@ set-constr) = {} ; :: according to ABCMIZ_A:def_13 ::_thesis: verum end; end; theorem :: ABCMIZ_A:40 the_arity_of (@ set-constr) = {} by Def13; definition func set-type -> quasi-type equals :: ABCMIZ_A:def 17 ({} (QuasiAdjs MaxConstrSign)) ast ((@ set-constr) term); coherence ({} (QuasiAdjs MaxConstrSign)) ast ((@ set-constr) term) is quasi-type ; end; :: deftheorem defines set-type ABCMIZ_A:def_17_:_ set-type = ({} (QuasiAdjs MaxConstrSign)) ast ((@ set-constr) term); theorem :: ABCMIZ_A:41 ( adjs set-type = {} & the_base_of set-type = (@ set-constr) term ) by MCART_1:7; definition let l be FinSequence of Vars ; func args l -> FinSequence of QuasiTerms MaxConstrSign means :Def18: :: ABCMIZ_A:def 18 ( len it = len l & ( for i being Nat st i in dom l holds it . i = (l /. i) -term MaxConstrSign ) ); existence ex b1 being FinSequence of QuasiTerms MaxConstrSign st ( len b1 = len l & ( for i being Nat st i in dom l holds b1 . i = (l /. i) -term MaxConstrSign ) ) proof deffunc H1( Nat) -> expression of MaxConstrSign , a_Term MaxConstrSign = (l /. $1) -term MaxConstrSign; consider g being FinSequence such that A1: len g = len l and A2: for i being Nat st i in dom g holds g . i = H1(i) from FINSEQ_1:sch_2(); A3: dom g = dom l by A1, FINSEQ_3:29; rng g c= QuasiTerms MaxConstrSign proof let j be set ; :: according to TARSKI:def_3 ::_thesis: ( not j in rng g or j in QuasiTerms MaxConstrSign ) assume j in rng g ; ::_thesis: j in QuasiTerms MaxConstrSign then consider z being set such that A4: ( z in dom g & j = g . z ) by FUNCT_1:def_3; reconsider z = z as Nat by A4; j = H1(z) by A2, A4; hence j in QuasiTerms MaxConstrSign by ABCMIZ_1:49; ::_thesis: verum end; then reconsider g = g as FinSequence of QuasiTerms MaxConstrSign by FINSEQ_1:def_4; take g ; ::_thesis: ( len g = len l & ( for i being Nat st i in dom l holds g . i = (l /. i) -term MaxConstrSign ) ) thus ( len g = len l & ( for i being Nat st i in dom l holds g . i = (l /. i) -term MaxConstrSign ) ) by A1, A2, A3; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence of QuasiTerms MaxConstrSign st len b1 = len l & ( for i being Nat st i in dom l holds b1 . i = (l /. i) -term MaxConstrSign ) & len b2 = len l & ( for i being Nat st i in dom l holds b2 . i = (l /. i) -term MaxConstrSign ) holds b1 = b2 proof let a1, a2 be FinSequence of QuasiTerms MaxConstrSign; ::_thesis: ( len a1 = len l & ( for i being Nat st i in dom l holds a1 . i = (l /. i) -term MaxConstrSign ) & len a2 = len l & ( for i being Nat st i in dom l holds a2 . i = (l /. i) -term MaxConstrSign ) implies a1 = a2 ) assume that A5: len a1 = len l and A6: for i being Nat st i in dom l holds a1 . i = (l /. i) -term MaxConstrSign and A7: len a2 = len l and A8: for i being Nat st i in dom l holds a2 . i = (l /. i) -term MaxConstrSign ; ::_thesis: a1 = a2 A9: ( dom a1 = dom l & dom a2 = dom l ) by A5, A7, FINSEQ_3:29; now__::_thesis:_for_i_being_Nat_st_i_in_dom_a1_holds_ a1_._i_=_a2_._i let i be Nat; ::_thesis: ( i in dom a1 implies a1 . i = a2 . i ) assume i in dom a1 ; ::_thesis: a1 . i = a2 . i then ( a1 . i = (l /. i) -term MaxConstrSign & a2 . i = (l /. i) -term MaxConstrSign ) by A6, A8, A9; hence a1 . i = a2 . i ; ::_thesis: verum end; hence a1 = a2 by A9, FINSEQ_1:13; ::_thesis: verum end; end; :: deftheorem Def18 defines args ABCMIZ_A:def_18_:_ for l being FinSequence of Vars for b2 being FinSequence of QuasiTerms MaxConstrSign holds ( b2 = args l iff ( len b2 = len l & ( for i being Nat st i in dom l holds b2 . i = (l /. i) -term MaxConstrSign ) ) ); definition let c be Element of Constructors ; func base_exp_of c -> expression equals :: ABCMIZ_A:def 19 (@ c) -trm (args (loci_of c)); coherence (@ c) -trm (args (loci_of c)) is expression ; end; :: deftheorem defines base_exp_of ABCMIZ_A:def_19_:_ for c being Element of Constructors holds base_exp_of c = (@ c) -trm (args (loci_of c)); theorem Th42: :: ABCMIZ_A:42 for o being OperSymbol of MaxConstrSign holds ( o is constructor iff o in Constructors ) proof let o be OperSymbol of MaxConstrSign; ::_thesis: ( o is constructor iff o in Constructors ) A1: the carrier' of MaxConstrSign = {*,non_op} \/ Constructors by ABCMIZ_1:def_24; ( o is constructor iff ( o <> * & o <> non_op ) ) by ABCMIZ_1:def_11; then ( o is constructor iff o nin {*,non_op} ) by TARSKI:def_2; hence ( o is constructor iff o in Constructors ) by A1, ABCMIZ_1:39, XBOOLE_0:3, XBOOLE_0:def_3; ::_thesis: verum end; theorem :: ABCMIZ_A:43 for m being nullary OperSymbol of MaxConstrSign holds main-constr (m term) = m proof set C = MaxConstrSign ; let m be nullary OperSymbol of MaxConstrSign; ::_thesis: main-constr (m term) = m the_arity_of m = 0 by Def13; then ( len (the_arity_of m) = 0 & len {} = 0 ) ; then A1: ( m term = [m, the carrier of MaxConstrSign] -tree {} & m -trm (<*> (QuasiTerms MaxConstrSign)) = [m, the carrier of MaxConstrSign] -tree {} ) by ABCMIZ_1:def_29, ABCMIZ_1:def_35; hence main-constr (m term) = ((m term) . {}) `1 by Def9 .= [m, the carrier of MaxConstrSign] `1 by A1, TREES_4:def_4 .= m ; ::_thesis: verum end; theorem :: ABCMIZ_A:44 for m being constructor unary OperSymbol of MaxConstrSign for t being quasi-term holds main-constr (m term t) = m proof set C = MaxConstrSign ; let m be constructor unary OperSymbol of MaxConstrSign; ::_thesis: for t being quasi-term holds main-constr (m term t) = m let t be quasi-term; ::_thesis: main-constr (m term t) = m reconsider w = t as Element of QuasiTerms MaxConstrSign by ABCMIZ_1:49; reconsider p = <*w*> as FinSequence of QuasiTerms MaxConstrSign ; A1: len (the_arity_of m) = 1 by Def14; then the_arity_of m = 1 |-> a_Term by ABCMIZ_1:37 .= <*a_Term*> by FINSEQ_2:59 ; then ( len p = 1 & (the_arity_of m) . 1 = a_Term MaxConstrSign ) by FINSEQ_1:40; then A2: ( m term t = [m, the carrier of MaxConstrSign] -tree <*t*> & m -trm p = [m, the carrier of MaxConstrSign] -tree <*t*> ) by A1, ABCMIZ_1:def_30, ABCMIZ_1:def_35; hence main-constr (m term t) = ((m term t) . {}) `1 by Def9 .= [m, the carrier of MaxConstrSign] `1 by A2, TREES_4:def_4 .= m ; ::_thesis: verum end; theorem :: ABCMIZ_A:45 for a being quasi-adjective holds main-constr ((non_op MaxConstrSign) term a) = non_op proof set C = MaxConstrSign ; set m = non_op MaxConstrSign; let a be quasi-adjective; ::_thesis: main-constr ((non_op MaxConstrSign) term a) = non_op A1: len (the_arity_of (non_op MaxConstrSign)) = 1 by Def14; the_arity_of (non_op MaxConstrSign) = <*an_Adj*> by ABCMIZ_1:38; then (the_arity_of (non_op MaxConstrSign)) . 1 = an_Adj MaxConstrSign by FINSEQ_1:40; then A2: (non_op MaxConstrSign) term a = [(non_op MaxConstrSign), the carrier of MaxConstrSign] -tree <*a*> by A1, ABCMIZ_1:def_30; thus main-constr ((non_op MaxConstrSign) term a) = (((non_op MaxConstrSign) term a) . {}) `1 by Def9 .= [(non_op MaxConstrSign), the carrier of MaxConstrSign] `1 by A2, TREES_4:def_4 .= non_op ; ::_thesis: verum end; theorem :: ABCMIZ_A:46 for m being constructor binary OperSymbol of MaxConstrSign for t1, t2 being quasi-term holds main-constr (m term (t1,t2)) = m proof set C = MaxConstrSign ; let m be constructor binary OperSymbol of MaxConstrSign; ::_thesis: for t1, t2 being quasi-term holds main-constr (m term (t1,t2)) = m let t1, t2 be quasi-term; ::_thesis: main-constr (m term (t1,t2)) = m reconsider w1 = t1, w2 = t2 as Element of QuasiTerms MaxConstrSign by ABCMIZ_1:49; reconsider p = <*w1,w2*> as FinSequence of QuasiTerms MaxConstrSign ; A1: len (the_arity_of m) = 2 by Def15; then the_arity_of m = 2 |-> a_Term by ABCMIZ_1:37 .= <*a_Term,a_Term*> by FINSEQ_2:61 ; then ( (the_arity_of m) . 1 = a_Term MaxConstrSign & (the_arity_of m) . 2 = a_Term MaxConstrSign & len p = 2 ) by FINSEQ_1:44; then A2: ( m term (t1,t2) = [m, the carrier of MaxConstrSign] -tree <*t1,t2*> & m -trm p = [m, the carrier of MaxConstrSign] -tree p ) by A1, ABCMIZ_1:def_31, ABCMIZ_1:def_35; hence main-constr (m term (t1,t2)) = ((m term (t1,t2)) . {}) `1 by Def9 .= [m, the carrier of MaxConstrSign] `1 by A2, TREES_4:def_4 .= m ; ::_thesis: verum end; theorem :: ABCMIZ_A:47 for q being expression of MaxConstrSign , a_Type MaxConstrSign for a being quasi-adjective holds main-constr ((ast MaxConstrSign) term (a,q)) = * proof set C = MaxConstrSign ; set m = ast MaxConstrSign; let q be expression of MaxConstrSign , a_Type MaxConstrSign; ::_thesis: for a being quasi-adjective holds main-constr ((ast MaxConstrSign) term (a,q)) = * let a be quasi-adjective; ::_thesis: main-constr ((ast MaxConstrSign) term (a,q)) = * A1: len (the_arity_of (ast MaxConstrSign)) = 2 by Def15; the_arity_of (ast MaxConstrSign) = <*(an_Adj MaxConstrSign),(a_Type MaxConstrSign)*> by ABCMIZ_1:38; then ( (the_arity_of (ast MaxConstrSign)) . 1 = an_Adj MaxConstrSign & (the_arity_of (ast MaxConstrSign)) . 2 = a_Type MaxConstrSign ) by FINSEQ_1:44; then A2: (ast MaxConstrSign) term (a,q) = [(ast MaxConstrSign), the carrier of MaxConstrSign] -tree <*a,q*> by A1, ABCMIZ_1:def_31; thus main-constr ((ast MaxConstrSign) term (a,q)) = (((ast MaxConstrSign) term (a,q)) . {}) `1 by Def9 .= [(ast MaxConstrSign), the carrier of MaxConstrSign] `1 by A2, TREES_4:def_4 .= * ; ::_thesis: verum end; definition let T be quasi-type; func constrs T -> set equals :: ABCMIZ_A:def 20 (constrs (the_base_of T)) \/ (union { (constrs a) where a is quasi-adjective : a in adjs T } ); coherence (constrs (the_base_of T)) \/ (union { (constrs a) where a is quasi-adjective : a in adjs T } ) is set ; end; :: deftheorem defines constrs ABCMIZ_A:def_20_:_ for T being quasi-type holds constrs T = (constrs (the_base_of T)) \/ (union { (constrs a) where a is quasi-adjective : a in adjs T } ); theorem :: ABCMIZ_A:48 for q being pure expression of MaxConstrSign , a_Type MaxConstrSign for A being finite Subset of (QuasiAdjs MaxConstrSign) holds constrs (A ast q) = (constrs q) \/ (union { (constrs a) where a is quasi-adjective : a in A } ) ; theorem :: ABCMIZ_A:49 for a being quasi-adjective for T being quasi-type holds constrs (a ast T) = (constrs a) \/ (constrs T) proof let a be quasi-adjective; ::_thesis: for T being quasi-type holds constrs (a ast T) = (constrs a) \/ (constrs T) let T be quasi-type; ::_thesis: constrs (a ast T) = (constrs a) \/ (constrs T) set A = { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } ; set B = { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } ; A1: { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } = { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } \/ {(constrs a)} proof thus { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } c= { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } \/ {(constrs a)} :: according to XBOOLE_0:def_10 ::_thesis: { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } \/ {(constrs a)} c= { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } or z in { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } \/ {(constrs a)} ) assume z in { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } ; ::_thesis: z in { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } \/ {(constrs a)} then consider a9 being quasi-adjective such that A2: ( z = constrs a9 & a9 in {a} \/ (adjs T) ) ; ( a9 in {a} or a9 in adjs T ) by A2, XBOOLE_0:def_3; then ( a9 = a or a9 in adjs T ) by TARSKI:def_1; then ( z in {(constrs a)} or z in { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } ) by A2, TARSKI:def_1; hence z in { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } \/ {(constrs a)} by XBOOLE_0:def_3; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } \/ {(constrs a)} or z in { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } ) assume A3: z in { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } \/ {(constrs a)} ; ::_thesis: z in { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } A4: a in {a} by TARSKI:def_1; percases ( z in { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } or z in {(constrs a)} ) by A3, XBOOLE_0:def_3; suppose z in { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } ; ::_thesis: z in { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } then consider a9 being quasi-adjective such that A5: ( z = constrs a9 & a9 in adjs T ) ; a9 in {a} \/ (adjs T) by A5, XBOOLE_0:def_3; hence z in { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } by A5; ::_thesis: verum end; suppose z in {(constrs a)} ; ::_thesis: z in { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } then ( z = constrs a & a in {a} \/ (adjs T) ) by A4, TARSKI:def_1, XBOOLE_0:def_3; hence z in { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } ; ::_thesis: verum end; end; end; adjs (a ast T) = {a} \/ (adjs T) by ABCMIZ_1:82; hence constrs (a ast T) = (constrs (the_base_of (a ast T))) \/ (union { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } ) .= (constrs (the_base_of T)) \/ (union { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } ) by ABCMIZ_1:82 .= (constrs (the_base_of T)) \/ ((union {(constrs a)}) \/ (union { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } )) by A1, ZFMISC_1:78 .= (constrs (the_base_of T)) \/ ((constrs a) \/ (union { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } )) by ZFMISC_1:25 .= ((constrs (the_base_of T)) \/ (constrs a)) \/ (union { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } ) by XBOOLE_1:4 .= (constrs a) \/ ((constrs (the_base_of T)) \/ (union { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } )) by XBOOLE_1:4 .= (constrs a) \/ (constrs T) ; ::_thesis: verum end; begin definition let C be initialized ConstructorSignature; let t, p be expression of C; predt matches_with p means :: ABCMIZ_A:def 21 ex f being valuation of C st t = p at f; reflexivity for t being expression of C ex f being valuation of C st t = t at f proof let t be expression of C; ::_thesis: ex f being valuation of C st t = t at f take f = the empty valuation of C; ::_thesis: t = t at f thus t at f = t by ABCMIZ_1:139; ::_thesis: verum end; end; :: deftheorem defines matches_with ABCMIZ_A:def_21_:_ for C being initialized ConstructorSignature for t, p being expression of C holds ( t matches_with p iff ex f being valuation of C st t = p at f ); theorem :: ABCMIZ_A:50 for C being initialized ConstructorSignature for t1, t2, t3 being expression of C st t1 matches_with t2 & t2 matches_with t3 holds t1 matches_with t3 proof let C be initialized ConstructorSignature; ::_thesis: for t1, t2, t3 being expression of C st t1 matches_with t2 & t2 matches_with t3 holds t1 matches_with t3 let t1, t2, t3 be expression of C; ::_thesis: ( t1 matches_with t2 & t2 matches_with t3 implies t1 matches_with t3 ) given f1 being valuation of C such that A1: t1 = t2 at f1 ; :: according to ABCMIZ_A:def_21 ::_thesis: ( not t2 matches_with t3 or t1 matches_with t3 ) given f2 being valuation of C such that A2: t2 = t3 at f2 ; :: according to ABCMIZ_A:def_21 ::_thesis: t1 matches_with t3 take f2 at f1 ; :: according to ABCMIZ_A:def_21 ::_thesis: t1 = t3 at (f2 at f1) thus t1 = t3 at (f2 at f1) by A1, A2, ABCMIZ_1:149; ::_thesis: verum end; definition let C be initialized ConstructorSignature; let A, B be Subset of (QuasiAdjs C); predA matches_with B means :: ABCMIZ_A:def 22 ex f being valuation of C st B at f c= A; reflexivity for A being Subset of (QuasiAdjs C) ex f being valuation of C st A at f c= A proof let t be Subset of (QuasiAdjs C); ::_thesis: ex f being valuation of C st t at f c= t take f = the empty valuation of C; ::_thesis: t at f c= t let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in t at f or x in t ) assume x in t at f ; ::_thesis: x in t then ex a being quasi-adjective of C st ( x = a at f & a in t ) ; hence x in t by ABCMIZ_1:139; ::_thesis: verum end; end; :: deftheorem defines matches_with ABCMIZ_A:def_22_:_ for C being initialized ConstructorSignature for A, B being Subset of (QuasiAdjs C) holds ( A matches_with B iff ex f being valuation of C st B at f c= A ); theorem :: ABCMIZ_A:51 for C being initialized ConstructorSignature for A1, A2, A3 being Subset of (QuasiAdjs C) st A1 matches_with A2 & A2 matches_with A3 holds A1 matches_with A3 proof let C be initialized ConstructorSignature; ::_thesis: for A1, A2, A3 being Subset of (QuasiAdjs C) st A1 matches_with A2 & A2 matches_with A3 holds A1 matches_with A3 let t1, t2, t3 be Subset of (QuasiAdjs C); ::_thesis: ( t1 matches_with t2 & t2 matches_with t3 implies t1 matches_with t3 ) given f1 being valuation of C such that A1: t2 at f1 c= t1 ; :: according to ABCMIZ_A:def_22 ::_thesis: ( not t2 matches_with t3 or t1 matches_with t3 ) given f2 being valuation of C such that A2: t3 at f2 c= t2 ; :: according to ABCMIZ_A:def_22 ::_thesis: t1 matches_with t3 take f2 at f1 ; :: according to ABCMIZ_A:def_22 ::_thesis: t3 at (f2 at f1) c= t1 (t3 at f2) at f1 c= t2 at f1 by A2, ABCMIZ_1:146; then (t3 at f2) at f1 c= t1 by A1, XBOOLE_1:1; hence t3 at (f2 at f1) c= t1 by ABCMIZ_1:150; ::_thesis: verum end; definition let C be initialized ConstructorSignature; let T, P be quasi-type of C; predT matches_with P means :: ABCMIZ_A:def 23 ex f being valuation of C st ( (adjs P) at f c= adjs T & (the_base_of P) at f = the_base_of T ); reflexivity for T being quasi-type of C ex f being valuation of C st ( (adjs T) at f c= adjs T & (the_base_of T) at f = the_base_of T ) proof let t be quasi-type of C; ::_thesis: ex f being valuation of C st ( (adjs t) at f c= adjs t & (the_base_of t) at f = the_base_of t ) take f = the empty valuation of C; ::_thesis: ( (adjs t) at f c= adjs t & (the_base_of t) at f = the_base_of t ) thus (adjs t) at f c= adjs t ::_thesis: (the_base_of t) at f = the_base_of t proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (adjs t) at f or x in adjs t ) assume x in (adjs t) at f ; ::_thesis: x in adjs t then ex a being quasi-adjective of C st ( x = a at f & a in adjs t ) ; hence x in adjs t by ABCMIZ_1:139; ::_thesis: verum end; thus (the_base_of t) at f = the_base_of t by ABCMIZ_1:139; ::_thesis: verum end; end; :: deftheorem defines matches_with ABCMIZ_A:def_23_:_ for C being initialized ConstructorSignature for T, P being quasi-type of C holds ( T matches_with P iff ex f being valuation of C st ( (adjs P) at f c= adjs T & (the_base_of P) at f = the_base_of T ) ); theorem :: ABCMIZ_A:52 for C being initialized ConstructorSignature for T1, T2, T3 being quasi-type of C st T1 matches_with T2 & T2 matches_with T3 holds T1 matches_with T3 proof let C be initialized ConstructorSignature; ::_thesis: for T1, T2, T3 being quasi-type of C st T1 matches_with T2 & T2 matches_with T3 holds T1 matches_with T3 let t1, t2, t3 be quasi-type of C; ::_thesis: ( t1 matches_with t2 & t2 matches_with t3 implies t1 matches_with t3 ) given f1 being valuation of C such that A1: ( (adjs t2) at f1 c= adjs t1 & (the_base_of t2) at f1 = the_base_of t1 ) ; :: according to ABCMIZ_A:def_23 ::_thesis: ( not t2 matches_with t3 or t1 matches_with t3 ) given f2 being valuation of C such that A2: ( (adjs t3) at f2 c= adjs t2 & (the_base_of t3) at f2 = the_base_of t2 ) ; :: according to ABCMIZ_A:def_23 ::_thesis: t1 matches_with t3 take f2 at f1 ; :: according to ABCMIZ_A:def_23 ::_thesis: ( (adjs t3) at (f2 at f1) c= adjs t1 & (the_base_of t3) at (f2 at f1) = the_base_of t1 ) ((adjs t3) at f2) at f1 c= (adjs t2) at f1 by A2, ABCMIZ_1:146; then ((adjs t3) at f2) at f1 c= adjs t1 by A1, XBOOLE_1:1; hence ( (adjs t3) at (f2 at f1) c= adjs t1 & (the_base_of t3) at (f2 at f1) = the_base_of t1 ) by A1, A2, ABCMIZ_1:149, ABCMIZ_1:150; ::_thesis: verum end; definition let C be initialized ConstructorSignature; let t1, t2 be expression of C; let f be valuation of C; predf unifies t1,t2 means :Def24: :: ABCMIZ_A:def 24 t1 at f = t2 at f; end; :: deftheorem Def24 defines unifies ABCMIZ_A:def_24_:_ for C being initialized ConstructorSignature for t1, t2 being expression of C for f being valuation of C holds ( f unifies t1,t2 iff t1 at f = t2 at f ); theorem Th53: :: ABCMIZ_A:53 for C being initialized ConstructorSignature for t1, t2 being expression of C for f being valuation of C st f unifies t1,t2 holds f unifies t2,t1 proof let C be initialized ConstructorSignature; ::_thesis: for t1, t2 being expression of C for f being valuation of C st f unifies t1,t2 holds f unifies t2,t1 let t1, t2 be expression of C; ::_thesis: for f being valuation of C st f unifies t1,t2 holds f unifies t2,t1 let f be valuation of C; ::_thesis: ( f unifies t1,t2 implies f unifies t2,t1 ) assume t1 at f = t2 at f ; :: according to ABCMIZ_A:def_24 ::_thesis: f unifies t2,t1 hence t2 at f = t1 at f ; :: according to ABCMIZ_A:def_24 ::_thesis: verum end; definition let C be initialized ConstructorSignature; let t1, t2 be expression of C; predt1,t2 are_unifiable means :: ABCMIZ_A:def 25 ex f being valuation of C st f unifies t1,t2; reflexivity for t1 being expression of C ex f being valuation of C st f unifies t1,t1 proof let t be expression of C; ::_thesis: ex f being valuation of C st f unifies t,t set f = the valuation of C; take the valuation of C ; ::_thesis: the valuation of C unifies t,t thus t at the valuation of C = t at the valuation of C ; :: according to ABCMIZ_A:def_24 ::_thesis: verum end; symmetry for t1, t2 being expression of C st ex f being valuation of C st f unifies t1,t2 holds ex f being valuation of C st f unifies t2,t1 proof let t1, t2 be expression of C; ::_thesis: ( ex f being valuation of C st f unifies t1,t2 implies ex f being valuation of C st f unifies t2,t1 ) given f being valuation of C such that A1: f unifies t1,t2 ; ::_thesis: ex f being valuation of C st f unifies t2,t1 take f ; ::_thesis: f unifies t2,t1 thus t2 at f = t1 at f by A1, Def24; :: according to ABCMIZ_A:def_24 ::_thesis: verum end; end; :: deftheorem defines are_unifiable ABCMIZ_A:def_25_:_ for C being initialized ConstructorSignature for t1, t2 being expression of C holds ( t1,t2 are_unifiable iff ex f being valuation of C st f unifies t1,t2 ); definition let C be initialized ConstructorSignature; let t1, t2 be expression of C; predt1,t2 are_weakly-unifiable means :: ABCMIZ_A:def 26 ex g being one-to-one irrelevant valuation of C st ( variables_in t2 c= dom g & t1,t2 at g are_unifiable ); reflexivity for t1 being expression of C ex g being one-to-one irrelevant valuation of C st ( variables_in t1 c= dom g & t1,t1 at g are_unifiable ) proof let t be expression of C; ::_thesis: ex g being one-to-one irrelevant valuation of C st ( variables_in t c= dom g & t,t at g are_unifiable ) take C idval (variables_in t) ; ::_thesis: ( variables_in t c= dom (C idval (variables_in t)) & t,t at (C idval (variables_in t)) are_unifiable ) thus ( variables_in t c= dom (C idval (variables_in t)) & t,t at (C idval (variables_in t)) are_unifiable ) by ABCMIZ_1:131, ABCMIZ_1:137; ::_thesis: verum end; end; :: deftheorem defines are_weakly-unifiable ABCMIZ_A:def_26_:_ for C being initialized ConstructorSignature for t1, t2 being expression of C holds ( t1,t2 are_weakly-unifiable iff ex g being one-to-one irrelevant valuation of C st ( variables_in t2 c= dom g & t1,t2 at g are_unifiable ) ); theorem :: ABCMIZ_A:54 for C being initialized ConstructorSignature for t1, t2 being expression of C st t1,t2 are_unifiable holds t1,t2 are_weakly-unifiable proof let C be initialized ConstructorSignature; ::_thesis: for t1, t2 being expression of C st t1,t2 are_unifiable holds t1,t2 are_weakly-unifiable let t1, t2 be expression of C; ::_thesis: ( t1,t2 are_unifiable implies t1,t2 are_weakly-unifiable ) given f being valuation of C such that A1: f unifies t1,t2 ; :: according to ABCMIZ_A:def_25 ::_thesis: t1,t2 are_weakly-unifiable take g = C idval (variables_in t2); :: according to ABCMIZ_A:def_26 ::_thesis: ( variables_in t2 c= dom g & t1,t2 at g are_unifiable ) thus variables_in t2 c= dom g by ABCMIZ_1:131; ::_thesis: t1,t2 at g are_unifiable take f ; :: according to ABCMIZ_A:def_25 ::_thesis: f unifies t1,t2 at g thus f unifies t1,t2 at g by A1, ABCMIZ_1:137; ::_thesis: verum end; definition let C be initialized ConstructorSignature; let t, t1, t2 be expression of C; predt is_a_unification_of t1,t2 means :: ABCMIZ_A:def 27 ex f being valuation of C st ( f unifies t1,t2 & t = t1 at f ); end; :: deftheorem defines is_a_unification_of ABCMIZ_A:def_27_:_ for C being initialized ConstructorSignature for t, t1, t2 being expression of C holds ( t is_a_unification_of t1,t2 iff ex f being valuation of C st ( f unifies t1,t2 & t = t1 at f ) ); theorem :: ABCMIZ_A:55 for C being initialized ConstructorSignature for t1, t2, t being expression of C st t is_a_unification_of t1,t2 holds t is_a_unification_of t2,t1 proof let C be initialized ConstructorSignature; ::_thesis: for t1, t2, t being expression of C st t is_a_unification_of t1,t2 holds t is_a_unification_of t2,t1 let t1, t2, t be expression of C; ::_thesis: ( t is_a_unification_of t1,t2 implies t is_a_unification_of t2,t1 ) given f being valuation of C such that A1: ( f unifies t1,t2 & t = t1 at f ) ; :: according to ABCMIZ_A:def_27 ::_thesis: t is_a_unification_of t2,t1 take f ; :: according to ABCMIZ_A:def_27 ::_thesis: ( f unifies t2,t1 & t = t2 at f ) thus ( f unifies t2,t1 & t = t2 at f ) by A1, Def24, Th53; ::_thesis: verum end; theorem :: ABCMIZ_A:56 for C being initialized ConstructorSignature for t1, t2, t being expression of C st t is_a_unification_of t1,t2 holds ( t matches_with t1 & t matches_with t2 ) proof let C be initialized ConstructorSignature; ::_thesis: for t1, t2, t being expression of C st t is_a_unification_of t1,t2 holds ( t matches_with t1 & t matches_with t2 ) let t1, t2, t be expression of C; ::_thesis: ( t is_a_unification_of t1,t2 implies ( t matches_with t1 & t matches_with t2 ) ) given f being valuation of C such that A1: ( f unifies t1,t2 & t = t1 at f ) ; :: according to ABCMIZ_A:def_27 ::_thesis: ( t matches_with t1 & t matches_with t2 ) thus ex f being valuation of C st t = t1 at f by A1; :: according to ABCMIZ_A:def_21 ::_thesis: t matches_with t2 take f ; :: according to ABCMIZ_A:def_21 ::_thesis: t = t2 at f thus t = t2 at f by A1, Def24; ::_thesis: verum end; definition let C be initialized ConstructorSignature; let t, t1, t2 be expression of C; predt is_a_general-unification_of t1,t2 means :: ABCMIZ_A:def 28 ( t is_a_unification_of t1,t2 & ( for u being expression of C st u is_a_unification_of t1,t2 holds u matches_with t ) ); end; :: deftheorem defines is_a_general-unification_of ABCMIZ_A:def_28_:_ for C being initialized ConstructorSignature for t, t1, t2 being expression of C holds ( t is_a_general-unification_of t1,t2 iff ( t is_a_unification_of t1,t2 & ( for u being expression of C st u is_a_unification_of t1,t2 holds u matches_with t ) ) ); begin theorem Th57: :: ABCMIZ_A:57 for n being Nat for s being SortSymbol of MaxConstrSign ex m being constructor OperSymbol of s st len (the_arity_of m) = n proof set C = MaxConstrSign ; let n be Nat; ::_thesis: for s being SortSymbol of MaxConstrSign ex m being constructor OperSymbol of s st len (the_arity_of m) = n let s be SortSymbol of MaxConstrSign; ::_thesis: ex m being constructor OperSymbol of s st len (the_arity_of m) = n deffunc H1( Nat) -> set = [{},$1]; consider l being FinSequence such that A1: len l = n and A2: for i being Nat st i in dom l holds l . i = H1(i) from FINSEQ_1:sch_2(); A3: l is one-to-one proof let i, j be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not i in proj1 l or not j in proj1 l or not l . i = l . j or i = j ) assume A4: ( i in dom l & j in dom l & l . i = l . j ) ; ::_thesis: i = j reconsider i = i, j = j as Nat by A4; ( l . i = H1(i) & l . i = H1(j) ) by A2, A4; then i = H1(j) `2 by MCART_1:7; hence i = j ; ::_thesis: verum end; rng l c= Vars proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng l or z in Vars ) assume z in rng l ; ::_thesis: z in Vars then consider a being set such that A5: ( a in dom l & z = l . a ) by FUNCT_1:def_3; reconsider a = a as Nat by A5; z = H1(a) by A2, A5; hence z in Vars by ABCMIZ_1:25; ::_thesis: verum end; then reconsider l = l as one-to-one FinSequence of Vars by A3, FINSEQ_1:def_4; for i being Nat for x being variable st i in dom l & x = l . i holds for y being variable st y in vars x holds ex j being Nat st ( j in dom l & j < i & y = l . j ) proof let i be Nat; ::_thesis: for x being variable st i in dom l & x = l . i holds for y being variable st y in vars x holds ex j being Nat st ( j in dom l & j < i & y = l . j ) let x be variable; ::_thesis: ( i in dom l & x = l . i implies for y being variable st y in vars x holds ex j being Nat st ( j in dom l & j < i & y = l . j ) ) assume ( i in dom l & x = l . i ) ; ::_thesis: for y being variable st y in vars x holds ex j being Nat st ( j in dom l & j < i & y = l . j ) then x = H1(i) by A2; hence for y being variable st y in vars x holds ex j being Nat st ( j in dom l & j < i & y = l . j ) by MCART_1:7; ::_thesis: verum end; then reconsider l = l as quasi-loci by ABCMIZ_1:30; set m = [s,[l,0]]; the carrier of MaxConstrSign = {a_Type,an_Adj,a_Term} by ABCMIZ_1:def_9; then A6: [s,[l,0]] in Constructors by Th28; then [s,[l,0]] in {*,non_op} \/ Constructors by XBOOLE_0:def_3; then reconsider m = [s,[l,0]] as constructor OperSymbol of MaxConstrSign by A6, Th42, ABCMIZ_1:def_24; the_result_sort_of m = m `1 by ABCMIZ_1:def_24 .= s by MCART_1:7 ; then reconsider m = m as constructor OperSymbol of s by ABCMIZ_1:def_32; take m ; ::_thesis: len (the_arity_of m) = n thus len (the_arity_of m) = card ((m `2) `1) by ABCMIZ_1:def_24 .= card ([l,0] `1) by MCART_1:7 .= card l .= n by A1 ; ::_thesis: verum end; theorem Th58: :: ABCMIZ_A:58 for l being quasi-loci for s being SortSymbol of MaxConstrSign for m being constructor OperSymbol of s st len (the_arity_of m) = len l holds variables_in (m -trm (args l)) = rng l proof let l be quasi-loci; ::_thesis: for s being SortSymbol of MaxConstrSign for m being constructor OperSymbol of s st len (the_arity_of m) = len l holds variables_in (m -trm (args l)) = rng l set X = rng l; set n = len l; set C = MaxConstrSign ; let s be SortSymbol of MaxConstrSign; ::_thesis: for m being constructor OperSymbol of s st len (the_arity_of m) = len l holds variables_in (m -trm (args l)) = rng l let m be constructor OperSymbol of s; ::_thesis: ( len (the_arity_of m) = len l implies variables_in (m -trm (args l)) = rng l ) assume A1: len (the_arity_of m) = len l ; ::_thesis: variables_in (m -trm (args l)) = rng l set p = args l; set Y = { (variables_in t) where t is quasi-term of MaxConstrSign : t in rng (args l) } ; A2: len (args l) = len (the_arity_of m) by A1, Def18; then A3: variables_in (m -trm (args l)) = union { (variables_in t) where t is quasi-term of MaxConstrSign : t in rng (args l) } by ABCMIZ_1:90; A4: dom (args l) = dom l by A1, A2, FINSEQ_3:29; thus variables_in (m -trm (args l)) c= rng l :: according to XBOOLE_0:def_10 ::_thesis: rng l c= variables_in (m -trm (args l)) proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in variables_in (m -trm (args l)) or s in rng l ) assume s in variables_in (m -trm (args l)) ; ::_thesis: s in rng l then consider A being set such that A5: ( s in A & A in { (variables_in t) where t is quasi-term of MaxConstrSign : t in rng (args l) } ) by A3, TARSKI:def_4; consider t being quasi-term of MaxConstrSign such that A6: ( A = variables_in t & t in rng (args l) ) by A5; consider z being set such that A7: ( z in dom (args l) & t = (args l) . z ) by A6, FUNCT_1:def_3; reconsider z = z as Element of NAT by A7; l . z = l /. z by A4, A7, PARTFUN1:def_6; then A8: l /. z in rng l by A4, A7, FUNCT_1:def_3; (args l) . z = (l /. z) -term MaxConstrSign by A4, A7, Def18; then A = {(l /. z)} by A6, A7, ABCMIZ_1:86; hence s in rng l by A5, A8, TARSKI:def_1; ::_thesis: verum end; let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in rng l or s in variables_in (m -trm (args l)) ) assume s in rng l ; ::_thesis: s in variables_in (m -trm (args l)) then consider z being set such that A9: ( z in dom l & s = l . z ) by FUNCT_1:def_3; reconsider z = z as Element of NAT by A9; set t = (l /. z) -term MaxConstrSign; ( (args l) . z = (l /. z) -term MaxConstrSign & l . z = l /. z ) by A9, Def18, PARTFUN1:def_6; then ( variables_in ((l /. z) -term MaxConstrSign) = {s} & (l /. z) -term MaxConstrSign in rng (args l) ) by A4, A9, ABCMIZ_1:86, FUNCT_1:def_3; then ( s in {s} & {s} in { (variables_in t) where t is quasi-term of MaxConstrSign : t in rng (args l) } ) by TARSKI:def_1; hence s in variables_in (m -trm (args l)) by A3, TARSKI:def_4; ::_thesis: verum end; theorem Th59: :: ABCMIZ_A:59 for X being finite Subset of Vars st varcl X = X holds for s being SortSymbol of MaxConstrSign ex m being constructor OperSymbol of s ex p being FinSequence of QuasiTerms MaxConstrSign st ( len p = len (the_arity_of m) & vars (m -trm p) = X ) proof let X be finite Subset of Vars; ::_thesis: ( varcl X = X implies for s being SortSymbol of MaxConstrSign ex m being constructor OperSymbol of s ex p being FinSequence of QuasiTerms MaxConstrSign st ( len p = len (the_arity_of m) & vars (m -trm p) = X ) ) assume A1: varcl X = X ; ::_thesis: for s being SortSymbol of MaxConstrSign ex m being constructor OperSymbol of s ex p being FinSequence of QuasiTerms MaxConstrSign st ( len p = len (the_arity_of m) & vars (m -trm p) = X ) then consider l being quasi-loci such that A2: rng l = X by Th31; set n = len l; set C = MaxConstrSign ; let s be SortSymbol of MaxConstrSign; ::_thesis: ex m being constructor OperSymbol of s ex p being FinSequence of QuasiTerms MaxConstrSign st ( len p = len (the_arity_of m) & vars (m -trm p) = X ) consider m being constructor OperSymbol of s such that A3: len (the_arity_of m) = len l by Th57; take m ; ::_thesis: ex p being FinSequence of QuasiTerms MaxConstrSign st ( len p = len (the_arity_of m) & vars (m -trm p) = X ) set p = args l; take args l ; ::_thesis: ( len (args l) = len (the_arity_of m) & vars (m -trm (args l)) = X ) thus len (args l) = len (the_arity_of m) by A3, Def18; ::_thesis: vars (m -trm (args l)) = X thus vars (m -trm (args l)) = X by A1, A2, A3, Th58; ::_thesis: verum end; definition let d be PartFunc of Vars,QuasiTypes; attrd is even means :Def29: :: ABCMIZ_A:def 29 for x being variable for T being quasi-type st x in dom d & T = d . x holds vars T = vars x; end; :: deftheorem Def29 defines even ABCMIZ_A:def_29_:_ for d being PartFunc of Vars,QuasiTypes holds ( d is even iff for x being variable for T being quasi-type st x in dom d & T = d . x holds vars T = vars x ); definition let l be quasi-loci; mode type-distribution of l -> PartFunc of Vars,QuasiTypes means :Def30: :: ABCMIZ_A:def 30 ( dom it = rng l & it is even ); existence ex b1 being PartFunc of Vars,QuasiTypes st ( dom b1 = rng l & b1 is even ) proof defpred S1[ set , set ] means ex x being variable ex T being quasi-type st ( $1 = x & $2 = T & vars T = vars x ); A1: for z being set st z in rng l holds ex y being set st S1[z,y] proof set C = MaxConstrSign ; let z be set ; ::_thesis: ( z in rng l implies ex y being set st S1[z,y] ) assume z in rng l ; ::_thesis: ex y being set st S1[z,y] then reconsider x = z as variable ; varcl (vars x) = vars x by Th2; then consider m being constructor OperSymbol of a_Type MaxConstrSign, p being FinSequence of QuasiTerms MaxConstrSign such that A2: ( len p = len (the_arity_of m) & vars (m -trm p) = vars x ) by Th59; ( a_Type MaxConstrSign in the carrier of MaxConstrSign & the carrier of MaxConstrSign c= rng the ResultSort of MaxConstrSign ) by ABCMIZ_1:def_54; then consider o being set such that A3: ( o in dom the ResultSort of MaxConstrSign & a_Type MaxConstrSign = the ResultSort of MaxConstrSign . o ) by FUNCT_1:def_3; reconsider o = o as OperSymbol of MaxConstrSign by A3; the_result_sort_of o = a_Type MaxConstrSign by A3; then the_result_sort_of m = a_Type MaxConstrSign by ABCMIZ_1:def_32; then reconsider q = m -trm p as pure expression of MaxConstrSign , a_Type MaxConstrSign by A2, ABCMIZ_1:75; set B = {} (QuasiAdjs MaxConstrSign); reconsider T = ({} (QuasiAdjs MaxConstrSign)) ast q as quasi-type ; take T ; ::_thesis: S1[z,T] take x ; ::_thesis: ex T being quasi-type st ( z = x & T = T & vars T = vars x ) take T ; ::_thesis: ( z = x & T = T & vars T = vars x ) thus ( z = x & T = T & vars T = vars x ) by A2, ABCMIZ_1:106; ::_thesis: verum end; consider f being Function such that A4: dom f = rng l and A5: for z being set st z in rng l holds S1[z,f . z] from CLASSES1:sch_1(A1); rng f c= QuasiTypes proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in QuasiTypes ) assume y in rng f ; ::_thesis: y in QuasiTypes then consider z being set such that A6: ( z in dom f & y = f . z ) by FUNCT_1:def_3; S1[z,y] by A4, A5, A6; hence y in QuasiTypes by ABCMIZ_1:def_43; ::_thesis: verum end; then reconsider f = f as PartFunc of Vars,QuasiTypes by A4, RELSET_1:4; take f ; ::_thesis: ( dom f = rng l & f is even ) thus dom f = rng l by A4; ::_thesis: f is even let x be variable; :: according to ABCMIZ_A:def_29 ::_thesis: for T being quasi-type st x in dom f & T = f . x holds vars T = vars x let T be quasi-type; ::_thesis: ( x in dom f & T = f . x implies vars T = vars x ) assume ( x in dom f & T = f . x ) ; ::_thesis: vars T = vars x then S1[x,T] by A4, A5; hence vars T = vars x ; ::_thesis: verum end; end; :: deftheorem Def30 defines type-distribution ABCMIZ_A:def_30_:_ for l being quasi-loci for b2 being PartFunc of Vars,QuasiTypes holds ( b2 is type-distribution of l iff ( dom b2 = rng l & b2 is even ) ); theorem :: ABCMIZ_A:60 for l being empty quasi-loci holds {} is type-distribution of l proof let l be empty quasi-loci; ::_thesis: {} is type-distribution of l reconsider d = {} as PartFunc of Vars,QuasiTypes by RELSET_1:12; for x being variable for T being quasi-type st x in dom d & T = d . x holds vars T = vars x ; then ( dom d = rng l & d is even ) by Def29; hence {} is type-distribution of l by Def30; ::_thesis: verum end;