:: Towards the construction of a model of Mizar concepts :: by Grzegorz Bancerek :: :: Received April 21, 2008 :: Copyright (c) 2008 Association of Mizar Users environ vocabularies TARSKI, QC_LANG3, PBOOLE, MSUALG_1, CATALG_1, FINSEQ_1, BINOP_1, BOOLE, CQC_LANG, FINSET_1, FUNCOP_1, CAT_4, UNIALG_2, DTCONSTR, TDGROUP, FUNCT_1, MATRIX_1, TREES_4, TREES_2, SETFAM_1, SQUARE_1, ORDINAL2, COMPLEX1, LATTICES, CLASSES1, RELAT_1, AMI_1, MCART_1, MSUALG_2, MSUALG_3, MATRIX_7, FREEALG, MSAFREE, ZF_REFLE, MSATERM, PROB_1, ORDERS_1, QUANTAL1, FINSEQ_4, ORDINAL1, WAYBEL_0, ASYMPT_0, ZF_MODEL, OPPCAT_1, LATTICE3, CARD_5, AOFA_000, FINSEQ_2, CARD_1, PARTFUN1, FUNCT_4, QC_LANG1, FUNCT_2, ZF_LANG, LANG1, ARYTM, CAT_3, TREES_3, FACIRC_1, YELLOW_0, YELLOW_1, ABCMIZ_0, ABCMIZ_1, FUNCT_7; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, SETFAM_1, RELAT_1, FUNCT_1, RELSET_1, BINOP_1, FINSUB_1, PARTFUN1, PROB_2, FACIRC_1, ENUMSET1, FUNCT_2, FUNCT_4, CAT_3, FUNCOP_1, ARYTM_0, XCMPLX_0, XXREAL_0, ORDINAL2, NAT_1, MEMBERED, MCART_1, FINSET_1, CARD_1, NUMBERS, CARD_3, FINSEQ_1, FINSEQ_2, FINSOP_1, FINSEQ_4, TREES_1, TREES_2, TREES_3, TREES_4, FUNCT_7, PROB_1, PBOOLE, MATRIX_7, STRUCT_0, LANG1, ORDINAL1, CLASSES1, CLASSES2, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_7, DTCONSTR, MSUALG_1, MSUALG_2, PRE_CIRC, MSAFREE, EQUATION, MSATERM, CATALG_1, MSAFREE3, AOFA_000; constructors XBOOLE_0, SUBSET_1, ARYTM_0, XREAL_0, REAL_1, XXREAL_0, CARD_1, RELAT_1, FUNCT_1, NAT_1, DOMAIN_1, WELLORD2, MATRIX_7, STRUCT_0, MSUALG_1, ZF_REFLE, MATRIX_2, PBOOLE, MSAFREE, MSAFREE1, CAT_3, FINSET_1, PROB_1, MCART_1, COMMACAT, FINSEQOP, FINSOP_1, FUNCT_6, FUNCT_7, LANG1, TREES_9, PRE_CIRC, EQUATION, YELLOW_1, FINSEQ_2, FINSEQ_4, ENUMSET1, MSUALG_2, MSUALG_3, MSUALG_4, RECDEF_1, DTCONSTR, MSATERM, MSUALG_6, CATALG_1, LATTICE3, WAYBEL_0, WELLORD1, FACIRC_1, CLASSES1, MSAFREE3, ZFMISC_1, TREES_3; registrations XBOOLE_0, SUBSET_1, XREAL_0, ORDINAL1, ORDINAL2, RELSET_1, FUNCT_1, FINSET_1, STRUCT_0, PBOOLE, MSUALG_1, MSUALG_2, MSUALG_3, FINSEQ_1, TREES_9, CLASSES2, PARTFUN2, FILTER_0, FINSEQ_5, PRALG_1, NAT_1, CARD_1, MSAFREE, CANTOR_1, TREES_3, MSAFREE1, PARTFUN1, MSATERM, ORDERS_2, TREES_2, DTCONSTR, WAYBEL_0, YELLOW_0, YELLOW_1, LATTICE3, MEMBERED, RELAT_1, INDEX_1, PUA2MSS1, INSTALG1, CATALG_1, MSAFREE3, FACIRC_1, EQUATION, MSUALG_6, MSUALG_9, PRE_CIRC, WAYBEL_8; requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL; definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, FACIRC_1, FINSEQ_1, FINSEQ_2, LANG1, LATTICE3, MSAFREE, MSAFREE3, CARD_3, PBOOLE, TREES_3, MSUALG_1, MSUALG_2, CATALG_1, WAYBEL_0; theorems TARSKI, XBOOLE_0, XBOOLE_1, TREES_1, PRE_CIRC, XXREAL_0, ZFMISC_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, SUBSET_1, ENUMSET1, FUNCT_4, PROB_2, LANG1, MATRIX_7, NAT_1, MCART_1, PBOOLE, FINSET_1, RELAT_1, RELSET_1, STRUCT_0, ORDINAL3, CARD_1, CARD_3, CARD_5, CLASSES1, ORDINAL1, SETFAM_1, MSUALG_1, MSUALG_2, TREES_3, TREES_4, FINSEQ_3, FUNCOP_1, MSAFREE, MSATERM, MSAFREE3, BAGORDER, PARTFUN1, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_7, DTCONSTR, MSAFREE1, FUNCT_7, GRFUNC_1, CARD_2; schemes XBOOLE_0, FUNCT_1, NAT_1, FRAENKEL, WELLORD2, PBOOLE, MSATERM, DTCONSTR, CLASSES1, FUNCT_2; begin :: Variables reserve i for Nat, j for Element of NAT, X,Y,x,y,z for set; theorem ThF0: for f being Function holds f.x c= Union f proof let f be Function; x in dom f or not x in dom f; then f.x in rng f or f.x = {} by FUNCT_1:def 4,12; hence thesis by XBOOLE_1:2,ZFMISC_1:92; end; theorem for f being Function st Union f = {} holds f.x = {} by ThF0,XBOOLE_1:3; theorem Th89: for f being Function for x,y being set st f = [x,y] holds x = y proof let f be Function, x,y be set; assume f = [x,y]; then A6: {x} in f & {x,y} in f by TARSKI:def 2; then consider a,b being set such that A2: {x} = [a,b] by RELAT_1:def 1; A5: {a} = {a,b} & x = {a} by A2,ZFMISC_1:8,9; consider c,d being set such that A4: {x,y} = [c,d] by A6,RELAT_1:def 1; A7: x = {c} & y = {c,d} or x = {c,d} & y = {c} by A4,ZFMISC_1:10; then c = a by A5,ZFMISC_1:8; hence thesis by A7,A5,A6,A2,A4,FUNCT_1:def 1; end; theorem Lem'id: (id X).:Y c= Y proof let x be set; assume x in (id X).:Y; then ex y being set st [y,x] in id X & y in Y by RELAT_1:def 13; hence thesis by RELAT_1:def 10; end; theorem Th90: for S being non void Signature for X being non-empty ManySortedSet of the carrier of S for t being Term of S, X holds t is non pair proof let S be non void Signature; let X be non-empty ManySortedSet of the carrier of S; let t be Term of S, X; given x,y being set such that A1: t = [x,y]; (ex s being SortSymbol of S, v being Element of X.s st t.{} = [v,s]) or t.{} in [:the OperSymbols of S,{the carrier of S}:] by MSATERM:2; then (ex s being SortSymbol of S, v being Element of X.s st t.{} = [v,s]) or ex a,b being set st a in the OperSymbols of S & b in {the carrier of S} & t.{} = [a,b] by ZFMISC_1:def 2; then {{}} <> {{}, t.{}} by ZFMISC_1:9; then A4: [{}, t.{}] <> {x} by ZFMISC_1:9; {} in dom t by TREES_1:47; then [{}, t.{}] in t by FUNCT_1:def 4; then [{}, t.{}] = {x,y} & x = y by A1,A4,Th89,TARSKI:def 2; hence thesis by A4,ENUMSET1:69; end; registration let S be non void Signature; let X be non empty-yielding ManySortedSet of the carrier of S; cluster -> non pair Element of Free(S,X); coherence proof let e be Element of Free(S,X); e is Term of S, X \/ ((the carrier of S) --> {0}) by MSAFREE3:9; hence thesis by Th90; end; end; theorem Th1A: for x,y,z being set st x in {z}* & y in {z}* & Card x = Card y holds x = y proof let x,y,z be set such that A1: x in {z}* & y in {z}* and A2: Card x = Card y; reconsider x, y as FinSequence of {z} by A1,FINSEQ_1:def 11; A3: dom x = Seg len x by FINSEQ_1:def 3 .= dom y by A2,FINSEQ_1:def 3; now let i be Nat; assume i in dom x; then A4: x .i in rng x & y.i in rng y & rng x c= {z} & rng y c= {z} by A3,FUNCT_1:def 5; hence x .i = z by TARSKI:def 1 .= y.i by A4,TARSKI:def 1; end; hence thesis by A3,FINSEQ_1:17; end; registration cluster {} -> DTree-yielding; coherence by TREES_3:23; end; 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 non empty-yielding ManySortedSet of S; cluster -> DTree-yielding FinSequence of Free(S,X); coherence proof let p be FinSequence of Free(S,X); let x be set; assume x in rng p; then x is Element of Free(S,X); hence thesis; end; end; theorem LemExp: for S being non void Signature for X being non empty-yielding ManySortedSet of the carrier of S for t being Element of Free(S,X) holds (ex s being SortSymbol of S, v being set st t = root-tree [v,s] & v in X.s) or ex o being OperSymbol of S, 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})) proof let S be non void Signature; let X be non empty-yielding ManySortedSet of the carrier of S; let t be Element of Free(S,X); set V = X\/((the carrier of S)-->{0}); reconsider t' = t as Term of S,V by MSAFREE3:9; defpred P[set] means $1 is Element of Free(S,X) implies (ex s being SortSymbol of S, v being set st $1 = root-tree [v,s] & v in X.s) or ex o being OperSymbol of S, p being FinSequence of Free(S,X) st $1 = [o,the carrier of S]-tree p & len p = len the_arity_of o & p is DTree-yielding & p is ArgumentSeq of Sym(o,V); A1: for s being SortSymbol of S, v being Element of V.s holds P[root-tree [v,s]] proof let s be SortSymbol of S; let v be Element of V.s; set t = root-tree [v,s]; assume B1: t is Element of Free(S,X); {} in dom t by TREES_1:47; then t.{} in rng t by FUNCT_1:12; then [v,s] in rng t by TREES_4:3; then v in X.s by B1,MSAFREE3:36; hence thesis; end; A2: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,V) st for t being Term of S,V st t in rng p holds P[t] holds P[[o,the carrier of S]-tree p] proof let o be OperSymbol of S; let p be ArgumentSeq of Sym(o,V) such that for t being Term of S,V st t in rng p holds P[t]; set t = [o,the carrier of S]-tree p; assume t is Element of Free(S,X); then consider s being set such that B4: s in dom the Sorts of Free(S,X) & t in (the Sorts of Free(S,X)).s by CARD_5:10; reconsider s as Element of S by B4,PBOOLE:def 3; B5: t = Sym(o,V)-tree p & the Sorts of Free(S,X) = S-Terms(X,V) & the_sort_of(Sym(o,V)-tree p) = the_result_sort_of o by MSATERM:20,MSAFREE3:25; then s = the_result_sort_of o by B4,MSAFREE3:18; then rng p c= Union (S-Terms(X,V)) by B4,B5,MSAFREE3:20; then p is FinSequence of Free(S,X) & len the_arity_of o = len p by B5,FINSEQ_1:def 4,MSATERM:22; hence thesis; end; for t being Term of S,V holds P[t] from MSATERM:sch 1(A1,A2); then P[t']; hence (ex s being SortSymbol of S, v being set st t = root-tree [v,s] & v in X.s) or ex o being OperSymbol of S, 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,V); end; definition let A be set; func varcl A means: VARCL: A c= it & (for x,y st [x,y] in it holds x c= it) & for B being set st A c= B & for x,y st [x,y] in B holds x c= B holds it c= B; uniqueness proof let B1, B2 be set; assume A1: not thesis; then B1 c= B2 & B2 c= B1; hence thesis by A1,XBOOLE_0:def 10; end; existence proof set F = {C where C is Subset of Rank the_rank_of A: A c= C & for x,y st [x,y] in C holds x c= C}; take D = meet F; A1: A c= Rank the_rank_of A by CLASSES1:def 8; A3: now let x,y; assume [x,y] in Rank the_rank_of A; then {x} in {{x,y},{x}} & {{x,y},{x}} c= Rank the_rank_of A by TARSKI:def 2,ORDINAL1:def 2;then x in {x} & {x} c= Rank the_rank_of A by TARSKI:def 1,ORDINAL1:def 2; hence x c= Rank the_rank_of A by ORDINAL1:def 2; end; Rank the_rank_of A c= Rank the_rank_of A; then A4: Rank the_rank_of A in F by A1,A3; hereby let x; assume A5: x in A; now let C be set; assume C in F; then ex B being Subset of Rank the_rank_of A st C = B & A c= B & for x,y st [x,y] in B holds x c= B; hence x in C by A5; end; hence x in D by A4,SETFAM_1:def 1; end; hereby let x,y; assume A6: [x,y] in D; thus x c= D proof let z; assume A7: z in x; now let X; assume X in F; then [x,y] in X & ex B being Subset of Rank the_rank_of A st X = B & A c= B & for x,y st [x,y] in B holds x c= B by A6,SETFAM_1:def 1; then x c= X; hence z in X by A7; end; hence z in D by A4,SETFAM_1:def 1; end; end; let B being set; assume A8: A c= B & for x,y st [x,y] in B holds x c= B; set C = B /\ Rank the_rank_of A; reconsider C as Subset of Rank the_rank_of A by XBOOLE_1:17; A9: A c= C by A1,A8,XBOOLE_1:19; now let x,y; assume [x,y] in C; then [x,y] in B & [x,y] in Rank the_rank_of A by XBOOLE_0:def 3; then x c= B & x c= Rank the_rank_of A by A3,A8; hence x c= C by XBOOLE_1:19; end; then C in F by A9; then D c= C & C c= B by SETFAM_1:4,XBOOLE_1:17; hence D c= B by XBOOLE_1:1; end; projectivity; end; theorem Th11: varcl {} = {} proof {} c= {} & (for x,y st [x,y] in {} holds x c= {}) & for B being set st {} c= B & for x,y st [x,y] in B holds x c= B holds {} c= B; hence thesis by VARCL; end; theorem Th13: for A,B being set st A c= B holds varcl A c= varcl B proof let A, B be set such that A1: A c= B; B c= varcl B by VARCL; then A c= varcl B & (for x,y st [x,y] in varcl B holds x c= varcl B) by A1,VARCL,XBOOLE_1:1; hence thesis by VARCL; end; theorem Th14: for A being set holds varcl union A = union {varcl a where a is Element of A: not contradiction} proof let A be set; set X = {varcl a where a is Element of A: not contradiction}; A0: union A c= union X proof let x; assume x in union A; then consider Y such that A3: x in Y & Y in A by TARSKI:def 4; reconsider Y as Element of A by A3; Y c= varcl Y by VARCL; then varcl Y in X & x in varcl Y by A3; hence thesis by TARSKI:def 4; end; now let x,y be set; assume [x,y] in union X; then consider Y being set such that A1: [x,y] in Y & Y in X by TARSKI:def 4; consider a being Element of A such that A2: Y = varcl a by A1; x c= Y & Y c= union X by A1,A2,VARCL,ZFMISC_1:92; hence x c= union X by XBOOLE_1:1; end; hence varcl union A c= union X by A0,VARCL; let x; assume x in union X; then consider Y being set such that A4: x in Y & Y in X by TARSKI:def 4; consider a being Element of A such that A5: Y = varcl a by A4; A is empty or A is not empty; then a in A or a is empty by SUBSET_1:def 2; then a c= union A by XBOOLE_1:2,ZFMISC_1:92; then Y c= varcl union A by A5,Th13; hence thesis by A4; end; scheme Sch14{A() -> set, F(set) -> set, P[set]}: varcl union {F(z) where z is Element of A(): P[z]} = union {varcl F(z) where z is Element of A(): P[z]} proof set Z = {F(z) where z is Element of A(): P[z]}; set X = {varcl F(z) where z is Element of A(): P[z]}; A0: union Z c= union X proof let x; assume x in union Z; then consider Y such that A3: x in Y & Y in Z by TARSKI:def 4; consider z being Element of A() such that A4: Y = F(z) & P[z] by A3; Y c= varcl Y by VARCL; then varcl Y in X & x in varcl Y by A3,A4; hence thesis by TARSKI:def 4; end; now let x,y be set; assume [x,y] in union X; then consider Y being set such that A1: [x,y] in Y & Y in X by TARSKI:def 4; consider z being Element of A() such that A2: Y = varcl F(z) & P[z] by A1; x c= Y & Y c= union X by A1,A2,VARCL,ZFMISC_1:92; hence x c= union X by XBOOLE_1:1; end; hence varcl union Z c= union X by A0,VARCL; let x; assume x in union X; then consider Y being set such that A4: x in Y & Y in X by TARSKI:def 4; consider z being Element of A() such that A5: Y = varcl F(z) & P[z] by A4; F(z) in Z by A5; then Y c= varcl union Z by A5,Th13,ZFMISC_1:92; hence thesis by A4; end; theorem Th10: varcl (X \/ Y) = (varcl X) \/ (varcl Y) proof set A = {varcl a where a is Element of {X,Y}: not contradiction}; X \/ Y = union {X,Y} by ZFMISC_1:93; then A1: varcl (X \/ Y) = union A by Th14; A = {varcl X, varcl Y} proof thus now let x; assume x in A; then consider a being Element of {X,Y} such that A2: x = varcl a; a = X or a = Y by TARSKI:def 2; hence x in {varcl X, varcl Y} by A2,TARSKI:def 2; end; let x; assume x in {varcl X, varcl Y}; then x = varcl X & X in {X,Y} or x = varcl Y & Y in {X,Y} by TARSKI:def 2; hence x in A; end; hence thesis by A1,ZFMISC_1:93; end; theorem Th8: for A being non empty set st for a being Element of A holds varcl a = a holds varcl meet A = meet A proof let B be non empty set; set A = meet B; assume A1: for a being Element of B holds varcl a = a; now thus A c= A; let x,y; assume A2: [x,y] in A; now let Y; assume Y in B; then [x,y] in Y & Y = varcl Y by A1,A2,SETFAM_1:def 1; hence x c= Y by VARCL; end; hence x c= A by SETFAM_1:6; end; hence varcl A c= A by VARCL; thus thesis by VARCL; end; theorem Th9: varcl ((varcl X) /\ (varcl Y)) = (varcl X) /\ (varcl Y) proof set A = (varcl X) /\ (varcl Y); now thus A c= A; let x,y; assume [x,y] in A; then [x,y] in varcl X & [x,y] in varcl Y by XBOOLE_0:def 3; then x c= varcl X & x c= varcl Y by VARCL; hence x c= A by XBOOLE_1:19; end; hence varcl ((varcl X) /\ (varcl Y)) c= (varcl X) /\ (varcl Y) by VARCL; thus thesis by VARCL; end; registration let A be empty set; cluster varcl A -> empty; coherence by Th11; end; deffunc F(set,set) = {[varcl A, j] where A is Subset of $2, j is Element of NAT: A is finite}; definition func Vars means: VARSdef: ex V being ManySortedSet of NAT st it = Union V & V.0 = {[{}, i] where i is Element of NAT: not contradiction} & 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 proof consider f being Function such that A1: dom f = NAT and A2: f.0 = {[{}, i] where i is Element of NAT: not contradiction} and A3: for n being Nat holds f.(n+1) = F(n,f.n) from NAT_1:sch 11; reconsider f as ManySortedSet of NAT by A1,PBOOLE:def 3; take Union f, V = f; thus Union f = Union V; thus V.0 = {[{}, i] where i is Element of NAT: not contradiction} by A2; let n be Nat; thus thesis by A3; end; uniqueness proof let A1, A2 be set; given V1 being ManySortedSet of NAT such that A1: A1 = Union V1 and A2: V1.0 = {[{}, i] where i is Element of NAT: not contradiction} and A3: for n being Nat holds V1.(n+1) = F(n,V1.n); given V2 being ManySortedSet of NAT such that B1: A2 = Union V2 and B2: V2.0 = {[{}, i] where i is Element of NAT: not contradiction} and B3: for n being Nat holds V2.(n+1) = F(n,V2.n); C1: dom V1 = NAT by PBOOLE:def 3; C2: dom V2 = NAT by PBOOLE:def 3; V1 = V2 from NAT_1:sch 15(C1,A2,A3,C2,B2,B3); hence thesis by A1,B1; end; end; theorem Lem1: for V being ManySortedSet of NAT st V.0 = {[{}, i] where i is Element of NAT: not contradiction} & 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} for i,j being Element of NAT st i <= j holds V.i c= V.j proof let V be ManySortedSet of NAT such that A1: V.0 = {[{}, i] where i is Element of NAT: not contradiction} and A2: 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}; defpred Q[Nat] means V.0 c= V.$1; B2: now let j; assume Q[j]; B3: V.(j+1) = {[varcl A, k] where A is Subset of V.j, k is Element of NAT: A is finite} by A2; thus Q[j+1] proof let x; assume x in V.0; then (ex i being Element of NAT st x = [{}, i]) & {} c= V.j by A1,XBOOLE_1:2; hence thesis by B3,Th11; end; end; defpred P[Nat] means for i st i <= $1 holds V.i c= V.$1; A4: P[ 0 ] by NAT_1:3; A5: now let j; assume B4: P[j]; B5: V.j c= V.(j+1) proof per cases by NAT_1:6; suppose j = 0; hence thesis by B2; end; suppose ex k being Nat st j = k+1; then consider k being Nat such that B6: j = k+1; reconsider k as Element of NAT by ORDINAL1:def 13; B7: V.j = {[varcl A, n] where A is Subset of V.k, n is Element of NAT: A is finite} by A2,B6; B8: V.(j+1) = {[varcl A, n] where A is Subset of V.j,n is Element of NAT: A is finite} by A2; B9: V.k c= V.j by B4,B6,NAT_1:11; let x; assume x in V.j; then consider A being Subset of V.k, n being Element of NAT such that C1: x = [varcl A, n] & A is finite by B7; A c= V.j by B9,XBOOLE_1:1; hence thesis by B8,C1; end; end; thus P[j+1] proof let i; assume i <= j+1; then i = j+1 or V.i c= V.j by B4,NAT_1:8; hence V.i c= V.(j+1) by B5,XBOOLE_1:1; end; end; for j holds P[j] from NAT_1:sch 1(A4,A5); hence thesis; end; theorem Lem2: for V being ManySortedSet of NAT st V.0 = {[{}, i] where i is Element of NAT: not contradiction} & 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} for A being finite Subset of Vars ex i being Element of NAT st A c= V.i proof let V be ManySortedSet of NAT such that A1: V.0 = {[{}, i] where i is Element of NAT: not contradiction} and A2: 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}; let A be finite Subset of Vars; A3: Vars = Union V by A1,A2,VARSdef; defpred P[set,set] means $1 in V.$2; A4: now let x; assume x in A; then consider Y such that A5: x in Y & Y in rng V by A3,TARSKI:def 4; consider i being set such that A6: i in dom V & Y = V.i by A5,FUNCT_1:def 5; take i; thus i in NAT & P[x,i] by A5,A6,PBOOLE:def 3; end; consider f being Function such that A8: dom f = A & rng f c= NAT and A9: for x st x in A holds P[x,f.x] from WELLORD2:sch 1(A4); per cases; suppose A = {}; then A c= V.0 by XBOOLE_1:2; hence thesis; end; suppose A <> {}; then reconsider B = rng f as finite non empty Subset of NAT by A8,FINSET_1:26,RELAT_1:65; reconsider i = max B as Element of NAT by ORDINAL1:def 13; take i; let x be set; assume B1: x in A; then B2: f.x in B by A8,FUNCT_1:def 5; then reconsider j = f.x as Element of NAT; j <= i by B2,PRE_CIRC:def 1; then V.j c= V.i & x in V.j by A1,A2,A9,B1,Lem1; hence thesis; end; end; theorem Th15: {[{}, i] where i is Element of NAT: not contradiction} c= Vars proof consider V being ManySortedSet of NAT such that A1: Vars = Union V and A2: V.0 = {[{}, i] where i is Element of NAT: not contradiction} and 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} by VARSdef; dom V = NAT by PBOOLE:def 3; then V.0 in rng V by FUNCT_1:def 5; hence thesis by A1,A2,ZFMISC_1:92; end; theorem Lem3: for A being finite Subset of Vars, i being Nat holds [varcl A, i] in Vars proof let A be finite Subset of Vars, i be Nat; consider V being ManySortedSet of NAT such that A4: Vars = Union V and A1: V.0 = {[{}, k] where k is Element of NAT: not contradiction} and A2: for n being Nat holds V.(n+1) = {[varcl b, j] where b is Subset of V.n, j is Element of NAT: b is finite} by VARSdef; consider j being Element of NAT such that A3: A c= V.j by A1,A2,Lem2; V.(j+1) = {[varcl B, k] where B is Subset of V.j, k is Element of NAT: B is finite} & i in NAT by A2,ORDINAL1:def 13; then [varcl A, i] in V.(j+1) & dom V = NAT by A3,PBOOLE:def 3; hence thesis by A4,CARD_5:10; end; theorem Th16: Vars = {[varcl A, j] where A is Subset of Vars, j is Element of NAT: A is finite} proof consider V being ManySortedSet of NAT such that A1: Vars = Union V and A2: V.0 = {[{}, i] where i is Element of NAT: not contradiction} and A0: 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} by VARSdef; set X = {[varcl A, j] where A is Subset of Vars, j is Element of NAT: A is finite}; B1: dom V = NAT by PBOOLE:def 3; defpred P[Nat] means V.$1 c= X; A3: P[ 0] proof let x; assume x in V.0; then {} c= Vars & ex i being Element of NAT st x = [{}, i] by A2,XBOOLE_1:2; hence thesis by Th11; end; A4: now let i be Element of NAT; assume P[i]; A6: V.(i+1) = {[varcl A, j] where A is Subset of V.i, j is Element of NAT: A is finite} by A0; thus P[i+1] proof let x; assume x in V.(i+1); then consider A being Subset of V.i, j being Element of NAT such that A7: x = [varcl A, j] & A is finite by A6; V.i in rng V by B1,FUNCT_1:def 5; then V.i c= Vars by A1,ZFMISC_1:92; then A c= Vars by XBOOLE_1:1; hence thesis by A7; end; end; A8: for i being Element of NAT holds P[i] from NAT_1:sch 1(A3,A4); now let x; assume x in rng V; then ex y st y in NAT & x = V.y by B1,FUNCT_1:def 5; hence x c= X by A8; end; hence Vars c= X by A1,ZFMISC_1:94; let x; assume x in X; then ex A being Subset of Vars, j being Element of NAT st x = [varcl A, j] & A is finite; hence thesis by Lem3; end; theorem Th17: varcl Vars = Vars proof consider V being ManySortedSet of NAT such that A1: Vars = Union V and A2: V.0 = {[{}, i] where i is Element of NAT: not contradiction} and A3: 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} by VARSdef; defpred P[Nat] means varcl(V.$1) = V.$1; now let x,y; assume [x,y] in V.0; then ex i being Element of NAT st [x,y] = [{}, i] by A2; then x = {} by ZFMISC_1:33; hence x c= V.0 by XBOOLE_1:2; end; then varcl (V.0) c= V.0 & V.0 c= varcl (V.0) by VARCL; then B1: P[ 0] by XBOOLE_0:def 10; B2: now let i; assume B3: P[i]; reconsider i' = i as Element of NAT by ORDINAL1:def 13; B4: V.(i+1) = {[varcl A, j] where A is Subset of V.i, j is Element of NAT: A is finite} by A3; now let x,y; assume [x,y] in V.(i+1); then consider A being Subset of V.i, j being Element of NAT such that B5: [x,y] = [varcl A, j] & A is finite by B4; x = varcl A & i <= i+1 by B5,NAT_1:11,ZFMISC_1:33; then x c= V.i & V.i' c= V.(i'+1) by A2,A3,B3,Th13,Lem1; hence x c= V.(i+1) by XBOOLE_1:1; end; then varcl (V.(i+1)) c= V.(i+1) & V.(i+1) c= varcl (V.(i+1)) by VARCL; hence P[i+1] by XBOOLE_0:def 10; end; B3: P[i] from NAT_1:sch 2(B1,B2); A4: varcl Vars = union {varcl a where a is Element of rng V: not contradiction} by A1,Th14; thus now let x; assume x in varcl Vars; then consider Y such that A5: x in Y & Y in {varcl a where a is Element of rng V: not contradiction} by A4,TARSKI:def 4; consider a being Element of rng V such that A6: Y = varcl a by A5; consider i being set such that A7: i in dom V & a = V.i by FUNCT_1:def 5; reconsider i as Element of NAT by A7,PBOOLE:def 3; varcl (V.i) = a by B3,A7; hence x in Vars by A1,A5,A6,A7,CARD_5:10; end; thus Vars c= varcl Vars by VARCL; end; theorem Lem4: for X st the_rank_of X is finite holds X is finite proof let X; assume the_rank_of X is finite; then the_rank_of X in NAT by CARD_1:103; then Rank the_rank_of X is finite & X c= Rank the_rank_of X by CARD_3:57,CLASSES1:def 8; hence thesis by FINSET_1:13; end; theorem Lem5: the_rank_of varcl X = the_rank_of X proof A1: X c= Rank the_rank_of X by CLASSES1:def 8; set a = the_rank_of X; a c= succ a & succ a c= succ succ a by ORDINAL3:1; then a c= succ succ a by XBOOLE_1:1; then A2: Rank a c= Rank succ succ a by CLASSES1:43; now let x,y; assume [x,y] in Rank the_rank_of X; then x in Rank a by A2,CLASSES1:51; hence x c= Rank the_rank_of X by ORDINAL1:def 2; end; then varcl X c= Rank a by A1,VARCL; hence the_rank_of varcl X c= a by CLASSES1:73; X c= varcl X by VARCL; hence thesis by CLASSES1:75; end; theorem Lem6: for X being finite Subset of Rank omega holds X in Rank omega proof let X be finite Subset of Rank omega; deffunc F(set) = the_rank_of $1; consider f being Function such that A1: dom f = X and A2: for x st x in X holds f.x = F(x) from FUNCT_1:sch 3; A3: rng f c= NAT proof let y; assume y in rng f; then consider x such that A4: x in X & y = f.x by A1,FUNCT_1:def 5; the_rank_of x in omega by A4,CLASSES1:74; hence thesis by A2,A4; end; per cases; suppose X = {}; then the_rank_of X = {} & {} in omega & omega is ordinal by CLASSES1:79,ORDINAL1:def 12; hence thesis by CLASSES1:74; end; suppose X <> {}; then reconsider Y = rng f as finite non empty Subset of NAT by A1,A3,RELAT_1:65,FINSET_1:26; reconsider mY = max Y as Element of NAT by ORDINAL1:def 13; set i = 1+mY; X c= Rank i proof let x; assume x in X; then A5: f.x in Y & f.x = the_rank_of x by A1,A2,FUNCT_1:def 5; then reconsider j = f.x as Element of NAT; j <= mY by A5,PRE_CIRC:def 1; then j c= mY by NAT_1:40; then j in succ mY by ORDINAL1:34; then succ j c= succ mY & succ mY = i & j in succ j by NAT_1:39,ORDINAL1:33; hence thesis by A5,CLASSES1:74; end; then the_rank_of X c= i by CLASSES1:73; then the_rank_of X in succ i & i+1 c= omega & i+1 = succ i by ORDINAL1:def 2,34,NAT_1:39; hence thesis by CLASSES1:74; end; end; theorem Lem7: Vars c= Rank omega proof consider V being ManySortedSet of NAT such that A1: Vars = Union V and A2: V.0 = {[{}, i] where i is Element of NAT: not contradiction} and A3: 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} by VARSdef; let x; assume x in Vars; then consider i being set such that A4: i in dom V & x in V.i by A1,CARD_5:10; reconsider i as Element of NAT by A4,PBOOLE:def 3; defpred P[Nat] means V.$1 c= Rank omega; A5: P[ 0] proof let x; assume x in V.0; then consider i being Element of NAT such that B1: x = [{}, i] by A2; i+1 = succ i by NAT_1:39; then B3: {} c= i & i in i+1 by XBOOLE_1:2,ORDINAL1:10; then {} in i+1 & the_rank_of {} = {} & the_rank_of i = i by ORDINAL1:22,CLASSES1:81; then {} in Rank (i+1) & i in Rank (i+1) by B3,CLASSES1:74; then B2: x in Rank succ succ (i+1) by B1,CLASSES1:51; succ (i+1) = i+1+1 & succ (i+1+1) = i+1+1+1 by NAT_1:39; then succ succ (i+1) c= omega by ORDINAL1:def 2; then Rank succ succ (i+1) c= Rank omega by CLASSES1:43; hence thesis by B2; end; A6: now let n be Element of NAT such that C1: P[n]; C2: V.(n+1) = {[varcl a, j] where a is Subset of V.n, j is Element of NAT: a is finite} by A3; thus P[n+1] proof let x; assume x in V.(n+1); then consider a being Subset of V.n, j being Element of NAT such that C3: x = [varcl a, j] & a is finite by C2; a c= Rank omega by C1,XBOOLE_1:1; then a in Rank omega by C3,Lem6; then reconsider i = the_rank_of a as Element of NAT by CLASSES1:74; reconsider k = j \/ i as Element of NAT by ORDINAL3:15; C5: the_rank_of varcl a = i & the_rank_of j = j by Lem5,CLASSES1:81; i c= k & j c= k & k in succ k by XBOOLE_1:7,ORDINAL1:10; then i in succ k & j in succ k & succ k = k+1 by ORDINAL1:22,NAT_1:39; then varcl a in Rank (k+1) & j in Rank (k+1) by C5,CLASSES1:74; then C6: x in Rank succ succ (k+1) by C3,CLASSES1:51; succ (k+1) = k+1+1 & succ (k+1+1) = k+1+1+1 by NAT_1:39; then succ succ (k+1) c= omega by ORDINAL1:def 2; then Rank succ succ (k+1) c= Rank omega by CLASSES1:43; hence thesis by C6; end; end; for n being Element of NAT holds P[n] from NAT_1:sch 1(A5,A6); then V.i c= Rank omega; hence thesis by A4; end; theorem Th18: for A being finite Subset of Vars holds varcl A is finite Subset of Vars proof let A be finite Subset of Vars; A c= Rank omega by Lem7,XBOOLE_1:1; then A in Rank omega by Lem6; then the_rank_of A in omega by CLASSES1:74; then the_rank_of varcl A in omega by Lem5; then the_rank_of varcl A is finite by CARD_1:103; hence thesis by Lem4,Th13,Th17; end; registration cluster Vars -> non empty; correctness proof consider j being Element of NAT; [{},j] in {[{}, i] where i is Element of NAT: not contradiction}; hence thesis by Th15; end; end; definition mode variable is Element of Vars; end; registration let x be variable; cluster x`1 -> finite; coherence proof 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 Th16; x`1 = varcl A by A1,MCART_1:7; hence thesis by A1,Th18; end; end; notation let x be variable; synonym vars x for x`1; end; definition let x be variable; redefine func vars x -> Subset of Vars; coherence proof 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 Th16; x`1 = varcl A by A1,MCART_1:7; hence thesis by A1,Th18; end; end; theorem [{}, i] in Vars proof i in NAT by ORDINAL1:def 13; then [{}, i] in {[{}, j]: not contradiction}; hence thesis by Th15; end; theorem Lem8: for A being Subset of Vars holds varcl {[varcl A, j]} = (varcl A) \/ {[varcl A, j]} proof let A be Subset of Vars; A2: {[varcl A, j]} c= (varcl A) \/ {[varcl A, j]} & varcl A c= (varcl A) \/ {[varcl A, j]} by XBOOLE_1:7; now let x,y; assume [x,y] in (varcl A) \/ {[varcl A, j]}; then [x,y] in varcl A or [x,y] in {[varcl A, j]} by XBOOLE_0:def 2; then [x,y] in varcl A or [x,y] = [varcl A, j] by TARSKI:def 1; then x c= varcl A or x = varcl A by VARCL,ZFMISC_1:33; hence x c= (varcl A) \/ {[varcl A, j]} by A2,XBOOLE_1:1; end; hence varcl {[varcl A, j]} c= (varcl A) \/ {[varcl A, j]} by A2,VARCL; A1: {[varcl A, j]} c= varcl {[varcl A, j]} by VARCL; [varcl A, j] in {[varcl A, j]} by TARSKI:def 1; then varcl A c= varcl {[varcl A, j]} by A1,VARCL; hence thesis by A1,XBOOLE_1:8; end; theorem Th82: for x being variable holds varcl {x} = (vars x) \/ {x} proof let x be variable; x in Vars; then consider A being Subset of Vars, j such that A1: x = [varcl A, j] & A is finite by Th16; varcl {x} = (varcl A) \/ {x} by A1,Lem8; hence thesis by A1,MCART_1:7; end; theorem for x being variable holds [(vars x) \/ {x}, i] in Vars proof let x be variable; x in Vars; then consider A being Subset of Vars, j such that A1: x = [varcl A, j] & A is finite by Th16; varcl {x} = (varcl A) \/ {x} & vars x = varcl A & i in NAT by A1,Lem8,MCART_1:7,ORDINAL1:def 13; hence thesis by Th16; end; begin :: Quasi loci notation let R be Relation, A be set; synonym R dom A for R|A; end; definition func QuasiLoci -> FinSequenceSet of Vars means: QuasiLociDef: for p being FinSequence of Vars holds p in it iff p is one-to-one & for i st i in dom p holds (p.i)`1 c= rng (p dom i); existence proof defpred P[set] means ex p being Function st p = $1 & p is one-to-one & for i st i in dom p holds (p.i)`1 c= rng (p|i); consider L being set such that A1: x in L iff x in Vars* & P[ x ] from XBOOLE_0:sch 1; L is FinSequenceSet of Vars proof let x; assume x in L; then x in Vars* by A1; hence thesis by FINSEQ_1:def 11; end; then reconsider L as FinSequenceSet of Vars; take L; let p be FinSequence of Vars; p in L iff p in Vars* & ex q being Function st q = p & q is one-to-one & for i st i in dom q holds (q.i)`1 c= rng (q|i) by A1; hence thesis by FINSEQ_1:def 11; end; correctness proof let L1, L2 be FinSequenceSet of Vars such that A1: for p being FinSequence of Vars holds p in L1 iff p is one-to-one & for i st i in dom p holds (p.i)`1 c= rng (p|(i qua set)) and A2: for p being FinSequence of Vars holds p in L2 iff p is one-to-one & for i st i in dom p holds (p.i)`1 c= rng (p|(i qua set)); thus now let x; assume A3: x in L1; then reconsider p = x as FinSequence of Vars by FINSEQ_2:def 3; p is one-to-one & for i st i in dom p holds (p.i)`1 c= rng (p|(i qua set)) by A1,A3; hence x in L2 by A2; end; let x; assume A4: x in L2; then reconsider p = x as FinSequence of Vars by FINSEQ_2:def 3; p is one-to-one & for i st i in dom p holds (p.i)`1 c= rng (p|(i qua set)) by A2,A4; hence x in L1 by A1; end; end; theorem Th31: <*>Vars in QuasiLoci proof for i st i in dom {} holds ((<*>Vars).i)`1 c= rng ((<*>Vars)|(i qua set)); hence thesis by QuasiLociDef; end; registration cluster QuasiLoci -> non empty; correctness by Th31; end; definition mode quasi-loci is Element of QuasiLoci; end; registration cluster -> one-to-one quasi-loci; coherence by QuasiLociDef; end; theorem Th32: for l being one-to-one FinSequence of Vars holds l is quasi-loci iff for i being Nat, x being variable st i in dom l & x = l.i for y being variable st y in vars x ex j being Nat st j in dom l & j < i & y = l.j proof let l be one-to-one FinSequence of Vars; thus now assume A1: l is quasi-loci; let i be Nat, x be variable such that A2: i in dom l & x = l.i; let y be variable such that A3: y in vars x; vars x c= rng (l|(i qua set)) by A1,A2,QuasiLociDef; then consider z such that A4: z in dom (l dom i) & y = (l dom i).z by A3,FUNCT_1:def 5; dom (l dom i) = dom l /\ i by RELAT_1:90; then A5: z in dom l & z in i by A4,XBOOLE_0:def 3; then reconsider z as Element of NAT; reconsider j = z as Nat; take j; Card z = z & Card i = i by CARD_1:def 5; hence j in dom l & j < i & y = l.j by A4,A5,NAT_1:42,FUNCT_1:70; end; assume A6: for i being Nat, x being variable st i in dom l & x = l.i for y being variable st y in vars x ex j being Nat st j in dom l & j < i & y = l.j; now let i; assume A8: i in dom l; then l.i in rng l & rng l c= Vars by FUNCT_1:def 5; then reconsider x = l.i as variable; thus (l.i)`1 c= rng (l dom i) proof let y; assume y in (l.i)`1; then A7: y in vars x; then reconsider y as variable; consider j being Nat such that A9: j in dom l & j < i & y = l.j by A6,A7,A8; Card i = i & Card j = j by CARD_1:def 5; then j in i by A9,NAT_1:42; hence thesis by A9,FUNCT_1:73; end; end; hence thesis by QuasiLociDef; end; theorem Th7: for l being quasi-loci, x being variable holds l^<*x*> is quasi-loci iff not x in rng l & vars x c= rng l proof let l be quasi-loci, x be variable; A1: (l^<*x*>).(1+len l) = x by FINSEQ_1:59; A2: dom (l^<*x*>) = Seg (len l + len <*x*>) by FINSEQ_1:def 7 .= Seg (len l + 1) by FINSEQ_1:56; 1 <= 1+len l & 1+len l <= 1+len l by NAT_1:11; then A3: 1+len l in dom (l^<*x*>) by A2; A4: dom l = Seg len l by FINSEQ_1:def 3; thus now assume B1: l^<*x*> is quasi-loci; thus not x in rng l proof assume x in rng l; then consider a being set such that B2: a in dom l & x = l.a by FUNCT_1:def 5; reconsider a as Element of NAT by B2; B3: (l^<*x*>).a = x by B2,FINSEQ_1:def 7; a <= len l & len l < 1+len l & dom l c= dom (l^<*x*>) by A4,B2,FINSEQ_1:3,39,NAT_1:13; hence thesis by A1,A3,B1,B3,B2,FUNCT_1:def 8; end; thus vars x c= rng l proof let a be set; assume C1: a in vars x; then reconsider a as variable; consider j being Nat such that C2: j in dom (l^<*x*>) & j < 1+len l & a = (l^<*x*>).j by A1,A3,B1,C1,Th32; reconsider j as Element of NAT by ORDINAL1:def 13; j <= len l & j >= 1 by A2,C2,NAT_1:13,FINSEQ_1:3; then C3: j in dom l by A4; then a = l.j by C2,FINSEQ_1:def 7; hence thesis by C3,FUNCT_1:def 5; end; end; assume D1: not x in rng l & vars x c= rng l; EE: (l^<*x*>) is one-to-one proof let a,b be set; assume E1: a in dom (l^<*x*>) & b in dom (l^<*x*>) & (l^<*x*>).a = (l^<*x*>).b; then reconsider a,b as Element of NAT; E2: a >= 1 & b >= 1 & a <= 1+len l & b <= 1+len l by A2,E1,FINSEQ_1:3; then (a <= len l or a = 1+len l) & (b <= len l or b = 1+len l) by NAT_1:8; then (a in dom l or a = 1+len l) & (b in dom l or b = 1+len l) by A4,E2; then (a in dom l & l.a = (l^<*x*>).a & l.a in rng l or a = 1+len l) & (b in dom l & l.b = (l^<*x*>).b & l.b in rng l or b = 1+len l) by FUNCT_1:def 5,FINSEQ_1:def 7; hence thesis by FINSEQ_1:59,D1,E1,FUNCT_1:def 8; end; now let i be Nat, z be variable; assume D2: i in dom (l^<*x*>) & z = (l^<*x*>).i; then D3: i >= 1 & i <= 1+len l & i is Element of NAT by A2,FINSEQ_1:3; then i <= len l or i = 1+len l by NAT_1:8; then D9: i in dom l or i = 1+len l & z = x by A4,D2,D3,FINSEQ_1:59; let y be variable; assume D5: y in vars z; thus ex j being Nat st j in dom (l^<*x*>) & j < i & y = (l^<*x*>).j proof per cases by D9,D2,FINSEQ_1:def 7; suppose D8: i = 1+len l & z = x; then consider k being set such that D6: k in dom l & y = l.k by D1,D5,FUNCT_1:def 5; reconsider k as Element of NAT by D6; take k; dom l c= dom (l^<*x*>) & k <= len l by A4,D6,FINSEQ_1:3,39; hence thesis by D6,D8,FINSEQ_1:def 7,NAT_1:13; end; suppose i in dom l & z = l.i; then consider j being Nat such that D7: j in dom l & j < i & y = l.j by D5,Th32; take j; dom l c= dom (l^<*x*>) & j is Element of NAT by ORDINAL1:def 13,FINSEQ_1:39; hence thesis by D7,FINSEQ_1:def 7; end; end; end; hence thesis by EE,Th32; end; theorem Th6: for p,q being FinSequence st p^q is quasi-loci holds p is quasi-loci & q is FinSequence of Vars proof let p,q be FinSequence; assume A1: p^q is quasi-loci; then A2: p is one-to-one FinSequence of Vars by FINSEQ_1:50,FINSEQ_3:98; now let i be Nat, x be variable such that A3: i in dom p & x = p.i; let y be variable such that A4: y in vars x; dom p c= dom (p^q) by FINSEQ_1:39; then i in dom (p^q) & x = (p^q).i by A3,FINSEQ_1:def 7; then consider j being Nat such that A5: j in dom (p^q) & j < i & y = (p^q).j by A1,A4,Th32; take j; A6: dom p = Seg len p & dom (p^q) = Seg len (p^q) by FINSEQ_1:def 3; then A7: j >= 1 & i <= len p by A3,A5,FINSEQ_1:3; then j < len p by A5,XXREAL_0:2; hence j in dom p & j < i by A5,A6,A7; hence y = p.j by A5,FINSEQ_1:def 7; end; hence thesis by A1,A2,Th32,FINSEQ_1:50; end; theorem for l being quasi-loci holds varcl rng l = rng l proof let l be quasi-loci; now let x,y; assume A2: [x,y] in rng l; then reconsider xy = [x,y] as variable; consider i being set such that A3: i in dom l & xy = l.i by A2,FUNCT_1:def 5; reconsider i as Nat by A3,ORDINAL1:def 13; A5: vars xy = x by MCART_1:7; thus x c= rng l proof let a be set; assume A6: a in x; then reconsider a as variable by A5; ex j being Nat st j in dom l & j < i & a = l.j by A3,A5,A6,Th32; hence thesis by FUNCT_1:def 5; end; end; hence varcl rng l c= rng l by VARCL; thus rng l c= varcl rng l by VARCL; end; theorem Th33: for x being variable holds <*x*> is quasi-loci iff vars x = {} proof let x be variable; A1: <*x*> = (<*>Vars)^<*x*> by FINSEQ_1:47; A2: rng {} = {}; vars x c= {} implies vars x = {} by XBOOLE_1:3; hence thesis by A1,A2,Th7,Th31; end; theorem Th34: for x,y being variable holds <*x,y*> is quasi-loci iff vars x = {} & x <> y & vars y c= {x} proof let x,y be variable; A2: rng <*x*> = {x} by FINSEQ_1:55; A3: <*x*> is quasi-loci iff vars x = {} by Th33; y in {x} iff y = x by TARSKI:def 1; hence thesis by A2,A3,Th6,Th7; end; theorem 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} proof let x,y,z be variable; A2: rng <*x,y*> = {x,y} by FINSEQ_2:147; A3: <*x,y*> is quasi-loci iff vars x = {} & x <> y & vars y c= {x} by Th34; z in {x,y} iff z = x or z = y by TARSKI:def 2; hence thesis by A2,A3,Th6,Th7; end; definition let l be quasi-loci; redefine func l" -> PartFunc of Vars, NAT; coherence proof dom (l") = rng l & rng (l") = dom l by FUNCT_1:55; hence thesis by RELSET_1:11; end; end; begin :: Mizar Constructor Signature definition func a_Type equals 0; coherence; func an_Adj equals 1; coherence; func a_Term equals 2; coherence; func * equals 0; coherence; func non_op equals 1; coherence; :: func an_ExReg equals 3; coherence; :: func a_CondReg equals 4; coherence; :: func a_FuncReg equals 5; coherence; end; definition let C be Signature; attr C is constructor means: CONSTRSIGN: the carrier of C = {a_Type, an_Adj, a_Term} & {*, non_op} c= the OperSymbols 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 OperSymbols of C st o <> * & o <> non_op holds (the Arity of C).o in {a_Term}*; end; registration cluster constructor -> non empty non void Signature; coherence proof let C be Signature; assume A1: the carrier of C = {a_Type, an_Adj, a_Term}; assume {*, non_op} c= the OperSymbols of C; then the OperSymbols of C <> {} by XBOOLE_1:3; hence thesis by A1,STRUCT_0:def 1,MSUALG_1:def 5; end; end; definition func MinConstrSign -> strict Signature means: MINdef: it is constructor & the OperSymbols of it = {*, non_op}; existence proof set A = {a_Type, an_Adj, a_Term}; reconsider t = a_Type, a = an_Adj as Element of A by ENUMSET1:def 1; reconsider aa = <*a*> as Element of A*; set C = ManySortedSign(# A, {*, non_op}, (*, non_op) --> (<*a,t*>, aa), (*, non_op) --> (t, a) #); reconsider C as non void non empty strict ManySortedSign by MSUALG_1:def 5; take C; thus the carrier of C = {a_Type, an_Adj, a_Term} & {*, non_op} c= the OperSymbols of C; thus (the Arity of C).* = <*an_Adj, a_Type*> by FUNCT_4:66; thus (the Arity of C).non_op = <*an_Adj*> by FUNCT_4:66; thus (the ResultSort of C).* = a_Type by FUNCT_4:66; thus (the ResultSort of C).non_op = an_Adj by FUNCT_4:66; thus thesis by TARSKI:def 2; end; correctness proof let C1, C2 be strict Signature such that A1: C1 is constructor & the OperSymbols of C1 = {*, non_op} and A2: C2 is constructor & the OperSymbols of C2 = {*, non_op}; set A = {a_Type, an_Adj, a_Term}; A3: the carrier of C1 = A & the carrier of C2 = A by A1,A2,CONSTRSIGN; A4: (the Arity of C1).* = <*an_Adj, a_Type*> & (the Arity of C2).* = <*an_Adj, a_Type*> by A1,A2,CONSTRSIGN; A5: (the Arity of C1).non_op = <*an_Adj*> & (the Arity of C2).non_op = <*an_Adj*> by A1,A2,CONSTRSIGN; A6: (the ResultSort of C1).* = a_Type & (the ResultSort of C2).* = a_Type by A1,A2,CONSTRSIGN; A7: (the ResultSort of C1).non_op = an_Adj & (the ResultSort of C2).non_op = an_Adj by A1,A2,CONSTRSIGN; dom the Arity of C1 = {*, non_op} & dom the Arity of C2 = {*, non_op} by A1,A2,FUNCT_2:def 1; then A8: the Arity of C1 = (*, non_op) --> (<*an_Adj, a_Type*>, <*an_Adj*>) & the Arity of C2 = (*, non_op) --> (<*an_Adj, a_Type*>, <*an_Adj*>) by A4,A5,FUNCT_4:69; dom the ResultSort of C1 = {*, non_op} & dom the ResultSort of C2 = {*, non_op} by A1,A2,A3,FUNCT_2:def 1; then the ResultSort of C1 = (*, non_op) --> (a_Type, an_Adj) & the ResultSort of C2 = (*, non_op) --> (a_Type, an_Adj) by A6,A7,FUNCT_4:69; hence thesis by A1,A2,A3,A8; end; end; registration cluster MinConstrSign -> constructor; coherence by MINdef; end; registration cluster constructor strict Signature; existence proof take MinConstrSign; thus thesis; end; 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; attr o is constructor means: CNSTR2: o <> * & o <> non_op; end; theorem 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 proof let S be ConstructorSignature; let o be OperSymbol of S such that A1: o <> * & o <> non_op; reconsider t = a_Term as Element of {a_Term} by TARSKI:def 1; len ((len the_arity_of o)|->a_Term) = len the_arity_of o & the_arity_of o in {a_Term}* & (len the_arity_of o)|->t in {a_Term}* by A1,CONSTRSIGN,FINSEQ_1:def 11,FINSEQ_2:69; hence thesis by Th1A; end; definition let C be non empty non void Signature; attr C is initialized means: INITIALIZED: ex m, a being OperSymbol of C st the_result_sort_of m = a_Type & the_arity_of m = {} & :: set the_result_sort_of a = an_Adj & the_arity_of a = {}; :: empty end; definition let C be ConstructorSignature; A1: the carrier of C = {a_Type, an_Adj, a_Term} by CONSTRSIGN; func a_Type C -> SortSymbol of C equals a_Type; coherence by A1,ENUMSET1:def 1; func an_Adj C -> SortSymbol of C equals an_Adj; coherence by A1,ENUMSET1:def 1; func a_Term C -> SortSymbol of C equals a_Term; coherence by A1,ENUMSET1:def 1; A2: {*, non_op} c= the OperSymbols of C by CONSTRSIGN; A3: * in {*, non_op} & non_op in {*, non_op} by TARSKI:def 2; func non_op C -> OperSymbol of C equals non_op; coherence by A2,A3; func ast C -> OperSymbol of C equals *; coherence by A2,A3; end; theorem ::? 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 CONSTRSIGN; definition func Modes equals [:{a_Type},[:QuasiLoci,NAT:]:]; correctness; func Attrs equals [:{an_Adj},[:QuasiLoci,NAT:]:]; correctness; func Funcs equals [:{a_Term},[:QuasiLoci,NAT:]:]; correctness; end; registration cluster Modes -> non empty; coherence; cluster Attrs -> non empty; coherence; cluster Funcs -> non empty; coherence; end; definition func Constructors -> non empty set equals Modes \/ Attrs \/ Funcs; coherence; end; theorem {*, non_op} misses Constructors proof assume not thesis; then consider x such that A1: x in {*, non_op} and A2: x in Constructors by XBOOLE_0:3; x in Modes \/ Attrs or x in Funcs by A2,XBOOLE_0:def 2; then x in Modes or x in Attrs or x in Funcs by XBOOLE_0:def 2; then consider Y,Z being set such that A3: x in [:Y,Z:]; consider y,z such that A4: y in Y & z in Z & [y,z] = x by A3,ZFMISC_1:def 2; x = * or x = non_op by A1,TARSKI:def 2; then the_rank_of x = 0 or the_rank_of x = 1 by CLASSES1:81; then the_rank_of x c= 1 & 1 in succ 1 & succ {} = 0+1 by ORDINAL1:10,XBOOLE_1:2; then the_rank_of x in succ succ {} by ORDINAL1:22; then x in Rank succ succ {} by CLASSES1:74; hence thesis by A4,CLASSES1:33,51; end; definition let x be Element of [:QuasiLoci, NAT:]; redefine func x`1 -> quasi-loci; coherence by MCART_1:10; func x`2 -> Element of NAT; coherence 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; redefine func kind_of c -> Element of {a_Type, an_Adj, a_Term}; coherence proof c in Modes \/ Attrs or c in Funcs by XBOOLE_0:def 2; then c in Modes or c in Attrs or c in Funcs by XBOOLE_0:def 2; then c`1 in {a_Type} or c`1 in {an_Adj} or c`1 in {a_Term} by MCART_1:10; then c`1 = a_Type or c`1 = an_Adj or c`1 = a_Term by TARSKI:def 1; hence thesis by ENUMSET1:def 1; end; func c`2 -> Element of [:QuasiLoci, NAT:]; coherence proof c in Modes \/ Attrs or c in Funcs by XBOOLE_0:def 2; then c in Modes or c in Attrs or c in Funcs by XBOOLE_0:def 2; hence thesis by MCART_1:10; end; end; definition let c be Element of Constructors; func loci_of c -> quasi-loci equals c`2`1; coherence; func index_of c -> Nat equals c`2`2; coherence; end; theorem for c being Element of Constructors holds (kind_of c = a_Type iff c in Modes) & (kind_of c = an_Adj iff c in Attrs) & (kind_of c = a_Term iff c in Funcs) proof let x be Element of Constructors; A1: x in Modes \/ Attrs or x in Funcs by XBOOLE_0:def 2; (x in Modes implies x`1 in {a_Type}) & (x in Attrs implies x`1 in {an_Adj}) & (x in Funcs implies x`1 in {a_Term}) by MCART_1:10; hence thesis by A1,XBOOLE_0:def 2,TARSKI:def 1; end; definition func MaxConstrSign -> strict ConstructorSignature means: MAXdef: the OperSymbols 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 proof set S = {a_Type, an_Adj, a_Term}; set O = {*, non_op} \/ Constructors; deffunc F(Element of Constructors) = (len loci_of $1)|->a_Term; consider f being ManySortedSet of Constructors such that A1: for c being Element of Constructors holds f.c = F(c) from PBOOLE:sch 5; deffunc G(Element of Constructors) = kind_of $1; consider g being ManySortedSet of Constructors such that A2: for c being Element of Constructors holds g.c = G(c) from PBOOLE:sch 5; reconsider t = a_Type, a = an_Adj, tr = a_Term as Element of S by ENUMSET1:def 1; reconsider aa = <*a*> as Element of S*; set A = f+*(*, non_op)-->(<*a,t*>, aa); set R = g+*(*, non_op)-->(t, a); B0: dom (*, non_op)-->(<*a,t*>, aa) = {*, non_op} & dom (*, non_op)-->(t, a) = {*, non_op} & dom f = Constructors & dom g = Constructors by FUNCT_4:65,PBOOLE:def 3; then A3: dom A = O & dom R = O by FUNCT_4:def 1; rng f c= S* proof let y; assume y in rng f; then consider x such that B1: x in Constructors & y = f.x by B0,FUNCT_1:def 5; reconsider x as Element of Constructors by B1; y = (len loci_of x)|->tr by A1,B1; hence thesis by FINSEQ_1:def 11; end; then A5: rng f \/ rng (*, non_op)-->(<*a,t*>, aa) c= (S*) \/ (S*) by XBOOLE_1:13; rng g c= S proof let y; assume y in rng g; then consider x such that B2: x in Constructors & y = g.x by B0,FUNCT_1:def 5; reconsider x as Element of Constructors by B2; y = kind_of x by A2,B2; hence thesis; end; then A6: rng g \/ rng (*, non_op)-->(t, a) c= S \/ S by XBOOLE_1:13; rng A c= rng f \/ rng (*, non_op)-->(<*a,t*>, aa) by FUNCT_4:18; then reconsider A as Function of O, S* by A3,FUNCT_2:4,A5,XBOOLE_1:1; rng R c= rng g \/ rng (*, non_op)-->(t, a) by FUNCT_4:18; then reconsider R as Function of O, S by A3,FUNCT_2:4,A6,XBOOLE_1:1; reconsider Max = ManySortedSign(# S, O, A, R #) as non empty non void strict Signature by MSUALG_1:def 5; Max is constructor proof thus the carrier of Max = {a_Type, an_Adj, a_Term}; thus {*, non_op} c= the OperSymbols of Max by XBOOLE_1:7; B3: * in {*, non_op} & non_op in {*, non_op} by TARSKI:def 2; hence (the Arity of Max).* = ((*, non_op)-->(<*a,t*>, aa)).* by B0,FUNCT_4:14 .= <*an_Adj, a_Type*> by FUNCT_4:66; thus (the Arity of Max).non_op = ((*, non_op)-->(<*a,t*>, aa)).non_op by B0,B3,FUNCT_4:14 .= <*an_Adj*> by FUNCT_4:66; thus (the ResultSort of Max).* = ((*, non_op)-->(t, a)).* by B0,B3,FUNCT_4:14 .= a_Type by FUNCT_4:66; thus (the ResultSort of Max).non_op = ((*, non_op)-->(t, a)).non_op by B0,B3,FUNCT_4:14 .= an_Adj by FUNCT_4:66; let o be Element of the OperSymbols of Max; assume o <> * & o <> non_op; then B4: not o in {*, non_op} by TARSKI:def 2; then reconsider c = o as Element of Constructors by XBOOLE_0:def 2; reconsider tr as Element of {a_Term} by TARSKI:def 1; (the Arity of Max).o = f.c by B0,B4,FUNCT_4:def 1 .= (len loci_of c)|->tr by A1; hence (the Arity of Max).o in {a_Term}* by FINSEQ_1:def 11; end; then reconsider Max as strict ConstructorSignature; take Max; thus the OperSymbols of Max = {*, non_op} \/ Constructors; let o being OperSymbol of Max; assume o <> * & o <> non_op; then C1: not o in {*, non_op} by TARSKI:def 2; then reconsider c = o as Element of Constructors by XBOOLE_0:def 2; thus (the ResultSort of Max).o = g.c by B0,C1,FUNCT_4:def 1 .= o`1 by A2; thus Card ((the Arity of Max).o) = Card (f.c) by B0,C1,FUNCT_4:def 1 .= Card (F(c) qua set) by A1 .= Card o`2`1 by FINSEQ_2:69; end; uniqueness proof let it1, it2 be strict ConstructorSignature such that A1: the OperSymbols of it1 = {*, non_op} \/ Constructors and A2: for o being OperSymbol of it1 st o is constructor holds (the ResultSort of it1).o = o`1 & Card ((the Arity of it1).o) = Card o`2`1 and A3: the OperSymbols of it2 = {*, non_op} \/ Constructors and A4: for o being OperSymbol of it2 st o is constructor holds (the ResultSort of it2).o = o`1 & Card ((the Arity of it2).o) = Card o`2`1; set S = {a_Type, an_Adj, a_Term}; set O = {*, non_op} \/ Constructors; A5: the carrier of it1 = S & the carrier of it2 = S by CONSTRSIGN; BB: now let c be Element of Constructors; reconsider o1 = c as OperSymbol of it1 by A1,XBOOLE_0:def 2; reconsider o2 = o1 as OperSymbol of it2 by A1,A3; assume B3: c <> * & c <> non_op; then o1 is constructor & o2 is constructor by CNSTR2; then B1: Card ((the Arity of it1).o1) = Card (c`2`1 qua set) & Card ((the Arity of it2).o2) = Card (c`2`1 qua set) by A2,A4; (the Arity of it1).o1 in {a_Term}* & (the Arity of it2).o2 in {a_Term}* by B3,CONSTRSIGN; then reconsider p1 = (the Arity of it1).o1, p2 = (the Arity of it2).o2 as FinSequence of {a_Term} by FINSEQ_1:def 11; B2: dom p1 = Seg len p1 & dom p2 = Seg len p2 by FINSEQ_1:def 3; now let i be Nat; assume i in dom p1; then p1.i in rng p1 & rng p1 c= {a_Term} & p2.i in rng p2 & rng p2 c= {a_Term} by B1,B2,FUNCT_1:def 5; then p1.i = a_Term & p2.i = a_Term by TARSKI:def 1; hence p1.i = p2.i; end; hence (the Arity of it1).c = (the Arity of it2).c by B1,B2,FINSEQ_1:17; end; now let o be OperSymbol of it1; o in {*, non_op} or not o in {*, non_op}; then o = * or o = non_op or o in Constructors & o <> * & o <> non_op by A1,XBOOLE_0:def 2,TARSKI:def 2; then (the Arity of it1).o = <*an_Adj,a_Type*> & (the Arity of it2).o = <*an_Adj,a_Type*> or (the Arity of it1).o = <*an_Adj*> & (the Arity of it2).o = <*an_Adj*> or (the Arity of it1).o = (the Arity of it2).o by BB,CONSTRSIGN; hence (the Arity of it1).o = (the Arity of it2).o; end; then A6: the Arity of it1 = the Arity of it2 by A1,A3,A5,FUNCT_2:113; now let o be OperSymbol of it1; reconsider o' = o as OperSymbol of it2 by A1,A3; not o in {*, non_op} or o in {*,non_op}; then o = * or o = non_op or o in Constructors & o is constructor & o' is constructor by A1,CNSTR2,XBOOLE_0:def 2,TARSKI:def 2; then (the ResultSort of it1).o = a_Type & (the ResultSort of it2).o = a_Type or (the ResultSort of it1).o = an_Adj & (the ResultSort of it2).o = an_Adj or (the ResultSort of it1).o = o`1 & (the ResultSort of it2).o = o`1 by A2,A4,CONSTRSIGN; hence (the ResultSort of it1).o = (the ResultSort of it2).o; end; hence thesis by A6,A1,A3,A5,FUNCT_2:113; end; end; registration cluster MinConstrSign -> non initialized; correctness proof given m, a being OperSymbol of MinConstrSign such that the_result_sort_of m = a_Type and A2: the_arity_of m = {} and the_result_sort_of a = an_Adj & the_arity_of a = {}; the OperSymbols of MinConstrSign = {*, non_op} by MINdef; then m = * or m = non_op by TARSKI:def 2; hence contradiction by A2,CONSTRSIGN; end; cluster MaxConstrSign -> initialized; correctness proof set m = [a_Type, [{}, 0]], a = [an_Adj, [{}, 0]]; a_Type in {a_Type} & an_Adj in {an_Adj} & [<*> Vars, 0] in [:QuasiLoci, NAT:] by Th31,ZFMISC_1:def 2,TARSKI:def 1; then m in Modes & a in Attrs by ZFMISC_1:def 2; then m in Modes \/ Attrs & a in Modes \/ Attrs by XBOOLE_0:def 2; then m in Constructors & a in Constructors & the OperSymbols of MaxConstrSign = {*, non_op} \/ Constructors by MAXdef,XBOOLE_0:def 2; then reconsider m,a as OperSymbol of MaxConstrSign by XBOOLE_0:def 2; A1: m is constructor & a is constructor by CNSTR2; take m, a; thus the_result_sort_of m = m`1 by A1,MAXdef .= a_Type by MCART_1:7; len the_arity_of m = Card m`2`1 by A1,MAXdef .= Card [{}, 0]`1 by MCART_1:7 .= 0 by MCART_1:7,CARD_1:47; hence the_arity_of m = {} by CARD_2:59; thus the_result_sort_of a = a`1 by A1,MAXdef .= an_Adj by MCART_1:7; len the_arity_of a = Card a`2`1 by A1,MAXdef .= Card [{}, 0]`1 by MCART_1:7 .= 0 by MCART_1:7,CARD_1:47; hence the_arity_of a = {} by CARD_2:59; end; end; registration cluster initialized strict ConstructorSignature; correctness proof take MaxConstrSign; thus thesis; end; end; registration let C be initialized ConstructorSignature; cluster constructor OperSymbol of C; existence proof consider m, a being OperSymbol of C such that A1: the_result_sort_of m = a_Type & the_arity_of m = {} and the_result_sort_of a = an_Adj & the_arity_of a = {} by INITIALIZED; take m; thus m <> * by A1,CONSTRSIGN; thus thesis by A1,CONSTRSIGN; end; end; begin :: Mizar Expressions definition let C be ConstructorSignature; A0: the carrier of C = {a_Type, an_Adj, a_Term} by CONSTRSIGN; func MSVars C -> ManySortedSet of the carrier of C means: MSVARS: it.a_Type = {} & it.an_Adj = {} & it.a_Term = Vars; uniqueness proof let V1,V2 be ManySortedSet of the carrier of C such that A1: V1.a_Type = {} & V1.an_Adj = {} & V1.a_Term = Vars and A2: V2.a_Type = {} & V2.an_Adj = {} & V2.a_Term = Vars; now let x; assume x in the carrier of C; then x = a_Type or x = an_Adj or x = a_Term by A0,ENUMSET1:def 1; hence V1.x = V2.x by A1,A2; end; hence thesis by PBOOLE:3; end; existence proof deffunc F(set) = IFEQ($1, a_Term, Vars, {}); consider V being ManySortedSet of the carrier of C such that A1: for x st x in the carrier of C holds V.x = F(x) from PBOOLE:sch 4; take V; A2: IFEQ(a_Type, a_Term, Vars, {}) = {} & IFEQ(an_Adj, a_Term, Vars, {}) = {} & IFEQ(a_Term, a_Term, Vars, {}) = Vars by FUNCOP_1:def 8; a_Type in the carrier of C & an_Adj in the carrier of C & a_Term in the carrier of C by A0,ENUMSET1:def 1; hence thesis by A1,A2; end; end; :: 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 -> non empty-yielding; coherence proof take a_Term; the carrier of C = {a_Type, an_Adj, a_Term} by CONSTRSIGN; hence a_Term in the carrier of C by ENUMSET1:def 1; thus thesis by MSVARS; end; end; registration let C be initialized ConstructorSignature; cluster Free(C, MSVars C) -> non-empty; correctness proof set X = MSVars C; consider m, a being OperSymbol of C such that A1: the_result_sort_of m = a_Type & the_arity_of m = {} and A2: the_result_sort_of a = an_Adj & the_arity_of a = {} by INITIALIZED; A3: root-tree [m, the carrier of C] in (the Sorts of Free(C, X)).a_Type by A1,MSAFREE3:6; A4: root-tree [a, the carrier of C] in (the Sorts of Free(C, X)).an_Adj by A2,MSAFREE3:6; consider x being variable; a_Term C = a_Term & (MSVars C).a_Term = Vars by MSVARS; then A5: root-tree [x, a_Term] in (the Sorts of Free(C, X)).a_Term by MSAFREE3:5; assume the Sorts of Free(C, X) is not non-empty; then {} in rng the Sorts of Free(C, X) by RELAT_1:def 9; then consider s being set such that A6: s in dom the Sorts of Free(C, X) & {} = (the Sorts of Free(C, X)).s by FUNCT_1:def 5; s in the carrier of C by A6,PBOOLE:def 3; then s in {a_Type, an_Adj, a_Term} by CONSTRSIGN; hence thesis by A3,A4,A5,A6,ENUMSET1:def 1; end; end; definition let S be non void Signature; let X be non empty-yielding ManySortedSet of the carrier of S; let t be Element of Free(S,X); attr t is ground means Union (S variables_in t) = {}; attr t is compound means: COMP: t.{} in [:the OperSymbols of S, {the carrier of S}:]; end; reserve C for initialized ConstructorSignature, s for SortSymbol of C, o for OperSymbol of C, c for constructor OperSymbol of C; definition let C; mode expression of C is Element of Free(C, MSVars C); end; definition let C, s; mode expression of C, s -> expression of C means: ELEMENT: it in (the Sorts of Free(C, MSVars C)).s; existence proof consider t being Element of (the Sorts of Free(C, MSVars C)).s; dom the Sorts of Free(C, MSVars C) = the carrier of C by PBOOLE:def 3; then t in Union the Sorts of Free(C, MSVars C) by CARD_5:10; hence thesis; end; end; theorem Th42: z is expression of C, s iff z in (the Sorts of Free(C, MSVars C)).s proof A1: dom the Sorts of Free(C, MSVars C) = the carrier of C by PBOOLE:def 3; (the Sorts of Free(C, MSVars C)).s c= Union the Sorts of Free(C, MSVars C) proof let x; thus thesis by A1,CARD_5:10; end; hence thesis by ELEMENT; end; definition let C; let c such that A: len the_arity_of c = 0; func c term -> expression of C equals [c, the carrier of C]-tree {}; coherence proof A1: root-tree [c, the carrier of C] in (the Sorts of Free(C, MSVars C)).the_result_sort_of c by MSAFREE3:6,A,CARD_2:59; dom the Sorts of Free(C, MSVars C) = the carrier of C by PBOOLE:def 3; then root-tree [c, the carrier of C] in Union (the Sorts of Free(C, MSVars C)) by A1,CARD_5:10; hence thesis by TREES_4:20; end; end; theorem Th43a: for o st len the_arity_of o = 1 for a being expression of C st ex s 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 proof let o be OperSymbol of C such that A: len the_arity_of o = 1; set X = MSVars C; set Y = X \/ ((the carrier of C)-->{0}); let a be expression of C; given s being SortSymbol of C such that A0: s = (the_arity_of o).1 & a is expression of C, s; reconsider ta = a as Term of C,Y by MSAFREE3:9; A2: dom <*ta*> = Seg 1 & dom <*s*> = Seg 1 by FINSEQ_1:55; A4: the_arity_of o = <*s*> by A,A0,FINSEQ_1:57; B1: the Sorts of Free(C, X) = C-Terms(X, Y) by MSAFREE3:25; now let i be Nat; assume i in dom <*ta*>; then A3: i = 1 by A2,TARSKI:def 1,FINSEQ_1:4; let t be Term of C, Y; assume t = <*ta*>.i; then the Sorts of Free(C, X) c= the Sorts of FreeMSA Y & t = a by B1,A3,FINSEQ_1:57,PBOOLE:def 23; then (the Sorts of Free(C, X)).s c= (the Sorts of FreeMSA Y).s & t in (the Sorts of Free(C, X)).s by A0,Th42,PBOOLE:def 5; hence the_sort_of t = (the_arity_of o).i by A0,A3,MSAFREE3:8; end; then reconsider p = <*ta*> as ArgumentSeq of Sym(o, Y) by A2,A4,MSATERM:25; A5: variables_in (Sym(o, Y)-tree p) c= X proof let s be set; assume s in the carrier of C; then reconsider s' = s as SortSymbol of C; let x; assume x in (variables_in (Sym(o, Y)-tree p)).s; then consider t being DecoratedTree such that B2: t in rng p & x in (C variables_in t).s' by MSAFREE3:12; C variables_in a c= X & rng p = {a} by FINSEQ_1:55,MSAFREE3:28; then (C variables_in a).s' c= X.s' & t = a by B2,TARSKI:def 1,PBOOLE:def 5; hence thesis by B2; end; set s' = the_result_sort_of o; A7: the_sort_of (Sym(o, Y)-tree p) = the_result_sort_of o by MSATERM:20; (the Sorts of Free(C, X)).s' = {t where t is Term of C,Y: the_sort_of t = s' & variables_in t c= X} by B1,MSAFREE3:def 6; then [o, the carrier of C]-tree <*a*> in (the Sorts of Free(C, X)).s' by A5,A7; hence thesis by Th42; end; definition let C,o such that A: len the_arity_of o = 1; let e be expression of C such that B: ex s being SortSymbol of C st s = (the_arity_of o).1 & e is expression of C, s; func o term e -> expression of C equals: TERM1: [o, the carrier of C]-tree<*e*>; coherence by A,B,Th43a; end; reserve a,b for expression of C, an_Adj C; theorem ThNon: (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*> proof A1: the_result_sort_of non_op C = an_Adj C & the_arity_of non_op C = <*an_Adj C*> by CONSTRSIGN; then A2: len the_arity_of non_op C = 1 & (the_arity_of non_op C).1 = an_Adj C by FINSEQ_1:57; then (non_op C)term a = [non_op, the carrier of C]-tree <*a*> by TERM1; hence thesis by A1,A2,Th43a; end; theorem ThNon': (non_op C)term a = (non_op C)term b implies a = b proof assume (non_op C)term a = (non_op C)term b; then [non_op, the carrier of C]-tree <*a*> = (non_op C)term b by ThNon .= [non_op, the carrier of C]-tree <*b*> by ThNon; then <*a*> = <*b*> by TREES_4:15; hence a = b by FINSEQ_1:97; end; registration let C,a; cluster (non_op C)term a -> compound; coherence proof (non_op C)term a = [non_op, the carrier of C]-tree <*a*> by ThNon; then ((non_op C)term a).{} = [non_op C, the carrier of C] by TREES_4:def 4; hence ((non_op C)term a).{} in [:the OperSymbols of C, {the carrier of C}:] by ZFMISC_1:129; end; end; registration let C; cluster compound expression of C; existence proof consider a; (non_op C)term a is compound; hence thesis; end; end; theorem Th43b: for o st len the_arity_of o = 2 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 proof let o be OperSymbol of C such that A: len the_arity_of o = 2; set X = MSVars C; set Y = X \/ ((the carrier of C)-->{0}); let a,b be expression of C; given s1,s2 being SortSymbol of C such that A0: s1 = (the_arity_of o).1 & s2 = (the_arity_of o).2 & a is expression of C, s1 & b is expression of C, s2; reconsider ta = a, tb = b as Term of C,Y by MSAFREE3:9; A2: dom <*ta,tb*> = Seg 2 & dom <*s1,s2*> = Seg 2 by FINSEQ_3:29; A4: the_arity_of o = <*s1,s2*> by A,A0,FINSEQ_1:61; B1: the Sorts of Free(C, X) = C-Terms(X, Y) by MSAFREE3:25; now let i be Nat; assume i in dom <*ta,tb*>; then A3: i = 1 or i = 2 by A2,TARSKI:def 2,FINSEQ_1:4; let t be Term of C, Y; assume t = <*ta,tb*>.i; then the Sorts of Free(C, X) c= the Sorts of FreeMSA Y & (i = 1 & t = a or i = 2 & t = b) by B1,A3,FINSEQ_1:61,PBOOLE:def 23; then (the Sorts of Free(C, X)).s1 c= (the Sorts of FreeMSA Y).s1 & (the Sorts of Free(C, X)).s2 c= (the Sorts of FreeMSA Y).s2 & (i = 1 & t in (the Sorts of Free(C, X)).s1 or i = 2 & t in (the Sorts of Free(C, X)).s2) by A0,Th42,PBOOLE:def 5; hence the_sort_of t = (the_arity_of o).i by A0,MSAFREE3:8; end; then reconsider p = <*ta,tb*> as ArgumentSeq of Sym(o, Y) by A2,A4,MSATERM:25; A5: variables_in (Sym(o, Y)-tree p) c= X proof let s be set; assume s in the carrier of C; then reconsider s' = s as SortSymbol of C; let x; assume x in (variables_in (Sym(o, Y)-tree p)).s; then consider t being DecoratedTree such that B2: t in rng p & x in (C variables_in t).s' by MSAFREE3:12; C variables_in a c= X & C variables_in b c= X & rng p = {a,b} by FINSEQ_2:147,MSAFREE3:28; then (C variables_in a).s' c= X.s' & (C variables_in b).s' c= X.s' & (t = a or t = b) by B2,TARSKI:def 2,PBOOLE:def 5; hence thesis by B2; end; set s' = the_result_sort_of o; A7: the_sort_of (Sym(o, Y)-tree p) = the_result_sort_of o by MSATERM:20; (the Sorts of Free(C, X)).s' = {t where t is Term of C,Y: the_sort_of t = s' & variables_in t c= X} by B1,MSAFREE3:def 6; then [o, the carrier of C]-tree <*a,b*> in (the Sorts of Free(C, X)).s' by A5,A7; hence thesis by Th42; end; definition let C,o such that A: len the_arity_of o = 2; let e1,e2 be expression of C such that B: 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; func o term(e1,e2) -> expression of C equals: TERM2: [o, the carrier of C]-tree<*e1,e2*>; coherence by A,B,Th43b; end; reserve t, t1,t2 for expression of C, a_Type C; theorem ThAst: (ast C)term(a,t) is expression of C, a_Type C & (ast C)term(a,t) = [ *, the carrier of C]-tree <*a,t*> proof A1: the_result_sort_of ast C = a_Type C & the_arity_of ast C = <*an_Adj C, a_Type C*> by CONSTRSIGN; then A2: len the_arity_of ast C = 2 & (the_arity_of ast C).1 = an_Adj C & (the_arity_of ast C).2 = a_Type C by FINSEQ_1:61; then (ast C)term(a,t) = [ *, the carrier of C]-tree <*a,t*> by TERM2; hence thesis by A1,A2,Th43b; end; theorem (ast C)term(a,t1) = (ast C)term(b,t2) implies a = b & t1 = t2 proof assume (ast C)term(a,t1) = (ast C)term(b,t2); then [ *, the carrier of C]-tree<*a,t1*> = (ast C)term(b,t2) by ThAst .= [ *, the carrier of C]-tree<*b,t2*> by ThAst; then <*a,t1*> = <*b,t2*> by TREES_4:15; hence thesis by FINSEQ_1:98; end; registration let C,a,t; cluster (ast C)term(a,t) -> compound; coherence proof (ast C)term(a,t) = [ *, the carrier of C]-tree <*a,t*> by ThAst; then ((ast C)term(a,t)).{} = [ast C, the carrier of C] by TREES_4:def 4; hence ((ast C)term(a,t)).{} in [:the OperSymbols of C, {the carrier of C}:] by ZFMISC_1:129; end; end; definition let S be non void Signature; let s be SortSymbol of S such that A: ex o being OperSymbol of S st the_result_sort_of o = s; mode OperSymbol of s -> OperSymbol of S means the_result_sort_of it = s; existence by A; end; definition let C be ConstructorSignature; redefine func non_op C -> OperSymbol of an_Adj C; coherence proof the_result_sort_of non_op C = an_Adj C by CONSTRSIGN; hence ex o being OperSymbol of C st the_result_sort_of o = an_Adj C; thus thesis by CONSTRSIGN; end; func ast C -> OperSymbol of a_Type C; coherence proof the_result_sort_of ast C = a_Type C by CONSTRSIGN; hence ex o being OperSymbol of C st the_result_sort_of o = a_Type C; thus thesis by CONSTRSIGN; end; end; theorem Th90A: for s1,s2 being SortSymbol of C st s1 <> s2 for t1 being expression of C, s1 for t2 being expression of C, s2 holds t1 <> t2 proof set X = MSVars C; set Y = X \/ ((the carrier of C) --> {0}); consider A being MSSubset of FreeMSA Y such that A1: Free(C, X) = GenMSAlg A & A = (Reverse Y)""X by MSAFREE3:def 2; let s1,s2 be SortSymbol of C; the Sorts of Free(C, X) is MSSubset of FreeMSA Y by A1,MSUALG_2:def 10; then the Sorts of Free(C, X) c= the Sorts of FreeMSA Y by PBOOLE:def 23; then A2: (the Sorts of Free(C,X)).s1 c= (the Sorts of FreeMSA Y).s1 & (the Sorts of Free(C,X)).s2 c= (the Sorts of FreeMSA Y).s2 by PBOOLE:def 5; assume s1 <> s2; then A3: (the Sorts of FreeMSA Y).s1 misses (the Sorts of FreeMSA Y).s2 by PROB_2:def 3; let t1 be expression of C, s1; let t2 be expression of C, s2; t1 in (the Sorts of Free(C,X)).s1 & t2 in (the Sorts of Free(C,X)).s2 by ELEMENT; hence thesis by A2,A3,XBOOLE_0:3; end; begin :: Quasi-terms definition let C; A: (the Sorts of Free(C, MSVars C)).a_Term C c= Union the Sorts of Free(C, MSVars C) proof let x; dom the Sorts of Free(C, MSVars C) = the carrier of C by PBOOLE:def 3; hence thesis by CARD_5:10; end; func QuasiTerms C -> Subset of Free(C, MSVars C) equals (the Sorts of Free(C, MSVars C)).a_Term C; coherence by A; end; registration let C; cluster QuasiTerms C -> non empty constituted-DTrees; coherence proof thus QuasiTerms C is non empty; let x; assume x in QuasiTerms C; then x is expression of C; hence thesis; end; end; definition let C; mode quasi-term of C is expression of C, a_Term C; end; theorem ::? z is quasi-term of C iff z in QuasiTerms C by Th42; definition let x be variable; let C; func x-term C -> quasi-term of C equals root-tree [x, a_Term]; coherence proof (MSVars C).a_Term = Vars & a_Term = a_Term C by MSVARS; then root-tree [x, a_Term] in QuasiTerms C by MSAFREE3:5; hence thesis by Th42; end; end; theorem ThT0: for x1,x2 being variable for C1,C2 being initialized ConstructorSignature st x1-term C1 = x2-term C2 holds x1 = x2 proof let x1,x2 be variable; let C1,C2 be initialized ConstructorSignature; assume x1-term C1 = x2-term C2; then [x1, a_Term] = [x2, a_Term] by TREES_4:4; hence x1 = x2 by ZFMISC_1:33; end; registration let x be variable; let C; cluster x-term C -> non compound; coherence proof a_Term C in the carrier of C; then a_Term C <> the carrier of C; then (x-term C).{} = [x, a_Term C] & a_Term C nin {the carrier of C} by TARSKI:def 1,TREES_4:3; hence (x-term C).{} nin [:the OperSymbols of C, {the carrier of C}:] by ZFMISC_1:106; end; end; theorem Th83: 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)* proof set o = c; A0: o <> * & o <> non_op by CNSTR2; let p be DTree-yielding FinSequence; set V = (MSVars C) \/ ((the carrier of C) --> {0}); BB: the Sorts of Free(C, MSVars C) = C-Terms(MSVars C, V) by MSAFREE3:25; thus now assume A2: [o, the carrier of C]-tree p is expression of C; then CC: [o, the carrier of C]-tree p is Term of C, V by MSAFREE3:9; then A3: p is ArgumentSeq of Sym(o,V) by MSATERM:1; hence len p = len the_arity_of o by MSATERM:22; reconsider q = p as ArgumentSeq of Sym(o,V) by CC,MSATERM:1; A5: the_sort_of ((Sym(o,V))-tree q) = the_result_sort_of o by MSATERM:20; A6: variables_in ((Sym(o,V))-tree q) c= MSVars C by A2,MSAFREE3:28; (C-Terms(MSVars C,V)).the_result_sort_of o = {t where t is Term of C,V: the_sort_of t = the_result_sort_of o & variables_in t c= MSVars C} by MSAFREE3:def 6; then Sym(o,V)-tree p in (C-Terms(MSVars C,V)).the_result_sort_of o by A5,A6; then A4: rng p c= Union (C-Terms(MSVars C,V)) by A3,MSAFREE3:20; rng p c= QuasiTerms C proof let a be set; assume B0: a in rng p; then reconsider ta = a as expression of C by A4,MSAFREE3:25; consider i being set such that B1: i in dom p & a = p.i by B0,FUNCT_1:def 5; reconsider i as Nat by B1,FINSEQ_3:25; reconsider t = p.i as Term of C, V by A3,B1,MSATERM:22; (the Arity of C).o in {a_Term}* by A0,CONSTRSIGN; then dom p = dom the_arity_of o & the_arity_of o is FinSequence of {a_Term} by A3,FINSEQ_1:def 11,MSATERM:22; then (the_arity_of o).i in rng the_arity_of o & rng the_arity_of o c= {a_Term C} by B1,FUNCT_1:def 5,FINSEQ_1:def 4; then (the_arity_of o).i = a_Term C by TARSKI:def 1; then B2: the_sort_of t = a_Term C by A3,B1,MSATERM:23; t = ta by B1; then variables_in t c= MSVars C by MSAFREE3:28; then t in {T where T is Term of C,V: the_sort_of T = a_Term C & variables_in T c= MSVars C} by B2; then t in (C-Terms(MSVars C,V)).a_Term C by MSAFREE3:def 6; hence thesis by B1,MSAFREE3:24; end; then p is FinSequence of QuasiTerms C by FINSEQ_1:def 4; hence p in (QuasiTerms C)* by FINSEQ_1:def 11; end; assume A3: len p = len the_arity_of o; assume A4: p in (QuasiTerms C)*; C-Terms(MSVars C, V) is opers_closed & Free(C, MSVars C) = (FreeMSA V)|(C-Terms(MSVars C, V)) by MSAFREE3:22,26; then the Sorts of Free(C, MSVars C) is ManySortedSubset of the Sorts of FreeMSA V by MSUALG_2:def 10; then the Sorts of Free(C, MSVars C) c= the Sorts of FreeMSA V by PBOOLE:def 23; then A7: QuasiTerms C c= (the Sorts of FreeMSA V).a_Term C by PBOOLE:def 5; 0B: p is FinSequence of QuasiTerms C by A4,FINSEQ_1:def 11; then B0: rng p c= QuasiTerms C by FINSEQ_1:def 4; now let i be Nat; assume B1: i in dom p; then p.i in rng p by FUNCT_1:def 5; then B3: p.i in QuasiTerms C by B0; then reconsider t = p.i as expression of C; (the Arity of C).o in {a_Term}* by A0,CONSTRSIGN; then dom p = dom the_arity_of o & the_arity_of o is FinSequence of {a_Term} by A3,FINSEQ_3:31,FINSEQ_1:def 11; then (the_arity_of o).i in rng the_arity_of o & rng the_arity_of o c= {a_Term C} by B1,FUNCT_1:def 5,FINSEQ_1:def 4; then B2: (the_arity_of o).i = a_Term C by TARSKI:def 1; reconsider T = t as Term of C,V by MSAFREE3:9; take T; thus T = p.i; T in (the Sorts of FreeMSA V).a_Term C by B3,A7; then T in FreeSort(V, a_Term C) by MSAFREE:def 13; hence the_sort_of T = (the_arity_of o).i by B2,MSATERM:def 5; end; then A5: p is ArgumentSeq of Sym(o,V) by A3,MSATERM:24; A6: dom the Sorts of Free(C, MSVars C) = the carrier of C by PBOOLE:def 3; rng p c= Union (C-Terms(MSVars C, V)) by BB,0B,FINSEQ_1:def 4; then Sym(o,V)-tree p in (C-Terms(MSVars C, V)).the_result_sort_of o by A5,MSAFREE3:20; hence [o, the carrier of C]-tree p is expression of C by BB,A6,CARD_5:10; end; reserve p for FinSequence of QuasiTerms C; definition let C,c; let p such that A: len p = len the_arity_of c; B: p in (QuasiTerms C)* by FINSEQ_1:def 11; func c-trm p -> compound expression of C equals: TERM: [c, the carrier of C]-tree p; coherence proof reconsider t = [c, the carrier of C]-tree p as expression of C by A,B,Th83; t.{} = [c, the carrier of C] by TREES_4:def 4; then t.{} in [:the OperSymbols of C, {the carrier of C}:] by ZFMISC_1:129; hence thesis by COMP; end; end; theorem Th43c: len p = len the_arity_of c implies c-trm p is expression of C, the_result_sort_of c proof set X = MSVars C; set V = X\/((the carrier of C)-->{0}); assume len p = len the_arity_of c; then A0: Sym(c,V)-tree p = c-trm p by TERM; A1: the Sorts of Free(C,X) = C-Terms(X,V) by MSAFREE3:25; c-trm p is Term of C,V by MSAFREE3:9; then reconsider q = p as ArgumentSeq of Sym(c,V) by A0,MSATERM:1; rng q c= Union the Sorts of Free(C,X) by FINSEQ_1:def 4; then c-trm p in (C-Terms(X,V)).the_result_sort_of c by A0,A1,MSAFREE3:20; hence c-trm p is expression of C, the_result_sort_of c by A1,ELEMENT; end; theorem Th100: for e being expression of C holds (ex x being variable st e = x-term C) or (ex c being constructor OperSymbol of C st 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 st ex t being expression of C, a_Type C st e = (ast C)term(a,t)) proof let t be expression of C; set X = MSVars C; set V = X\/((the carrier of C)-->{0}); per cases by LemExp; suppose ex s being SortSymbol of C, v being set st t = root-tree [v,s] & v in X.s; then consider s being SortSymbol of C, v being set such that 01: t = root-tree [v,s] & v in X.s; {} in dom t by TREES_1:47; then t.{} in rng t & the carrier of C = {a_Type, an_Adj, a_Term} by CONSTRSIGN,FUNCT_1:12; then 02: v in X.s & (s = a_Term or s = an_Adj or s = a_Type) by 01,ENUMSET1:def 1; then reconsider v as variable by MSVARS; t = v-term C by 01,02,MSVARS; hence thesis; end; suppose ex o being OperSymbol of C, p being FinSequence of Free(C,X) st t = [o,the carrier of C]-tree p & len p = len the_arity_of o & p is DTree-yielding & p is ArgumentSeq of Sym(o,V); then consider o being OperSymbol of C, p being FinSequence of Free(C,X) such that 03: t = [o, the carrier of C]-tree p & len p = len the_arity_of o and 04: p is DTree-yielding & p is ArgumentSeq of Sym(o,V); per cases by CNSTR2; suppose o = *; then 05: the_arity_of o = <*an_Adj,a_Type*> & o = ast C & the_result_sort_of o = a_Type by CONSTRSIGN; then 06: dom p = dom the_arity_of o & dom the_arity_of o = Seg 2 & len the_arity_of o = 2 by 04,MSATERM:22,FINSEQ_3:29,FINSEQ_1:61; 07: 1 in Seg 2 & 2 in Seg 2; then p.1 in rng p & p.2 in rng p by 06,FUNCT_1:12; then reconsider p1 = p.1, p2 = p.2 as expression of C; reconsider t1 = p1, t2 = p2 as Term of C,V by MSAFREE3:9; 08: C variables_in p1 c= X & variables_in t1 = C variables_in t1 & C variables_in p2 c= X & variables_in t2 = C variables_in t2 by MSAFREE3:28; 09: <*an_Adj,a_Type*>.2 = a_Type C & <*an_Adj,a_Type*>.1 = an_Adj C by FINSEQ_1:61; the_sort_of t1 = (the_arity_of o).1 by 04,06,07,MSATERM:23; then t1 in {q where q is Term of C,V: the_sort_of q = an_Adj C & variables_in q c= X} by 05,08,09; then p1 in C-Terms(X,V).an_Adj C by MSAFREE3:def 6; then p1 in (the Sorts of Free(C,X)).an_Adj C by MSAFREE3:25; then reconsider a = p1 as expression of C, an_Adj C by ELEMENT; the_sort_of t2 = (the_arity_of o).2 by 04,06,07,MSATERM:23; then t2 in {q where q is Term of C,V: the_sort_of q = a_Type C & variables_in q c= X} by 05,08,09; then p2 in C-Terms(X,V).a_Type C by MSAFREE3:def 6; then p2 in (the Sorts of Free(C,X)).a_Type C by MSAFREE3:25; then reconsider q = p2 as expression of C, a_Type C by ELEMENT; p = <*a,q*> by 03,06,FINSEQ_1:61; then t = (ast C)term(a,q) by 03, 05,06,09,TERM2; hence thesis; end; suppose o = non_op; then 05: the_arity_of o = <*an_Adj*> & o = non_op C & the_result_sort_of o = an_Adj by CONSTRSIGN; then 06: dom p = dom the_arity_of o & dom the_arity_of o = Seg 1 & len the_arity_of o = 1 by 04,MSATERM:22,FINSEQ_1:55,56; 07: 1 in Seg 1; then p.1 in rng p by 06,FUNCT_1:12; then reconsider p1 = p.1 as expression of C; reconsider t1 = p1 as Term of C,V by MSAFREE3:9; 08: C variables_in p1 c= X & variables_in t1 = C variables_in t1 by MSAFREE3:28; 09: <*an_Adj*>.1 = an_Adj C by FINSEQ_1:57; the_sort_of t1 = (the_arity_of o).1 by 04,06,07,MSATERM:23; then t1 in {q where q is Term of C,V: the_sort_of q = an_Adj C & variables_in q c= X} by 05,08,09; then p1 in C-Terms(X,V).an_Adj C by MSAFREE3:def 6; then p1 in (the Sorts of Free(C,X)).an_Adj C by MSAFREE3:25; then reconsider a = p1 as expression of C, an_Adj C by ELEMENT; p = <*a*> by 03,06,FINSEQ_1:57; then t = (non_op C)term(a) by 03,05,06,09,TERM1; hence thesis; end; suppose o is constructor; then reconsider o as constructor OperSymbol of C; t = [o, the carrier of C]-tree p by 03; then p in (QuasiTerms C)* by Th83; then reconsider p as FinSequence of QuasiTerms C by FINSEQ_1:def 11; t = o-trm p by 03,TERM; hence thesis by 03; end; end; end; theorem ThDiff01: len p = len the_arity_of c implies c-trm p <> (non_op C)term a proof assume len p = len the_arity_of c; then c-trm p = [c, the carrier of C]-tree p by TERM; then A0: (c-trm p).{} = [c, the carrier of C] by TREES_4:def 4; assume c-trm p = (non_op C)term a; then c-trm p = [non_op, the carrier of C]-tree<*a*> by ThNon; then [c, the carrier of C] = [non_op, the carrier of C] by A0,TREES_4:def 4;then c = non_op by ZFMISC_1:33; hence thesis by CNSTR2; end; theorem ThDiff02: len p = len the_arity_of c implies c-trm p <> (ast C)term(a,t) proof assume len p = len the_arity_of c; then c-trm p = [c, the carrier of C]-tree p by TERM; then A0: (c-trm p).{} = [c, the carrier of C] by TREES_4:def 4; assume c-trm p = (ast C)term(a,t); then c-trm p = [ *, the carrier of C]-tree<*a,t*> by ThAst; then [c, the carrier of C] = [ *, the carrier of C] by A0,TREES_4:def 4;then c = * by ZFMISC_1:33; hence thesis by CNSTR2; end; theorem (non_op C)term a <> (ast C)term(b,t) proof assume (non_op C)term a = (ast C)term(b,t); then (non_op C)term a = [ *, the carrier of C]-tree<*b,t*> by ThAst; then ((non_op C)term a).{} = [ *, the carrier of C] by TREES_4:def 4; then ([non_op,the carrier of C]-tree<*a*>).{} = [ *, the carrier of C] by ThNon; then [non_op, the carrier of C] = [ *, the carrier of C] by TREES_4:def 4; hence thesis by ZFMISC_1:33; end; reserve e for expression of C; theorem ThNon2: e.{} = [non_op, the carrier of C] implies ex a st e = (non_op C)term a proof assume A0: e.{} = [non_op, the carrier of C]; non_op C in the OperSymbols of C; then A1: e.{} in [:the OperSymbols of C, {the carrier of C}:] by A0,ZFMISC_1:129; per cases by Th100; suppose ex x being variable st e = x-term C; hence thesis by A1,COMP; end; suppose ex c,p st len p = len the_arity_of c & e = c-trm p; then consider c being constructor OperSymbol of C, p being FinSequence of QuasiTerms C such that A2: len p = len the_arity_of c & e = c-trm p; e = [c, the carrier of C]-tree p by A2,TERM; then e.{} = [c, the carrier of C] by TREES_4:def 4; then non_op = c by A0,ZFMISC_1:33; hence thesis by CNSTR2; end; suppose ex a st e = (non_op C)term a; hence thesis; end; suppose ex a,t st e = (ast C)term(a,t); then consider a,t such that A3: e = (ast C)term(a,t); e = [ *, the carrier of C]-tree <*a,t*> by A3,ThAst; then e.{} = [ *, the carrier of C] by TREES_4:def 4; hence thesis by A0,ZFMISC_1:33; end; end; theorem ThAst2: e.{} = [ *, the carrier of C] implies ex a, t st e = (ast C)term(a,t) proof assume A0: e.{} = [ *, the carrier of C]; ast C in the OperSymbols of C; then A1: e.{} in [:the OperSymbols of C, {the carrier of C}:] by A0,ZFMISC_1:129; per cases by Th100; suppose ex x being variable st e = x-term C; hence thesis by A1,COMP; end; suppose ex c,p st len p = len the_arity_of c & e = c-trm p; then consider c being constructor OperSymbol of C, p being FinSequence of QuasiTerms C such that A2: len p = len the_arity_of c & e = c-trm p; e = [c, the carrier of C]-tree p by A2,TERM; then e.{} = [c, the carrier of C] by TREES_4:def 4; then * = c by A0,ZFMISC_1:33; hence thesis by CNSTR2; end; suppose ex a being expression of C, an_Adj C st e = (non_op C)term a; then consider a being expression of C, an_Adj C such that A3: e = (non_op C)term a; e = [non_op, the carrier of C]-tree <*a*> by A3,ThNon; then e.{} = [non_op, the carrier of C] by TREES_4:def 4; hence thesis by A0,ZFMISC_1:33; end; suppose ex a,t st e = (ast C)term(a,t); hence thesis; end; end; begin :: Quasi-adjectives reserve a,a' for expression of C, an_Adj C; definition let C,a; func Non a -> expression of C, an_Adj C equals: NON'OPA: a|<* 0 *> if ex a' st a = (non_op C)term a' otherwise (non_op C)term a; coherence proof thus now given a' being expression of C, an_Adj C such that A0: a = (non_op C)term a'; A1: a = [non_op, the carrier of C]-tree <*a'*> by A0,ThNon; 0 < 1 & len <*a'*> = 1 by FINSEQ_1:57; then a|<* 0*> = <*a'*>.(0+1) by A1,TREES_4:def 4; hence a|<* 0*> is expression of C, an_Adj C by FINSEQ_1:57; end; thus thesis by ThNon; end; consistency; end; definition let C,a; attr a is positive means: POSITIVE: not ex a' st a = (non_op C)term a'; end; registration let C; cluster positive expression of C, an_Adj C; existence proof consider m, a being OperSymbol of C such that the_result_sort_of m = a_Type & the_arity_of m = {} and A2: the_result_sort_of a = an_Adj & the_arity_of a = {} by INITIALIZED; set X = MSVars C; root-tree [a, the carrier of C] in (the Sorts of Free(C, X)).an_Adj & an_Adj C = an_Adj by A2,MSAFREE3:6; then reconsider v = root-tree [a, the carrier of C] as expression of C, an_Adj C by Th42; take v; given a' being expression of C, an_Adj C such that A1: v = (non_op C)term a'; v = [non_op, the carrier of C]-tree<*a'*> by A1,ThNon; then [non_op, the carrier of C] = v.{} by TREES_4:def 4 .= [a, the carrier of C] by TREES_4:3; then a = non_op C by ZFMISC_1:33; hence contradiction by A2,CONSTRSIGN; end; end; theorem Th44: for a being positive expression of C, an_Adj C holds Non a = (non_op C)term a proof let a be positive expression of C, an_Adj C; not ex a' being expression of C, an_Adj C st a = (non_op C)term a' by POSITIVE; hence thesis by NON'OPA; end; definition let C,a; attr a is negative means: NEGATIVE: ex a' st a' is positive & a = (non_op C)term a'; end; registration let C; let a be positive expression of C, an_Adj C; cluster Non a -> negative non positive; coherence proof thus Non a is negative proof take a; thus thesis by Th44; end; take a; thus thesis by Th44; end; end; registration let C; cluster negative non positive expression of C, an_Adj C; existence proof consider a being positive expression of C, an_Adj C; take Non a; thus thesis; end; end; theorem Th45g: for a being non positive expression of C, an_Adj C ex a' being expression of C, an_Adj C st a = (non_op C)term a' & Non a = a' proof let a be non positive expression of C, an_Adj C; consider a' being expression of C, an_Adj C such that A1: a = (non_op C)term a' by POSITIVE; A2: a = [non_op, the carrier of C]-tree<*a'*> by A1,ThNon; take a'; 0 < 1 & len <*a'*> = 1 by FINSEQ_1:57; then a|<* 0*> = <*a'*>.(0+1) by A2,TREES_4:def 4 .= a' by FINSEQ_1:57; hence thesis by A1,NON'OPA; end; theorem Th45: for a being negative expression of C, an_Adj C ex a' being positive expression of C, an_Adj C st a = (non_op C)term a' & Non a = a' proof let a be negative expression of C, an_Adj C; consider a' being expression of C, an_Adj C such that A1: a' is positive & a = (non_op C)term a' by NEGATIVE; A2: a = [non_op, the carrier of C]-tree<*a'*> by A1,ThNon; reconsider a' as positive expression of C, an_Adj C by A1; take a'; 0 < 1 & len <*a'*> = 1 by FINSEQ_1:57; then a|<* 0*> = <*a'*>.(0+1) by A2,TREES_4:def 4 .= a' by FINSEQ_1:57; hence thesis by A1,NON'OPA; end; theorem Th44b: for a being non positive expression of C, an_Adj C holds (non_op C)term (Non a) = a proof let a be non positive expression of C, an_Adj C; consider a' being expression of C, an_Adj C such that A1: a = (non_op C)term a' & Non a = a' by Th45g; thus thesis by A1; end; registration let C; let a be negative expression of C, an_Adj C; cluster Non a -> positive; coherence proof ex a' being positive expression of C, an_Adj C st a = (non_op C)term a' & Non a = a' by Th45; hence thesis; end; end; definition let C,a; attr a is regular means: REG: a is positive or a is negative; end; registration let C; cluster positive -> regular non negative expression of C, an_Adj C; coherence proof let a be expression of C, an_Adj C; assume A1: a is positive; hence a is regular by REG; thus not ex a' being expression of C, an_Adj C st a' is positive & a = (non_op C)term a' by A1,POSITIVE; end; cluster negative -> regular non positive expression of C, an_Adj C; coherence proof let a be expression of C, an_Adj C; assume A1: a is negative; hence a is regular by REG; ex a' being expression of C, an_Adj C st a' is positive & a = (non_op C)term a' by A1,NEGATIVE; hence ex a' being expression of C, an_Adj C st a = (non_op C)term a'; end; end; registration let C; cluster regular expression of C, an_Adj C; existence proof consider a being positive expression of C, an_Adj C; take a; thus thesis; end; end; definition let C; set X = {a: a is regular}; B: X c= Union the Sorts of Free(C, MSVars C) proof let x; assume x in X; then ex a st x = a & a is regular; hence thesis; end; func QuasiAdjs C -> Subset of Free(C, MSVars C) equals {a: a is regular}; coherence by B; end; registration let C; cluster QuasiAdjs C -> non empty constituted-DTrees; coherence proof consider v being positive expression of C, an_Adj C; v in {a: a is regular}; hence QuasiAdjs C is non empty; let x; assume x in QuasiAdjs C; then x is expression of C; hence thesis; end; end; definition let C; mode quasi-adjective of C is regular expression of C, an_Adj C; end; theorem Th52: z is quasi-adjective of C iff z in QuasiAdjs C proof z in QuasiAdjs C iff ex a st z = a & a is regular; hence thesis; end; theorem ::? 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 REG; registration let C; cluster non positive -> negative quasi-adjective of C; coherence by REG; cluster non negative -> positive quasi-adjective of C; coherence by REG; end; registration let C; cluster positive quasi-adjective of C; existence proof consider a being positive expression of C, an_Adj C; a is quasi-adjective of C; hence thesis; end; cluster negative quasi-adjective of C; existence proof consider a being negative expression of C, an_Adj C; a is quasi-adjective of C; hence thesis; end; end; theorem ThPos: 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 st len p = len the_arity_of v & a = v-trm p proof let e be positive quasi-adjective of C; per cases by Th100; suppose ex x being variable st e = x-term C; hence thesis by Th90A; end; suppose ex c being constructor OperSymbol of C st ex p being FinSequence of QuasiTerms C st len p = len the_arity_of c & e = c-trm p; then consider c being constructor OperSymbol of C, p being FinSequence of QuasiTerms C such that A2: len p = len the_arity_of c & e = c-trm p; take c; e is expression of C, the_result_sort_of c by A2,Th43c; hence the_result_sort_of c = an_Adj C by Th90A; take p; thus len p = len the_arity_of c & e = c-trm p by A2; end; suppose ex a st e = (non_op C)term a; hence thesis by POSITIVE; end; suppose ex a,t st e = (ast C)term(a,t); then e is expression of C, a_Type C by ThAst; hence thesis by Th90A; end; end; theorem ThPos2: 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 proof let v be constructor OperSymbol of C such that A0: the_result_sort_of v = an_Adj C; assume A1: len p = len the_arity_of v; then reconsider a = v-trm p as expression of C, an_Adj C by A0,Th43c; a is positive proof assume ex a' st a = (non_op C)term a'; hence thesis by A1,ThDiff01; end; then a is positive expression of C, an_Adj C; hence v-trm p is positive quasi-adjective of C; end; registration let C; let a be quasi-adjective of C; cluster Non a -> regular; coherence proof per cases by REG; suppose a is positive; then reconsider a' = a as positive expression of C, an_Adj C; Non a' is negative; hence thesis; end; suppose a is negative; then reconsider a' = a as negative expression of C, an_Adj C; Non a' is positive; hence thesis; end; end; end; theorem Th46: for a being quasi-adjective of C holds Non Non a = a proof let a be quasi-adjective of C; per cases by REG; suppose a is positive; then reconsider a' = a as positive expression of C, an_Adj C; consider b being positive expression of C, an_Adj C such that A1: Non a' = (non_op C)term b & Non Non a' = b by Th45; Non a' = (non_op C)term a by Th44; hence thesis by A1,ThNon'; end; suppose a is negative; then reconsider a' = a as negative expression of C, an_Adj C; ex b being positive expression of C, an_Adj C st a' = (non_op C)term b & Non a' = b by Th45; hence thesis by Th44; end; end; theorem for a1,a2 being quasi-adjective of C st Non a1 = Non a2 holds a1 = a2 proof let a1,a2 be quasi-adjective of C; Non Non a1 = a1 & Non Non a2 = a2 by Th46; hence thesis; end; theorem for a being quasi-adjective of C holds Non a <> a proof let a be quasi-adjective of C; per cases by REG; suppose a is positive; then reconsider a' = a as positive quasi-adjective of C; Non a' is negative quasi-adjective of C; hence thesis; end; suppose a is negative; then reconsider a' = a as negative quasi-adjective of C; Non a' is positive quasi-adjective of C; hence thesis; end; end; begin :: Quasi-types definition let C; let q be expression of C, a_Type C; attr q is pure means: PURE: not ex a, t st q = (ast C)term(a,t); end; theorem ThP: for m being OperSymbol of C st the_result_sort_of m = a_Type & the_arity_of m = {} ex t st t = root-tree [m, the carrier of C] & t is pure proof let m be OperSymbol of C such that A2: the_result_sort_of m = a_Type & the_arity_of m = {}; set X = MSVars C; root-tree [m, the carrier of C] in (the Sorts of Free(C, X)).a_Type & a_Type C = a_Type by A2,MSAFREE3:6; then reconsider T = root-tree [m, the carrier of C] as expression of C, a_Type C by Th42; take T; thus T = root-tree [m, the carrier of C]; given a,t such that A1: T = (ast C)term(a,t); T = [ *, the carrier of C]-tree<*a,t*> by A1,ThAst; then [ *, the carrier of C] = T.{} by TREES_4:def 4 .= [m, the carrier of C] by TREES_4:3; then m = ast C by ZFMISC_1:33; hence contradiction by A2,CONSTRSIGN; end; theorem ThP2: for v being OperSymbol of C st the_result_sort_of v = an_Adj & the_arity_of v = {} ex a st a = root-tree [v, the carrier of C] & a is positive proof let m be OperSymbol of C such that A2: the_result_sort_of m = an_Adj & the_arity_of m = {}; set X = MSVars C; root-tree [m, the carrier of C] in (the Sorts of Free(C, X)).an_Adj by A2,MSAFREE3:6; then reconsider T = root-tree [m, the carrier of C] as expression of C, an_Adj C by Th42; take T; thus T = root-tree [m, the carrier of C]; given a being expression of C, an_Adj C such that A1: T = (non_op C)term a; T = [non_op, the carrier of C]-tree<*a*> by A1,ThNon; then [non_op, the carrier of C] = T.{} by TREES_4:def 4 .= [m, the carrier of C] by TREES_4:3; then m = non_op by ZFMISC_1:33; hence contradiction by A2,CONSTRSIGN; end; registration let C; cluster pure expression of C, a_Type C; existence proof consider m, a being OperSymbol of C such that A2: the_result_sort_of m = a_Type & the_arity_of m = {} and the_result_sort_of a = an_Adj & the_arity_of a = {} by INITIALIZED; ex t being expression of C, a_Type C st t = root-tree [m, the carrier of C] & t is pure by A2,ThP; hence thesis; end; end; reserve q for pure expression of C, a_Type C, A for finite Subset of QuasiAdjs C; definition let C; func QuasiTypes C equals {[A,t]: t is pure}; coherence; end; registration let C; cluster QuasiTypes C -> non empty; coherence proof consider q; {} is finite Subset of QuasiAdjs C by XBOOLE_1:2; then [{},q] in {[A,t]: t is pure}; hence thesis; end; end; definition let C; mode quasi-type of C means: QUASITYPE: it in QuasiTypes C; existence proof consider T being Element of QuasiTypes C; take T; thus thesis; end; end; theorem Th54: z is quasi-type of C iff ex A,q st z = [A,q] proof z in QuasiTypes C iff ex t,A st z = [A,t] & t is pure; hence thesis by QUASITYPE; end; theorem Th55: [x,y] is quasi-type of C iff x is finite Subset of QuasiAdjs C & y is pure expression of C, a_Type C proof thus now assume [x,y] is quasi-type of C; then consider A,q such that A1: [x,y] = [A,q] by Th54; thus x is finite Subset of QuasiAdjs C & y is pure expression of C, a_Type C by A1,ZFMISC_1:33; end; thus thesis by Th54; end; reserve T for quasi-type of C; registration let C; cluster -> pair quasi-type of C; coherence proof let x be quasi-type of C; ex A,q st x = [A,q] by Th54; hence thesis; end; end; theorem ThPure: ex m being constructor OperSymbol of C st the_result_sort_of m = a_Type C & ex p st len p = len the_arity_of m & q = m-trm p proof set e = q; per cases by Th100; suppose ex x being variable st e = x-term C; hence thesis by Th90A; end; suppose ex c being constructor OperSymbol of C st ex p being FinSequence of QuasiTerms C st len p = len the_arity_of c & e = c-trm p; then consider c being constructor OperSymbol of C, p being FinSequence of QuasiTerms C such that A2: len p = len the_arity_of c & e = c-trm p; take c; e is expression of C, the_result_sort_of c by A2,Th43c; hence the_result_sort_of c = a_Type C by Th90A; take p; thus len p = len the_arity_of c & e = c-trm p by A2; end; suppose ex a st e = (non_op C)term a; then e is expression of C, an_Adj C by ThNon; hence thesis by Th90A; end; suppose ex a st ex q being expression of C, a_Type C st e = (ast C)term(a,q); hence thesis by PURE; end; end; theorem ThPure2: 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 proof let v be constructor OperSymbol of C such that A0: the_result_sort_of v = a_Type C; assume A1: len p = len the_arity_of v; then reconsider a = v-trm p as expression of C, a_Type C by A0,Th43c; a is pure proof assume ex a',t st a = (ast C)term(a',t); hence thesis by A1,ThDiff02; end; hence v-trm p is pure expression of C, a_Type C; end; theorem QuasiTerms C misses QuasiAdjs C & QuasiTerms C misses QuasiTypes C & QuasiTypes C misses QuasiAdjs C proof set X = MSVars C; set Y = X \/ ((the carrier of C) --> {0}); consider A being MSSubset of FreeMSA Y such that A1: Free(C, X) = GenMSAlg A & A = (Reverse Y)""X by MSAFREE3:def 2; the Sorts of Free(C, X) is MSSubset of FreeMSA Y by A1,MSUALG_2:def 10; then A2: the Sorts of Free(C, X) c= the Sorts of FreeMSA Y by PBOOLE:def 23; A3: QuasiTerms C c= (the Sorts of FreeMSA Y).a_Term C by A2,PBOOLE:def 5; A4: (the Sorts of Free(C,X)).an_Adj C c= (the Sorts of FreeMSA Y).an_Adj C by A2,PBOOLE:def 5; QuasiAdjs C c= (the Sorts of Free(C,X)).an_Adj C proof let x; assume x in QuasiAdjs C; then ex a st x = a & a is regular; hence thesis by ELEMENT; end; then A5: QuasiAdjs C c= (the Sorts of FreeMSA Y).an_Adj C by A4,XBOOLE_1:1; (the Sorts of FreeMSA Y).a_Term C misses (the Sorts of FreeMSA Y).an_Adj C by PROB_2:def 3; hence QuasiTerms C misses QuasiAdjs C by A3,A5,XBOOLE_1:64; now let x be set; assume x in QuasiTerms C & x in QuasiTypes C; then x is quasi-term of C & x is quasi-type of C by Th42,QUASITYPE; hence contradiction; end; hence QuasiTerms C misses QuasiTypes C by XBOOLE_0:3; now let x be set; assume x in QuasiAdjs C & x in QuasiTypes C; then x is quasi-adjective of C & x is quasi-type of C by Th52,QUASITYPE; hence contradiction; end; hence thesis by XBOOLE_0:3; end; theorem ::? for e being set holds (e is quasi-term of C implies e is not quasi-adjective of C) & (e is quasi-term of C implies e is not quasi-type of C) & (e is quasi-type of C implies e is not quasi-adjective of C) by Th90A; notation let C,A,q; synonym A ast q for [A,q]; end; definition let C,A,q; redefine func A ast q -> quasi-type of C; coherence by Th55; end; registration let C,T; cluster T`1 -> finite; coherence proof ex A,q st T = [A,q] by Th54; hence thesis by MCART_1:7; end; end; notation let C,T; synonym adjs T for T`1; synonym the_base_of T for T`2; end; definition let C,T; redefine func adjs T -> Subset of QuasiAdjs C; coherence proof ex A,q st T = [A,q] by Th54; hence thesis by MCART_1:7; end; func the_base_of T -> pure expression of C, a_Type C; coherence proof ex A,q st T = [A,q] by Th54; hence thesis by MCART_1:7; end; end; theorem ::? adjs (A ast q) = A & the_base_of (A ast q) = q by MCART_1:7; theorem ::? 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 ZFMISC_1:33; theorem Th59: T = (adjs T) ast the_base_of T proof ex A,q st T = [A,q] by Th54; hence thesis by MCART_1:8; end; theorem for T1,T2 being quasi-type of C st adjs T1 = adjs T2 & the_base_of T1 = the_base_of T2 holds T1 = T2 proof let T1,T2 be quasi-type of C; T1 = (adjs T1) ast the_base_of T1 by Th59; hence thesis by Th59; end; definition let C,T; let a be quasi-adjective of C; func a ast T -> quasi-type of C equals [{a} \/ adjs T, the_base_of T]; coherence proof a in QuasiAdjs C; then {a} c= QuasiAdjs C by ZFMISC_1:37; then {a} \/ adjs T is Subset of QuasiAdjs C by XBOOLE_1:8; hence thesis by Th55; end; end; theorem ::? 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 for a being quasi-adjective of C holds a ast (a ast T) = a ast T proof let a be quasi-adjective of C; thus a ast (a ast T) = [{a} \/ ({a} \/ adjs T), the_base_of (a ast T)] by MCART_1:7 .= [{a} \/ {a} \/ adjs T, the_base_of (a ast T)] by XBOOLE_1:4 .= a ast T by MCART_1:7; end; theorem for a,b being quasi-adjective of C holds a ast (b ast T) = b ast (a ast T) proof let a,b be quasi-adjective of C; thus a ast (b ast T) = [{a} \/ ({b} \/ adjs T), the_base_of (b ast T)] by MCART_1:7 .= [{b} \/ ({a} \/ adjs T), the_base_of (b ast T)] by XBOOLE_1:4 .= [{b} \/ ({a} \/ adjs T), the_base_of T] by MCART_1:7 .= [{b} \/ adjs (a ast T), the_base_of T] by MCART_1:7 .= b ast (a ast T) by MCART_1:7; end; begin :: Variables in quasi-types registration let S be non void Signature; let s be SortSymbol of S; let X be non-empty ManySortedSet of the carrier of S; let t be Term of S,X; cluster (variables_in t).s -> finite; coherence proof defpred P[non empty Relation] means for s being SortSymbol of S holds (S variables_in $1).s is finite; A1: for z being SortSymbol of S, v being Element of X.z holds P[root-tree[v,z]] proof let z be SortSymbol of S, v be Element of X.z; let s be SortSymbol of S; s = z or s <> z; hence thesis by MSAFREE3:11; end; A2: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X) st for t being Term of S,X st t in rng p holds P[t] holds P[[o,the carrier of S]-tree p] proof let o be OperSymbol of S, p be ArgumentSeq of Sym(o,X) such that B1: for t being Term of S,X st t in rng p for s being SortSymbol of S holds (S variables_in t).s is finite; let s be SortSymbol of S; deffunc F(Term of S,X) = (S variables_in $1).s; set A = {F(q) where q is Term of S,X: q in rng p}; B2: rng p is finite; B3: A is finite from FRAENKEL:sch 21(B2); now let B be set; assume B in A; then ex q being Term of S,X st B = (S variables_in q).s & q in rng p; hence B is finite by B1; end; then B5: union A is finite by B3,FINSET_1:25; (S variables_in ([o,the carrier of S]-tree p)).s c= union A proof let x be set; assume x in (S variables_in ([o,the carrier of S]-tree p)).s; then consider t being DecoratedTree such that B6: t in rng p & x in (S variables_in t).s by MSAFREE3:12; consider i being set such that B7: i in dom p & t = p.i by B6,FUNCT_1:def 5; reconsider i as Nat by B7,ORDINAL1:def 13; reconsider t = p.i as Term of S,X by B7,MSATERM:22; (S variables_in t).s in A by B6,B7; hence thesis by B6,B7,TARSKI:def 4; end; hence thesis by B5,FINSET_1:13; end; for t being Term of S,X holds P[t] from MSATERM:sch 1(A1,A2); hence thesis; end; end; registration let S be non void Signature; let s be SortSymbol of S; let X be non empty-yielding ManySortedSet of the carrier of S; let t be Element of Free(S,X); cluster (S variables_in t).s -> finite; coherence proof reconsider t as Term of S, X \/ ((the carrier of S) --> {0}) by MSAFREE3:9; (S variables_in t).s = (variables_in t).s; hence thesis; end; end; definition let S be non void Signature; let X be non empty-yielding 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: VARS'INF: for t being Element of Free(S,X) holds it.t = (S variables_in t).s; uniqueness proof let f1,f2 be Function of Union the Sorts of Free(S,X), bool (X.s) such that A1: for t being Element of Free(S,X) holds f1.t = (S variables_in t).s and A2: for t being Element of Free(S,X) holds f2.t = (S variables_in t).s; now let x be Element of Union the Sorts of Free(S,X); reconsider t = x as Element of Free(S,X); thus f1.x = (S variables_in t).s by A1 .= f2.x by A2; end; hence thesis by FUNCT_2:113; end; existence proof defpred P[set,set] means ex t being Element of Free(S,X) st t = $1 & $2 = (S variables_in t).s; A3: now let x; assume x in Union the Sorts of Free(S,X); then reconsider t = x as Element of Free(S,X); S variables_in t c= X by MSAFREE3:28; then (S variables_in t).s c= X.s by PBOOLE:def 5; hence ex y st y in bool (X.s) & P[x,y]; end; consider f being Function such that A4: dom f = Union the Sorts of Free(S,X) & rng f c= bool (X.s) and A5: for x st x in Union the Sorts of Free(S,X) holds P[x, f.x] from WELLORD2:sch 1(A3); reconsider f as Function of Union the Sorts of Free(S,X), bool (X.s) by A4,FUNCT_2:4; take f; let x be Element of Free(S,X); ex t being Element of Free(S,X) st t = x & f.x = (S variables_in t).s by A5; hence thesis; end; end; definition let C be initialized ConstructorSignature; let e be expression of C; func variables_in e -> Subset of Vars equals (C variables_in e).a_Term C; coherence proof (MSVars C).a_Term C = Vars & C variables_in e c= MSVars C by MSVARS,MSAFREE3:28; hence thesis by PBOOLE:def 5; end; end; registration let C,e; cluster variables_in e -> finite; coherence; end; definition let C,e; func vars e -> finite Subset of Vars equals varcl variables_in e; coherence by Th18; end; theorem ::? varcl vars e = vars e; theorem ::? for x being variable holds variables_in (x-term C) = {x} by MSAFREE3:11; theorem for x being variable holds vars (x-term C) = {x} \/ vars x proof let x be variable; thus vars (x-term C) = varcl {x} by MSAFREE3:11 .= {x} \/ vars x by Th82; end; theorem Th84: 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} proof let p be DTree-yielding FinSequence; set X = {variables_in t where t is quasi-term of C: t in rng p}; assume A0: e = [c, the carrier of C]-tree p; then p in (QuasiTerms C)* by Th83; then p is FinSequence of QuasiTerms C by FINSEQ_1:def 11; then A2: rng p c= QuasiTerms C by FINSEQ_1:def 4; thus variables_in e c= union X proof let a be set; assume a in variables_in e; then consider t being DecoratedTree such that A3: t in rng p & a in (C variables_in t).a_Term C by A0,MSAFREE3:12; reconsider t as quasi-term of C by A2,A3,Th42; a in variables_in t & variables_in t in X by A3; hence thesis by TARSKI:def 4; end; let a be set; assume a in union X; then consider Y being set such that A4: a in Y & Y in X by TARSKI:def 4; ex t being quasi-term of C st Y = variables_in t & t in rng p by A4; hence thesis by A0,A4,MSAFREE3:12; end; theorem Th84': 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} proof let p be DTree-yielding FinSequence; assume A1: e = [c, the carrier of C]-tree p; set A = {variables_in t where t is quasi-term of C: t in rng p}; set B = {vars t where t is quasi-term of C: t in rng p}; per cases; suppose A3: A = {}; consider b being Element of B; now assume B <> {}; then b in B; then consider t being quasi-term of C such that A4: b = vars t & t in rng p; variables_in t in A by A4; hence contradiction by A3; end; hence vars e = union B by A1,A3,Th11,Th84,ZFMISC_1:2; end; suppose A <> {}; then reconsider A as non empty set; set D = {varcl s where s is Element of A: not contradiction}; A5: B c= D proof let a be set; assume a in B; then consider t being quasi-term of C such that B1: a = vars t & t in rng p; variables_in t in A by B1; then reconsider s = variables_in t as Element of A; a = varcl s by B1; hence thesis; end; A6: D c= B proof let a be set; assume a in D; then consider s being Element of A such that B2: a = varcl s; s in A; then consider t being quasi-term of C such that B3: s = variables_in t & t in rng p; vars t = a by B2,B3; hence thesis by B3; end; thus vars e = varcl union A by A1,Th84 .= union D by Th14 .= union B by A5,A6,XBOOLE_0:def 10; end; end; theorem len p = len the_arity_of c implies variables_in (c-trm p) = union {variables_in t where t is quasi-term of C: t in rng p} proof assume len p = len the_arity_of c; then c-trm p = [c, the carrier of C]-tree p by TERM; hence thesis by Th84; end; theorem len p = len the_arity_of c implies vars (c-trm p) = union {vars t where t is quasi-term of C: t in rng p} proof assume len p = len the_arity_of c; then c-trm p = [c, the carrier of C]-tree p by TERM; hence thesis by Th84'; end; theorem for S being ManySortedSign, o being set holds S variables_in ([o, the carrier of S]-tree {}) = [0] the carrier of S proof let S be ManySortedSign, o be set; now let s be set; assume A1: s in the carrier of S; now let x; rng {} = {}; then x in (S variables_in ([o, the carrier of S]-tree {})).s iff ex q being DecoratedTree st q in {} & x in (S variables_in q).s by A1,MSAFREE3:12; hence x in (S variables_in ([o, the carrier of S]-tree {})).s iff x in ([0] the carrier of S).s by PBOOLE:5; end; hence (S variables_in ([o, the carrier of S]-tree {})).s = ([0] the carrier of S).s by TARSKI:2; end; hence thesis by PBOOLE:3; end; theorem Aux1: for S being ManySortedSign, o being set, t being DecoratedTree holds S variables_in ([o, the carrier of S]-tree <*t*>) = S variables_in t proof let S be ManySortedSign, o be set, t be DecoratedTree; now let s be set; assume A1: s in the carrier of S; A2: t in {t} by TARSKI:def 1; now let x; rng <*t*> = {t} by FINSEQ_1:56; then x in (S variables_in ([o, the carrier of S]-tree <*t*>)).s iff ex q being DecoratedTree st q in {t} & x in (S variables_in q).s by A1,MSAFREE3:12; hence x in (S variables_in ([o, the carrier of S]-tree <*t*>)).s iff x in (S variables_in t).s by A2,TARSKI:def 1; end; hence (S variables_in ([o, the carrier of S]-tree <*t*>)).s = (S variables_in t).s by TARSKI:2; end; hence thesis by PBOOLE:3; end; theorem Aux1': variables_in ((non_op C)term a) = variables_in a proof (non_op C)term a = [non_op, the carrier of C]-tree <*a*> by ThNon; hence thesis by Aux1; end; theorem ::? vars ((non_op C)term a) = vars a by Aux1'; theorem Aux2: for S being ManySortedSign, o being set, t1,t2 being DecoratedTree holds S variables_in ([o, the carrier of S]-tree <*t1,t2*>) = (S variables_in t1) \/ (S variables_in t2) proof let S be ManySortedSign, o be set, t1,t2 be DecoratedTree; now let s be set; assume A1: s in the carrier of S; A2: t1 in {t1,t2} & t2 in {t1,t2} by TARSKI:def 2; now let x; rng <*t1,t2*> = {t1,t2} by FINSEQ_2:147; then x in (S variables_in ([o, the carrier of S]-tree <*t1,t2*>)).s iff ex q being DecoratedTree st q in {t1,t2} & x in (S variables_in q).s by A1,MSAFREE3:12; then x in (S variables_in ([o, the carrier of S]-tree <*t1,t2*>)).s iff x in (S variables_in t1).s or x in (S variables_in t2).s by A2,TARSKI:def 2; then x in (S variables_in ([o, the carrier of S]-tree <*t1,t2*>)).s iff x in (S variables_in t1).s \/ (S variables_in t2).s by XBOOLE_0:def 2; hence x in (S variables_in ([o, the carrier of S]-tree <*t1,t2*>)).s iff x in ((S variables_in t1) \/ (S variables_in t2)).s by A1,PBOOLE:def 7; end; hence (S variables_in ([o, the carrier of S]-tree <*t1,t2*>)).s = ((S variables_in t1) \/ (S variables_in t2)).s by TARSKI:2; end; hence thesis by PBOOLE:3; end; theorem Aux2': variables_in ((ast C)term(a,t)) = (variables_in a)\/(variables_in t) proof (ast C)term(a,t) = [ *, the carrier of C]-tree <*a,t*> by ThAst; then variables_in ((ast C)term(a,t)) = ((C variables_in a)\/(C variables_in t)).a_Term by Aux2; hence thesis by PBOOLE:def 7; end; theorem vars ((ast C)term(a,t)) = (vars a)\/(vars t) proof thus vars ((ast C)term(a,t)) = varcl((variables_in a)\/(variables_in t)) by Aux2' .= (vars a)\/(vars t) by Th10; end; theorem Th71: variables_in Non a = variables_in a proof per cases; suppose a is non positive; then consider a' being expression of C, an_Adj C such that A2: a = (non_op C)term a' & Non a = a' by Th45g; [non_op C, the carrier of C]-tree<*a'*> = a by A2,ThNon; hence thesis by A2,Aux1; end; suppose a is positive; then Non a = (non_op C)term a by Th44 .= [non_op, the carrier of C]-tree <*a*> by ThNon; hence thesis by Aux1; end; end; theorem ::? vars Non a = vars a by Th71; definition let C; let T be quasi-type of C; func variables_in T -> Subset of Vars equals (union (((MSVars C, a_Term C) variables_in).:adjs T)) \/ variables_in the_base_of T; coherence proof ((MSVars C, a_Term C) variables_in).:adjs T is Subset of bool Vars & union bool Vars = Vars by MSVARS,ZFMISC_1:99; then (union (((MSVars C, a_Term C) variables_in).:adjs T)) c= Vars by ZFMISC_1:95; hence thesis by XBOOLE_1:8; end; end; registration let C; let T be quasi-type of C; cluster variables_in T -> finite; coherence proof now let A be set; assume A in ((MSVars C, a_Term C) variables_in).:adjs T; then consider x being set such that A2: x in Union the Sorts of Free(C, MSVars C) & x in adjs T & A = ((MSVars C, a_Term C) variables_in).x by FUNCT_2:115; reconsider x as expression of C by A2; A = (C variables_in x).a_Term C by A2,VARS'INF; hence A is finite; end; then A3: union (((MSVars C, a_Term C) variables_in).:adjs T) is finite by FINSET_1:25; thus thesis by A3,FINSET_1:14; end; end; definition let C; let T be quasi-type of C; func vars T -> finite Subset of Vars equals varcl variables_in T; coherence by Th18; end; theorem ::? for T being quasi-type of C holds varcl vars T = vars T; theorem Th72: 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) proof let T be quasi-type of C; let a be quasi-adjective of C; A1: dom ((MSVars C, a_Term C) variables_in) = Union the Sorts of Free(C, MSVars C) by FUNCT_2:def 1; thus variables_in (a ast T) = (union (((MSVars C, a_Term C) variables_in).:adjs(a ast T))) \/ variables_in the_base_of T by MCART_1:7 .= (union (((MSVars C, a_Term C) variables_in).:({a} \/ adjs T))) \/ variables_in the_base_of T by MCART_1:7 .= (union ((((MSVars C, a_Term C) variables_in).:{a}) \/ (((MSVars C, a_Term C) variables_in).:adjs T))) \/ variables_in the_base_of T by RELAT_1:153 .= (union (((MSVars C, a_Term C) variables_in).:{a})) \/ (union (((MSVars C, a_Term C) variables_in).:adjs T)) \/ variables_in the_base_of T by ZFMISC_1:96 .= (union (Im((MSVars C, a_Term C) variables_in,a))) \/ variables_in T by XBOOLE_1:4 .= (union {((MSVars C, a_Term C) variables_in).a}) \/ variables_in T by A1,FUNCT_1:117 .= (((MSVars C, a_Term C) variables_in).a) \/ variables_in T by ZFMISC_1:31 .= (variables_in a) \/ variables_in T by VARS'INF; end; theorem for T being quasi-type of C for a being quasi-adjective of C holds vars (a ast T) = (vars a) \/ (vars T) proof let T be quasi-type of C; let a be quasi-adjective of C; thus vars (a ast T) = varcl((variables_in a)\/variables_in T) by Th72 .= (vars a) \/ vars T by Th10; end; theorem ThAA: variables_in (A ast q) = (union {variables_in a where a is quasi-adjective of C: a in A}) \/ (variables_in q) proof set X = ((MSVars C, a_Term C) variables_in).:A; set Y = {variables_in a where a is quasi-adjective of C: a in A}; A1: X c= Y proof let z be set; assume z in X; then consider a being set such that B1: a in dom ((MSVars C, a_Term C) variables_in) & a in A & z = ((MSVars C, a_Term C) variables_in).a by FUNCT_1:def 12; reconsider a as quasi-adjective of C by B1,Th52; z = variables_in a by B1,VARS'INF; hence thesis by B1; end; A2: Y c= X proof let z be set; assume z in Y; then consider a being quasi-adjective of C such that B2: z = variables_in a & a in A; z = ((MSVars C, a_Term C) variables_in).a & dom ((MSVars C, a_Term C) variables_in) = Union the Sorts of Free(C, MSVars C) by B2,VARS'INF,FUNCT_2:def 1; hence thesis by B2,FUNCT_1:def 12; end; thus variables_in (A ast q) = (union (((MSVars C, a_Term C) variables_in).:adjs(A ast q))) \/ variables_in q by MCART_1:7 .= (union (((MSVars C, a_Term C) variables_in).:A)) \/ variables_in q by MCART_1:7 .= (union {variables_in a where a is quasi-adjective of C: a in A}) \/ (variables_in q) by A1,A2,XBOOLE_0:def 10; end; theorem vars (A ast q) = (union {vars a where a is quasi-adjective of C: a in A}) \/ (vars q) proof set X = {variables_in a where a is quasi-adjective of C: a in A}; set Y = {vars a where a is quasi-adjective of C: a in A}; A1: union X c= union Y proof let x be set; assume x in union X; then consider Z being set such that B0: x in Z & Z in X by TARSKI:def 4; consider a being quasi-adjective of C such that B1: Z = variables_in a & a in A by B0; Z c= vars a by B1,VARCL; then vars a in Y & x in vars a by B0,B1; hence x in union Y by TARSKI:def 4; end; for x,y st [x,y] in union Y holds x c= union Y proof let x,y; assume [x,y] in union Y; then consider Z being set such that B2: [x,y] in Z & Z in Y by TARSKI:def 4; consider a being quasi-adjective of C such that B3: Z = vars a & a in A by B2; x c= Z & Z c= union Y by B2,B3,VARCL,ZFMISC_1:92; hence x c= union Y by XBOOLE_1:1; end; then A3: varcl union X c= union Y by A1,VARCL; A4: union Y c= varcl union X proof let x be set; assume x in union Y; then consider Z being set such that B4: x in Z & Z in Y by TARSKI:def 4; consider a being quasi-adjective of C such that B5: Z = vars a & a in A by B4; variables_in a in X by B5; then vars a c= varcl union X by Th13,ZFMISC_1:92; hence thesis by B4,B5; end; thus vars (A ast q) = varcl((union X) \/ (variables_in q)) by ThAA .= (varcl union X) \/ (vars q) by Th10 .= (union Y) \/ (vars q) by A3,A4,XBOOLE_0:def 10; end; theorem ThAAe: variables_in (({}QuasiAdjs C) ast q) = variables_in q proof set A = {}QuasiAdjs C; set AA = {variables_in a where a is quasi-adjective of C: a in A}; AA c= {} proof let x; assume x in AA; then ex a being quasi-adjective of C st x = variables_in a & a in A; hence thesis; end; then AA = {} & variables_in (A ast q) = (union AA) \/ (variables_in q) by ThAA,XBOOLE_1:3; hence thesis by ZFMISC_1:2; end; theorem ThG: e is ground iff variables_in e = {} proof thus e is ground implies variables_in e = {} proof assume Union (C variables_in e) = {}; hence variables_in e = {} by ThF0,XBOOLE_1:3; end; assume that Z1: variables_in e = {} and Z2: Union (C variables_in e) <> {}; consider x being Element of Union (C variables_in e); consider y such that Z3: y in dom (C variables_in e) & x in (C variables_in e).y by Z2,CARD_5:10; dom (C variables_in e) = the carrier of C by PBOOLE:def 3 .= {a_Type, an_Adj, a_Term} by CONSTRSIGN; then Z4: y = a_Type or y = an_Adj or y = a_Term by Z3,ENUMSET1:def 1; C variables_in e c= MSVars C & (MSVars C).an_Adj = {} & (MSVars C).a_Type = {} by MSVARS,MSAFREE3:28; then (C variables_in e).an_Adj C c= {} & (C variables_in e).a_Type C c= {} by PBOOLE:def 5; hence thesis by Z1,Z3,Z4; end; definition let C; let T be quasi-type of C; attr T is ground means: GROUND2: variables_in T = {}; end; registration let C; cluster ground pure expression of C, a_Type C; existence proof consider m, a being OperSymbol of C such that A1: the_result_sort_of m = a_Type & the_arity_of m = {} and the_result_sort_of a = an_Adj & the_arity_of a = {} by INITIALIZED; root-tree [m, the carrier of C] in (the Sorts of Free(C,MSVars C)).a_Type C by A1,MSAFREE3:6; then reconsider mm = root-tree [m, the carrier of C] as expression of C, a_Type C by Th42; take mm; set p = <*>Union the Sorts of Free(C, MSVars C); A2: mm = [m, the carrier of C]-tree p by TREES_4:20; m <> * & m <> non_op by A1,CONSTRSIGN; then A3: m is constructor by CNSTR2; variables_in mm c= {} proof let x; assume x in variables_in mm; then x in union {variables_in t where t is quasi-term of C: t in rng p} by A2,A3,Th84; then consider Y such that A4: x in Y & Y in {variables_in t where t is quasi-term of C: t in rng p} by TARSKI:def 4; ex t being quasi-term of C st Y = variables_in t & t in rng p by A4; hence thesis; end; then variables_in mm = {} by XBOOLE_1:3; hence mm is ground by ThG; ex t being expression of C, a_Type C st t = root-tree [m, the carrier of C] & t is pure by A1,ThP; hence thesis; end; cluster ground quasi-adjective of C; existence proof consider m, a being OperSymbol of C such that the_result_sort_of m = a_Type & the_arity_of m = {} and A1: the_result_sort_of a = an_Adj & the_arity_of a = {} by INITIALIZED; consider mm being expression of C, an_Adj C such that A5: mm = root-tree [a, the carrier of C] & mm is positive by A1,ThP2; reconsider mm as quasi-adjective of C by A5,REG; take mm; set p = <*>Union the Sorts of Free(C, MSVars C); A2: mm = [a, the carrier of C]-tree p by A5,TREES_4:20; a <> * & a <> non_op by A1,CONSTRSIGN; then A3: a is constructor by CNSTR2; variables_in mm c= {} proof let x; assume x in variables_in mm; then x in union {variables_in t where t is quasi-term of C: t in rng p} by A2,A3,Th84; then consider Y such that A4: x in Y & Y in {variables_in t where t is quasi-term of C: t in rng p} by TARSKI:def 4; ex t being quasi-term of C st Y = variables_in t & t in rng p by A4; hence thesis; end; then variables_in mm = {} by XBOOLE_1:3; hence thesis by ThG; end; end; theorem ThG2: for t being ground pure expression of C, a_Type C holds ({} QuasiAdjs C) ast t is ground proof let t be ground pure expression of C, a_Type C; set T = ({} QuasiAdjs C) ast t; thus variables_in T = variables_in t by ThAAe .= {} by ThG; end; registration let C; let t be ground pure expression of C, a_Type C; cluster ({} QuasiAdjs C) ast t -> ground quasi-type of C; coherence by ThG2; end; registration let C; cluster ground quasi-type of C; existence proof consider t being ground pure expression of C, a_Type C; take ({} QuasiAdjs C) ast t; thus thesis; end; end; registration let C; let T be ground quasi-type of C; let a be ground quasi-adjective of C; cluster a ast T -> ground; coherence proof thus variables_in(a ast T) = (variables_in a)\/variables_in T by Th72 .= {}\/variables_in T by ThG .= {} by GROUND2; end; end; begin :: Smooth Type Widening :: Type widening is smooth iff :: vars-function is sup-semilattice homomorphism from widening sup-semilattice :: into VarPoset definition func VarPoset -> strict non empty Poset equals (InclPoset {varcl A where A is finite Subset of Vars: not contradiction})opp; coherence proof consider A0 being finite Subset of Vars; set V = {varcl A where A is finite Subset of Vars: not contradiction}; varcl A0 in V; then reconsider V as non empty set; reconsider P = InclPoset V as non empty Poset; P opp is non empty; hence thesis; end; end; theorem Th22: for x, y being Element of VarPoset holds x <= y iff y c= x proof let x, y be Element of VarPoset; set V = {varcl A where A is finite Subset of Vars: not contradiction}; consider A0 being finite Subset of Vars; varcl A0 in V; then reconsider V as non empty set; reconsider a = x, b = y as Element of (InclPoset V) opp; x <= y iff ~a >= ~b by YELLOW_7:1; hence thesis by YELLOW_1:3; end; :: registration :: let V1,V2 be Element of VarPoset; :: identify V1 <= V2 with V2 c= V1; :: compatibility by Th22; :: end; theorem Th21: for x holds x is Element of VarPoset iff x is finite Subset of Vars & varcl x = x proof let x; set V = {varcl A where A is finite Subset of Vars: not contradiction}; consider A0 being finite Subset of Vars; varcl A0 in V; then reconsider V as non empty set; A2: the carrier of InclPoset V = V by YELLOW_1:1; x is Element of VarPoset iff x in V by A2; then x is Element of VarPoset iff ex A being finite Subset of Vars st x = varcl A; hence thesis by Th18; end; registration cluster VarPoset -> with_infima with_suprema; coherence proof set V = {varcl A where A is finite Subset of Vars: not contradiction}; consider A0 being finite Subset of Vars; varcl A0 in V; then reconsider V as non empty set; now let x,y; assume x in V; then consider A1 being finite Subset of Vars such that A2: x = varcl A1; assume y in V; then consider A2 being finite Subset of Vars such that A3: y = varcl A2; x \/ y = varcl (A1 \/ A2) by A2,A3,Th10; hence x \/ y in V; end; then InclPoset V is with_suprema by YELLOW_1:11; hence VarPoset is with_infima by LATTICE3:10; now let x,y; assume x in V; then consider A1 being finite Subset of Vars such that A2: x = varcl A1; assume y in V; then consider A2 being finite Subset of Vars such that A3: y = varcl A2; reconsider V1 = varcl A1, V2 = varcl A2 as finite Subset of Vars by Th18; x /\ y = varcl (V1 /\ V2) by A2,A3,Th9; hence x /\ y in V; end; then InclPoset V is with_infima by YELLOW_1:12; hence VarPoset is with_suprema by YELLOW_7:16; end; end; theorem Th23: for V1, V2 being Element of VarPoset holds V1 "\/" V2 = V1 /\ V2 & V1 "/\" V2 = V1 \/ V2 proof let V1, V2 be Element of VarPoset; set V = {varcl A where A is finite Subset of Vars: not contradiction}; consider A0 being finite Subset of Vars; varcl A0 in V; then reconsider V as non empty set; A1: VarPoset = (InclPoset V) opp; A2: the carrier of InclPoset V = V by YELLOW_1:1; reconsider v1 = V1, v2 = V2 as Element of (InclPoset V) opp; reconsider a1 = V1, a2 = V2 as Element of InclPoset V; V1 in V by A2; then consider A1 being finite Subset of Vars such that A4: V1 = varcl A1; V2 in V by A2; then consider A2 being finite Subset of Vars such that A5: V2 = varcl A2; A6: a1~ = v1 & a2~ = v2; A7: InclPoset V is with_infima with_suprema by A1,LATTICE3:10,YELLOW_7:16; reconsider x1 = V1, x2 = V2 as finite Subset of Vars by A4,A5,Th18; V1 /\ V2 = varcl (x1 /\ x2) by A4,A5,Th9; then V1 /\ V2 in V; then a1 "/\" a2 = V1 /\ V2 by YELLOW_1:9; hence V1 "\/" V2 = V1 /\ V2 by A6,A7,YELLOW_7:21; V1 \/ V2 = varcl (A1 \/ A2) by A4,A5,Th10; then a1 \/ a2 in V; then a1 "\/" a2 = V1 \/ V2 by YELLOW_1:8; hence thesis by A6,A7,YELLOW_7:23; end; registration let V1,V2 be Element of VarPoset; identify V1 "\/" V2 with V1 /\ V2; compatibility by Th23; identify V1 "/\" V2 with V1 \/ V2; compatibility by Th23; end; theorem Th24: for X being non empty Subset of VarPoset holds ex_sup_of X, VarPoset & sup X = meet X proof let X be non empty Subset of VarPoset; consider a being Element of X; meet X c= a & a is finite Subset of Vars by Th21,SETFAM_1:4; then A1: meet X is finite & meet X c= Vars by XBOOLE_1:1,FINSET_1:13; for a being Element of X holds varcl a = a by Th21; then varcl meet X = meet X by Th8; then reconsider m = meet X as Element of VarPoset by A1,Th21; A4: now thus X is_<=_than m proof let n be Element of VarPoset; assume n in X; then m c= n by SETFAM_1:4; hence thesis by Th22; end; let b be Element of VarPoset; assume A2: X is_<=_than b; now let Y; assume A3: Y in X; then reconsider c = Y as Element of VarPoset; c <= b by A2,LATTICE3:def 9,A3; hence b c= Y by Th22; end; then b c= m by SETFAM_1:6; hence m <= b by Th22; end; hence ex_sup_of X, VarPoset by YELLOW_0:15; hence thesis by A4,YELLOW_0:def 9; end; registration cluster VarPoset -> up-complete; coherence proof for X being non empty directed Subset of VarPoset holds ex_sup_of X, VarPoset by Th24; hence thesis by WAYBEL_0:75; end; end; theorem Top VarPoset = {} proof set V = {varcl A where A is finite Subset of Vars: not contradiction}; {} Vars in V by Th11; then VarPoset opp is lower-bounded & (Bottom InclPoset V)~ = {} & VarPoset opp = InclPoset V by YELLOW_1:13,YELLOW_7:31; hence thesis by YELLOW_7:33; end; definition let C; func vars-function C -> Function of QuasiTypes C, the carrier of VarPoset means for T being quasi-type of C holds it.T = vars T; uniqueness proof let f1,f2 be Function of QuasiTypes C, the carrier of VarPoset such that A1: for T being quasi-type of C holds f1.T = vars T and A2: for T being quasi-type of C holds f2.T = vars T; now let T be Element of QuasiTypes C; reconsider t = T as quasi-type of C by QUASITYPE; thus f1.T = vars t by A1 .= f2.T by A2; end; hence thesis by FUNCT_2:113; end; existence proof defpred P[set,set] means ex T being quasi-type of C st $1 = T & $2 = vars T; A1: for x st x in QuasiTypes C ex y being set st P[x,y] proof let x; assume x in QuasiTypes C; then reconsider T = x as quasi-type of C by QUASITYPE; take y = vars T, T; thus thesis; end; A2: for x,y1,y2 being set st x in QuasiTypes C & P[x,y1] &P[x,y2] holds y1 = y2; consider f being Function such that A3: dom f = QuasiTypes C and A4: for x st x in QuasiTypes C holds P[x,f.x] from FUNCT_1:sch 2(A2,A1); rng f c= the carrier of VarPoset proof let y; assume y in rng f; then consider x such that A5: x in dom f & y = f.x by FUNCT_1:def 5; consider T being quasi-type of C such that A6: x = T & y = vars T by A3,A4,A5; varcl vars T = vars T; then y is Element of VarPoset by A6,Th21; hence thesis; end; then reconsider f as Function of QuasiTypes C, the carrier of VarPoset by A3,FUNCT_2:4; take f; let x be quasi-type of C; x in QuasiTypes C by QUASITYPE; then ex T being quasi-type of C st x = T & f.x = vars T by A4; hence thesis; end; end; definition let L be non empty Poset; attr L is smooth means ex C being initialized ConstructorSignature, 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; registration let C be initialized ConstructorSignature; let T be ground quasi-type of C; cluster RelStr(#{T}, id {T}#) -> smooth; coherence proof set L = RelStr(#{T}, id {T}#); T in QuasiTypes C by QUASITYPE; then A1: {T} c= QuasiTypes C by ZFMISC_1:37; then reconsider f = (vars-function C)|{T} as Function of L, VarPoset by FUNCT_2:38; take C, f; thus the carrier of L c= QuasiTypes C by A1; thus f = (vars-function C)|the carrier of L; let x,y be Element of L; set F = {x,y}; assume ex_sup_of F, L; A2: x = T & y = T by TARSKI:def 1; then A4: F = {T} & dom f = {T} by ENUMSET1:69,FUNCT_2:def 1; then A3: Im(f,T) = {f.x} by A2,FUNCT_1:117; hence ex_sup_of f.:F, VarPoset by A4,YELLOW_0:38; thus sup (f.:F) = f.x by A4,A3,YELLOW_0:39 .= f.sup F by A2,TARSKI:def 1; end; end; begin :: Structural induction scheme StructInd {C() -> initialized ConstructorSignature, P[set], t() -> expression of C()}: P[t()] provided W1: for x being variable holds P[x-term C()] and W2: for c being constructor OperSymbol of C() for p being FinSequence of QuasiTerms C() st len p = len the_arity_of c & for t being quasi-term of C() st t in rng p holds P[t] holds P[c-trm p] and W3: for a being expression of C(), an_Adj C() st P[a] holds P[(non_op C())term a] and W4: for a being expression of C(), an_Adj C() st P[a] for t being expression of C(), a_Type C() st P[t] holds P[(ast C())term(a,t)] proof defpred Q[set] means $1 is expression of C() implies P[ $1 ]; set X = MSVars C(); set V = X \/ ((the carrier of C())-->{0}); set S = C(), C = C(); B0: t() is Term of S,V by MSAFREE3:9; B1: for s being SortSymbol of S, v being Element of V.s holds Q[root-tree [v,s]] proof let s be SortSymbol of S; let v be Element of V.s; set t = root-tree [v,s]; assume C1: t is expression of S; t.{} = [v,s] & s in the carrier of C by TREES_4:3; then C2: (t.{})`2 = s & s <> the carrier of C by MCART_1:7; per cases by C1,Th100; suppose ex x being variable st t = x-term C; hence P[t] by W1; end; suppose ex c being constructor OperSymbol of C st ex p being FinSequence of QuasiTerms C st len p = len the_arity_of c & t = c-trm p; then consider c being (constructor OperSymbol of C), p being FinSequence of QuasiTerms C such that C3: len p = len the_arity_of c & t = c-trm p; t = [c, the carrier of C]-tree p by C3,TERM; then t.{} = [c, the carrier of C] by TREES_4:def 4; hence P[t] by C2,MCART_1:7; end; suppose ex a being expression of C(), an_Adj C() st t = (non_op C)term a; then consider a being expression of C(), an_Adj C() such that C4: t = (non_op C)term a; the_arity_of non_op C = <*an_Adj C*> & <*an_Adj C*>.1 = an_Adj C & len <*an_Adj C*> = 1 by CONSTRSIGN,FINSEQ_1:57; then t = [non_op C, the carrier of C]-tree<*a*> by C4,TERM1; then t.{} = [non_op C, the carrier of C] by TREES_4:def 4; hence P[t] by C2,MCART_1:7; end; suppose ex a being expression of C(), an_Adj C() st ex q being expression of C, a_Type C st t = (ast C)term(a,q); then consider a being expression of C, an_Adj C, q being expression of C, a_Type C such that C5: t = (ast C)term(a,q); the_arity_of ast C = <*an_Adj C,a_Type C*> & <*an_Adj C,a_Type C*>.1 = an_Adj C & <*an_Adj C,a_Type C*>.2 = a_Type C & len <*an_Adj C,a_Type C*> = 2 by CONSTRSIGN,FINSEQ_1:61; then t = [ast C, the carrier of C]-tree<*a,q*> by C5,TERM2; then t.{} = [ast C, the carrier of C] by TREES_4:def 4; hence P[t] by C2,MCART_1:7; end; end; B2: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,V) st for t being Term of S,V st t in rng p holds Q[t] holds Q[[o,the carrier of S]-tree p] proof let o be OperSymbol of S; let p be ArgumentSeq of Sym(o,V) such that Z0: for t being Term of S,V st t in rng p holds Q[t]; set t = [o,the carrier of S]-tree p; assume C1: t is expression of S; per cases by C1,Th100; suppose ex x being variable st t = x-term C; hence P[t] by W1; end; suppose ex c being constructor OperSymbol of C st ex p being FinSequence of QuasiTerms C st len p = len the_arity_of c & t = c-trm p; then consider c being (constructor OperSymbol of C), q being FinSequence of QuasiTerms C such that C3: len q = len the_arity_of c & t = c-trm q; t = [c, the carrier of C]-tree q by C3,TERM; then C4: p = q by TREES_4:15; now let t be quasi-term of C; t is Term of S,V by MSAFREE3:9; hence t in rng q implies P[t] by Z0,C4; end; hence P[t] by C3,W2; end; suppose ex a being expression of C(), an_Adj C() st t = (non_op C)term a; then consider a being expression of C(), an_Adj C() such that C4: t = (non_op C)term a; the_arity_of non_op C = <*an_Adj C*> & <*an_Adj C*>.1 = an_Adj C & len <*an_Adj C*> = 1 by CONSTRSIGN,FINSEQ_1:57; then t = [non_op C, the carrier of C]-tree<*a*> by C4,TERM1; then 00: p = <*a*> by TREES_4:15; rng <*a*> = {a} & a in {a} & a is Term of S,V by TARSKI:def 1,FINSEQ_1:56,MSAFREE3:9; hence P[t] by C4,W3,00,Z0; end; suppose ex a being expression of C(), an_Adj C() st ex q being expression of C, a_Type C st t = (ast C)term(a,q); then consider a being expression of C, an_Adj C, q being expression of C, a_Type C such that C5: t = (ast C)term(a,q); the_arity_of ast C = <*an_Adj C,a_Type C*> & <*an_Adj C,a_Type C*>.1 = an_Adj C & <*an_Adj C,a_Type C*>.2 = a_Type C & len <*an_Adj C,a_Type C*> = 2 by CONSTRSIGN,FINSEQ_1:61; then t = [ast C, the carrier of C]-tree<*a,q*> by C5,TERM2; then 00: p = <*a,q*> by TREES_4:15; rng <*a,q*> = {a,q} & a in {a,q} & q in {a,q} & a is Term of S,V & q is Term of S,V by TARSKI:def 2,FINSEQ_2:147,MSAFREE3:9; then P[a] & P[q] by 00,Z0; hence P[t] by C5,W4; end; end; for t being Term of S,V holds Q[t] from MSATERM:sch 1(B1,B2); hence thesis by B0; end; definition let S be ManySortedSign; attr S is with_an_operation_for_each_sort means: WOFES: the carrier of S c= rng the ResultSort of S; let X be ManySortedSet of the carrier of S; attr X is with_missing_variables means: WMV: X"{{}} c= rng the ResultSort of S; end; theorem LemMV: 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 = {} ex o being OperSymbol of S st the_result_sort_of o = s proof let S be non void Signature; let X be ManySortedSet of the carrier of S; A0: dom X = the carrier of S by PBOOLE:def 3; hereby assume X is with_missing_variables; then Z0: X"{{}} c= rng the ResultSort of S by WMV; let s be SortSymbol of S; assume X.s = {}; then X.s in {{}} by TARSKI:def 1; then s in X"{{}} by A0,FUNCT_1:def 13; then consider o being set such that Z1: o in the OperSymbols of S & (the ResultSort of S).o = s by Z0,FUNCT_2:17; reconsider o as OperSymbol of S by Z1; take o; thus the_result_sort_of o = s by Z1; end; assume Z2: for s being SortSymbol of S st X.s = {} ex o being OperSymbol of S st the_result_sort_of o = s; let x be set; assume x in X"{{}}; then A1: x in dom X & X.x in {{}} by FUNCT_1:def 13; then reconsider x as SortSymbol of S by A0; X.x = {} by A1,TARSKI:def 1; then ex o being OperSymbol of S st the_result_sort_of o = x by Z2; hence thesis by FUNCT_2:6; end; registration cluster MaxConstrSign -> with_an_operation_for_each_sort; coherence proof set C = MaxConstrSign; set m = [a_Type, [{}, 0]], a = [an_Adj, [{}, 0]], f = [a_Term, [{}, 0]]; a_Type in {a_Type} & an_Adj in {an_Adj} & a_Term in {a_Term} & [<*> Vars, 0] in [:QuasiLoci, NAT:] by Th31,ZFMISC_1:def 2,TARSKI:def 1; then A0: m in Modes & a in Attrs & f in Funcs by ZFMISC_1:def 2; then m in Modes \/ Attrs & a in Modes \/ Attrs by XBOOLE_0:def 2; then m in Constructors & a in Constructors & f in Constructors & the OperSymbols of MaxConstrSign = {*, non_op} \/ Constructors by A0,MAXdef,XBOOLE_0:def 2; then reconsider m,a,f as OperSymbol of MaxConstrSign by XBOOLE_0:def 2; m is constructor & a is constructor & f is constructor by CNSTR2; then (the ResultSort of C).m = m`1 & (the ResultSort of C).a = a`1 & (the ResultSort of C).f = f`1 by MAXdef; then A1: (the ResultSort of C).m = a_Type & (the ResultSort of C).a = an_Adj & (the ResultSort of C).f = a_Term by MCART_1:7; A2: the carrier of C = {a_Type, an_Adj, a_Term} by CONSTRSIGN; let x be set; assume x in the carrier of C; then x = a_Type or x = an_Adj or x = a_Term by A2,ENUMSET1:def 1; hence thesis by A1,FUNCT_2:6; end; let C be ConstructorSignature; cluster MSVars C -> with_missing_variables; coherence proof set X = MSVars C; let x be set; assume x in X"{{}}; then A1: x in dom X & X.x in {{}} by FUNCT_1:def 13; then x in the carrier of C by PBOOLE:def 3; then x in {a_Type, an_Adj, a_Term} by CONSTRSIGN; then A2: x = a_Type or x = an_Adj or x = a_Term by ENUMSET1:def 1; A3: X.x = {} by A1,TARSKI:def 1; (the ResultSort of C).(ast C) = a_Type & (the ResultSort of C).(non_op C) = an_Adj by CONSTRSIGN; hence thesis by A2,A3,MSVARS,FUNCT_2:6; end; end; registration let S be ManySortedSign; cluster non-empty -> with_missing_variables ManySortedSet of the carrier of S; coherence proof let X be ManySortedSet of the carrier of S such that A0: X is non-empty; let x be set; assume x in X"{{}}; then x in dom X & X.x in {{}} by FUNCT_1:def 13; then X.x in rng X & X.x = {} by TARSKI:def 1,FUNCT_1:def 5; hence thesis by A0,RELAT_1:def 9; end; end; registration let S be ManySortedSign; cluster with_missing_variables ManySortedSet of the carrier of S; existence proof consider A being non-empty ManySortedSet of the carrier of S; take A; thus thesis; end; end; registration cluster initialized with_an_operation_for_each_sort strict ConstructorSignature; existence proof take MaxConstrSign; thus thesis; end; end; registration let C be with_an_operation_for_each_sort ManySortedSign; cluster -> with_missing_variables ManySortedSet of the carrier of C; coherence proof let X be ManySortedSet of the carrier of C; A1: X"{{}} c= dom X by RELAT_1:167; A2: dom X = the carrier of C by PBOOLE:def 3; the carrier of C c= rng the ResultSort of C by WOFES; hence X"{{}} c= rng the ResultSort of C by A1,A2,XBOOLE_1:1; end; end; definition let G be non empty DTConstrStr; redefine func Terminals G -> Subset of G; coherence proof the carrier of G = Terminals G \/NonTerminals G by LANG1:1; hence thesis by XBOOLE_1:7; end; func NonTerminals G -> Subset of G; coherence proof the carrier of G = Terminals G \/NonTerminals G by LANG1:1; hence thesis by XBOOLE_1:7; end; end; theorem LemTerm0: 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) proof let D1,D2 be non empty DTConstrStr such that 01: the Rules of D1 c= the Rules of D2; thus 00: NonTerminals D1 c= NonTerminals D2 proof let x be set; assume x in NonTerminals D1; then ex s being Symbol of D1 st x = s & ex n being FinSequence st s ==> n; then consider s being Symbol of D1, n being FinSequence such that 02: x = s & s ==> n; 03: [s,n] in the Rules of D1 by 02,LANG1:def 1; then [s,n] in the Rules of D2 by 01; then reconsider s' = s as Symbol of D2 by ZFMISC_1:106; s' ==> n by 01,03,LANG1:def 1; hence thesis by 02; end; hereby let x be set; assume x in (the carrier of D1) /\ Terminals D2; then 04: x in the carrier of D1 & x in Terminals D2 & Terminals D2 \/ NonTerminals D2 = the carrier of D2 by XBOOLE_0:def 3,LANG1:1; then reconsider s' = x as Symbol of D1; reconsider s = x as Symbol of D2 by 04; assume not x in Terminals D1; then consider n being FinSequence such that 05: s' ==> n; [s',n] in the Rules of D1 by 05,LANG1:def 1; then s ==> n by 01,LANG1:def 1; then not ex s being Symbol of D2 st x = s & not ex n being FinSequence st s ==> n; hence contradiction by 04; end; assume Terminals D1 c= Terminals D2; then Terminals D1 \/ NonTerminals D1 c= Terminals D2 \/ NonTerminals D2 by 00,XBOOLE_1:13; then Terminals D1 \/ NonTerminals D1 c= the carrier of D2 by LANG1:1; hence thesis by LANG1:1; end; theorem LemTS0: 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 proof let G,G' be non empty DTConstrStr such that Z0: Terminals G c= Terminals G' and Z1: the Rules of G c= the Rules of G'; Z2: the carrier of G' = (Terminals G') \/ NonTerminals G' & the carrier of G c= the carrier of G' by Z0,Z1,LemTerm0,LANG1:1; defpred P[set] means $1 in TS G'; A1: for s being Symbol of G st s in Terminals G holds P[root-tree s] proof let s be Symbol of G; assume 00: s in Terminals G; then reconsider s' = s as Symbol of G' by Z0,Z2,XBOOLE_0:def 2; root-tree s = root-tree s'; hence P[root-tree s] by 00,Z0,DTCONSTR:def 4; end; A2: for nt being Symbol of G, ts being FinSequence of TS(G) st nt ==> roots ts & for t being DecoratedTree of the carrier of G st t in rng ts holds P[t] holds P[nt-tree ts] proof let n be Symbol of G; let s be FinSequence of TS(G) such that 01: [n, roots s] in the Rules of G and 02: for t being DecoratedTree of the carrier of G st t in rng s holds P[t]; rng s c= TS G' proof let x be set; assume 03: x in rng s; then x is DecoratedTree of the carrier of G by TREES_3:def 6; hence thesis by 02,03; end; then reconsider s' = s as FinSequence of TS G' by FINSEQ_1:def 4; n in the carrier of G; then reconsider n' = n as Symbol of G' by Z2; n' ==> roots s' by Z1,01,LANG1:def 1; hence thesis by DTCONSTR:def 4; end; A3: for t being DecoratedTree of the carrier of G st t in TS(G) holds P[t] from DTCONSTR:sch 7(A1,A2); let x be set; assume A4: x in TS G; then reconsider t = x as Element of FinTrees(the carrier of G); P[t] by A3,A4; hence thesis; end; theorem LemX: for S being ManySortedSign for X,Y being ManySortedSet of the carrier of S st X c= Y holds X is with_missing_variables implies Y is with_missing_variables proof let S be ManySortedSign; let X,Y be ManySortedSet of the carrier of S such that Z0: X c= Y and Z1: X"{{}} c= rng the ResultSort of S; let x be set; assume x in Y"{{}}; then A0: x in dom Y & Y.x in {{}} & dom Y = the carrier of S & dom X = the carrier of S by FUNCT_1:def 13,PBOOLE:def 3; then Y.x = {} & X.x c= Y.x by Z0,TARSKI:def 1,PBOOLE:def 5; then X.x = {} by XBOOLE_1:3; then X.x in {{}} by TARSKI:def 1; then x in X"{{}} by A0,FUNCT_1:def 13; hence thesis by Z1; end; theorem LemY0: for S being set for X,Y being ManySortedSet of S st X c= Y holds Union coprod X c= Union coprod Y proof let S be set; let X,Y be ManySortedSet of S such that Z0: X c= Y; B0: dom X = S & dom Y = S by PBOOLE:def 3; let x be set; assume x in Union coprod X; then B1: x`2 in dom X & x`1 in X.x`2 & x = [x`1,x`2] by CARD_3:33; then X.x`2 c= Y.x`2 by Z0,B0,PBOOLE:def 5; hence thesis by B0,B1,CARD_3:33; end; theorem 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 LemY0,XBOOLE_1:9; theorem ThTNT: 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 OperSymbols of S,{the carrier of S}:] & Terminals DTConMSA X = Union coprod X proof let S be non void Signature; let X be ManySortedSet of the carrier of S such that A0: X is with_missing_variables; set D = DTConMSA X, A = [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod (X qua ManySortedSet of the carrier of S)); A1: Union(coprod X) misses [:the OperSymbols of S,{the carrier of S}:] by MSAFREE:4; A2: the carrier of D = (Terminals D) \/ (NonTerminals D) & (Terminals D) misses (NonTerminals D) by DTCONSTR:8,LANG1:1; thus NonTerminals DTConMSA X c= [:the OperSymbols of S,{the carrier of S}:] by MSAFREE:6; thus A10:[:the OperSymbols of S,{the carrier of S}:] c= NonTerminals D proof let o,x2 be set; assume A11: [o,x2] in [:the OperSymbols of S,{the carrier of S}:]; then A12: o in the OperSymbols of S & x2 in {the carrier of S} by ZFMISC_1:106;then reconsider o as OperSymbol of S; A13: the carrier of S = x2 by A12,TARSKI:def 1; then reconsider xa = [o,the carrier of S] as Element of (the carrier of D) by A11,XBOOLE_0:def 2; set O = the_arity_of o; defpred P[set,set] means $2 in A & (X.(O.$1) <> {} implies $2 in coprod(O.$1,X)) & (X.(O.$1) = {} implies ex o being OperSymbol of S st $2 = [o,the carrier of S] & the_result_sort_of o = O.$1); A14: for a be set st a in Seg len O ex b be set st P[a,b] proof let a be set; assume a in Seg len O; then A18: a in dom O by FINSEQ_1:def 3; then A15: O.a in rng O & rng O c= the carrier of S by FUNCT_1:def 5; then reconsider s = O.a as SortSymbol of S; per cases; suppose X.(O.a) is non empty; then consider x be set such that A16: x in X.(O.a) by XBOOLE_0:def 1; take y = [x,O.a]; A19: y in coprod(O.a,X) by A15,A16,MSAFREE:def 2; A20: O.a in rng O & rng O c= the carrier of S by A18,FUNCT_1:def 5; dom coprod(X) = the carrier of S by PBOOLE:def 3; then (coprod(X)).(O.a) in rng coprod(X) by A20,FUNCT_1:def 5; then coprod(O.a,X) in rng coprod(X) by A20,MSAFREE:def 3; then y in Union coprod(X) by A19,TARSKI:def 4; hence thesis by A15,A16,MSAFREE:def 2,XBOOLE_0:def 2; end; suppose AA: X.(O.a) = {}; then consider o being OperSymbol of S such that A3: the_result_sort_of o = s by A0,LemMV; take y = [o,the carrier of S]; the carrier of S in {the carrier of S} by TARSKI:def 1; then y in [:the OperSymbols of S,{the carrier of S}:] by ZFMISC_1:106; hence thesis by AA,A3,XBOOLE_0:def 2; end; end; consider b be Function such that A17: dom b = Seg len O & for a be set st a in Seg len O holds P[a,b.a] from CLASSES1:sch 1(A14); reconsider b as FinSequence by A17,FINSEQ_1:def 2; rng b c= A proof let a be set; assume a in rng b; then ex c being set st c in dom b & b.c = a by FUNCT_1:def 5; hence a in A by A17; end; then reconsider b as FinSequence of A by FINSEQ_1:def 4; reconsider b as Element of A* by FINSEQ_1:def 11; A21: len b = len O by A17,FINSEQ_1:def 3; now let c be set; assume A22: c in dom b; then A23: P[c,b.c] by A17; dom O = Seg len O by FINSEQ_1:def 3; then A24: O.c in rng O & rng O c= the carrier of S by A17,A22,FUNCT_1:def 5; dom coprod(X) = the carrier of S by PBOOLE:def 3; then (coprod(X)).(O.c) in rng coprod(X) by A24,FUNCT_1:def 5; then coprod(O.c,X) in rng coprod(X) by A24,MSAFREE:def 3; then AB: X.(O.c) <> {} implies b.c in Union coprod(X) by A23,TARSKI:def 4; thus b.c in [:the OperSymbols of S,{the carrier of S}:] implies for o1 being OperSymbol of S st [o1,the carrier of S] = b.c holds the_result_sort_of o1 = O.c by A23,A1,AB,XBOOLE_0:3,ZFMISC_1:33; assume B1: b.c in Union (coprod X); now assume X.(O.c) = {}; then consider o being OperSymbol of S such that B2: b.c = [o,the carrier of S] & the_result_sort_of o = O.c by A17,A22; the carrier of S in {the carrier of S} by TARSKI:def 1; then b.c in [:the OperSymbols of S,{the carrier of S}:] by B2,ZFMISC_1:106; hence contradiction by B1,A1,XBOOLE_0:3; end; hence b.c in coprod(O.c,X) by A17,A22; end; then [xa,b] in REL(X) by A21,MSAFREE:5; then xa ==> b by LANG1:def 1; hence thesis by A13; end; thus Terminals D c= Union coprod X proof let x be set; assume A25: x in Terminals D; then not x in [:the OperSymbols of S,{the carrier of S}:] by A2,A10,XBOOLE_0:3; hence thesis by A25,XBOOLE_0:def 2; end; thus Union coprod X c= Terminals DTConMSA X by MSAFREE:6; end; theorem 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 proof let S be non void Signature; let X,Y be ManySortedSet of the carrier of S such that Z0: X c= Y and Z1: X is with_missing_variables; Z2: Y is with_missing_variables by Z0,Z1,LemX; set G = DTConMSA X, G' = DTConMSA Y; A1: the carrier of G c= the carrier of G' by Z0,LemY0,XBOOLE_1:9; Terminals G = Union coprod X & Terminals G' = Union coprod Y by Z1,Z2,ThTNT; hence A2: Terminals G c= Terminals G' by Z0,LemY0; A3: (the carrier of G)* c= (the carrier of G')* by A1,FINSEQ_1:83; thus the Rules of G c= the Rules of G' proof let a,b be set; assume C1: [a,b] in the Rules of G; then C2: a in [:the OperSymbols of S,{the carrier of S}:] & b in ([:the OperSymbols of S,{the carrier of S}:] \/ Union coprod X)* by MSAFREE1:2; then consider a1,a2 being set such that C3: a1 in the OperSymbols of S & a2 in {the carrier of S} & a = [a1,a2] by ZFMISC_1:def 2; reconsider a1 as OperSymbol of S by C3; reconsider a as Element of [:the OperSymbols of S,{the carrier of S}:] \/ Union coprod X by C2,XBOOLE_0:def 2; reconsider a' = a as Element of [:the OperSymbols of S,{the carrier of S}:] \/ Union coprod Y by C2,XBOOLE_0:def 2; reconsider b as Element of ([:the OperSymbols of S,{the carrier of S}:] \/ Union coprod X)* by C2; reconsider b' = b as Element of ([:the OperSymbols of S,{the carrier of S}:] \/ Union coprod Y)* by C2,A3; now let o be OperSymbol of S; assume C4: [o,the carrier of S] = a'; hence CC: len b' = len (the_arity_of o) by C1,MSAFREE:def 9; let x be set; assume C5: x in dom b'; hence b'.x in [:the OperSymbols of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = b.x holds the_result_sort_of o1 = (the_arity_of o).x by C1,C4,MSAFREE:def 9; C6: Union coprod X misses [:the OperSymbols of S,{the carrier of S}:] & Union coprod Y misses [:the OperSymbols of S,{the carrier of S}:] by MSAFREE:4; C7: b.x in [:the OperSymbols of S,{the carrier of S}:] \/ Union coprod X by C5,DTCONSTR:2; dom b' = Seg len b' & dom the_arity_of o = Seg len b' by CC,FINSEQ_1:def 3; then C9: (the_arity_of o).x in the carrier of S by C5,DTCONSTR:2; assume b'.x in Union coprod Y; then (b.x in [:the OperSymbols of S,{the carrier of S}:] or b.x in Union coprod X) & b.x nin [:the OperSymbols of S,{the carrier of S}:] by C6,C7,XBOOLE_0:3,def 2; then b.x in coprod((the_arity_of o).x,X) by C1,C4,C5,MSAFREE:def 9; then consider a being set such that C8: a in X.((the_arity_of o).x) & b.x = [a, (the_arity_of o).x] by C9,MSAFREE:def 2; X.((the_arity_of o).x) c= Y.((the_arity_of o).x) by Z0,C9,PBOOLE:def 5; hence b'.x in coprod((the_arity_of o).x,Y) by C8,C9,MSAFREE:def 2; end; hence thesis by C2,MSAFREE:def 9; end; hence thesis by A2,LemTS0; end; theorem LemTerm: for t being set holds t in Terminals DTConMSA MSVars C iff ex x being variable st t = [x,a_Term C] proof let t be set; set X = MSVars C; A0: Terminals DTConMSA X = Union coprod X by ThTNT; A1: dom X = the carrier of C by PBOOLE:def 3; A2: the carrier of C = {a_Type, an_Adj, a_Term} by CONSTRSIGN; A3: X.a_Type = {} & X.an_Adj = {} & X.a_Term = Vars by MSVARS; hereby assume t in Terminals DTConMSA X; then A4: t`2 in dom X & t`1 in X.t`2 & t = [t`1,t`2] by A0,CARD_3:33; then A5: t`2 = a_Type or t`2 = an_Adj or t`2 = a_Term by A1,A2,ENUMSET1:def 1; then reconsider x = t`1 as variable by A3,A4; take x; thus t = [x,a_Term C] by A3,A4,A5; end; given x being variable such that A6: t = [x,a_Term C]; t`1 = x & t`2 = a_Term by A6,MCART_1:7; hence t in Terminals DTConMSA MSVars C by A0,A1,A3,A6,CARD_3:33; end; theorem LemNTerm: 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] proof let t be set; set X = MSVars C; A0: NonTerminals DTConMSA X = [:the OperSymbols of C,{the carrier of C}:] by ThTNT; hereby assume t in NonTerminals DTConMSA MSVars C; then consider a,b being set such that A1: a in the OperSymbols of C & b in {the carrier of C} & t = [a,b] by A0,ZFMISC_1:def 2; reconsider a as OperSymbol of C by A1; b = the carrier of C & (a is constructor or a is not constructor) by A1,TARSKI:def 1; hence 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] by A1,CNSTR2; end; the carrier of C in {the carrier of C} by TARSKI:def 1; hence thesis by A0,ZFMISC_1:106; end; theorem LemFT: 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}) proof let S be non void Signature; let X be with_missing_variables ManySortedSet of the carrier of S; set V = X \/ ((the carrier of S)-->{0}); set A = Free(S, X); set U = the Sorts of A; A1: U = S-Terms(X, V) by MSAFREE3:25; let t be set; assume t in Union U; then consider s being set such that Z1: s in dom U & t in U.s by CARD_5:10; reconsider s as SortSymbol of S by PBOOLE:def 3,Z1; U.s = {r where r is Term of S,V: the_sort_of r = s & variables_in r c= X} by A1,MSAFREE3:def 6; then ex r being Term of S,V st t = r & the_sort_of r = s & variables_in r c= X by Z1; hence thesis; end; theorem 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 proof let S be non void Signature; let X be with_missing_variables ManySortedSet of the carrier of S; set V = X \/ ((the carrier of S)-->{0}); set A = Free(S, X); set U = the Sorts of A; A1: U = S-Terms(X, V) by MSAFREE3:25; let t be Term of S, X \/ ((the carrier of S)-->{0}); assume t in Union U; then consider s being set such that Z1: s in dom U & t in U.s by CARD_5:10; reconsider s as SortSymbol of S by PBOOLE:def 3,Z1; U.s = {r where r is Term of S,V: the_sort_of r = s & variables_in r c= X} by A1,MSAFREE3:def 6; then ex r being Term of S,V st t = r & the_sort_of r = s & variables_in r c= X by Z1; hence thesis by Z1; end; theorem 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 proof let G be non empty DTConstrStr; let s be Element of G; let p be FinSequence; assume s ==> p; then [s,p] in the Rules of G by LANG1:def 1; then p in (the carrier of G)* by ZFMISC_1:106; hence p is FinSequence of the carrier of G by FINSEQ_1:def 11; end; theorem LemArr: 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 proof let S be non void Signature; let X,Y be ManySortedSet of the carrier of S; A1: dom X = the carrier of S & dom Y = the carrier of S by PBOOLE:def 3; set G1 = DTConMSA X; set G2 = DTConMSA Y; let g1 be Symbol of G1; let g2 be Symbol of G2; let p1 be FinSequence of the carrier of G1; let p2 be FinSequence of the carrier of G2; assume A0: g1 = g2 & p1 = p2 & g1 ==> p1; then Y4: [g1, p1] in REL X by LANG1:def 1; then Y5: g1 in [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X) & p1 in ([:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X))* by ZFMISC_1:106; then Y6: g1 in [:the OperSymbols of S,{the carrier of S}:] by Y4,MSAFREE:def 9; Y9: p2 in ([:the OperSymbols of S, {the carrier of S}:] \/ Union (coprod Y))* by FINSEQ_1:def 11; now let o' be OperSymbol of S; assume Y7: [o',the carrier of S] = g2; hence Z4: len p2 = len the_arity_of o' by A0,Y4,Y5,MSAFREE:def 9; let x be set; assume Y8: x in dom p2; hence p2.x in [:the OperSymbols of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = p2.x holds the_result_sort_of o1 = (the_arity_of o').x by A0,Y4,Y5,Y7,MSAFREE:def 9; x in dom the_arity_of o' by Z4,Y8,FINSEQ_3:31; then (the_arity_of o').x in rng the_arity_of o' by FUNCT_1:def 5; then reconsider i = (the_arity_of o').x as SortSymbol of S; assume p2.x in Union coprod Y; then B1: (p2.x)`2 in dom Y & (p2.x)`1 in Y.(p2.x)`2 & p2.x = [(p2.x)`1,(p2.x)`2] by CARD_3:33; p2.x in rng p1 by A0,Y8,FUNCT_1:def 5; then the carrier of S nin the carrier of S & p2.x in [:the OperSymbols of S,{the carrier of S}:] or p2.x in Union coprod X by XBOOLE_0:def 2; then p2.x in coprod(i,X) by A0,Y4,Y5,Y7,Y8,A1,B1,ZFMISC_1:129,MSAFREE:def 9; then consider a being set such that Z3: a in X.i & p2.x = [a,i] by MSAFREE:def 2; i = (p2.x)`2 by B1,Z3,ZFMISC_1:33; hence p2.x in coprod((the_arity_of o').x,Y) by B1,MSAFREE:def 2; end; then [g2, p2] in REL Y by A0,Y6,Y9,MSAFREE:def 9; hence thesis by LANG1:def 1; end; theorem LemTS: 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 proof let S be non void Signature; let X be with_missing_variables ManySortedSet of the carrier of S; set V = X \/ ((the carrier of S)-->{0}); set A = Free(S, X); set U = the Sorts of A; set G = DTConMSA X; A1: U = S-Terms(X, V) by MSAFREE3:25; A2: dom U = the carrier of S by PBOOLE:def 3; defpred P[set] means $1 in Union U implies $1 in TS G; T1: for s being SortSymbol of S, v being Element of V.s holds P[root-tree [v,s]] proof let s be SortSymbol of S; let v be Element of V.s; assume root-tree [v,s] in Union U; then consider s1 being set such that Z1: s1 in dom U & root-tree [v,s] in U.s1 by CARD_5:10; reconsider s1 as SortSymbol of S by Z1,PBOOLE:def 3; U.s1={t where t is Term of S,V: the_sort_of t = s1 & variables_in t c= X} by A1,MSAFREE3:def 6; then consider t being Term of S,V such that Z2: root-tree [v,s] = t & the_sort_of t = s1 & variables_in t c= X by Z1; s1 = s & (variables_in t).s = {v} by Z2,MSATERM:14,MSAFREE3:11; then {v} c= X.s by Z2,PBOOLE:def 5; then v in X.s by ZFMISC_1:37; then [v,s] in Terminals G by MSAFREE:7; hence root-tree [v,s] in TS G by DTCONSTR:def 4; end; T2: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,V) st for t being Term of S,V st t in rng p holds P[t] holds P[[o,the carrier of S]-tree p] proof let o be OperSymbol of S; let p be ArgumentSeq of Sym(o,V) such that Y0: for t being Term of S,V st t in rng p holds P[t] and Y1: [o,the carrier of S]-tree p in Union U; consider s being set such that Z1: s in dom U & [o,the carrier of S]-tree p in U.s by Y1,CARD_5:10; reconsider s as SortSymbol of S by Z1,PBOOLE:def 3; U.s={t where t is Term of S,V: the_sort_of t = s & variables_in t c= X} by A1,MSAFREE3:def 6; then consider t being Term of S,V such that Z2: [o,the carrier of S]-tree p = t & the_sort_of t = s & variables_in t c= X by Z1; t.{} = [o,the carrier of S] by Z2,TREES_4:def 4; then the_result_sort_of o = s by Z2,MSATERM:17; then Y2: rng p c= Union U by A1,Z1,MSAFREE3:20; rng p c= TS G proof let x be set; assume Y3: x in rng p; then x is Term of S,V by Y2,LemFT; hence x in TS G by Y0,Y2,Y3; end; then reconsider q = p as FinSequence of TS G by FINSEQ_1:def 4; NonTerminals G = [:the OperSymbols of S,{the carrier of S}:] by ThTNT; then [o,the carrier of S] in NonTerminals G by ZFMISC_1:129; then reconsider oo = [o,the carrier of S] as Symbol of G; Sym(o,V) ==> roots p by MSATERM:21; then oo ==> roots q by LemArr; hence [o,the carrier of S]-tree p in TS G by DTCONSTR:def 4; end; TT: for t being Term of S,V holds P[t] from MSATERM:sch 1(T1,T2); A4: NonTerminals DTConMSA X = [:the OperSymbols of S,{the carrier of S}:] & Terminals DTConMSA X = Union coprod X by ThTNT; defpred Q[set] means $1 in Union U; D1: for s being Symbol of G st s in Terminals G holds Q[root-tree s] proof let s be Symbol of G; assume s in Terminals G; then B1: s`2 in dom X & s`1 in X.s`2 & s = [s`1,s`2] by A4,CARD_3:33; B2: dom X = the carrier of S & dom U = the carrier of S by PBOOLE:def 3; then root-tree s in (the Sorts of Free(S,X)).s`2 by B1,MSAFREE3:5; hence Q[root-tree s] by B1,B2,CARD_5:10; end; D2: for nt being Symbol of G, ts being FinSequence of TS G st nt ==> roots ts & for t being DecoratedTree of the carrier of G st t in rng ts holds Q[t] holds Q[nt-tree ts] proof let nt be Symbol of G; let ts be FinSequence of TS G such that Z1: nt ==> roots ts and Z2: for t being DecoratedTree of the carrier of G st t in rng ts holds Q[t]; nt in NonTerminals G by Z1; then consider o,z being set such that Z3: o in the OperSymbols of S & z in {the carrier of S} & nt = [o,z] by A4,ZFMISC_1:def 2; reconsider o as OperSymbol of S by Z3; Z5: rng ts c= Union U proof let a be set; assume Z6: a in rng ts; a is DecoratedTree of the carrier of G by Z6,TREES_3:def 6; hence thesis by Z2,Z6; end; rng ts c= TS DTConMSA V proof let a be set; assume a in rng ts; then a is Element of S-TermsV & S-TermsV = TS DTConMSA V by Z5,LemFT,MSATERM:def 1; hence thesis; end; then reconsider p = ts as FinSequence of TS DTConMSA V by FINSEQ_1:def 4; reconsider q = p as FinSequence of S-TermsV by MSATERM:def 1; Z4: z = the carrier of S by Z3,TARSKI:def 1; then Sym(o, V) ==> roots p by Z1,Z3,LemArr; then reconsider q as ArgumentSeq of Sym(o, V) by MSATERM:21; set t = Sym(o, V)-tree q; t in U.the_result_sort_of o by A1,Z5,MSAFREE3:20; hence Q[nt-tree ts] by A2,Z3,Z4,CARD_5:10; end; DD: for t being DecoratedTree of the carrier of G st t in TS G holds Q[t] from DTCONSTR:sch 7(D1,D2); thus Union U c= TS DTConMSA X proof let x be set; assume B1: x in Union U; then consider s being set such that B2: s in dom U & x in U.s by CARD_5:10; reconsider s as SortSymbol of S by PBOOLE:def 3,B2; x in U.s by B2; then x is Term of S,V by A1,MSAFREE3:17; hence thesis by B1,TT; end; let x be set; assume C0: x in TS G; then reconsider TG = TS G as non empty Subset of FinTrees(the carrier of G); x is Element of TG by C0; hence thesis by DD; end; 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 :TT: for s being SortSymbol of S holds it.:((the Sorts of Free(S,X)).s) c= (the Sorts of Free(S,X)).s; existence proof set f = id Union the Sorts of Free(S,X); dom f = Union the Sorts of Free(S,X) & rng f = Union the Sorts of Free(S,X) by RELAT_1:71; then reconsider f as UnOp of Union the Sorts of Free(S,X) by FUNCT_2:4; :: Zamiast RELAT_1:71 i FUNCT_2:4 powinna byc mozliwosc odwolania :: sie do redefinicji PARTFUN1:func 6 take f; thus thesis by Lem'id; end; end; theorem ThTr: 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 proof let S be non void Signature; let X be non empty ManySortedSet of the carrier of S; A0: dom the Sorts of Free(S,X) = the carrier of S by PBOOLE:def 3; let f be UnOp of Union the Sorts of Free(S,X); A1: dom f = Union the Sorts of Free(S,X) by FUNCT_2:67; hereby assume Z0: f is term-transformation of S,X; let s be SortSymbol of S; Z1: f.:((the Sorts of Free(S,X)).s) c= (the Sorts of Free(S,X)).s by TT,Z0; (the Sorts of Free(S,X)).s in rng the Sorts of Free(S,X) by A0,FUNCT_1:def 5; then Z2: (the Sorts of Free(S,X)).s c= Union the Sorts of Free(S,X) by ZFMISC_1:92; let a be set; assume a in (the Sorts of Free(S,X)).s; then f.a in f.:((the Sorts of Free(S,X)).s) by A1,Z2,FUNCT_1:def 12; hence f.a in (the Sorts of Free(S,X)).s by Z1; end; assume A2: 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; let s be SortSymbol of S; let x be set; assume x in f.:((the Sorts of Free(S,X)).s); then ex a being set st a in dom f & a in (the Sorts of Free(S,X)).s & x = f.a by FUNCT_1:def 12; hence x in (the Sorts of Free(S,X)).s by A2; end; theorem ThTr2: 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 qua set) = len p proof let S be non void Signature; let X be non empty ManySortedSet of the carrier of S; set A = Free(S,X); let f be term-transformation of S,X; let s be SortSymbol of S; let p be FinSequence of (the Sorts of A).s; Union the Sorts of A = {} or Union the Sorts of A <> {}; then Z1: dom the Sorts of A = the carrier of S & dom f = Union the Sorts of A by PBOOLE:def 3,FUNCT_2:def 1; (the Sorts of A).s in rng the Sorts of A by Z1,FUNCT_1:def 5; then (the Sorts of A).s c= Union the Sorts of A by ZFMISC_1:92; then rng p c= dom f by Z1,XBOOLE_1:1; then Z7: dom (f*p) = dom p by RELAT_1:46; dom p = Seg len p by FINSEQ_1:def 3; then Z2: f*p is FinSequence by Z7,FINSEQ_1:def 2; rng(f*p) c= (the Sorts of A).s proof let z be set; assume z in rng(f*p); then consider i being set such that V1: i in dom(f*p) & z = (f*p).i by FUNCT_1:def 5; p.i in rng p by Z7,V1,FUNCT_1:def 5; then f.(p.i) in (the Sorts of A).s by ThTr; hence thesis by V1,FUNCT_1:22; end; hence f*p is FinSequence of (the Sorts of Free(S,X)).s by Z2,FINSEQ_1:def 4; then reconsider q = f*p as FinSequence of (the Sorts of A).s; thus Card (f*p qua set) = len q .= len p by Z7,FINSEQ_3:31; end; definition let S be non void Signature; let X be ManySortedSet of the carrier of S; let t be term-transformation of S,X; attr t is substitution means 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; scheme StructDef {C() -> initialized ConstructorSignature, V,N(set) -> (expression of C()), F,A(set,set) -> (expression of C())}: ex f being term-transformation of C(), MSVars C() st (for x being variable holds f.(x-term C()) = V(x)) & (for c being constructor OperSymbol of C() for p,q being FinSequence of QuasiTerms C() st len p = len the_arity_of c & q = f*p holds f.(c-trm p) = F(c, q)) & (for a being expression of C(), an_Adj C() holds f.((non_op C())term a) = N(f.a)) & (for a being expression of C(), an_Adj C() for t being expression of C(), a_Type C() holds f.((ast C())term(a,t)) = A(f.a, f.t)) provided A1: for x being variable holds V(x) is quasi-term of C() and A2: for c being constructor OperSymbol of C() for p being FinSequence of QuasiTerms C() st len p = len the_arity_of c holds F(c, p) is expression of C(), the_result_sort_of c and A3: for a being expression of C(), an_Adj C() holds N(a) is expression of C(), an_Adj C() and A4: for a being expression of C(), an_Adj C() for t being expression of C(), a_Type C() holds A(a,t) is expression of C(), a_Type C() proof set V = MSVars C(); set X = V\/((the carrier of C())-->{0}); set A = Free(C(), V); set U = the Sorts of A; set D = Union U; set G = DTConMSA V; deffunc TermVal(Symbol of G) = V($1`1); deffunc NTermVal(Symbol of G, FinSequence, Function) = IFEQ($1`1,*, A($3.1,$3.2), IFEQ($1`1,non_op, N($3.1), F($1`1,$3))); consider f being Function of TS G, D such that A6: for t being Symbol of G st t in Terminals G holds f.(root-tree t) = TermVal(t) and A7: for nt being Symbol of G, ts being FinSequence of TS G st nt ==> roots ts holds f.(nt-tree ts) = NTermVal(nt, roots ts, f * ts) from DTCONSTR:sch 8; A5: D = TS G by LemTS; then reconsider f as Function of D,D; f is term-transformation of C(), V proof let s be SortSymbol of C(); let x be set; assume x in f.:((the Sorts of A).s); then consider a being Element of D such that B1: a in (the Sorts of A).s & x = f.a by FUNCT_2:116; defpred P[expression of C()] means for s being SortSymbol of C() st $1 in (the Sorts of A).s holds f.$1 in (the Sorts of A).s; W1: for x being variable holds P[x-term C()] proof let y be variable; set a = y-term C(); let s be SortSymbol of C(); assume C1: a in (the Sorts of A).s; C2: [y,a_Term C()] in Terminals G by LemTerm; then reconsider t = [y,a_Term C()] as Symbol of G; f.a = TermVal(t) by A6,C2 .= V(y) by MCART_1:7; then C3: f.a is quasi-term of C() & a is expression of C(), s by A1,C1,ELEMENT; then s = a_Term C() by Th90A; hence thesis by C3,ELEMENT; end; W2: for c being constructor OperSymbol of C() for p being FinSequence of QuasiTerms C() st len p = len the_arity_of c & for t being quasi-term of C() st t in rng p holds P[t] holds P[c-trm p] proof let c be constructor OperSymbol of C(); let p be FinSequence of QuasiTerms C(); assume that Z0: len p = len the_arity_of c and Z1: for t being quasi-term of C() st t in rng p holds P[t]; set a = c-trm p; set nt = [c, the carrier of C()]; let s be SortSymbol of C() such that 00: a in (the Sorts of A).s; nt in NonTerminals G by LemNTerm; then reconsider nt as Symbol of G; reconsider ts = p as FinSequence of TS G by A5; Z3: a = nt-tree ts by Z0,TERM; reconsider aa = a as Term of C(), X by MSAFREE3:9; the Sorts of A = C()-Terms(V,X) by MSAFREE3:25; then the Sorts of A c= the Sorts of FreeMSA X by PBOOLE:def 23; then (the Sorts of A).s c= (the Sorts of FreeMSA X).s by PBOOLE:def 5; then aa in (FreeSort X).s by 00; then aa in FreeSort(X,s) by MSAFREE:def 13; then 01: the_sort_of aa = s by MSATERM:def 5; Z4: nt`1 = c & c <> * & c <> non_op by CNSTR2,MCART_1:7; Z5: rng p c= QuasiTerms C() by FINSEQ_1:def 4; dom f = D by FUNCT_2:def 1; then Z7: rng p c= dom f; rng(f*p) c= QuasiTerms C() proof let z be set; assume z in rng(f*p); then consider i being set such that V1: i in dom(f*p) & z = (f*p).i by FUNCT_1:def 5; i in dom p by V1,Z7,RELAT_1:46; then V2: p.i in rng p by FUNCT_1:def 5; then reconsider pi = p.i as quasi-term of C() by Z5,Th42; pi in (the Sorts of A).a_Term C() & P[pi] by Z1,V2,Th42; then f.pi in (the Sorts of A).a_Term C(); hence thesis by V1,FUNCT_1:22; end; then reconsider q = f*p as FinSequence of QuasiTerms C() by FINSEQ_1:def 4; rng p c= C()-Terms X proof let z be set; assume z in rng p; then z is Element of C()-TermsX by MSAFREE3:9; hence thesis; end; then reconsider r = p as FinSequence of C()-Terms X by FINSEQ_1:def 4; Z6: len q = len p by Z7,FINSEQ_2:33; a is Term of C(), X by MSAFREE3:9; then r is ArgumentSeq of Sym(c, X) by Z3,MSATERM:1; then 02: the_result_sort_of c = s & Sym(c, X) ==> roots r by 01,Z3,MSATERM:20,21; then nt ==> roots ts by LemArr; then f.a = NTermVal(nt, roots ts, f * ts) by A7,Z3 .= IFEQ(c,non_op, N((f * ts).1), F(c, f * ts)) by Z4,FUNCOP_1:def 8 .= F(c, f * ts) by Z4,FUNCOP_1:def 8; then f.a is expression of C(), the_result_sort_of c by Z0,Z6,A2; hence f.a in (the Sorts of A).s by 02,ELEMENT; end; W3: for a being expression of C(), an_Adj C() st P[a] holds P[(non_op C())term a] proof let v be expression of C(), an_Adj C() such that Z1: P[v]; Y1: v in U.an_Adj C() by ELEMENT; then Y2: f.v in U.an_Adj C() by Z1; then reconsider fv = f.v as expression of C(), an_Adj C() by ELEMENT; let s be SortSymbol of C(); assume 00: (non_op C())term v in U.s; then (non_op C())term v is expression of C(), an_Adj C() & (non_op C())term v is expression of C(), s by ELEMENT,ThNon; then 03: s = an_Adj C() by Th90A; set QA = U.an_Adj C(); rng <*v*> = {v} by FINSEQ_1:55; then rng <*v*> c= QA by Y1,ZFMISC_1:37; then reconsider p = <*v*> as FinSequence of QA by FINSEQ_1:def 4; set c = non_op C(); set a = (non_op C())term v; set nt = [c, the carrier of C()]; nt in NonTerminals G by LemNTerm; then reconsider nt as Symbol of G; reconsider ts = p as FinSequence of TS G by A5; Z3: a = nt-tree ts by ThNon; reconsider aa = a as Term of C(), X by MSAFREE3:9; the Sorts of A = C()-Terms(V,X) by MSAFREE3:25; then the Sorts of A c= the Sorts of FreeMSA X by PBOOLE:def 23; then (the Sorts of A).s c= (the Sorts of FreeMSA X).s by PBOOLE:def 5; then aa in (FreeSort X).s by 00; then aa in FreeSort(X,s) by MSAFREE:def 13; then 01: the_sort_of aa = s by MSATERM:def 5; Z4: nt`1 = c & c <> * by MCART_1:7; dom f = D by FUNCT_2:def 1; then 08: f*p = <*fv*> by BAGORDER:3; rng <*fv*> = {fv} by FINSEQ_1:55; then rng <*fv*> c= QA by Y2,ZFMISC_1:37; then reconsider q = f*p as FinSequence of QA by 08,FINSEQ_1:def 4; rng p c= C()-Terms X proof let z be set; assume z in rng p; then z is expression of C(), an_Adj C() by Th42; then z is Element of C()-TermsX by MSAFREE3:9; hence thesis; end; then reconsider r = p as FinSequence of C()-Terms X by FINSEQ_1:def 4; a is Term of C(), X by MSAFREE3:9; then r is ArgumentSeq of Sym(c, X) by Z3,MSATERM:1; then the_result_sort_of c = s & Sym(c, X) ==> roots r by 01,Z3,MSATERM:20,21; then nt ==> roots ts by LemArr; then f.a = NTermVal(nt, roots ts, f * ts) by A7,Z3 .= IFEQ(c,non_op, N((f * ts).1), F(c, f * ts)) by Z4,FUNCOP_1:def 8 .= N((f*ts).1) by FUNCOP_1:def 8 .= N(fv) by 08,FINSEQ_1:57; then f.a is expression of C(), an_Adj C() by A3; hence f.a in (the Sorts of A).s by 03,ELEMENT; end; W4: for a being expression of C(), an_Adj C() st P[a] for t being expression of C(), a_Type C() st P[t] holds P[(ast C())term(a,t)] proof let v be expression of C(), an_Adj C() such that Z0: P[v]; let t be expression of C(), a_Type C() such that Z1: P[t]; v in U.an_Adj C() & t in U.a_Type C() by ELEMENT; then Y2: f.v in U.an_Adj C() & f.t in U.a_Type C() by Z0,Z1; then reconsider fv = f.v as expression of C(), an_Adj C() by ELEMENT; reconsider ft = f.t as expression of C(), a_Type C() by Y2,ELEMENT; let s be SortSymbol of C(); assume 00: (ast C())term(v,t) in U.s; then (ast C())term(v,t) is expression of C(), a_Type C() & (ast C())term(v,t) is expression of C(), s by ELEMENT,ThAst; then 03: s = a_Type C() by Th90A; set QA = U.a_Type C(); reconsider p = <*v,t*> as FinSequence of D; set c = ast C(); set a = (ast C())term(v,t); set nt = [c, the carrier of C()]; nt in NonTerminals G by LemNTerm; then reconsider nt as Symbol of G; reconsider ts = p as FinSequence of TS G by A5; Z3: a = nt-tree ts by ThAst; reconsider aa = a as Term of C(), X by MSAFREE3:9; the Sorts of A = C()-Terms(V,X) by MSAFREE3:25; then the Sorts of A c= the Sorts of FreeMSA X by PBOOLE:def 23; then (the Sorts of A).s c= (the Sorts of FreeMSA X).s by PBOOLE:def 5; then aa in (FreeSort X).s by 00; then aa in FreeSort(X,s) by MSAFREE:def 13; then 01: the_sort_of aa = s by MSATERM:def 5; Z4: nt`1 = c & c <> non_op by MCART_1:7; 08: f*p = <*fv,ft*> by FINSEQ_2:40; reconsider q = f*p as FinSequence of D; rng p c= C()-Terms X proof let z be set; assume z in rng p; then z is Element of C()-TermsX by MSAFREE3:9; hence thesis; end; then reconsider r = p as FinSequence of C()-Terms X by FINSEQ_1:def 4; a is Term of C(), X by MSAFREE3:9; then r is ArgumentSeq of Sym(c, X) by Z3,MSATERM:1; then the_result_sort_of c = s & Sym(c, X) ==> roots r by 01,Z3,MSATERM:20,21; then nt ==> roots ts by LemArr; then f.a = NTermVal(nt, roots ts, f * ts) by A7,Z3 .= A((f*ts).1,(f*ts).2) by Z4,FUNCOP_1:def 8 .= A(fv,(f*ts).2) by 08,FINSEQ_1:61 .= A(fv,ft) by 08,FINSEQ_1:61; then f.a is expression of C(), a_Type C() by A4; hence f.a in (the Sorts of A).s by 03,ELEMENT; end; P[a] from StructInd(W1,W2,W3,W4); hence thesis by B1; end; then reconsider f as term-transformation of C(), MSVars C(); take f; hereby let x be variable; x in Vars; then 00: x in V.a_Term C() by MSVARS; then reconsider x' = x as Element of V.a_Term C(); reconsider xx = [x',a_Term C()] as Symbol of G by 00,MSAFREE3:3; x-term C() = root-tree xx & xx in Terminals G by 00,MSAFREE:7; hence f.(x-term C()) = V(xx`1) by A6 .= V(x) by MCART_1:7; end; hereby let c be constructor OperSymbol of C(); the carrier of C() in {the carrier of C()} by TARSKI:def 1; then [c, the carrier of C()]in[:the OperSymbols of C(),{the carrier of C()}:] by ZFMISC_1:106; then reconsider cc = [c,the carrier of C()] as Symbol of G by XBOOLE_0:def 2; let p,q be FinSequence of QuasiTerms C(); assume Z0: len p = len the_arity_of c & q = f*p; set a = c-trm p; set nt = [c, the carrier of C()]; nt in NonTerminals G by LemNTerm; then reconsider nt as Symbol of G; reconsider ts = p as FinSequence of TS G by A5; Z3: a = nt-tree ts by Z0,TERM; reconsider aa = a as Term of C(), X by MSAFREE3:9; Z4: nt`1 = c & c <> * & c <> non_op by CNSTR2,MCART_1:7; rng p c= C()-Terms X proof let z be set; assume z in rng p; then z is Element of C()-TermsX by MSAFREE3:9; hence thesis; end; then reconsider r = p as FinSequence of C()-Terms X by FINSEQ_1:def 4; a is Term of C(), X by MSAFREE3:9; then r is ArgumentSeq of Sym(c, X) by Z3,MSATERM:1; then Sym(c, X) ==> roots r by MSATERM:21; then nt ==> roots ts by LemArr; then f.a = NTermVal(nt, roots ts, f * ts) by A7,Z3 .= IFEQ(c,non_op, N((f * ts).1), F(c, f * ts)) by Z4,FUNCOP_1:def 8 .= F(c, f * ts) by Z4,FUNCOP_1:def 8; hence f.(c-trm p) = F(c, q) by Z0; end; hereby let v be expression of C(), an_Adj C(); Y1: v in U.an_Adj C() by ELEMENT; then Y2: f.v in U.an_Adj C() by ThTr; then reconsider fv = f.v as expression of C(), an_Adj C() by ELEMENT; set QA = U.an_Adj C(); rng <*v*> = {v} by FINSEQ_1:55; then rng <*v*> c= QA by Y1,ZFMISC_1:37; then reconsider p = <*v*> as FinSequence of QA by FINSEQ_1:def 4; set c = non_op C(); set a = (non_op C())term v; set nt = [c, the carrier of C()]; nt in NonTerminals G by LemNTerm; then reconsider nt as Symbol of G; reconsider ts = p as FinSequence of TS G by A5; Z3: a = nt-tree ts by ThNon; reconsider aa = a as Term of C(), X by MSAFREE3:9; Z4: nt`1 = c & c <> * by MCART_1:7; dom f = D by FUNCT_2:def 1; then 08: f*p = <*fv*> by BAGORDER:3; rng <*fv*> = {fv} by FINSEQ_1:55; then rng <*fv*> c= QA by Y2,ZFMISC_1:37; then reconsider q = f*p as FinSequence of QA by 08,FINSEQ_1:def 4; rng p c= C()-Terms X proof let z be set; assume z in rng p; then z is expression of C(), an_Adj C() by Th42; then z is Element of C()-TermsX by MSAFREE3:9; hence thesis; end; then reconsider r = p as FinSequence of C()-Terms X by FINSEQ_1:def 4; a is Term of C(), X by MSAFREE3:9; then r is ArgumentSeq of Sym(c, X) by Z3,MSATERM:1; then Sym(c, X) ==> roots r by MSATERM:21; then nt ==> roots ts by LemArr; then f.a = NTermVal(nt, roots ts, f * ts) by A7,Z3 .= IFEQ(c,non_op, N((f * ts).1), F(c, f * ts)) by Z4,FUNCOP_1:def 8 .= N((f*ts).1) by FUNCOP_1:def 8; hence f.((non_op C())term v) = N(f.v) by 08,FINSEQ_1:57; end; let v be expression of C(), an_Adj C(); let t be expression of C(), a_Type C(); v in U.an_Adj C() & t in U.a_Type C() by ELEMENT; then Y2: f.v in U.an_Adj C() & f.t in U.a_Type C() by ThTr; then reconsider fv = f.v as expression of C(), an_Adj C() by ELEMENT; reconsider ft = f.t as expression of C(), a_Type C() by Y2,ELEMENT; reconsider p = <*v,t*> as FinSequence of D; set c = ast C(); set a = (ast C())term(v,t); set nt = [c, the carrier of C()]; nt in NonTerminals G by LemNTerm; then reconsider nt as Symbol of G; reconsider ts = p as FinSequence of TS G by A5; Z3: a = nt-tree ts by ThAst; reconsider aa = a as Term of C(), X by MSAFREE3:9; Z4: nt`1 = c & c <> non_op by MCART_1:7; 08: f*p = <*fv,ft*> by FINSEQ_2:40; reconsider q = f*p as FinSequence of D; rng p c= C()-Terms X proof let z be set; assume z in rng p; then z is Element of C()-TermsX by MSAFREE3:9; hence thesis; end; then reconsider r = p as FinSequence of C()-Terms X by FINSEQ_1:def 4; a is Term of C(), X by MSAFREE3:9; then r is ArgumentSeq of Sym(c, X) by Z3,MSATERM:1; then Sym(c, X) ==> roots r by MSATERM:21; then nt ==> roots ts by LemArr; then f.a = NTermVal(nt, roots ts, f * ts) by A7,Z3 .= A((f*ts).1,(f*ts).2) by Z4,FUNCOP_1:def 8 .= A(fv,(f*ts).2) by 08,FINSEQ_1:61; hence thesis by 08,FINSEQ_1:61; end; begin :: Substitution definition let A be set; let x,y be set; let a,b be Element of A; redefine func IFIN(x,y,a,b) -> Element of A; coherence 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; attr f is irrelevant means: IRR: for x being variable st x in dom f ex y being variable st f.x = y-term C; end; notation let C be initialized ConstructorSignature; let f be valuation of C; antonym f is relevant for f is irrelevant; end; registration let X,Y be set; cluster empty PartFunc of X,Y; existence proof dom {} = {}; then {} is PartFunc of X,Y by PARTFUN1:55; hence thesis; end; end; registration let C be initialized ConstructorSignature; cluster empty -> irrelevant valuation of C; coherence proof let f be valuation of C; assume f is empty; then reconsider f as empty valuation of C; let x be variable; dom f = {}; hence thesis; end; end; registration let C be initialized ConstructorSignature; cluster empty irrelevant one-to-one valuation of C; existence proof consider f being empty valuation of C; take f; thus thesis; end; end; definition let C be initialized ConstructorSignature; let X be Subset of Vars; func C idval X -> valuation of C equals {[x, x-term C] where x is variable: x in X}; coherence proof set f = {[x, x-term C] where x is variable: x in X}; defpred P[variable,set] means $2 = $1-term C; AA: now let x be variable; reconsider t = x-term C as Element of QuasiTerms C by ELEMENT; take t; thus P[x,t]; end; consider g being Function of Vars, QuasiTerms C such that A0: for x being variable holds P[x,g.x] from FUNCT_2:sch 3(AA); A1: f c= g proof let a be set; assume a in f; then consider x being variable such that A2: a = [x, x-term C] & x in X; g.x = x-term C & dom g = Vars by A0,FUNCT_2:def 1; hence thesis by A2,FUNCT_1:8; end; then f is Function by GRFUNC_1:6; hence thesis by A1,PARTFUN1:33; end; end; theorem ThIV: 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 proof let X be Subset of Vars; set f = C idval X; thus dom f c= X proof let a being set; assume a in dom f; then [a,f.a] in f by FUNCT_1:def 4; then ex x being variable st [a,f.a] = [x,x-term C] & x in X; hence thesis by ZFMISC_1:33; end; hereby let x be set; assume A0: x in X; then reconsider a = x as variable; [a,a-term C] in f by A0; hence x in dom f by FUNCT_1:8; end; let x be variable; assume x in X; then [x,x-term C] in C idval X; hence (C idval X).x = x-term C by FUNCT_1:8; end; registration let C be initialized ConstructorSignature; let X be Subset of Vars; cluster C idval X -> irrelevant one-to-one; coherence proof set f = C idval X; A1: dom f = X by ThIV; hereby let x be variable; assume A0: x in dom f; take y = x; thus f.x = y-term C by A0,A1,ThIV; end; let x,y be set; assume A2: x in dom f & y in dom f; then reconsider x,y as variable; f.x = x-term C & f.y = y-term C by A1,A2,ThIV; hence thesis by ThT0; end; end; registration let C be initialized ConstructorSignature; let X be empty Subset of Vars; cluster C idval X -> empty; coherence proof dom (C idval X) = X by ThIV; hence thesis by RELAT_1:64; end; end; definition let C; let f be valuation of C; func f# -> term-transformation of C, MSVars C means: SUBST: (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 proof deffunc V(variable) = IFIN($1, dom f, (f/.$1 qua Element of (QuasiTerms C) qua non empty Subset of Free(C, MSVars C)) qua (expression of C), $1-term C); deffunc F(constructor OperSymbol of C,FinSequence of QuasiTerms C) = $1-trm $2; deffunc N(expression of C) = (non_op C)term $1; deffunc A((expression of C), expression of C) = (ast C)term($1,$2); A1: for x being variable holds V(x) is quasi-term of C proof let x be variable; (x in dom f or not x in dom f) & f/.x is quasi-term of C & x-term C is quasi-term of C by Th42; hence V(x) is quasi-term of C by MATRIX_7:def 1; end; A2: for c being constructor OperSymbol of C for p being FinSequence of QuasiTerms C st len p = len the_arity_of c holds F(c, p) is expression of C, the_result_sort_of c by Th43c; A3: for a holds N(a) is expression of C, an_Adj C by ThNon; A4: for a,t holds A(a,t) is expression of C, a_Type C by ThAst; consider f' being term-transformation of C, MSVars C such that A5: (for x being variable holds f'.(x-term C) = V(x)) & (for c being constructor OperSymbol of C for p,q being FinSequence of QuasiTerms C st len p = len the_arity_of c & q = f'*p holds f'.(c-trm p) = F(c, q)) & (for a holds f'.((non_op C)term a) = N(f'.a)) & (for a,t holds f'.((ast C)term(a,t)) = A(f'.a, f'.t)) from StructDef(A1,A2,A3,A4); take f'; hereby let x be variable; A6: f'.(x-term C) = V(x) by A5; x in dom f implies f/.x = f.x by PARTFUN1:def 8; hence x in dom f implies f'.(x-term C) = f.x by A6,MATRIX_7:def 1; thus not x in dom f implies f'.(x-term C) = x-term C by A6,MATRIX_7:def 1; end; thus thesis by A5; end; correctness proof let f1,f2 be term-transformation of C, MSVars C such that A1: (for x being variable holds (x in dom f implies f1.(x-term C) = f.x) & (not x in dom f implies f1.(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 = f1*p holds f1.(c-trm p) = c-trm q) & (for a being expression of C, an_Adj C holds f1.((non_op C)term a) = (non_op C)term (f1.a)) & (for a being expression of C, an_Adj C for t being expression of C, a_Type C holds f1.((ast C)term(a,t)) = (ast C)term(f1.a, f1.t)) and A2: (for x being variable holds (x in dom f implies f2.(x-term C) = f.x) & (not x in dom f implies f2.(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 = f2*p holds f2.(c-trm p) = c-trm q) & (for a being expression of C, an_Adj C holds f2.((non_op C)term a) = (non_op C)term (f2.a)) & (for a being expression of C, an_Adj C for t being expression of C, a_Type C holds f2.((ast C)term(a,t)) = (ast C)term(f2.a, f2.t)); set D = Union the Sorts of Free(C, MSVars C); A3: dom f1 = D & dom f2 = D by FUNCT_2:def 1; defpred P[expression of C] means f1.$1 = f2.$1; W1: for x being variable holds P[x-term C] proof let x be variable; x in dom f or x nin dom f; then x in dom f & f1.(x-term C) = f.x or x nin dom f & f1.(x-term C) = x-term C by A1; hence P[x-term C] by A2; end; W2: for c being constructor OperSymbol of C for p being FinSequence of QuasiTerms C st len p = len the_arity_of c & for t being quasi-term of C st t in rng p holds P[t] holds P[c-trm p] proof let c be constructor OperSymbol of C; let p be FinSequence of QuasiTerms C; assume that Z0: len p = len the_arity_of c and Z1: for t being quasi-term of C st t in rng p holds P[t]; Z3: rng p c= QuasiTerms C & rng(f1*p) = f1.:rng p & rng(f2*p) = f2.:rng p by RELAT_1:160,FINSEQ_1:def 4; then rng(f1*p) c= f1.:QuasiTerms C & rng(f2*p) c= f2.:QuasiTerms C & f1.:QuasiTerms C c= QuasiTerms C & f2.:QuasiTerms C c= QuasiTerms C by TT,RELAT_1:156; then rng(f1*p) c= QuasiTerms C & rng(f2*p) c= QuasiTerms C by XBOOLE_1:1; then reconsider q1 = f1*p, q2 = f2*p as FinSequence of QuasiTerms C by FINSEQ_1:def 4; rng p c= D; then Z2: dom q1 = dom p & dom q2 = dom p by A3,RELAT_1:46; now let i be Nat; assume i in dom p; then 00: q1.i = f1.(p.i) & q2.i = f2.(p.i) & p.i in rng p by FUNCT_1:23,def 5; then p.i is quasi-term of C by Z3,Th42; hence q1.i = q2.i by Z1,00; end; then q1 = q2 by Z2,FINSEQ_1:17; then f1.(c-trm p) = c-trm q2 by A1,Z0; hence P[c-trm p] by A2,Z0; end; W3: for a being expression of C, an_Adj C st P[a] holds P[(non_op C)term a] proof let a be expression of C, an_Adj C; assume P[a]; then f1.((non_op C)term a) = (non_op C)term (f2.a) by A1; hence P[(non_op C)term a] by A2; end; W4: for a being expression of C, an_Adj C st P[a] for t being expression of C, a_Type C st P[t] holds P[(ast C)term(a,t)] proof let a be expression of C, an_Adj C such that Y0: P[a]; let t be expression of C, a_Type C; assume P[t]; then f1.((ast C)term(a,t)) = (ast C)term(f2.a,f2.t) by A1,Y0; hence P[(ast C)term(a,t)] by A2; end; now let t be expression of C; thus P[t] from StructInd(W1,W2,W3,W4); end; hence thesis by FUNCT_2:113; end; end; registration let C; let f be valuation of C; cluster f# -> substitution; coherence proof let o be OperSymbol of C; let p,q be FinSequence of Free(C, MSVars C) such that 00: [o, the carrier of C]-tree p in Union the Sorts of Free(C, MSVars C) & q = f# *p; 0D: dom (f# ) = Union the Sorts of Free(C, MSVars C) by FUNCT_2:def 1; reconsider t = [o, the carrier of C]-tree p as expression of C by 00; 0R: t.{} = [o, the carrier of C] by TREES_4:def 4; set V = (MSVars C)\/((the carrier of C)-->{0}); per cases by CNSTR2; suppose o is constructor; then reconsider c = o as constructor OperSymbol of C; t = [c, the carrier of C]-tree p; then 01: len p = len the_arity_of c & p in (QuasiTerms C)* by Th83; then reconsider p' = p as FinSequence of QuasiTerms C by FINSEQ_1:def 11; reconsider q' = f# *p' as FinSequence of QuasiTerms C by ThTr2; 02: len q' = len p by ThTr2; thus f# .([o, the carrier of C]-tree p) = f# .(c-trm p') by 01,TERM .= c-trm q' by 01,SUBST .= [o, the carrier of C]-tree q by 00,01,02,TERM; end; suppose X0: o = *; then consider a being expression of C, an_Adj C, s being expression of C, a_Type C such that X1: t = (ast C)term(a,s) by 0R,ThAst2; a in (the Sorts of Free(C, MSVars C)).an_Adj C by ELEMENT; then f#.a in (the Sorts of Free(C, MSVars C)).an_Adj C by ThTr; then reconsider fa = f#.a as expression of C, an_Adj C by Th42; s in (the Sorts of Free(C, MSVars C)).a_Type C by ELEMENT; then f#.s in (the Sorts of Free(C, MSVars C)).a_Type C by ThTr; then reconsider fs = f#.s as expression of C, a_Type C by Th42; t = [ast C, the carrier of C]-tree <*a,s*> by X1,ThAst; then p = <*a,s*> & a in dom (f# ) & s in dom(f# ) by 0D,TREES_4:15; then q = <*fa, fs*> by 00,FINSEQ_2:145; then [o, the carrier of C]-tree q = (ast C)term(fa, fs) by X0,ThAst; hence f# .([o, the carrier of C]-tree p) = [o, the carrier of C]-tree q by X1,SUBST; end; suppose X0: o = non_op; then consider a such that X1: t = (non_op C)term a by 0R,ThNon2; a in (the Sorts of Free(C, MSVars C)).an_Adj C by ELEMENT; then f#.a in (the Sorts of Free(C, MSVars C)).an_Adj C by ThTr; then reconsider fa = f#.a as expression of C, an_Adj C by Th42; t = [non_op C, the carrier of C]-tree <*a*> by X1,ThNon; then p = <*a*> & a in dom (f# ) by 0D,TREES_4:15; then q = <*fa*> by 00,BAGORDER:3; then [o, the carrier of C]-tree q = (non_op C)term fa by X0,ThNon; hence f# .([o, the carrier of C]-tree p) = [o, the carrier of C]-tree q by X1,SUBST; end; end; end; reserve f for valuation of C; definition let C,f,e; func e at f -> expression of C equals f#.e; coherence; end; definition let C,f; let p be FinSequence such that A: rng p c= Union the Sorts of Free(C, MSVars C); func p at f -> FinSequence equals: PF: f# * p; coherence proof set A = Free(C, MSVars C); dom (f# ) = Union the Sorts of A by FUNCT_2:def 1; then Z7: dom (f# *p) = dom p by A,RELAT_1:46; dom p = Seg len p by FINSEQ_1:def 3; hence f# *p is FinSequence by Z7,FINSEQ_1:def 2; end; end; definition let C,f; let p be FinSequence of QuasiTerms C; redefine func p at f -> FinSequence of QuasiTerms C equals f# * p; coherence proof A1: f# *p is FinSequence of QuasiTerms C by ThTr2; rng p c= Union the Sorts of Free(C, MSVars C); hence thesis by A1,PF; end; compatibility proof rng p c= Union the Sorts of Free(C, MSVars C); hence thesis by PF; end; end; reserve x for variable; theorem ::? not x in dom f implies (x-term C)at f = x-term C by SUBST; theorem ::? x in dom f implies (x-term C)at f = f.x by SUBST; theorem ThS1: ::? len p = len the_arity_of c implies (c-trm p)at f = c-trm p at f by SUBST; theorem ::? ((non_op C)term a)at f = (non_op C)term(a at f) by SUBST; theorem ::? ((ast C)term(a,t))at f = (ast C)term(a at f,t at f) by SUBST; theorem ThS2': for X being Subset of Vars holds e at (C idval X) = e proof set t = e; let X be Subset of Vars; set f = C idval X; defpred P[expression of C] means $1 at f = $1; W1: for x being variable holds P[x-term C] proof let x be variable; (x in X or x nin X) & dom f = X & (x in X implies f.x = x-term C) by ThIV; hence thesis by SUBST; end; W2: for c being constructor OperSymbol of C for p being FinSequence of QuasiTerms C st len p = len the_arity_of c & for t being quasi-term of C st t in rng p holds P[t] holds P[c-trm p] proof let c be constructor OperSymbol of C; let p be FinSequence of QuasiTerms C such that Z0: len p = len the_arity_of c and Z1: for t being quasi-term of C st t in rng p holds P[t]; len (p at f) = len p by ThTr2; then Z2: dom (p at f) = dom p by FINSEQ_3:31; now let i be Nat; assume i in dom p; then Z3: (p at f).i = f# .(p.i) & p.i in rng p by FUNCT_1:23,def 5; rng p c= QuasiTerms C by FINSEQ_1:def 4; then reconsider pi = p.i as quasi-term of C by Z3,Th42; (p at f).i = pi at f by Z3; hence (p at f).i = p.i by Z1,Z3; end; then p at f = p by Z2,FINSEQ_1:17; hence P[c-trm p] by Z0,SUBST; end; W3: for a being expression of C, an_Adj C st P[a] holds P[(non_op C)term a] by SUBST; W4: for a being expression of C, an_Adj C st P[a] for t being expression of C, a_Type C st P[t] holds P[(ast C)term(a,t)] by SUBST; thus P[t] from StructInd(W1,W2,W3,W4); end; theorem for X being Subset of Vars holds (C idval X)# = id Union the Sorts of Free(C, MSVars C) proof let X be Subset of Vars; set f = C idval X; A0: dom (f# ) = Union the Sorts of Free(C, MSVars C) by FUNCT_2:def 1; now let x be set; assume x in Union the Sorts of Free(C, MSVars C); then reconsider t = x as expression of C; thus (f# ).x = t at f .= x by ThS2'; end; hence f# = id Union the Sorts of Free(C, MSVars C) by A0,FUNCT_1:34; end; theorem ThS2: for f being empty valuation of C holds e at f = e proof let f be empty valuation of C; consider X being empty Subset of Vars; f = C idval X; hence thesis by ThS2'; end; theorem for f being empty valuation of C holds f# = id Union the Sorts of Free(C, MSVars C) proof let f be empty valuation of C; A0: dom (f# ) = Union the Sorts of Free(C, MSVars C) by FUNCT_2:def 1; now let x be set; assume x in Union the Sorts of Free(C, MSVars C); then reconsider t = x as expression of C; thus (f# ).x = t at f .= x by ThS2; end; hence f# = id Union the Sorts of Free(C, MSVars C) by A0,FUNCT_1:34; end; :: 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,f; let t be quasi-term of C; redefine func t at f -> quasi-term of C; coherence proof t in QuasiTerms C by ELEMENT; then t at f in QuasiTerms C by ThTr; hence thesis by Th42; end; end; definition let C,f; let a be expression of C, an_Adj C; redefine func a at f -> expression of C, an_Adj C; coherence proof a in (the Sorts of Free(C, MSVars C)).an_Adj C by ELEMENT; then a at f in (the Sorts of Free(C, MSVars C)).an_Adj C by ThTr; hence thesis by Th42; end; end; registration let C,f; let a be positive expression of C, an_Adj C; cluster a at f -> positive expression of C, an_Adj C; coherence proof consider v being constructor OperSymbol of C such that A0: the_result_sort_of v = an_Adj C and A1: ex p being FinSequence of QuasiTerms C st len p = len the_arity_of v & a = v-trm p by ThPos; consider p being FinSequence of QuasiTerms C such that A2: len p = len the_arity_of v & a = v-trm p by A1; len (p at f) = len p & a at f = v-trm(p at f) by A2,ThS1,ThTr2; hence thesis by A0,A2,ThPos2; end; end; Lemma: for C be initialized ConstructorSignature, f be valuation of C, a be positive expression of C, an_Adj C holds a at f is positive; registration let C,f; let a be negative expression of C, an_Adj C; cluster a at f -> negative expression of C, an_Adj C; coherence proof (non_op C)term (Non a) = a by Th44b; then a at f = (non_op C)term((Non a)at f) by SUBST .= Non ((Non a)at f) by Th44; hence thesis; end; end; definition let C,f; let a be quasi-adjective of C; redefine func a at f -> quasi-adjective of C; coherence proof per cases by REG; suppose a is positive; then reconsider a as positive quasi-adjective of C; a at f is positive; hence thesis; end; suppose a is negative; then reconsider a as negative quasi-adjective of C; a at f is negative; hence thesis; end; end; end; theorem (Non a) at f = Non (a at f) proof per cases; suppose a is positive; then reconsider b = a as positive expression of C, an_Adj C; reconsider af = b at f as positive expression of C, an_Adj C by Lemma; :: Niech madry czlowiek powie czemu jest potrzebna etykieta "Lemma"?! thus (Non a) at f = ((non_op C)term b) at f by Th44 .= (non_op C)term af by SUBST .= Non (a at f) by Th44; end; suppose a is non positive; then consider b being expression of C, an_Adj C such that A0: a = (non_op C)term b & Non a = b by Th45g; A1: a at f = (non_op C)term(b at f) by A0,SUBST; then a at f is non positive by POSITIVE; then ex k being expression of C, an_Adj C st a at f = (non_op C)term k & Non(a at f) = k by Th45g; :: b at f = k by A1,A2,ThNon'; hence (Non a)at f = Non (a at f) by A0,A1,ThNon'; end; end; definition let C,f; let t be expression of C, a_Type C; redefine func t at f -> expression of C, a_Type C; coherence proof t in (the Sorts of Free(C, MSVars C)).a_Type C by ELEMENT; then t at f in (the Sorts of Free(C, MSVars C)).a_Type C by ThTr; hence thesis by Th42; end; end; registration let C,f; let t be pure expression of C, a_Type C; cluster t at f -> pure expression of C, a_Type C; coherence proof consider m being constructor OperSymbol of C such that A0: the_result_sort_of m = a_Type C and A1: ex p being FinSequence of QuasiTerms C st len p = len the_arity_of m & t = m-trm p by ThPure; consider p being FinSequence of QuasiTerms C such that A2: len p = len the_arity_of m & t = m-trm p by A1; len (p at f) = len p & t at f = m-trm(p at f) by A2,ThS1,ThTr2; hence thesis by A0,A2,ThPure2; end; end; theorem for f being irrelevant one-to-one valuation of C ex g being irrelevant one-to-one 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 proof let f be irrelevant one-to-one valuation of C; set Y = {x where x is variable: x-term C in rng f}; defpred P[set,set] means ex x being set st x in dom f & f.x = root-tree [ $1, a_Term] & $2 = root-tree [x, a_Term]; B0: for x,y1,y2 being set st x in Y & P[x,y1] & P[x,y2] holds y1 = y2 by FUNCT_1:def 8; B1: for x being set st x in Y ex y being set st P[x,y] proof let x be set; assume x in Y; then B2: ex z being variable st x = z & z-term C in rng f; then reconsider z = x as variable; consider y being set such that B3: y in dom f & z-term C = f.y by B2,FUNCT_1:def 5; reconsider y as variable by B3; take y-term C; thus P[x,y-term C] by B3; end; consider g being Function such that A0: dom g = Y and A1: for y being set st y in Y holds P[y,g.y] from FUNCT_1:sch 2(B0,B1); A2: Y c= Vars proof let x be set; assume x in Y; then ex z being variable st x = z & z-term C in rng f; hence thesis; end; rng g c= QuasiTerms C proof let y be set; assume y in rng g; then consider x being set such that C2: x in dom g & y = g.x by FUNCT_1:def 5; reconsider x as variable by A0,A2,C2; consider z being set such that C3: z in dom f & f.z = x-term C & g.x = root-tree [z,a_Term] by A0,A1,C2; reconsider z as variable by C3; y = z-term C by C2,C3; hence thesis by ELEMENT; end; then reconsider g as valuation of C by A0,A2,RELSET_1:11; A3: g is irrelevant proof let x be variable; assume x in dom g; then consider y being set such that C1: y in dom f & f.y = x-term C & g.x = root-tree [y,a_Term] by A0,A1; reconsider y as variable by C1; take y; thus thesis by C1; end; g is one-to-one proof let z1,z2 be set; assume C4: z1 in dom g & z2 in dom g & g.z1 = g.z2; then reconsider z1,z2 as variable; consider x1 being set such that C5: x1 in dom f & f.x1 = z1-term C & g.z1 = root-tree[x1,a_Term] by A0,A1,C4; consider x2 being set such that C6: x2 in dom f & f.x2 = z2-term C & g.z1 = root-tree[x2,a_Term] by A0,A1,C4; reconsider x1,x2 as variable by C5,C6; x1-term C = x2-term C by C5,C6; then x1 = x2 by ThT0; hence thesis by C5,C6,ThT0; end; then reconsider g as irrelevant one-to-one valuation of C by A3; take g; let x,y be variable; hereby assume Z0: x in dom f & f.x = y-term C; then f.x in rng f by FUNCT_1:def 5; hence y in dom g by A0,Z0; then P[y,g.y] by A0,A1; hence g.y = x-term C by Z0,FUNCT_1:def 8; end; assume y in dom g & g.y = x-term C; then consider z being set such that Z2: z in dom f & f.z = root-tree [y, a_Term] & x-term C = root-tree [z, a_Term] by A0,A1; reconsider z as variable by Z2; x-term C = z-term C by Z2; hence thesis by Z2,ThT0; end; theorem for f,g being irrelevant one-to-one valuation of C st for x,y being variable holds x in dom f & f.x = y-term C implies y in dom g & g.y = x-term C for e st variables_in e c= dom f holds e at f at g = e proof let f,g be irrelevant one-to-one valuation of C such that A0: for x,y being variable holds x in dom f & f.x = y-term C implies y in dom g & g.y = x-term C; let t be expression of C; defpred P[expression of C] means variables_in $1 c= dom f implies $1 at f at g = $1; W1: for x being variable holds P[x-term C] proof let x be variable; assume variables_in (x-term C) c= dom f; then {x} c= dom f by MSAFREE3:11; then A2: x in dom f by ZFMISC_1:37; then consider y being variable such that A3: f.x = y-term C by IRR; y in dom g & g.y = x-term C & (x-term C) at f = y-term C by A0,A2,A3,SUBST; hence thesis by SUBST; end; W2: for c being constructor OperSymbol of C for p being FinSequence of QuasiTerms C st len p = len the_arity_of c & for t being quasi-term of C st t in rng p holds P[t] holds P[c-trm p] proof let c be constructor OperSymbol of C; let p be FinSequence of QuasiTerms C such that Z0: len p = len the_arity_of c and Z1: for t being quasi-term of C st t in rng p holds P[t] and 00: variables_in (c-trm p) c= dom f; c-trm p = [c, the carrier of C]-tree p by Z0,TERM; then 01: variables_in (c-trm p) = union {variables_in s where s is quasi-term of C: s in rng p} by Th84; Z5: len (p at f) = len p & len (p at f at g) = len (p at f) by ThTr2; then Z2: dom (p at f) = dom p & dom (p at f at g) = dom (p at f) by FINSEQ_3:31; now let i be Nat; assume i in dom p; then Z3: (p at f).i = f# .(p.i) & (p at f at g).i = g# .((p at f).i) & p.i in rng p by Z2,FUNCT_1:23,def 5; rng p c= QuasiTerms C by FINSEQ_1:def 4; then reconsider pi = p.i as quasi-term of C by Z3,Th42; variables_in pi in {variables_in s where s is quasi-term of C: s in rng p} by Z3; then Z4: variables_in pi c= variables_in (c-trm p) by 01,ZFMISC_1:92; (p at f at g).i = pi at f at g by Z3; hence (p at f at g).i = p.i by Z1,Z3,Z4,00,XBOOLE_1:1; end; then p at f at g = p & (c-trm p) at f = c-trm (p at f) by Z0,Z2,SUBST,FINSEQ_1:17; hence (c-trm p) at f at g = c-trm p by Z0,Z5,SUBST; end; W3: for a being expression of C, an_Adj C st P[a] holds P[(non_op C)term a] proof let a be expression of C, an_Adj C such that A4: P[a] and A5: variables_in ((non_op C)term a) c= dom f; A6: (non_op C)term a = [non_op, the carrier of C]-tree <*a*> by ThNon; thus ((non_op C)term a) at f at g = ((non_op C)term (a at f)) at g by SUBST .= (non_op C)term a by A4,A5,A6,Aux1,SUBST; end; W4: for a being expression of C, an_Adj C st P[a] for t being expression of C, a_Type C st P[t] holds P[(ast C)term(a,t)] proof let a be expression of C, an_Adj C such that A7: P[a]; let t be expression of C, a_Type C such that A8: P[t] and A9: variables_in ((ast C)term(a,t)) c= dom f; (ast C)term(a,t) = [ *, the carrier of C]-tree <*a,t*> by ThAst; then AA: variables_in ((ast C)term(a,t)) = ((C variables_in a)\/(C variables_in t)).a_Term by Aux2 .= (variables_in a)\/variables_in t by PBOOLE:def 7; thus ((ast C)term(a,t)) at f at g = ((ast C)term (a at f, t at f)) at g by SUBST .= (ast C)term(a,t) by A7,A8,AA,SUBST,A9,XBOOLE_1:11; end; thus P[t] from StructInd(W1,W2,W3,W4); end; definition let C,f; let A be Subset of QuasiAdjs C; func A at f -> Subset of QuasiAdjs C equals {a at f where a is quasi-adjective of C: a in A}; coherence proof set X = {a at f where a is quasi-adjective of C: a in A}; X c= QuasiAdjs C proof let x be set; assume x in X; then ex a being quasi-adjective of C st x = a at f & a in A; hence thesis; end; hence thesis; end; end; theorem ThZ0: for A being Subset of QuasiAdjs C for a being quasi-adjective of C st A = {a} holds A at f = {a at f} proof let A be Subset of QuasiAdjs C; let a be quasi-adjective of C such that A0: A = {a}; thus A at f c= {a at f} proof let x be set; assume x in A at f; then ex b being quasi-adjective of C st x = b at f & b in A; then x = a at f by A0,TARSKI:def 1; hence thesis by TARSKI:def 1; end; let x be set; assume x in {a at f}; then x = a at f & a in A by A0,TARSKI:def 1; hence thesis; end; theorem ThZ1: for A,B being Subset of QuasiAdjs C holds (A \/ B) at f = (A at f) \/ (B at f) proof let A,B be Subset of QuasiAdjs C; thus (A \/ B) at f c= (A at f) \/ (B at f) proof let x be set; assume x in (A \/ B) at f; then consider a being quasi-adjective of C such that A1: x = a at f & a in A \/ B; a in A or a in B by A1,XBOOLE_0:def 2; then x in A at f or x in B at f by A1; hence thesis by XBOOLE_0:def 2; end; let x be set; assume x in (A at f) \/ (B at f); then x in (A at f) or x in (B at f) by XBOOLE_0:def 2; then A c= A\/B & (ex a being quasi-adjective of C st x = a at f & a in A) or B c= A\/B & ex a being quasi-adjective of C st x = a at f & a in B by XBOOLE_1:7; hence thesis; end; theorem for A,B being Subset of QuasiAdjs C st A c= B holds A at f c= B at f proof let A,B be Subset of QuasiAdjs C; assume A c= B; then A\/B = B by XBOOLE_1:12; then B at f = (A at f)\/(B at f) by ThZ1; hence A at f c= B at f by XBOOLE_1:7; end; registration let C be initialized ConstructorSignature; let f be valuation of C; let A be finite Subset of QuasiAdjs C; cluster A at f -> finite; coherence proof A0: A is finite; deffunc F(expression of C) = $1 at f; A1: { F(w) where w is expression of C: w in A } is finite from FRAENKEL:sch 21(A0); A at f c= { F(w) where w is expression of C: w in A } proof let x be set; assume x in A at f; then ex a being quasi-adjective of C st x = a at f & a in A; hence thesis; end; hence thesis by A1,FINSET_1:13; end; end; definition let C be initialized ConstructorSignature; let f be valuation of C; let T be quasi-type of C; func T at f -> quasi-type of C equals ((adjs T) at f)ast((the_base_of T) at f); coherence; end; theorem ::? 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 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) proof let T be quasi-type of C; let a be quasi-adjective of C; a in QuasiAdjs C; then reconsider A = {a} as Subset of QuasiAdjs C by ZFMISC_1:37; thus (a ast T) at f = [(adjs (a ast T)) at f ,((the_base_of T) at f)] by MCART_1:7 .= [(A\/(adjs T)) at f ,((the_base_of T) at f)] by MCART_1:7 .= [(A at f)\/((adjs T) at f),(the_base_of T) at f] by ThZ1 .= [{a at f}\/((adjs T) at f),(the_base_of T) at f] by ThZ0 .= [{a at f}\/(adjs (T at f)),(the_base_of T) at f] by MCART_1:7 .= (a at f) ast (T at f) by MCART_1:7; end; definition let C be initialized ConstructorSignature; let f,g be valuation of C; func f at g -> valuation of C means: SUBST2: 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 proof deffunc h(set) = ((In($1,Vars)-term C) at f) at g; consider h being Function such that A0: dom h = (dom f) \/ dom g and A1: for x being set st x in (dom f) \/ dom g holds h.x = h(x) from FUNCT_1:sch 3; rng h c= QuasiTerms C proof let y be set; assume y in rng h; then consider x being set such that A2: x in dom h & y = h.x by FUNCT_1:def 5; y = h(x) by A0,A1,A2; hence thesis by ELEMENT; end; then reconsider h as valuation of C by A0,RELSET_1:11; take h; thus dom h = (dom f) \/ dom g by A0; let x be variable; assume x in dom h; then h.x = h(x) by A0,A1; hence thesis by FUNCT_7:def 1; end; uniqueness proof let h1,h2 be valuation of C such that A1: dom h1 = (dom f) \/ dom g and B1: for x being variable st x in dom h1 holds h1.x = ((x-term C) at f) at g and A2: dom h2 = (dom f) \/ dom g and B2: for x being variable st x in dom h2 holds h2.x = ((x-term C) at f) at g; now let x be variable; assume x in dom h1; then h1.x = ((x-term C) at f) at g & h2.x = ((x-term C) at f) at g by A1,A2,B1,B2; hence h1.x = h2.x; end; hence thesis by A1,A2,PARTFUN1:34; end; end; registration let C be initialized ConstructorSignature; let f,g be irrelevant valuation of C; cluster f at g -> irrelevant; coherence proof let x be variable; assume A0: x in dom (f at g); then A1: (f at g).x = ((x-term C) at f) at g by SUBST2; A2: dom (f at g) = dom f \/ dom g by SUBST2; per cases; suppose A3: x in dom f; then consider y being variable such that A4: f.x = y-term C by IRR; (x-term C) at f = y-term C by A3,A4,SUBST; then (y in dom g implies (f at g).x = g.y) & (y nin dom g implies (f at g).x = y-term C) by A1,SUBST; hence thesis by IRR; end; suppose x nin dom f; then A7: (x-term C) at f = x-term C & x in dom g by A0,A2,SUBST,XBOOLE_0:def 2; then (f at g).x = g.x by A1,SUBST; hence thesis by A7,IRR; end; end; end; theorem ThS3: for f1,f2 being valuation of C holds (e at f1) at f2 = e at (f1 at f2) proof set t = e; let f1,f2 be valuation of C; A0: dom (f1 at f2) = (dom f1) \/ dom f2 by SUBST2; defpred P[expression of C] means ($1 at f1) at f2 = $1 at (f1 at f2); W1: for x being variable holds P[x-term C] proof let x be variable; per cases; suppose Z0: x in dom (f1 at f2); then (x-term C) at (f1 at f2) = (f1 at f2).x by SUBST; hence thesis by Z0,SUBST2; end; suppose Z0: x nin dom (f1 at f2); then x nin dom f1 & x nin dom f2 by A0,XBOOLE_0:def 2; then (x-term C) at f1 = x-term C & (x-term C) at f2 = x-term C by SUBST; hence thesis by Z0,SUBST; end; end; W2: for c being constructor OperSymbol of C for p being FinSequence of QuasiTerms C st len p = len the_arity_of c & for t being quasi-term of C st t in rng p holds P[t] holds P[c-trm p] proof let c be constructor OperSymbol of C; let p be FinSequence of QuasiTerms C such that Z0: len p = len the_arity_of c and Z1: for t being quasi-term of C st t in rng p holds P[t]; Z5: len (p at f1) = len p & len (p at (f1 at f2)) = len p & len ((p at f1) at f2) = len (p at f1) by ThTr2; then Z2: dom (p at f1) = dom p & dom (p at (f1 at f2)) = dom p & dom ((p at f1) at f2) = dom p by FINSEQ_3:31; now let i be Nat; assume i in dom p; then Z3: ((p at f1) at f2).i = f2# .((p at f1).i) & (p at f1).i = f1# .(p.i) & (p at (f1 at f2)).i = (f1 at f2)#.(p.i) & p.i in rng p by Z2,FUNCT_1:23,def 5; rng p c= QuasiTerms C by FINSEQ_1:def 4; then reconsider pi = p.i as quasi-term of C by Z3,Th42; thus (p at f1 at f2).i = (pi at f1) at f2 by Z3 .= pi at (f1 at f2) by Z1,Z3 .= (p at (f1 at f2)).i by Z3; end; then Z4: p at f1 at f2 = p at (f1 at f2) by Z2,FINSEQ_1:17; thus (c-trm p) at f1 at f2 = (c-trm(p at f1)) at f2 by Z0,SUBST .= c-trm (p at (f1 at f2)) by Z0,Z5,Z4,SUBST .= (c-trm p) at (f1 at f2) by Z0,SUBST; end; W3: for a being expression of C, an_Adj C st P[a] holds P[(non_op C)term a] proof let a be expression of C, an_Adj C; assume P[a]; then ((non_op C)term (a at f1)) at f2 = (non_op C)term (a at (f1 at f2)) by SUBST .= ((non_op C)term a) at (f1 at f2) by SUBST; hence P[(non_op C)term a] by SUBST; end; W4: for a being expression of C, an_Adj C st P[a] for t being expression of C, a_Type C st P[t] holds P[(ast C)term(a,t)] proof let a be expression of C, an_Adj C such that Z1: P[a]; let t be expression of C, a_Type C; assume P[t]; then ((ast C)term (a at f1,t at f1)) at f2 = (ast C)term (a at (f1 at f2),t at (f1 at f2)) by Z1,SUBST .= ((ast C)term(a,t)) at (f1 at f2) by SUBST; hence P[(ast C)term(a,t)] by SUBST; end; thus P[t] from StructInd(W1,W2,W3,W4); end; theorem ThZ3: 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) proof let A be Subset of QuasiAdjs C; let f1,f2 be valuation of C; thus (A at f1) at f2 c= A at (f1 at f2) proof let x be set; assume x in (A at f1) at f2; then consider a being quasi-adjective of C such that A0: x = a at f2 & a in A at f1; consider b being quasi-adjective of C such that A1: a = b at f1 & b in A by A0; x = b at (f1 at f2) by A0,A1,ThS3; hence thesis by A1; end; let x be set; assume x in A at (f1 at f2); then consider a being quasi-adjective of C such that A2: x = a at (f1 at f2) & a in A; x = a at f1 at f2 & a at f1 in A at f1 by A2,ThS3; hence thesis; end; theorem 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) proof let T be quasi-type of C; let f1,f2 be valuation of C; thus (T at f1) at f2 = (((adjs T) at f1) at f2)ast((the_base_of (T at f1))at f2) by MCART_1:7 .= ((adjs T) at (f1 at f2))ast((the_base_of (T at f1))at f2) by ThZ3 .= ((adjs T) at (f1 at f2))ast(((the_base_of T) at f1)at f2) by MCART_1:7 .= T at (f1 at f2) by ThS3; end;