:: 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, XXREAL_2, 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, MEMBERED, XXREAL_2; 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, XXREAL_2; 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, 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, CARD_2, XXREAL_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,XXREAL_2:def 8; 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; 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,XXREAL_2:def 8; 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: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 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 succ (i+1) c= omega; 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 succ (k+1) c= omega; 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; hence thesis by Lem4,Th13,Th17; end; registration cluster Vars -> non empty; correctness proof [{},0] 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; 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 = {}; 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 the carrier of C = {a_Type, an_Adj, a_Term}; assume {*, non_op} c= the OperSymbols of C; then the OperSymbols of C <> {}; hence thesis by 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,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; 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 = {}; 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 = {}; 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; 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 by REG; 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; 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; 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; 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; 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; 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; 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; 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; 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 <> *