:: Towards the construction of a model of Mizar concepts :: by Grzegorz Bancerek :: :: Received April 21, 2008 :: Copyright (c) 2008-2012 Association of Mizar Users begin theorem Th1: :: ABCMIZ_1:1 for x being set for f being Function holds f . x c= Union f proofend; theorem :: ABCMIZ_1:2 for x being set for f being Function st Union f = {} holds f . x = {} by Th1, XBOOLE_1:3; theorem Th3: :: ABCMIZ_1:3 for f being Function for x, y being set st f = [x,y] holds x = y proofend; theorem Th4: :: ABCMIZ_1:4 for X, Y being set holds (id X) .: Y c= Y proofend; theorem Th5: :: ABCMIZ_1:5 for S being non void Signature for X being V8() ManySortedSet of the carrier of S for t being Term of S,X holds not t is pair proofend; registration let S be non void Signature; let X be V9() ManySortedSet of the carrier of S; cluster -> non pair for Element of Union the Sorts of (Free (S,X)); coherence for b1 being Element of (Free (S,X)) holds not b1 is pair proofend; end; theorem Th6: :: ABCMIZ_1:6 for x, y, z being set st x in {z} * & y in {z} * & card x = card y holds x = y proofend; definition let S be non void Signature; let A be MSAlgebra over S; mode Subset of A is Subset of (Union the Sorts of A); mode FinSequence of A is FinSequence of Union the Sorts of A; end; registration let S be non void Signature; let X be V9() ManySortedSet of S; cluster -> DTree-yielding for FinSequence of Union the Sorts of (Free (S,X)); coherence for b1 being FinSequence of (Free (S,X)) holds b1 is DTree-yielding proofend; end; theorem Th7: :: ABCMIZ_1:7 for S being non void Signature for X being V9() ManySortedSet of the carrier of S for t being Element of (Free (S,X)) holds ( ex s being SortSymbol of S ex v being set st ( t = root-tree [v,s] & v in X . s ) or ex o being OperSymbol of S ex p being FinSequence of (Free (S,X)) st ( t = [o, the carrier of S] -tree p & len p = len (the_arity_of o) & p is DTree-yielding & p is ArgumentSeq of Sym (o,(X \/ ( the carrier of S --> {0}))) ) ) proofend; definition let A be set ; func varcl A -> set means :Def1: :: ABCMIZ_1:def 1 ( A c= it & ( for x, y being set st [x,y] in it holds x c= it ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds x c= B ) holds it c= B ) ); uniqueness for b1, b2 being set st A c= b1 & ( for x, y being set st [x,y] in b1 holds x c= b1 ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds x c= B ) holds b1 c= B ) & A c= b2 & ( for x, y being set st [x,y] in b2 holds x c= b2 ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds x c= B ) holds b2 c= B ) holds b1 = b2 proofend; existence ex b1 being set st ( A c= b1 & ( for x, y being set st [x,y] in b1 holds x c= b1 ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds x c= B ) holds b1 c= B ) ) proofend; projectivity for b1 being set for b2 being set st b2 c= b1 & ( for x, y being set st [x,y] in b1 holds x c= b1 ) & ( for B being set st b2 c= B & ( for x, y being set st [x,y] in B holds x c= B ) holds b1 c= B ) holds ( b1 c= b1 & ( for x, y being set st [x,y] in b1 holds x c= b1 ) & ( for B being set st b1 c= B & ( for x, y being set st [x,y] in B holds x c= B ) holds b1 c= B ) ) ; end; :: deftheorem Def1 defines varcl ABCMIZ_1:def_1_:_ for A being set for b2 being set holds ( b2 = varcl A iff ( A c= b2 & ( for x, y being set st [x,y] in b2 holds x c= b2 ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds x c= B ) holds b2 c= B ) ) ); theorem Th8: :: ABCMIZ_1:8 varcl {} = {} proofend; theorem Th9: :: ABCMIZ_1:9 for A, B being set st A c= B holds varcl A c= varcl B proofend; theorem Th10: :: ABCMIZ_1:10 for A being set holds varcl (union A) = union { (varcl a) where a is Element of A : verum } proofend; scheme :: ABCMIZ_1:sch 1 Sch14{ F1() -> set , F2( set ) -> set , P1[ set ] } : varcl (union { F2(z) where z is Element of F1() : P1[z] } ) = union { (varcl F2(z)) where z is Element of F1() : P1[z] } proofend; theorem Th11: :: ABCMIZ_1:11 for X, Y being set holds varcl (X \/ Y) = (varcl X) \/ (varcl Y) proofend; theorem Th12: :: ABCMIZ_1:12 for A being non empty set st ( for a being Element of A holds varcl a = a ) holds varcl (meet A) = meet A proofend; theorem Th13: :: ABCMIZ_1:13 for X, Y being set holds varcl ((varcl X) /\ (varcl Y)) = (varcl X) /\ (varcl Y) proofend; registration let A be empty set ; cluster varcl A -> empty ; coherence varcl A is empty by Th8; end; deffunc H1( set , set ) -> set = { [(varcl A),j] where A is Subset of $2, j is Element of NAT : A is finite } ; definition func Vars -> set means :Def2: :: ABCMIZ_1:def 2 ex V being ManySortedSet of NAT st ( it = Union V & V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) ); existence ex b1 being set ex V being ManySortedSet of NAT st ( b1 = Union V & V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) ) proofend; uniqueness for b1, b2 being set st ex V being ManySortedSet of NAT st ( b1 = Union V & V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) ) & ex V being ManySortedSet of NAT st ( b2 = Union V & V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines Vars ABCMIZ_1:def_2_:_ for b1 being set holds ( b1 = Vars iff ex V being ManySortedSet of NAT st ( b1 = Union V & V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) ) ); theorem Th14: :: ABCMIZ_1:14 for V being ManySortedSet of NAT st V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) holds for i, j being Element of NAT st i <= j holds V . i c= V . j proofend; theorem Th15: :: ABCMIZ_1:15 for V being ManySortedSet of NAT st V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) holds for A being finite Subset of Vars ex i being Element of NAT st A c= V . i proofend; theorem Th16: :: ABCMIZ_1:16 { [{},i] where i is Element of NAT : verum } c= Vars proofend; theorem Th17: :: ABCMIZ_1:17 for A being finite Subset of Vars for i being Nat holds [(varcl A),i] in Vars proofend; theorem Th18: :: ABCMIZ_1:18 Vars = { [(varcl A),j] where A is Subset of Vars, j is Element of NAT : A is finite } proofend; theorem Th19: :: ABCMIZ_1:19 varcl Vars = Vars proofend; theorem Th20: :: ABCMIZ_1:20 for X being set st the_rank_of X is finite holds X is finite proofend; theorem Th21: :: ABCMIZ_1:21 for X being set holds the_rank_of (varcl X) = the_rank_of X proofend; theorem Th22: :: ABCMIZ_1:22 for X being finite Subset of (Rank omega) holds X in Rank omega proofend; theorem Th23: :: ABCMIZ_1:23 Vars c= Rank omega proofend; theorem Th24: :: ABCMIZ_1:24 for A being finite Subset of Vars holds varcl A is finite Subset of Vars proofend; registration cluster Vars -> non empty ; correctness coherence not Vars is empty ; proofend; end; definition mode variable is Element of Vars ; end; registration let x be variable; cluster vars x -> finite ; coherence x `1 is finite proofend; end; notation let x be variable; synonym vars x for x `1 ; end; definition let x be variable; :: original:vars redefine func vars x -> Subset of Vars; coherence vars x is Subset of Vars proofend; end; theorem :: ABCMIZ_1:25 for i being Nat holds [{},i] in Vars proofend; theorem Th26: :: ABCMIZ_1:26 for j being Element of NAT for A being Subset of Vars holds varcl {[(varcl A),j]} = (varcl A) \/ {[(varcl A),j]} proofend; theorem Th27: :: ABCMIZ_1:27 for x being variable holds varcl {x} = (vars x) \/ {x} proofend; theorem :: ABCMIZ_1:28 for i being Nat for x being variable holds [((vars x) \/ {x}),i] in Vars proofend; begin notation let R be Relation; let A be set ; synonym R dom A for R | A; end; definition func QuasiLoci -> FinSequenceSet of Vars means :Def3: :: ABCMIZ_1:def 3 for p being FinSequence of Vars holds ( p in it iff ( p is one-to-one & ( for i being Nat st i in dom p holds (p . i) `1 c= rng (p dom i) ) ) ); existence ex b1 being FinSequenceSet of Vars st for p being FinSequence of Vars holds ( p in b1 iff ( p is one-to-one & ( for i being Nat st i in dom p holds (p . i) `1 c= rng (p dom i) ) ) ) proofend; correctness uniqueness for b1, b2 being FinSequenceSet of Vars st ( for p being FinSequence of Vars holds ( p in b1 iff ( p is one-to-one & ( for i being Nat st i in dom p holds (p . i) `1 c= rng (p dom i) ) ) ) ) & ( for p being FinSequence of Vars holds ( p in b2 iff ( p is one-to-one & ( for i being Nat st i in dom p holds (p . i) `1 c= rng (p dom i) ) ) ) ) holds b1 = b2; proofend; end; :: deftheorem Def3 defines QuasiLoci ABCMIZ_1:def_3_:_ for b1 being FinSequenceSet of Vars holds ( b1 = QuasiLoci iff for p being FinSequence of Vars holds ( p in b1 iff ( p is one-to-one & ( for i being Nat st i in dom p holds (p . i) `1 c= rng (p dom i) ) ) ) ); theorem Th29: :: ABCMIZ_1:29 <*> Vars in QuasiLoci proofend; registration cluster QuasiLoci -> non empty ; correctness coherence not QuasiLoci is empty ; by Th29; end; definition mode quasi-loci is Element of QuasiLoci ; end; registration cluster -> one-to-one for Element of QuasiLoci ; coherence for b1 being quasi-loci holds b1 is one-to-one by Def3; end; theorem Th30: :: ABCMIZ_1:30 for l being one-to-one FinSequence of Vars holds ( l is quasi-loci iff 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 ) ) proofend; theorem Th31: :: ABCMIZ_1:31 for l being quasi-loci for x being variable holds ( l ^ <*x*> is quasi-loci iff ( not x in rng l & vars x c= rng l ) ) proofend; theorem Th32: :: ABCMIZ_1:32 for p, q being FinSequence st p ^ q is quasi-loci holds ( p is quasi-loci & q is FinSequence of Vars ) proofend; theorem :: ABCMIZ_1:33 for l being quasi-loci holds varcl (rng l) = rng l proofend; theorem Th34: :: ABCMIZ_1:34 for x being variable holds ( <*x*> is quasi-loci iff vars x = {} ) proofend; theorem Th35: :: ABCMIZ_1:35 for x, y being variable holds ( <*x,y*> is quasi-loci iff ( vars x = {} & x <> y & vars y c= {x} ) ) proofend; theorem :: ABCMIZ_1:36 for x, y, z being variable holds ( <*x,y,z*> is quasi-loci iff ( vars x = {} & x <> y & vars y c= {x} & x <> z & y <> z & vars z c= {x,y} ) ) proofend; definition let l be quasi-loci; :: original:" redefine funcl " -> PartFunc of Vars,NAT; coherence l " is PartFunc of Vars,NAT proofend; end; begin definition func a_Type -> set equals :: ABCMIZ_1:def 4 0 ; coherence 0 is set ; func an_Adj -> set equals :: ABCMIZ_1:def 5 1; coherence 1 is set ; func a_Term -> set equals :: ABCMIZ_1:def 6 2; coherence 2 is set ; func * -> set equals :: ABCMIZ_1:def 7 0 ; coherence 0 is set ; func non_op -> set equals :: ABCMIZ_1:def 8 1; coherence 1 is set ; end; :: deftheorem defines a_Type ABCMIZ_1:def_4_:_ a_Type = 0 ; :: deftheorem defines an_Adj ABCMIZ_1:def_5_:_ an_Adj = 1; :: deftheorem defines a_Term ABCMIZ_1:def_6_:_ a_Term = 2; :: deftheorem defines * ABCMIZ_1:def_7_:_ * = 0 ; :: deftheorem defines non_op ABCMIZ_1:def_8_:_ non_op = 1; definition let C be Signature; attrC is constructor means :Def9: :: ABCMIZ_1:def 9 ( the carrier of C = {a_Type,an_Adj,a_Term} & {*,non_op} c= the carrier' of C & the Arity of C . * = <*an_Adj,a_Type*> & the Arity of C . non_op = <*an_Adj*> & the ResultSort of C . * = a_Type & the ResultSort of C . non_op = an_Adj & ( for o being Element of the carrier' of C st o <> * & o <> non_op holds the Arity of C . o in {a_Term} * ) ); end; :: deftheorem Def9 defines constructor ABCMIZ_1:def_9_:_ for C being Signature holds ( C is constructor iff ( the carrier of C = {a_Type,an_Adj,a_Term} & {*,non_op} c= the carrier' of C & the Arity of C . * = <*an_Adj,a_Type*> & the Arity of C . non_op = <*an_Adj*> & the ResultSort of C . * = a_Type & the ResultSort of C . non_op = an_Adj & ( for o being Element of the carrier' of C st o <> * & o <> non_op holds the Arity of C . o in {a_Term} * ) ) ); registration clusterV259() constructor -> non empty non void for ManySortedSign ; coherence for b1 being Signature st b1 is constructor holds ( not b1 is empty & not b1 is void ) proofend; end; definition func MinConstrSign -> strict Signature means :Def10: :: ABCMIZ_1:def 10 ( it is constructor & the carrier' of it = {*,non_op} ); existence ex b1 being strict Signature st ( b1 is constructor & the carrier' of b1 = {*,non_op} ) proofend; correctness uniqueness for b1, b2 being strict Signature st b1 is constructor & the carrier' of b1 = {*,non_op} & b2 is constructor & the carrier' of b2 = {*,non_op} holds b1 = b2; proofend; end; :: deftheorem Def10 defines MinConstrSign ABCMIZ_1:def_10_:_ for b1 being strict Signature holds ( b1 = MinConstrSign iff ( b1 is constructor & the carrier' of b1 = {*,non_op} ) ); registration cluster MinConstrSign -> strict constructor ; coherence MinConstrSign is constructor by Def10; end; registration cluster strict V259() constructor for ManySortedSign ; existence ex b1 being Signature st ( b1 is constructor & b1 is strict ) proofend; end; definition mode ConstructorSignature is constructor Signature; end; :: theorem ::? :: for C being ConstructorSignature holds the carrier of C = 3 :: by CONSTRSIGN,YELLOW11:1; definition let C be ConstructorSignature; let o be OperSymbol of C; attro is constructor means :Def11: :: ABCMIZ_1:def 11 ( o <> * & o <> non_op ); end; :: deftheorem Def11 defines constructor ABCMIZ_1:def_11_:_ for C being ConstructorSignature for o being OperSymbol of C holds ( o is constructor iff ( o <> * & o <> non_op ) ); theorem :: ABCMIZ_1:37 for S being ConstructorSignature for o being OperSymbol of S st o is constructor holds the_arity_of o = (len (the_arity_of o)) |-> a_Term proofend; definition let C be non empty non void Signature; attrC is initialized means :Def12: :: ABCMIZ_1:def 12 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 = {} ); end; :: deftheorem Def12 defines initialized ABCMIZ_1:def_12_:_ for C being non empty non void Signature holds ( C is initialized iff 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 = {} ) ); definition let C be ConstructorSignature; A1: the carrier of C = {a_Type,an_Adj,a_Term} by Def9; func a_Type C -> SortSymbol of C equals :: ABCMIZ_1:def 13 a_Type ; coherence a_Type is SortSymbol of C by A1, ENUMSET1:def_1; func an_Adj C -> SortSymbol of C equals :: ABCMIZ_1:def 14 an_Adj ; coherence an_Adj is SortSymbol of C by A1, ENUMSET1:def_1; func a_Term C -> SortSymbol of C equals :: ABCMIZ_1:def 15 a_Term ; coherence a_Term is SortSymbol of C by A1, ENUMSET1:def_1; A2: {*,non_op} c= the carrier' of C by Def9; A3: * in {*,non_op} by TARSKI:def_2; A4: non_op in {*,non_op} by TARSKI:def_2; func non_op C -> OperSymbol of C equals :: ABCMIZ_1:def 16 non_op ; coherence non_op is OperSymbol of C by A2, A4; func ast C -> OperSymbol of C equals :: ABCMIZ_1:def 17 * ; coherence * is OperSymbol of C by A2, A3; end; :: deftheorem defines a_Type ABCMIZ_1:def_13_:_ for C being ConstructorSignature holds a_Type C = a_Type ; :: deftheorem defines an_Adj ABCMIZ_1:def_14_:_ for C being ConstructorSignature holds an_Adj C = an_Adj ; :: deftheorem defines a_Term ABCMIZ_1:def_15_:_ for C being ConstructorSignature holds a_Term C = a_Term ; :: deftheorem defines non_op ABCMIZ_1:def_16_:_ for C being ConstructorSignature holds non_op C = non_op ; :: deftheorem defines ast ABCMIZ_1:def_17_:_ for C being ConstructorSignature holds ast C = * ; theorem :: ABCMIZ_1:38 for C being ConstructorSignature holds ( the_arity_of (non_op C) = <*(an_Adj C)*> & the_result_sort_of (non_op C) = an_Adj C & the_arity_of (ast C) = <*(an_Adj C),(a_Type C)*> & the_result_sort_of (ast C) = a_Type C ) by Def9; definition func Modes -> set equals :: ABCMIZ_1:def 18 [:{a_Type},[:QuasiLoci,NAT:]:]; correctness coherence [:{a_Type},[:QuasiLoci,NAT:]:] is set ; ; func Attrs -> set equals :: ABCMIZ_1:def 19 [:{an_Adj},[:QuasiLoci,NAT:]:]; correctness coherence [:{an_Adj},[:QuasiLoci,NAT:]:] is set ; ; func Funcs -> set equals :: ABCMIZ_1:def 20 [:{a_Term},[:QuasiLoci,NAT:]:]; correctness coherence [:{a_Term},[:QuasiLoci,NAT:]:] is set ; ; end; :: deftheorem defines Modes ABCMIZ_1:def_18_:_ Modes = [:{a_Type},[:QuasiLoci,NAT:]:]; :: deftheorem defines Attrs ABCMIZ_1:def_19_:_ Attrs = [:{an_Adj},[:QuasiLoci,NAT:]:]; :: deftheorem defines Funcs ABCMIZ_1:def_20_:_ Funcs = [:{a_Term},[:QuasiLoci,NAT:]:]; registration cluster Modes -> non empty ; coherence not Modes is empty ; cluster Attrs -> non empty ; coherence not Attrs is empty ; cluster Funcs -> non empty ; coherence not Funcs is empty ; end; definition func Constructors -> non empty set equals :: ABCMIZ_1:def 21 (Modes \/ Attrs) \/ Funcs; coherence (Modes \/ Attrs) \/ Funcs is non empty set ; end; :: deftheorem defines Constructors ABCMIZ_1:def_21_:_ Constructors = (Modes \/ Attrs) \/ Funcs; theorem :: ABCMIZ_1:39 {*,non_op} misses Constructors proofend; definition let x be Element of [:QuasiLoci,NAT:]; :: original:vars redefine funcx `1 -> quasi-loci; coherence vars x is quasi-loci by MCART_1:10; :: original:the_base_of redefine funcx `2 -> Element of NAT ; coherence the_base_of is Element of NAT by MCART_1:10; end; notation let c be Element of Constructors ; synonym kind_of c for c `1 ; end; definition let c be Element of Constructors ; :: original:vars redefine func kind_of c -> Element of {a_Type,an_Adj,a_Term}; coherence vars c is Element of {a_Type,an_Adj,a_Term} proofend; :: original:the_base_of redefine funcc `2 -> Element of [:QuasiLoci,NAT:]; coherence the_base_of is Element of [:QuasiLoci,NAT:] proofend; end; definition let c be Element of Constructors ; func loci_of c -> quasi-loci equals :: ABCMIZ_1:def 22 (c `2) `1 ; coherence (c `2) `1 is quasi-loci ; func index_of c -> Nat equals :: ABCMIZ_1:def 23 (c `2) `2 ; coherence (c `2) `2 is Nat ; end; :: deftheorem defines loci_of ABCMIZ_1:def_22_:_ for c being Element of Constructors holds loci_of c = (c `2) `1 ; :: deftheorem defines index_of ABCMIZ_1:def_23_:_ for c being Element of Constructors holds index_of c = (c `2) `2 ; theorem :: ABCMIZ_1:40 for c being Element of Constructors holds ( ( kind_of c = a_Type implies c in Modes ) & ( c in Modes implies kind_of c = a_Type ) & ( kind_of c = an_Adj implies c in Attrs ) & ( c in Attrs implies kind_of c = an_Adj ) & ( kind_of c = a_Term implies c in Funcs ) & ( c in Funcs implies kind_of c = a_Term ) ) proofend; definition func MaxConstrSign -> strict ConstructorSignature means :Def24: :: ABCMIZ_1:def 24 ( the carrier' of it = {*,non_op} \/ Constructors & ( for o being OperSymbol of it st o is constructor holds ( the ResultSort of it . o = o `1 & card ( the Arity of it . o) = card ((o `2) `1) ) ) ); existence ex b1 being strict ConstructorSignature st ( the carrier' of b1 = {*,non_op} \/ Constructors & ( for o being OperSymbol of b1 st o is constructor holds ( the ResultSort of b1 . o = o `1 & card ( the Arity of b1 . o) = card ((o `2) `1) ) ) ) proofend; uniqueness for b1, b2 being strict ConstructorSignature st the carrier' of b1 = {*,non_op} \/ Constructors & ( for o being OperSymbol of b1 st o is constructor holds ( the ResultSort of b1 . o = o `1 & card ( the Arity of b1 . o) = card ((o `2) `1) ) ) & the carrier' of b2 = {*,non_op} \/ Constructors & ( for o being OperSymbol of b2 st o is constructor holds ( the ResultSort of b2 . o = o `1 & card ( the Arity of b2 . o) = card ((o `2) `1) ) ) holds b1 = b2 proofend; end; :: deftheorem Def24 defines MaxConstrSign ABCMIZ_1:def_24_:_ for b1 being strict ConstructorSignature holds ( b1 = MaxConstrSign iff ( the carrier' of b1 = {*,non_op} \/ Constructors & ( for o being OperSymbol of b1 st o is constructor holds ( the ResultSort of b1 . o = o `1 & card ( the Arity of b1 . o) = card ((o `2) `1) ) ) ) ); registration cluster MinConstrSign -> strict non initialized ; correctness coherence not MinConstrSign is initialized ; proofend; cluster MaxConstrSign -> strict initialized ; correctness coherence MaxConstrSign is initialized ; proofend; end; registration cluster non empty non void V58() strict V259() constructor initialized for ManySortedSign ; correctness existence ex b1 being ConstructorSignature st ( b1 is initialized & b1 is strict ); proofend; end; registration let C be initialized ConstructorSignature; cluster constructor for Element of the carrier' of C; existence ex b1 being OperSymbol of C st b1 is constructor proofend; end; begin definition let C be ConstructorSignature; A1: the carrier of C = {a_Type,an_Adj,a_Term} by Def9; func MSVars C -> ManySortedSet of the carrier of C means :Def25: :: ABCMIZ_1:def 25 ( it . a_Type = {} & it . an_Adj = {} & it . a_Term = Vars ); uniqueness for b1, b2 being ManySortedSet of the carrier of C st b1 . a_Type = {} & b1 . an_Adj = {} & b1 . a_Term = Vars & b2 . a_Type = {} & b2 . an_Adj = {} & b2 . a_Term = Vars holds b1 = b2 proofend; existence ex b1 being ManySortedSet of the carrier of C st ( b1 . a_Type = {} & b1 . an_Adj = {} & b1 . a_Term = Vars ) proofend; end; :: deftheorem Def25 defines MSVars ABCMIZ_1:def_25_:_ for C being ConstructorSignature for b2 being ManySortedSet of the carrier of C holds ( b2 = MSVars C iff ( b2 . a_Type = {} & b2 . an_Adj = {} & b2 . a_Term = Vars ) ); :: theorem :: for C being ConstructorSignature :: for x being variable holds :: (C variables_in root-tree [x, a_Term]).a_Term C = {x} by MSAFREE3:11; registration let C be ConstructorSignature; cluster MSVars C -> V9() ; coherence not MSVars C is empty-yielding proofend; end; registration let C be initialized ConstructorSignature; cluster Free (C,(MSVars C)) -> non-empty ; correctness coherence Free (C,(MSVars C)) is non-empty ; proofend; end; definition let S be non void Signature; let X be V9() ManySortedSet of the carrier of S; let t be Element of (Free (S,X)); attrt is ground means :: ABCMIZ_1:def 26 Union (S variables_in t) = {} ; attrt is compound means :Def27: :: ABCMIZ_1:def 27 t . {} in [: the carrier' of S,{ the carrier of S}:]; end; :: deftheorem defines ground ABCMIZ_1:def_26_:_ for S being non void Signature for X being V9() ManySortedSet of the carrier of S for t being Element of (Free (S,X)) holds ( t is ground iff Union (S variables_in t) = {} ); :: deftheorem Def27 defines compound ABCMIZ_1:def_27_:_ for S being non void Signature for X being V9() ManySortedSet of the carrier of S for t being Element of (Free (S,X)) holds ( t is compound iff t . {} in [: the carrier' of S,{ the carrier of S}:] ); definition let C be initialized ConstructorSignature; mode expression of C is Element of (Free (C,(MSVars C))); end; definition let C be initialized ConstructorSignature; let s be SortSymbol of C; mode expression of C,s -> expression of C means :Def28: :: ABCMIZ_1:def 28 it in the Sorts of (Free (C,(MSVars C))) . s; existence ex b1 being expression of C st b1 in the Sorts of (Free (C,(MSVars C))) . s proofend; end; :: deftheorem Def28 defines expression ABCMIZ_1:def_28_:_ for C being initialized ConstructorSignature for s being SortSymbol of C for b3 being expression of C holds ( b3 is expression of C,s iff b3 in the Sorts of (Free (C,(MSVars C))) . s ); theorem Th41: :: ABCMIZ_1:41 for z being set for C being initialized ConstructorSignature for s being SortSymbol of C holds ( z is expression of C,s iff z in the Sorts of (Free (C,(MSVars C))) . s ) proofend; definition let C be initialized ConstructorSignature; let c be constructor OperSymbol of C; assume A1: len (the_arity_of c) = 0 ; funcc term -> expression of C equals :: ABCMIZ_1:def 29 [c, the carrier of C] -tree {}; coherence [c, the carrier of C] -tree {} is expression of C proofend; end; :: deftheorem defines term ABCMIZ_1:def_29_:_ for C being initialized ConstructorSignature for c being constructor OperSymbol of C st len (the_arity_of c) = 0 holds c term = [c, the carrier of C] -tree {}; theorem Th42: :: ABCMIZ_1:42 for C being initialized ConstructorSignature for o being OperSymbol of C st len (the_arity_of o) = 1 holds for a being expression of C st ex s being SortSymbol of C st ( s = (the_arity_of o) . 1 & a is expression of C,s ) holds [o, the carrier of C] -tree <*a*> is expression of C, the_result_sort_of o proofend; definition let C be initialized ConstructorSignature; let o be OperSymbol of C; assume A1: len (the_arity_of o) = 1 ; let e be expression of C; assume A2: ex s being SortSymbol of C st ( s = (the_arity_of o) . 1 & e is expression of C,s ) ; funco term e -> expression of C equals :Def30: :: ABCMIZ_1:def 30 [o, the carrier of C] -tree <*e*>; coherence [o, the carrier of C] -tree <*e*> is expression of C by A1, A2, Th42; end; :: deftheorem Def30 defines term ABCMIZ_1:def_30_:_ for C being initialized ConstructorSignature for o being OperSymbol of C st len (the_arity_of o) = 1 holds for e being expression of C st ex s being SortSymbol of C st ( s = (the_arity_of o) . 1 & e is expression of C,s ) holds o term e = [o, the carrier of C] -tree <*e*>; theorem Th43: :: ABCMIZ_1:43 for C being initialized ConstructorSignature for a being expression of C, an_Adj C holds ( (non_op C) term a is expression of C, an_Adj C & (non_op C) term a = [non_op, the carrier of C] -tree <*a*> ) proofend; theorem Th44: :: ABCMIZ_1:44 for C being initialized ConstructorSignature for a, b being expression of C, an_Adj C st (non_op C) term a = (non_op C) term b holds a = b proofend; registration let C be initialized ConstructorSignature; let a be expression of C, an_Adj C; cluster(non_op C) term a -> compound ; coherence (non_op C) term a is compound proofend; end; registration let C be initialized ConstructorSignature; cluster non pair non empty Relation-like Function-like finite DecoratedTree-like compound for Element of Union the Sorts of (Free (C,(MSVars C))); existence ex b1 being expression of C st b1 is compound proofend; end; theorem Th45: :: ABCMIZ_1:45 for C being initialized ConstructorSignature for o being OperSymbol of C st len (the_arity_of o) = 2 holds for a, b being expression of C st ex s1, s2 being SortSymbol of C st ( s1 = (the_arity_of o) . 1 & s2 = (the_arity_of o) . 2 & a is expression of C,s1 & b is expression of C,s2 ) holds [o, the carrier of C] -tree <*a,b*> is expression of C, the_result_sort_of o proofend; definition let C be initialized ConstructorSignature; let o be OperSymbol of C; assume A1: len (the_arity_of o) = 2 ; let e1, e2 be expression of C; assume A2: ex s1, s2 being SortSymbol of C st ( s1 = (the_arity_of o) . 1 & s2 = (the_arity_of o) . 2 & e1 is expression of C,s1 & e2 is expression of C,s2 ) ; funco term (e1,e2) -> expression of C equals :Def31: :: ABCMIZ_1:def 31 [o, the carrier of C] -tree <*e1,e2*>; coherence [o, the carrier of C] -tree <*e1,e2*> is expression of C by A1, A2, Th45; end; :: deftheorem Def31 defines term ABCMIZ_1:def_31_:_ for C being initialized ConstructorSignature for o being OperSymbol of C st len (the_arity_of o) = 2 holds for e1, e2 being expression of C st ex s1, s2 being SortSymbol of C st ( s1 = (the_arity_of o) . 1 & s2 = (the_arity_of o) . 2 & e1 is expression of C,s1 & e2 is expression of C,s2 ) holds o term (e1,e2) = [o, the carrier of C] -tree <*e1,e2*>; theorem Th46: :: ABCMIZ_1:46 for C being initialized ConstructorSignature for a being expression of C, an_Adj C for t being expression of C, a_Type C holds ( (ast C) term (a,t) is expression of C, a_Type C & (ast C) term (a,t) = [*, the carrier of C] -tree <*a,t*> ) proofend; theorem :: ABCMIZ_1:47 for C being initialized ConstructorSignature for a, b being expression of C, an_Adj C for t1, t2 being expression of C, a_Type C st (ast C) term (a,t1) = (ast C) term (b,t2) holds ( a = b & t1 = t2 ) proofend; registration let C be initialized ConstructorSignature; let a be expression of C, an_Adj C; let t be expression of C, a_Type C; cluster(ast C) term (a,t) -> compound ; coherence (ast C) term (a,t) is compound proofend; end; definition let S be non void Signature; let s be SortSymbol of S; assume A1: ex o being OperSymbol of S st the_result_sort_of o = s ; mode OperSymbol of s -> OperSymbol of S means :: ABCMIZ_1:def 32 the_result_sort_of it = s; existence ex b1 being OperSymbol of S st the_result_sort_of b1 = s by A1; end; :: deftheorem defines OperSymbol ABCMIZ_1:def_32_:_ for S being non void Signature for s being SortSymbol of S st ex o being OperSymbol of S st the_result_sort_of o = s holds for b3 being OperSymbol of S holds ( b3 is OperSymbol of s iff the_result_sort_of b3 = s ); definition let C be ConstructorSignature; :: original:non_op redefine func non_op C -> OperSymbol of an_Adj C; coherence non_op C is OperSymbol of an_Adj C proofend; :: original:ast redefine func ast C -> OperSymbol of a_Type C; coherence ast C is OperSymbol of a_Type C proofend; end; theorem Th48: :: ABCMIZ_1:48 for C being initialized ConstructorSignature for s1, s2 being SortSymbol of C st s1 <> s2 holds for t1 being expression of C,s1 for t2 being expression of C,s2 holds t1 <> t2 proofend; begin definition let C be initialized ConstructorSignature; A1: the Sorts of (Free (C,(MSVars C))) . (a_Term C) c= Union the Sorts of (Free (C,(MSVars C))) proofend; func QuasiTerms C -> Subset of (Free (C,(MSVars C))) equals :: ABCMIZ_1:def 33 the Sorts of (Free (C,(MSVars C))) . (a_Term C); coherence the Sorts of (Free (C,(MSVars C))) . (a_Term C) is Subset of (Free (C,(MSVars C))) by A1; end; :: deftheorem defines QuasiTerms ABCMIZ_1:def_33_:_ for C being initialized ConstructorSignature holds QuasiTerms C = the Sorts of (Free (C,(MSVars C))) . (a_Term C); registration let C be initialized ConstructorSignature; cluster QuasiTerms C -> non empty constituted-DTrees ; coherence ( not QuasiTerms C is empty & QuasiTerms C is constituted-DTrees ) proofend; end; definition let C be initialized ConstructorSignature; mode quasi-term of C is expression of C, a_Term C; end; theorem :: ABCMIZ_1:49 for z being set for C being initialized ConstructorSignature holds ( z is quasi-term of C iff z in QuasiTerms C ) by Th41; definition let x be variable; let C be initialized ConstructorSignature; funcx -term C -> quasi-term of C equals :: ABCMIZ_1:def 34 root-tree [x,a_Term]; coherence root-tree [x,a_Term] is quasi-term of C proofend; end; :: deftheorem defines -term ABCMIZ_1:def_34_:_ for x being variable for C being initialized ConstructorSignature holds x -term C = root-tree [x,a_Term]; theorem Th50: :: ABCMIZ_1:50 for x1, x2 being variable for C1, C2 being initialized ConstructorSignature st x1 -term C1 = x2 -term C2 holds x1 = x2 proofend; registration let x be variable; let C be initialized ConstructorSignature; clusterx -term C -> non compound ; coherence not x -term C is compound proofend; end; theorem Th51: :: ABCMIZ_1:51 for C being initialized ConstructorSignature for c being constructor OperSymbol of C for p being DTree-yielding FinSequence holds ( [c, the carrier of C] -tree p is expression of C iff ( len p = len (the_arity_of c) & p in (QuasiTerms C) * ) ) proofend; definition let C be initialized ConstructorSignature; let c be constructor OperSymbol of C; let p be FinSequence of QuasiTerms C; assume B1: len p = len (the_arity_of c) ; A1: p in (QuasiTerms C) * by FINSEQ_1:def_11; funcc -trm p -> compound expression of C equals :Def35: :: ABCMIZ_1:def 35 [c, the carrier of C] -tree p; coherence [c, the carrier of C] -tree p is compound expression of C proofend; end; :: deftheorem Def35 defines -trm ABCMIZ_1:def_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 c -trm p = [c, the carrier of C] -tree p; theorem Th52: :: ABCMIZ_1:52 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 c -trm p is expression of C, the_result_sort_of c proofend; theorem Th53: :: ABCMIZ_1:53 for C being initialized ConstructorSignature for e being expression of C holds ( 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) ) proofend; theorem Th54: :: ABCMIZ_1:54 for C being initialized ConstructorSignature for c being constructor OperSymbol of C for a being expression of C, an_Adj C for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds c -trm p <> (non_op C) term a proofend; theorem Th55: :: ABCMIZ_1:55 for C being initialized ConstructorSignature for c being constructor OperSymbol of C for a being expression of C, an_Adj C for t being expression of C, a_Type C for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds c -trm p <> (ast C) term (a,t) proofend; theorem :: ABCMIZ_1:56 for C being initialized ConstructorSignature for a, b being expression of C, an_Adj C for t being expression of C, a_Type C holds (non_op C) term a <> (ast C) term (b,t) proofend; theorem Th57: :: ABCMIZ_1:57 for C being initialized ConstructorSignature for e being expression of C st e . {} = [non_op, the carrier of C] holds ex a being expression of C, an_Adj C st e = (non_op C) term a proofend; theorem Th58: :: ABCMIZ_1:58 for C being initialized ConstructorSignature for e being expression of C st e . {} = [*, the carrier of C] holds 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) proofend; begin definition let C be initialized ConstructorSignature; let a be expression of C, an_Adj C; func Non a -> expression of C, an_Adj C equals :Def36: :: ABCMIZ_1:def 36 a | <*0*> if ex a9 being expression of C, an_Adj C st a = (non_op C) term a9 otherwise (non_op C) term a; coherence ( ( ex a9 being expression of C, an_Adj C st a = (non_op C) term a9 implies a | <*0*> is expression of C, an_Adj C ) & ( ( for a9 being expression of C, an_Adj C holds not a = (non_op C) term a9 ) implies (non_op C) term a is expression of C, an_Adj C ) ) proofend; consistency for b1 being expression of C, an_Adj C holds verum ; end; :: deftheorem Def36 defines Non ABCMIZ_1:def_36_:_ for C being initialized ConstructorSignature for a being expression of C, an_Adj C holds ( ( ex a9 being expression of C, an_Adj C st a = (non_op C) term a9 implies Non a = a | <*0*> ) & ( ( for a9 being expression of C, an_Adj C holds not a = (non_op C) term a9 ) implies Non a = (non_op C) term a ) ); definition let C be initialized ConstructorSignature; let a be expression of C, an_Adj C; attra is positive means :Def37: :: ABCMIZ_1:def 37 for a9 being expression of C, an_Adj C holds not a = (non_op C) term a9; end; :: deftheorem Def37 defines positive ABCMIZ_1:def_37_:_ for C being initialized ConstructorSignature for a being expression of C, an_Adj C holds ( a is positive iff for a9 being expression of C, an_Adj C holds not a = (non_op C) term a9 ); registration let C be initialized ConstructorSignature; cluster non pair non empty Relation-like Function-like finite DecoratedTree-like positive for expression of C, an_Adj C; existence ex b1 being expression of C, an_Adj C st b1 is positive proofend; end; theorem Th59: :: ABCMIZ_1:59 for C being initialized ConstructorSignature for a being positive expression of C, an_Adj C holds Non a = (non_op C) term a proofend; definition let C be initialized ConstructorSignature; let a be expression of C, an_Adj C; attra is negative means :Def38: :: ABCMIZ_1:def 38 ex a9 being expression of C, an_Adj C st ( a9 is positive & a = (non_op C) term a9 ); end; :: deftheorem Def38 defines negative ABCMIZ_1:def_38_:_ for C being initialized ConstructorSignature for a being expression of C, an_Adj C holds ( a is negative iff ex a9 being expression of C, an_Adj C st ( a9 is positive & a = (non_op C) term a9 ) ); registration let C be initialized ConstructorSignature; let a be positive expression of C, an_Adj C; cluster Non a -> non positive negative ; coherence ( Non a is negative & not Non a is positive ) proofend; end; registration let C be initialized ConstructorSignature; cluster non pair non empty Relation-like Function-like finite DecoratedTree-like non positive negative for expression of C, an_Adj C; existence ex b1 being expression of C, an_Adj C st ( b1 is negative & not b1 is positive ) proofend; end; theorem Th60: :: ABCMIZ_1:60 for C being initialized ConstructorSignature for a being non positive expression of C, an_Adj C ex a9 being expression of C, an_Adj C st ( a = (non_op C) term a9 & Non a = a9 ) proofend; theorem Th61: :: ABCMIZ_1:61 for C being initialized ConstructorSignature for a being negative expression of C, an_Adj C ex a9 being positive expression of C, an_Adj C st ( a = (non_op C) term a9 & Non a = a9 ) proofend; theorem Th62: :: ABCMIZ_1:62 for C being initialized ConstructorSignature for a being non positive expression of C, an_Adj C holds (non_op C) term (Non a) = a proofend; registration let C be initialized ConstructorSignature; let a be negative expression of C, an_Adj C; cluster Non a -> positive ; coherence Non a is positive proofend; end; definition let C be initialized ConstructorSignature; let a be expression of C, an_Adj C; attra is regular means :Def39: :: ABCMIZ_1:def 39 ( a is positive or a is negative ); end; :: deftheorem Def39 defines regular ABCMIZ_1:def_39_:_ for C being initialized ConstructorSignature for a being expression of C, an_Adj C holds ( a is regular iff ( a is positive or a is negative ) ); registration let C be initialized ConstructorSignature; cluster positive -> non negative regular for expression of C, an_Adj C; coherence for b1 being expression of C, an_Adj C st b1 is positive holds ( b1 is regular & not b1 is negative ) proofend; cluster negative -> non positive regular for expression of C, an_Adj C; coherence for b1 being expression of C, an_Adj C st b1 is negative holds ( b1 is regular & not b1 is positive ) by Def39; end; registration let C be initialized ConstructorSignature; cluster non pair non empty Relation-like Function-like finite DecoratedTree-like regular for expression of C, an_Adj C; existence ex b1 being expression of C, an_Adj C st b1 is regular proofend; end; definition let C be initialized ConstructorSignature; set X = { a where a is expression of C, an_Adj C : a is regular } ; A1: { a where a is expression of C, an_Adj C : a is regular } c= Union the Sorts of (Free (C,(MSVars C))) proofend; func QuasiAdjs C -> Subset of (Free (C,(MSVars C))) equals :: ABCMIZ_1:def 40 { a where a is expression of C, an_Adj C : a is regular } ; coherence { a where a is expression of C, an_Adj C : a is regular } is Subset of (Free (C,(MSVars C))) by A1; end; :: deftheorem defines QuasiAdjs ABCMIZ_1:def_40_:_ for C being initialized ConstructorSignature holds QuasiAdjs C = { a where a is expression of C, an_Adj C : a is regular } ; registration let C be initialized ConstructorSignature; cluster QuasiAdjs C -> non empty constituted-DTrees ; coherence ( not QuasiAdjs C is empty & QuasiAdjs C is constituted-DTrees ) proofend; end; definition let C be initialized ConstructorSignature; mode quasi-adjective of C is regular expression of C, an_Adj C; end; theorem Th63: :: ABCMIZ_1:63 for z being set for C being initialized ConstructorSignature holds ( z is quasi-adjective of C iff z in QuasiAdjs C ) proofend; theorem :: ABCMIZ_1:64 for z being set for C being initialized ConstructorSignature holds ( z is quasi-adjective of C iff ( z is positive expression of C, an_Adj C or z is negative expression of C, an_Adj C ) ) by Def39; registration let C be initialized ConstructorSignature; cluster non positive regular -> negative for expression of C, an_Adj C; coherence for b1 being quasi-adjective of C st not b1 is positive holds b1 is negative by Def39; cluster non negative regular -> positive for expression of C, an_Adj C; coherence for b1 being quasi-adjective of C st not b1 is negative holds b1 is positive ; end; registration let C be initialized ConstructorSignature; cluster non pair non empty Relation-like Function-like finite DecoratedTree-like positive regular for expression of C, an_Adj C; existence ex b1 being quasi-adjective of C st b1 is positive proofend; cluster non pair non empty Relation-like Function-like finite DecoratedTree-like negative regular for expression of C, an_Adj C; existence ex b1 being quasi-adjective of C st b1 is negative proofend; end; theorem Th65: :: ABCMIZ_1:65 for C being initialized ConstructorSignature for a being positive quasi-adjective of C ex v being constructor OperSymbol of C st ( the_result_sort_of v = an_Adj C & ex p being FinSequence of QuasiTerms C st ( len p = len (the_arity_of v) & a = v -trm p ) ) proofend; theorem Th66: :: ABCMIZ_1:66 for C being initialized ConstructorSignature for p being FinSequence of QuasiTerms C for v being constructor OperSymbol of C st the_result_sort_of v = an_Adj C & len p = len (the_arity_of v) holds v -trm p is positive quasi-adjective of C proofend; registration let C be initialized ConstructorSignature; let a be quasi-adjective of C; cluster Non a -> regular ; coherence Non a is regular proofend; end; theorem Th67: :: ABCMIZ_1:67 for C being initialized ConstructorSignature for a being quasi-adjective of C holds Non (Non a) = a proofend; theorem :: ABCMIZ_1:68 for C being initialized ConstructorSignature for a1, a2 being quasi-adjective of C st Non a1 = Non a2 holds a1 = a2 proofend; theorem :: ABCMIZ_1:69 for C being initialized ConstructorSignature for a being quasi-adjective of C holds Non a <> a proofend; begin definition let C be initialized ConstructorSignature; let q be expression of C, a_Type C; attrq is pure means :Def41: :: ABCMIZ_1:def 41 for a being expression of C, an_Adj C for t being expression of C, a_Type C holds not q = (ast C) term (a,t); end; :: deftheorem Def41 defines pure ABCMIZ_1:def_41_:_ for C being initialized ConstructorSignature for q being expression of C, a_Type C holds ( q is pure iff for a being expression of C, an_Adj C for t being expression of C, a_Type C holds not q = (ast C) term (a,t) ); theorem Th70: :: ABCMIZ_1:70 for C being initialized ConstructorSignature for m being OperSymbol of C st the_result_sort_of m = a_Type & the_arity_of m = {} holds ex t being expression of C, a_Type C st ( t = root-tree [m, the carrier of C] & t is pure ) proofend; theorem Th71: :: ABCMIZ_1:71 for C being initialized ConstructorSignature for v being OperSymbol of C st the_result_sort_of v = an_Adj & the_arity_of v = {} holds ex a being expression of C, an_Adj C st ( a = root-tree [v, the carrier of C] & a is positive ) proofend; registration let C be initialized ConstructorSignature; cluster non pair non empty Relation-like Function-like finite DecoratedTree-like pure for expression of C, a_Type C; existence ex b1 being expression of C, a_Type C st b1 is pure proofend; end; definition let C be initialized ConstructorSignature; func QuasiTypes C -> set equals :: ABCMIZ_1:def 42 { [A,t] where t is expression of C, a_Type C, A is finite Subset of (QuasiAdjs C) : t is pure } ; coherence { [A,t] where t is expression of C, a_Type C, A is finite Subset of (QuasiAdjs C) : t is pure } is set ; end; :: deftheorem defines QuasiTypes ABCMIZ_1:def_42_:_ for C being initialized ConstructorSignature holds QuasiTypes C = { [A,t] where t is expression of C, a_Type C, A is finite Subset of (QuasiAdjs C) : t is pure } ; registration let C be initialized ConstructorSignature; cluster QuasiTypes C -> non empty ; coherence not QuasiTypes C is empty proofend; end; definition let C be initialized ConstructorSignature; mode quasi-type of C -> set means :Def43: :: ABCMIZ_1:def 43 it in QuasiTypes C; existence ex b1 being set st b1 in QuasiTypes C proofend; end; :: deftheorem Def43 defines quasi-type ABCMIZ_1:def_43_:_ for C being initialized ConstructorSignature for b2 being set holds ( b2 is quasi-type of C iff b2 in QuasiTypes C ); theorem Th72: :: ABCMIZ_1:72 for z being set for C being initialized ConstructorSignature holds ( z is quasi-type of C iff ex A being finite Subset of (QuasiAdjs C) ex q being pure expression of C, a_Type C st z = [A,q] ) proofend; theorem Th73: :: ABCMIZ_1:73 for x, y being set for C being initialized ConstructorSignature holds ( [x,y] is quasi-type of C iff ( x is finite Subset of (QuasiAdjs C) & y is pure expression of C, a_Type C ) ) proofend; registration let C be initialized ConstructorSignature; cluster -> pair for quasi-type of C; coherence for b1 being quasi-type of C holds b1 is pair proofend; end; theorem Th74: :: ABCMIZ_1:74 for C being initialized ConstructorSignature for q being pure expression of C, a_Type C ex m being constructor OperSymbol of C st ( the_result_sort_of m = a_Type C & ex p being FinSequence of QuasiTerms C st ( len p = len (the_arity_of m) & q = m -trm p ) ) proofend; theorem Th75: :: ABCMIZ_1:75 for C being initialized ConstructorSignature for p being FinSequence of QuasiTerms C for m being constructor OperSymbol of C st the_result_sort_of m = a_Type C & len p = len (the_arity_of m) holds m -trm p is pure expression of C, a_Type C proofend; theorem :: ABCMIZ_1:76 for C being initialized ConstructorSignature holds ( QuasiTerms C misses QuasiAdjs C & QuasiTerms C misses QuasiTypes C & QuasiTypes C misses QuasiAdjs C ) proofend; theorem :: ABCMIZ_1:77 for C being initialized ConstructorSignature for e being set holds ( ( e is quasi-term of C implies not e is quasi-adjective of C ) & ( e is quasi-term of C implies not e is quasi-type of C ) & ( e is quasi-type of C implies not e is quasi-adjective of C ) ) by Th48; notation let C be initialized ConstructorSignature; let A be finite Subset of (QuasiAdjs C); let q be pure expression of C, a_Type C; synonym A ast q for [C,A]; end; definition let C be initialized ConstructorSignature; let A be finite Subset of (QuasiAdjs C); let q be pure expression of C, a_Type C; :: original:ast redefine funcA ast q -> quasi-type of C; coherence q ast is quasi-type of C by Th73; end; registration let C be initialized ConstructorSignature; let T be quasi-type of C; cluster vars T -> finite ; coherence T `1 is finite proofend; end; notation let C be initialized ConstructorSignature; let T be quasi-type of C; synonym adjs T for C `1 ; synonym the_base_of T for C `2 ; end; definition let C be initialized ConstructorSignature; let T be quasi-type of C; :: original:vars redefine func adjs T -> Subset of (QuasiAdjs C); coherence vars T is Subset of (QuasiAdjs C) proofend; :: original:the_base_of redefine func the_base_of T -> pure expression of C, a_Type C; coherence the_base_of is pure expression of C, a_Type C proofend; end; theorem :: ABCMIZ_1:78 for C being initialized ConstructorSignature for q being pure expression of C, a_Type C for A being finite Subset of (QuasiAdjs C) holds ( adjs (A ast q) = A & the_base_of (A ast q) = q ) ; theorem :: ABCMIZ_1:79 for C being initialized ConstructorSignature for A1, A2 being finite Subset of (QuasiAdjs C) for q1, q2 being pure expression of C, a_Type C st A1 ast q1 = A2 ast q2 holds ( A1 = A2 & q1 = q2 ) by XTUPLE_0:1; theorem Th80: :: ABCMIZ_1:80 for C being initialized ConstructorSignature for T being quasi-type of C holds T = (adjs T) ast (the_base_of T) proofend; theorem :: ABCMIZ_1:81 for C being initialized ConstructorSignature for T1, T2 being quasi-type of C st adjs T1 = adjs T2 & the_base_of T1 = the_base_of T2 holds T1 = T2 proofend; definition let C be initialized ConstructorSignature; let T be quasi-type of C; let a be quasi-adjective of C; funca ast T -> quasi-type of C equals :: ABCMIZ_1:def 44 [({a} \/ (adjs T)),(the_base_of T)]; coherence [({a} \/ (adjs T)),(the_base_of T)] is quasi-type of C proofend; end; :: deftheorem defines ast ABCMIZ_1:def_44_:_ for C being initialized ConstructorSignature for T being quasi-type of C for a being quasi-adjective of C holds a ast T = [({a} \/ (adjs T)),(the_base_of T)]; theorem :: ABCMIZ_1:82 for C being initialized ConstructorSignature for T being quasi-type of C for a being quasi-adjective of C holds ( adjs (a ast T) = {a} \/ (adjs T) & the_base_of (a ast T) = the_base_of T ) by MCART_1:7; theorem :: ABCMIZ_1:83 for C being initialized ConstructorSignature for T being quasi-type of C for a being quasi-adjective of C holds a ast (a ast T) = a ast T proofend; theorem :: ABCMIZ_1:84 for C being initialized ConstructorSignature for T being quasi-type of C for a, b being quasi-adjective of C holds a ast (b ast T) = b ast (a ast T) proofend; begin registration let S be non void Signature; let s be SortSymbol of S; let X be V8() ManySortedSet of the carrier of S; let t be Term of S,X; cluster(variables_in t) . s -> finite ; coherence (variables_in t) . s is finite proofend; end; registration let S be non void Signature; let s be SortSymbol of S; let X be V9() ManySortedSet of the carrier of S; let t be Element of (Free (S,X)); cluster(S variables_in t) . s -> finite ; coherence (S variables_in t) . s is finite proofend; end; definition let S be non void Signature; let X be V9() ManySortedSet of the carrier of S; let s be SortSymbol of S; func(X,s) variables_in -> Function of (Union the Sorts of (Free (S,X))),(bool (X . s)) means :Def45: :: ABCMIZ_1:def 45 for t being Element of (Free (S,X)) holds it . t = (S variables_in t) . s; uniqueness for b1, b2 being Function of (Union the Sorts of (Free (S,X))),(bool (X . s)) st ( for t being Element of (Free (S,X)) holds b1 . t = (S variables_in t) . s ) & ( for t being Element of (Free (S,X)) holds b2 . t = (S variables_in t) . s ) holds b1 = b2 proofend; existence ex b1 being Function of (Union the Sorts of (Free (S,X))),(bool (X . s)) st for t being Element of (Free (S,X)) holds b1 . t = (S variables_in t) . s proofend; end; :: deftheorem Def45 defines variables_in ABCMIZ_1:def_45_:_ for S being non void Signature for X being V9() ManySortedSet of the carrier of S for s being SortSymbol of S for b4 being Function of (Union the Sorts of (Free (S,X))),(bool (X . s)) holds ( b4 = (X,s) variables_in iff for t being Element of (Free (S,X)) holds b4 . t = (S variables_in t) . s ); definition let C be initialized ConstructorSignature; let e be expression of C; func variables_in e -> Subset of Vars equals :: ABCMIZ_1:def 46 (C variables_in e) . (a_Term C); coherence (C variables_in e) . (a_Term C) is Subset of Vars proofend; end; :: deftheorem defines variables_in ABCMIZ_1:def_46_:_ for C being initialized ConstructorSignature for e being expression of C holds variables_in e = (C variables_in e) . (a_Term C); registration let C be initialized ConstructorSignature; let e be expression of C; cluster variables_in e -> finite ; coherence variables_in e is finite ; end; definition let C be initialized ConstructorSignature; let e be expression of C; func vars e -> finite Subset of Vars equals :: ABCMIZ_1:def 47 varcl (variables_in e); coherence varcl (variables_in e) is finite Subset of Vars by Th24; end; :: deftheorem defines vars ABCMIZ_1:def_47_:_ for C being initialized ConstructorSignature for e being expression of C holds vars e = varcl (variables_in e); theorem :: ABCMIZ_1:85 for C being initialized ConstructorSignature for e being expression of C holds varcl (vars e) = vars e ; theorem :: ABCMIZ_1:86 for C being initialized ConstructorSignature for x being variable holds variables_in (x -term C) = {x} by MSAFREE3:10; theorem :: ABCMIZ_1:87 for C being initialized ConstructorSignature for x being variable holds vars (x -term C) = {x} \/ (vars x) proofend; theorem Th88: :: ABCMIZ_1:88 for C being initialized ConstructorSignature for c being constructor OperSymbol of C for e being expression of C for p being DTree-yielding FinSequence st e = [c, the carrier of C] -tree p holds variables_in e = union { (variables_in t) where t is quasi-term of C : t in rng p } proofend; theorem Th89: :: ABCMIZ_1:89 for C being initialized ConstructorSignature for c being constructor OperSymbol of C for e being expression of C for p being DTree-yielding FinSequence st e = [c, the carrier of C] -tree p holds vars e = union { (vars t) where t is quasi-term of C : t in rng p } proofend; theorem :: ABCMIZ_1:90 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 variables_in (c -trm p) = union { (variables_in t) where t is quasi-term of C : t in rng p } proofend; theorem :: ABCMIZ_1:91 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 vars (c -trm p) = union { (vars t) where t is quasi-term of C : t in rng p } proofend; theorem :: ABCMIZ_1:92 for S being ManySortedSign for o being set holds S variables_in ([o, the carrier of S] -tree {}) = [[0]] the carrier of S proofend; theorem Th93: :: ABCMIZ_1:93 for S being ManySortedSign for o being set for t being DecoratedTree holds S variables_in ([o, the carrier of S] -tree <*t*>) = S variables_in t proofend; theorem Th94: :: ABCMIZ_1:94 for C being initialized ConstructorSignature for a being expression of C, an_Adj C holds variables_in ((non_op C) term a) = variables_in a proofend; theorem :: ABCMIZ_1:95 for C being initialized ConstructorSignature for a being expression of C, an_Adj C holds vars ((non_op C) term a) = vars a by Th94; theorem Th96: :: ABCMIZ_1:96 for S being ManySortedSign for o being set for t1, t2 being DecoratedTree holds S variables_in ([o, the carrier of S] -tree <*t1,t2*>) = (S variables_in t1) \/ (S variables_in t2) proofend; theorem Th97: :: ABCMIZ_1:97 for C being initialized ConstructorSignature for t being expression of C, a_Type C for a being expression of C, an_Adj C holds variables_in ((ast C) term (a,t)) = (variables_in a) \/ (variables_in t) proofend; theorem :: ABCMIZ_1:98 for C being initialized ConstructorSignature for t being expression of C, a_Type C for a being expression of C, an_Adj C holds vars ((ast C) term (a,t)) = (vars a) \/ (vars t) proofend; theorem Th99: :: ABCMIZ_1:99 for C being initialized ConstructorSignature for a being expression of C, an_Adj C holds variables_in (Non a) = variables_in a proofend; theorem :: ABCMIZ_1:100 for C being initialized ConstructorSignature for a being expression of C, an_Adj C holds vars (Non a) = vars a by Th99; definition let C be initialized ConstructorSignature; let T be quasi-type of C; func variables_in T -> Subset of Vars equals :: ABCMIZ_1:def 48 (union ((((MSVars C),(a_Term C)) variables_in) .: (adjs T))) \/ (variables_in (the_base_of T)); coherence (union ((((MSVars C),(a_Term C)) variables_in) .: (adjs T))) \/ (variables_in (the_base_of T)) is Subset of Vars proofend; end; :: deftheorem defines variables_in ABCMIZ_1:def_48_:_ for C being initialized ConstructorSignature for T being quasi-type of C holds variables_in T = (union ((((MSVars C),(a_Term C)) variables_in) .: (adjs T))) \/ (variables_in (the_base_of T)); registration let C be initialized ConstructorSignature; let T be quasi-type of C; cluster variables_in T -> finite ; coherence variables_in T is finite proofend; end; definition let C be initialized ConstructorSignature; let T be quasi-type of C; func vars T -> finite Subset of Vars equals :: ABCMIZ_1:def 49 varcl (variables_in T); coherence varcl (variables_in T) is finite Subset of Vars by Th24; end; :: deftheorem defines vars ABCMIZ_1:def_49_:_ for C being initialized ConstructorSignature for T being quasi-type of C holds vars T = varcl (variables_in T); theorem :: ABCMIZ_1:101 for C being initialized ConstructorSignature for T being quasi-type of C holds varcl (vars T) = vars T ; theorem Th102: :: ABCMIZ_1:102 for C being initialized ConstructorSignature for T being quasi-type of C for a being quasi-adjective of C holds variables_in (a ast T) = (variables_in a) \/ (variables_in T) proofend; theorem :: ABCMIZ_1:103 for C being initialized ConstructorSignature for T being quasi-type of C for a being quasi-adjective of C holds vars (a ast T) = (vars a) \/ (vars T) proofend; theorem Th104: :: ABCMIZ_1:104 for C being initialized ConstructorSignature for q being pure expression of C, a_Type C for A being finite Subset of (QuasiAdjs C) holds variables_in (A ast q) = (union { (variables_in a) where a is quasi-adjective of C : a in A } ) \/ (variables_in q) proofend; theorem :: ABCMIZ_1:105 for C being initialized ConstructorSignature for q being pure expression of C, a_Type C for A being finite Subset of (QuasiAdjs C) holds vars (A ast q) = (union { (vars a) where a is quasi-adjective of C : a in A } ) \/ (vars q) proofend; theorem Th106: :: ABCMIZ_1:106 for C being initialized ConstructorSignature for q being pure expression of C, a_Type C holds variables_in (({} (QuasiAdjs C)) ast q) = variables_in q proofend; theorem Th107: :: ABCMIZ_1:107 for C being initialized ConstructorSignature for e being expression of C holds ( e is ground iff variables_in e = {} ) proofend; definition let C be initialized ConstructorSignature; let T be quasi-type of C; attrT is ground means :Def50: :: ABCMIZ_1:def 50 variables_in T = {} ; end; :: deftheorem Def50 defines ground ABCMIZ_1:def_50_:_ for C being initialized ConstructorSignature for T being quasi-type of C holds ( T is ground iff variables_in T = {} ); registration let C be initialized ConstructorSignature; cluster non pair non empty Relation-like Function-like finite DecoratedTree-like ground pure for expression of C, a_Type C; existence ex b1 being expression of C, a_Type C st ( b1 is ground & b1 is pure ) proofend; cluster non pair non empty Relation-like Function-like finite DecoratedTree-like ground regular for expression of C, an_Adj C; existence ex b1 being quasi-adjective of C st b1 is ground proofend; end; theorem Th108: :: ABCMIZ_1:108 for C being initialized ConstructorSignature for t being ground pure expression of C, a_Type C holds ({} (QuasiAdjs C)) ast t is ground proofend; registration let C be initialized ConstructorSignature; let t be ground pure expression of C, a_Type C; clustert ast -> ground for quasi-type of C; coherence for b1 being quasi-type of C st b1 = ({} (QuasiAdjs C)) ast t holds b1 is ground by Th108; end; registration let C be initialized ConstructorSignature; cluster pair non empty ground for quasi-type of C; existence ex b1 being quasi-type of C st b1 is ground proofend; end; registration let C be initialized ConstructorSignature; let T be ground quasi-type of C; let a be ground quasi-adjective of C; clustera ast T -> ground ; coherence a ast T is ground proofend; end; begin :: Type widening is smooth iff :: vars-function is sup-semilattice homomorphism from widening sup-semilattice :: into VarPoset definition func VarPoset -> non empty strict Poset equals :: ABCMIZ_1:def 51 (InclPoset { (varcl A) where A is finite Subset of Vars : verum } ) opp ; coherence (InclPoset { (varcl A) where A is finite Subset of Vars : verum } ) opp is non empty strict Poset proofend; end; :: deftheorem defines VarPoset ABCMIZ_1:def_51_:_ VarPoset = (InclPoset { (varcl A) where A is finite Subset of Vars : verum } ) opp ; theorem Th109: :: ABCMIZ_1:109 for x, y being Element of VarPoset holds ( x <= y iff y c= x ) proofend; :: registration :: let V1,V2 be Element of VarPoset; :: identify V1 <= V2 with V2 c= V1; :: compatibility by Th22; :: end; theorem Th110: :: ABCMIZ_1:110 for x being set holds ( x is Element of VarPoset iff ( x is finite Subset of Vars & varcl x = x ) ) proofend; registration cluster VarPoset -> non empty strict with_suprema with_infima ; coherence ( VarPoset is with_infima & VarPoset is with_suprema ) proofend; end; theorem Th111: :: ABCMIZ_1:111 for V1, V2 being Element of VarPoset holds ( V1 "\/" V2 = V1 /\ V2 & V1 "/\" V2 = V1 \/ V2 ) proofend; registration let V1, V2 be Element of VarPoset; identifyV1 "\/" V2 with V1 /\ V2; compatibility V1 "\/" V2 = V1 /\ V2 by Th111; identifyV1 "/\" V2 with V1 \/ V2; compatibility V1 "/\" V2 = V1 \/ V2 by Th111; end; theorem Th112: :: ABCMIZ_1:112 for X being non empty Subset of VarPoset holds ( ex_sup_of X, VarPoset & sup X = meet X ) proofend; registration cluster VarPoset -> non empty strict up-complete ; coherence VarPoset is up-complete proofend; end; theorem :: ABCMIZ_1:113 Top VarPoset = {} proofend; definition let C be initialized ConstructorSignature; func vars-function C -> Function of (QuasiTypes C), the carrier of VarPoset means :: ABCMIZ_1:def 52 for T being quasi-type of C holds it . T = vars T; uniqueness for b1, b2 being Function of (QuasiTypes C), the carrier of VarPoset st ( for T being quasi-type of C holds b1 . T = vars T ) & ( for T being quasi-type of C holds b2 . T = vars T ) holds b1 = b2 proofend; existence ex b1 being Function of (QuasiTypes C), the carrier of VarPoset st for T being quasi-type of C holds b1 . T = vars T proofend; end; :: deftheorem defines vars-function ABCMIZ_1:def_52_:_ for C being initialized ConstructorSignature for b2 being Function of (QuasiTypes C), the carrier of VarPoset holds ( b2 = vars-function C iff for T being quasi-type of C holds b2 . T = vars T ); definition let L be non empty Poset; attrL is smooth means :: ABCMIZ_1:def 53 ex C being initialized ConstructorSignature ex f being Function of L,VarPoset st ( the carrier of L c= QuasiTypes C & f = (vars-function C) | the carrier of L & ( for x, y being Element of L holds f preserves_sup_of {x,y} ) ); end; :: deftheorem defines smooth ABCMIZ_1:def_53_:_ for L being non empty Poset holds ( L is smooth iff ex C being initialized ConstructorSignature ex f being Function of L,VarPoset st ( the carrier of L c= QuasiTypes C & f = (vars-function C) | the carrier of L & ( for x, y being Element of L holds f preserves_sup_of {x,y} ) ) ); registration let C be initialized ConstructorSignature; let T be ground quasi-type of C; cluster RelStr(# {T},(id {T}) #) -> smooth ; coherence RelStr(# {T},(id {T}) #) is smooth proofend; end; begin scheme :: ABCMIZ_1:sch 2 StructInd{ F1() -> initialized ConstructorSignature, P1[ set ], F2() -> expression of F1() } : P1[F2()] provided A1: for x being variable holds P1[x -term F1()] and A2: for c being constructor OperSymbol of F1() for p being FinSequence of QuasiTerms F1() st len p = len (the_arity_of c) & ( for t being quasi-term of F1() st t in rng p holds P1[t] ) holds P1[c -trm p] and A3: for a being expression of F1(), an_Adj F1() st P1[a] holds P1[(non_op F1()) term a] and A4: for a being expression of F1(), an_Adj F1() st P1[a] holds for t being expression of F1(), a_Type F1() st P1[t] holds P1[(ast F1()) term (a,t)] proofend; definition let S be ManySortedSign ; attrS is with_an_operation_for_each_sort means :Def54: :: ABCMIZ_1:def 54 the carrier of S c= rng the ResultSort of S; let X be ManySortedSet of the carrier of S; attrX is with_missing_variables means :Def55: :: ABCMIZ_1:def 55 X " {{}} c= rng the ResultSort of S; end; :: deftheorem Def54 defines with_an_operation_for_each_sort ABCMIZ_1:def_54_:_ for S being ManySortedSign holds ( S is with_an_operation_for_each_sort iff the carrier of S c= rng the ResultSort of S ); :: deftheorem Def55 defines with_missing_variables ABCMIZ_1:def_55_:_ for S being ManySortedSign for X being ManySortedSet of the carrier of S holds ( X is with_missing_variables iff X " {{}} c= rng the ResultSort of S ); theorem Th114: :: ABCMIZ_1:114 for S being non void Signature for X being ManySortedSet of the carrier of S holds ( X is with_missing_variables iff for s being SortSymbol of S st X . s = {} holds ex o being OperSymbol of S st the_result_sort_of o = s ) proofend; registration cluster MaxConstrSign -> strict with_an_operation_for_each_sort ; coherence MaxConstrSign is with_an_operation_for_each_sort proofend; let C be ConstructorSignature; cluster MSVars C -> with_missing_variables ; coherence MSVars C is with_missing_variables proofend; end; registration let S be ManySortedSign ; cluster Relation-like V8() the carrier of S -defined Function-like total -> with_missing_variables for set ; coherence for b1 being ManySortedSet of the carrier of S st b1 is V8() holds b1 is with_missing_variables proofend; end; registration let S be ManySortedSign ; cluster Relation-like the carrier of S -defined Function-like total with_missing_variables for set ; existence ex b1 being ManySortedSet of the carrier of S st b1 is with_missing_variables proofend; end; registration cluster non empty non void V58() strict V259() constructor initialized with_an_operation_for_each_sort for ManySortedSign ; existence ex b1 being ConstructorSignature st ( b1 is initialized & b1 is with_an_operation_for_each_sort & b1 is strict ) proofend; end; registration let C be with_an_operation_for_each_sort ManySortedSign ; cluster Relation-like the carrier of C -defined Function-like total -> with_missing_variables for set ; coherence for b1 being ManySortedSet of the carrier of C holds b1 is with_missing_variables proofend; end; definition let G be non empty DTConstrStr ; :: original:Terminals redefine func Terminals G -> Subset of G; coherence Terminals G is Subset of G proofend; :: original:NonTerminals redefine func NonTerminals G -> Subset of G; coherence NonTerminals G is Subset of G proofend; end; theorem Th115: :: ABCMIZ_1:115 for D1, D2 being non empty DTConstrStr st the Rules of D1 c= the Rules of D2 holds ( NonTerminals D1 c= NonTerminals D2 & the carrier of D1 /\ (Terminals D2) c= Terminals D1 & ( Terminals D1 c= Terminals D2 implies the carrier of D1 c= the carrier of D2 ) ) proofend; theorem Th116: :: ABCMIZ_1:116 for D1, D2 being non empty DTConstrStr st Terminals D1 c= Terminals D2 & the Rules of D1 c= the Rules of D2 holds TS D1 c= TS D2 proofend; theorem Th117: :: ABCMIZ_1:117 for S being ManySortedSign for X, Y being ManySortedSet of the carrier of S st X c= Y & X is with_missing_variables holds Y is with_missing_variables proofend; theorem Th118: :: ABCMIZ_1:118 for S being set for X, Y being ManySortedSet of S st X c= Y holds Union (coprod X) c= Union (coprod Y) proofend; theorem :: ABCMIZ_1:119 for S being non void Signature for X, Y being ManySortedSet of the carrier of S st X c= Y holds the carrier of (DTConMSA X) c= the carrier of (DTConMSA Y) by Th118, XBOOLE_1:9; theorem Th120: :: ABCMIZ_1:120 for S being non void Signature for X being ManySortedSet of the carrier of S st X is with_missing_variables holds ( NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConMSA X) = Union (coprod X) ) proofend; theorem :: ABCMIZ_1:121 for S being non void Signature for X, Y being ManySortedSet of the carrier of S st X c= Y & X is with_missing_variables holds ( Terminals (DTConMSA X) c= Terminals (DTConMSA Y) & the Rules of (DTConMSA X) c= the Rules of (DTConMSA Y) & TS (DTConMSA X) c= TS (DTConMSA Y) ) proofend; theorem Th122: :: ABCMIZ_1:122 for C being initialized ConstructorSignature for t being set holds ( t in Terminals (DTConMSA (MSVars C)) iff ex x being variable st t = [x,(a_Term C)] ) proofend; theorem Th123: :: ABCMIZ_1:123 for C being initialized ConstructorSignature for t being set holds ( t in NonTerminals (DTConMSA (MSVars C)) iff ( t = [(ast C), the carrier of C] or t = [(non_op C), the carrier of C] or ex c being constructor OperSymbol of C st t = [c, the carrier of C] ) ) proofend; theorem Th124: :: ABCMIZ_1:124 for S being non void Signature for X being with_missing_variables ManySortedSet of the carrier of S for t being set st t in Union the Sorts of (Free (S,X)) holds t is Term of S,(X \/ ( the carrier of S --> {0})) proofend; theorem :: ABCMIZ_1:125 for S being non void Signature for X being with_missing_variables ManySortedSet of the carrier of S for t being Term of S,(X \/ ( the carrier of S --> {0})) st t in Union the Sorts of (Free (S,X)) holds t in the Sorts of (Free (S,X)) . (the_sort_of t) proofend; theorem :: ABCMIZ_1:126 for G being non empty DTConstrStr for s being Element of G for p being FinSequence st s ==> p holds p is FinSequence of the carrier of G proofend; theorem Th127: :: ABCMIZ_1:127 for S being non void Signature for X, Y being ManySortedSet of the carrier of S for g1 being Symbol of (DTConMSA X) for g2 being Symbol of (DTConMSA Y) for p1 being FinSequence of the carrier of (DTConMSA X) for p2 being FinSequence of the carrier of (DTConMSA Y) st g1 = g2 & p1 = p2 & g1 ==> p1 holds g2 ==> p2 proofend; theorem Th128: :: ABCMIZ_1:128 for S being non void Signature for X being with_missing_variables ManySortedSet of the carrier of S holds Union the Sorts of (Free (S,X)) = TS (DTConMSA X) proofend; definition let S be non void Signature; let X be ManySortedSet of the carrier of S; mode term-transformation of S,X -> UnOp of (Union the Sorts of (Free (S,X))) means :Def56: :: ABCMIZ_1:def 56 for s being SortSymbol of S holds it .: ( the Sorts of (Free (S,X)) . s) c= the Sorts of (Free (S,X)) . s; existence ex b1 being UnOp of (Union the Sorts of (Free (S,X))) st for s being SortSymbol of S holds b1 .: ( the Sorts of (Free (S,X)) . s) c= the Sorts of (Free (S,X)) . s proofend; end; :: deftheorem Def56 defines term-transformation ABCMIZ_1:def_56_:_ for S being non void Signature for X being ManySortedSet of the carrier of S for b3 being UnOp of (Union the Sorts of (Free (S,X))) holds ( b3 is term-transformation of S,X iff for s being SortSymbol of S holds b3 .: ( the Sorts of (Free (S,X)) . s) c= the Sorts of (Free (S,X)) . s ); theorem Th129: :: ABCMIZ_1:129 for S being non void Signature for X being non empty ManySortedSet of the carrier of S for f being UnOp of (Union the Sorts of (Free (S,X))) holds ( f is term-transformation of S,X iff for s being SortSymbol of S for a being set st a in the Sorts of (Free (S,X)) . s holds f . a in the Sorts of (Free (S,X)) . s ) proofend; theorem Th130: :: ABCMIZ_1:130 for S being non void Signature for X being non empty ManySortedSet of the carrier of S for f being term-transformation of S,X for s being SortSymbol of S for p being FinSequence of the Sorts of (Free (S,X)) . s holds ( f * p is FinSequence of the Sorts of (Free (S,X)) . s & card (f * p) = len p ) proofend; definition let S be non void Signature; let X be ManySortedSet of the carrier of S; let t be term-transformation of S,X; attrt is substitution means :: ABCMIZ_1:def 57 for o being OperSymbol of S for p, q being FinSequence of (Free (S,X)) st [o, the carrier of S] -tree p in Union the Sorts of (Free (S,X)) & q = t * p holds t . ([o, the carrier of S] -tree p) = [o, the carrier of S] -tree q; end; :: deftheorem defines substitution ABCMIZ_1:def_57_:_ for S being non void Signature for X being ManySortedSet of the carrier of S for t being term-transformation of S,X holds ( t is substitution iff for o being OperSymbol of S for p, q being FinSequence of (Free (S,X)) st [o, the carrier of S] -tree p in Union the Sorts of (Free (S,X)) & q = t * p holds t . ([o, the carrier of S] -tree p) = [o, the carrier of S] -tree q ); scheme :: ABCMIZ_1:sch 3 StructDef{ F1() -> initialized ConstructorSignature, F2( set ) -> expression of F1(), F3( set ) -> expression of F1(), F4( set , set ) -> expression of F1(), F5( set , set ) -> expression of F1() } : ex f being term-transformation of F1(), MSVars F1() st ( ( for x being variable holds f . (x -term F1()) = F2(x) ) & ( for c being constructor OperSymbol of F1() for p, q being FinSequence of QuasiTerms F1() st len p = len (the_arity_of c) & q = f * p holds f . (c -trm p) = F4(c,q) ) & ( for a being expression of F1(), an_Adj F1() holds f . ((non_op F1()) term a) = F3((f . a)) ) & ( for a being expression of F1(), an_Adj F1() for t being expression of F1(), a_Type F1() holds f . ((ast F1()) term (a,t)) = F5((f . a),(f . t)) ) ) provided A1: for x being variable holds F2(x) is quasi-term of F1() and A2: for c being constructor OperSymbol of F1() for p being FinSequence of QuasiTerms F1() st len p = len (the_arity_of c) holds F4(c,p) is expression of F1(), the_result_sort_of c and A3: for a being expression of F1(), an_Adj F1() holds F3(a) is expression of F1(), an_Adj F1() and A4: for a being expression of F1(), an_Adj F1() for t being expression of F1(), a_Type F1() holds F5(a,t) is expression of F1(), a_Type F1() proofend; begin definition let A be set ; let x, y be set ; let a, b be Element of A; :: original:IFIN redefine func IFIN (x,y,a,b) -> Element of A; coherence IFIN (x,y,a,b) is Element of A by MATRIX_7:def_1; end; definition let C be initialized ConstructorSignature; mode valuation of C is PartFunc of Vars,(QuasiTerms C); end; definition let C be initialized ConstructorSignature; let f be valuation of C; attrf is irrelevant means :Def58: :: ABCMIZ_1:def 58 for x being variable st x in dom f holds ex y being variable st f . x = y -term C; end; :: deftheorem Def58 defines irrelevant ABCMIZ_1:def_58_:_ for C being initialized ConstructorSignature for f being valuation of C holds ( f is irrelevant iff for x being variable st x in dom f holds ex y being variable st f . x = y -term C ); notation let C be initialized ConstructorSignature; let f be valuation of C; antonym relevant f for irrelevant ; end; registration let C be initialized ConstructorSignature; cluster empty Function-like -> irrelevant for Element of bool [:Vars,(QuasiTerms C):]; coherence for b1 being valuation of C st b1 is empty holds b1 is irrelevant proofend; end; registration let C be initialized ConstructorSignature; cluster empty Relation-like Vars -defined QuasiTerms C -valued Function-like Function-yielding V115() for Element of bool [:Vars,(QuasiTerms C):]; existence ex b1 being valuation of C st b1 is empty proofend; end; definition let C be initialized ConstructorSignature; let X be Subset of Vars; funcC idval X -> valuation of C equals :: ABCMIZ_1:def 59 { [x,(x -term C)] where x is variable : x in X } ; coherence { [x,(x -term C)] where x is variable : x in X } is valuation of C proofend; end; :: deftheorem defines idval ABCMIZ_1:def_59_:_ for C being initialized ConstructorSignature for X being Subset of Vars holds C idval X = { [x,(x -term C)] where x is variable : x in X } ; theorem Th131: :: ABCMIZ_1:131 for C being initialized ConstructorSignature for X being Subset of Vars holds ( dom (C idval X) = X & ( for x being variable st x in X holds (C idval X) . x = x -term C ) ) proofend; registration let C be initialized ConstructorSignature; let X be Subset of Vars; clusterC idval X -> one-to-one irrelevant ; coherence ( C idval X is irrelevant & C idval X is one-to-one ) proofend; end; registration let C be initialized ConstructorSignature; let X be empty Subset of Vars; clusterC idval X -> empty ; coherence C idval X is empty proofend; end; definition let C be initialized ConstructorSignature; let f be valuation of C; funcf # -> term-transformation of C, MSVars C means :Def60: :: ABCMIZ_1:def 60 ( ( for x being variable holds ( ( x in dom f implies it . (x -term C) = f . x ) & ( not x in dom f implies it . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = it * p holds it . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds it . ((non_op C) term a) = (non_op C) term (it . a) ) & ( for a being expression of C, an_Adj C for t being expression of C, a_Type C holds it . ((ast C) term (a,t)) = (ast C) term ((it . a),(it . t)) ) ); existence ex b1 being term-transformation of C, MSVars C st ( ( for x being variable holds ( ( x in dom f implies b1 . (x -term C) = f . x ) & ( not x in dom f implies b1 . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b1 * p holds b1 . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b1 . ((non_op C) term a) = (non_op C) term (b1 . a) ) & ( for a being expression of C, an_Adj C for t being expression of C, a_Type C holds b1 . ((ast C) term (a,t)) = (ast C) term ((b1 . a),(b1 . t)) ) ) proofend; correctness uniqueness for b1, b2 being term-transformation of C, MSVars C st ( for x being variable holds ( ( x in dom f implies b1 . (x -term C) = f . x ) & ( not x in dom f implies b1 . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b1 * p holds b1 . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b1 . ((non_op C) term a) = (non_op C) term (b1 . a) ) & ( for a being expression of C, an_Adj C for t being expression of C, a_Type C holds b1 . ((ast C) term (a,t)) = (ast C) term ((b1 . a),(b1 . t)) ) & ( for x being variable holds ( ( x in dom f implies b2 . (x -term C) = f . x ) & ( not x in dom f implies b2 . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b2 * p holds b2 . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b2 . ((non_op C) term a) = (non_op C) term (b2 . a) ) & ( for a being expression of C, an_Adj C for t being expression of C, a_Type C holds b2 . ((ast C) term (a,t)) = (ast C) term ((b2 . a),(b2 . t)) ) holds b1 = b2; proofend; end; :: deftheorem Def60 defines # ABCMIZ_1:def_60_:_ for C being initialized ConstructorSignature for f being valuation of C for b3 being term-transformation of C, MSVars C holds ( b3 = f # iff ( ( for x being variable holds ( ( x in dom f implies b3 . (x -term C) = f . x ) & ( not x in dom f implies b3 . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b3 * p holds b3 . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b3 . ((non_op C) term a) = (non_op C) term (b3 . a) ) & ( for a being expression of C, an_Adj C for t being expression of C, a_Type C holds b3 . ((ast C) term (a,t)) = (ast C) term ((b3 . a),(b3 . t)) ) ) ); registration let C be initialized ConstructorSignature; let f be valuation of C; clusterf # -> substitution ; coherence f # is substitution proofend; end; definition let C be initialized ConstructorSignature; let f be valuation of C; let e be expression of C; funce at f -> expression of C equals :: ABCMIZ_1:def 61 (f #) . e; coherence (f #) . e is expression of C ; end; :: deftheorem defines at ABCMIZ_1:def_61_:_ for C being initialized ConstructorSignature for f being valuation of C for e being expression of C holds e at f = (f #) . e; definition let C be initialized ConstructorSignature; let f be valuation of C; let p be FinSequence; assume B1: rng p c= Union the Sorts of (Free (C,(MSVars C))) ; funcp at f -> FinSequence equals :Def62: :: ABCMIZ_1:def 62 (f #) * p; coherence (f #) * p is FinSequence proofend; end; :: deftheorem Def62 defines at ABCMIZ_1:def_62_:_ for C being initialized ConstructorSignature for f being valuation of C for p being FinSequence st rng p c= Union the Sorts of (Free (C,(MSVars C))) holds p at f = (f #) * p; definition let C be initialized ConstructorSignature; let f be valuation of C; let p be FinSequence of QuasiTerms C; :: original:at redefine funcp at f -> FinSequence of QuasiTerms C equals :: ABCMIZ_1:def 63 (f #) * p; coherence p at f is FinSequence of QuasiTerms C proofend; compatibility for b1 being FinSequence of QuasiTerms C holds ( b1 = p at f iff b1 = (f #) * p ) proofend; end; :: deftheorem defines at ABCMIZ_1:def_63_:_ for C being initialized ConstructorSignature for f being valuation of C for p being FinSequence of QuasiTerms C holds p at f = (f #) * p; theorem :: ABCMIZ_1:132 for C being initialized ConstructorSignature for f being valuation of C for x being variable st not x in dom f holds (x -term C) at f = x -term C by Def60; theorem :: ABCMIZ_1:133 for C being initialized ConstructorSignature for f being valuation of C for x being variable st x in dom f holds (x -term C) at f = f . x by Def60; theorem :: ABCMIZ_1:134 for C being initialized ConstructorSignature for c being constructor OperSymbol of C for p being FinSequence of QuasiTerms C for f being valuation of C st len p = len (the_arity_of c) holds (c -trm p) at f = c -trm (p at f) by Def60; theorem :: ABCMIZ_1:135 for C being initialized ConstructorSignature for a being expression of C, an_Adj C for f being valuation of C holds ((non_op C) term a) at f = (non_op C) term (a at f) by Def60; theorem :: ABCMIZ_1:136 for C being initialized ConstructorSignature for t being expression of C, a_Type C for a being expression of C, an_Adj C for f being valuation of C holds ((ast C) term (a,t)) at f = (ast C) term ((a at f),(t at f)) by Def60; theorem Th137: :: ABCMIZ_1:137 for C being initialized ConstructorSignature for e being expression of C for X being Subset of Vars holds e at (C idval X) = e proofend; theorem :: ABCMIZ_1:138 for C being initialized ConstructorSignature for X being Subset of Vars holds (C idval X) # = id (Union the Sorts of (Free (C,(MSVars C)))) proofend; theorem Th139: :: ABCMIZ_1:139 for C being initialized ConstructorSignature for e being expression of C for f being empty valuation of C holds e at f = e proofend; theorem :: ABCMIZ_1:140 for C being initialized ConstructorSignature for f being empty valuation of C holds f # = id (Union the Sorts of (Free (C,(MSVars C)))) proofend; :: theorem :: for t being expression of C :: for f1,f2 being valuation of C :: holds (t at f1) at f2 = ((f2# )*(f1# )).t by FUNCT_2:21; definition let C be initialized ConstructorSignature; let f be valuation of C; let t be quasi-term of C; :: original:at redefine funct at f -> quasi-term of C; coherence t at f is quasi-term of C proofend; end; definition let C be initialized ConstructorSignature; let f be valuation of C; let a be expression of C, an_Adj C; :: original:at redefine funca at f -> expression of C, an_Adj C; coherence a at f is expression of C, an_Adj C proofend; end; registration let C be initialized ConstructorSignature; let f be valuation of C; let a be positive expression of C, an_Adj C; clustera at f -> positive for expression of C, an_Adj C; coherence for b1 being expression of C, an_Adj C st b1 = a at f holds b1 is positive proofend; end; registration let C be initialized ConstructorSignature; let f be valuation of C; let a be negative expression of C, an_Adj C; clustera at f -> negative for expression of C, an_Adj C; coherence for b1 being expression of C, an_Adj C st b1 = a at f holds b1 is negative proofend; end; definition let C be initialized ConstructorSignature; let f be valuation of C; let a be quasi-adjective of C; :: original:at redefine funca at f -> quasi-adjective of C; coherence a at f is quasi-adjective of C proofend; end; theorem :: ABCMIZ_1:141 for C being initialized ConstructorSignature for a being expression of C, an_Adj C for f being valuation of C holds (Non a) at f = Non (a at f) proofend; definition let C be initialized ConstructorSignature; let f be valuation of C; let t be expression of C, a_Type C; :: original:at redefine funct at f -> expression of C, a_Type C; coherence t at f is expression of C, a_Type C proofend; end; registration let C be initialized ConstructorSignature; let f be valuation of C; let t be pure expression of C, a_Type C; clustert at f -> pure for expression of C, a_Type C; coherence for b1 being expression of C, a_Type C st b1 = t at f holds b1 is pure proofend; end; theorem :: ABCMIZ_1:142 for C being initialized ConstructorSignature for f being one-to-one irrelevant valuation of C ex g being one-to-one irrelevant valuation of C st for x, y being variable holds ( x in dom f & f . x = y -term C iff ( y in dom g & g . y = x -term C ) ) proofend; theorem :: ABCMIZ_1:143 for C being initialized ConstructorSignature for f, g being one-to-one irrelevant valuation of C st ( for x, y being variable st x in dom f & f . x = y -term C holds ( y in dom g & g . y = x -term C ) ) holds for e being expression of C st variables_in e c= dom f holds (e at f) at g = e proofend; definition let C be initialized ConstructorSignature; let f be valuation of C; let A be Subset of (QuasiAdjs C); funcA at f -> Subset of (QuasiAdjs C) equals :: ABCMIZ_1:def 64 { (a at f) where a is quasi-adjective of C : a in A } ; coherence { (a at f) where a is quasi-adjective of C : a in A } is Subset of (QuasiAdjs C) proofend; end; :: deftheorem defines at ABCMIZ_1:def_64_:_ for C being initialized ConstructorSignature for f being valuation of C for A being Subset of (QuasiAdjs C) holds A at f = { (a at f) where a is quasi-adjective of C : a in A } ; theorem Th144: :: ABCMIZ_1:144 for C being initialized ConstructorSignature for f being valuation of C for A being Subset of (QuasiAdjs C) for a being quasi-adjective of C st A = {a} holds A at f = {(a at f)} proofend; theorem Th145: :: ABCMIZ_1:145 for C being initialized ConstructorSignature for f being valuation of C for A, B being Subset of (QuasiAdjs C) holds (A \/ B) at f = (A at f) \/ (B at f) proofend; theorem :: ABCMIZ_1:146 for C being initialized ConstructorSignature for f being valuation of C for A, B being Subset of (QuasiAdjs C) st A c= B holds A at f c= B at f proofend; registration let C be initialized ConstructorSignature; let f be valuation of C; let A be finite Subset of (QuasiAdjs C); clusterA at f -> finite ; coherence A at f is finite proofend; end; definition let C be initialized ConstructorSignature; let f be valuation of C; let T be quasi-type of C; funcT at f -> quasi-type of C equals :: ABCMIZ_1:def 65 ((adjs T) at f) ast ((the_base_of T) at f); coherence ((adjs T) at f) ast ((the_base_of T) at f) is quasi-type of C ; end; :: deftheorem defines at ABCMIZ_1:def_65_:_ for C being initialized ConstructorSignature for f being valuation of C for T being quasi-type of C holds T at f = ((adjs T) at f) ast ((the_base_of T) at f); theorem :: ABCMIZ_1:147 for C being initialized ConstructorSignature for f being valuation of C for T being quasi-type of C holds ( adjs (T at f) = (adjs T) at f & the_base_of (T at f) = (the_base_of T) at f ) by MCART_1:7; theorem :: ABCMIZ_1:148 for C being initialized ConstructorSignature for f being valuation of C for T being quasi-type of C for a being quasi-adjective of C holds (a ast T) at f = (a at f) ast (T at f) proofend; definition let C be initialized ConstructorSignature; let f, g be valuation of C; funcf at g -> valuation of C means :Def66: :: ABCMIZ_1:def 66 ( dom it = (dom f) \/ (dom g) & ( for x being variable st x in dom it holds it . x = ((x -term C) at f) at g ) ); existence ex b1 being valuation of C st ( dom b1 = (dom f) \/ (dom g) & ( for x being variable st x in dom b1 holds b1 . x = ((x -term C) at f) at g ) ) proofend; uniqueness for b1, b2 being valuation of C st dom b1 = (dom f) \/ (dom g) & ( for x being variable st x in dom b1 holds b1 . x = ((x -term C) at f) at g ) & dom b2 = (dom f) \/ (dom g) & ( for x being variable st x in dom b2 holds b2 . x = ((x -term C) at f) at g ) holds b1 = b2 proofend; end; :: deftheorem Def66 defines at ABCMIZ_1:def_66_:_ for C being initialized ConstructorSignature for f, g, b4 being valuation of C holds ( b4 = f at g iff ( dom b4 = (dom f) \/ (dom g) & ( for x being variable st x in dom b4 holds b4 . x = ((x -term C) at f) at g ) ) ); registration let C be initialized ConstructorSignature; let f, g be irrelevant valuation of C; clusterf at g -> irrelevant ; coherence f at g is irrelevant proofend; end; theorem Th149: :: ABCMIZ_1:149 for C being initialized ConstructorSignature for e being expression of C for f1, f2 being valuation of C holds (e at f1) at f2 = e at (f1 at f2) proofend; theorem Th150: :: ABCMIZ_1:150 for C being initialized ConstructorSignature for A being Subset of (QuasiAdjs C) for f1, f2 being valuation of C holds (A at f1) at f2 = A at (f1 at f2) proofend; theorem :: ABCMIZ_1:151 for C being initialized ConstructorSignature for T being quasi-type of C for f1, f2 being valuation of C holds (T at f1) at f2 = T at (f1 at f2) proofend;