:: PRELAMB semantic presentation begin definition attrc1 is strict ; struct typealg -> 1-sorted ; aggrtypealg(# carrier, left_quotient, right_quotient, inner_product #) -> typealg ; sel left_quotient c1 -> BinOp of the carrier of c1; sel right_quotient c1 -> BinOp of the carrier of c1; sel inner_product c1 -> BinOp of the carrier of c1; end; registration cluster non empty strict for typealg ; existence ex b1 being typealg st ( not b1 is empty & b1 is strict ) proof set l = the BinOp of {{}}; take typealg(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) ; ::_thesis: ( not typealg(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) is empty & typealg(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) is strict ) thus not the carrier of typealg(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: typealg(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) is strict thus typealg(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}} #) is strict ; ::_thesis: verum end; end; definition let s be non empty typealg ; mode type of s is Element of s; end; definition let s be non empty typealg ; let x, y be type of s; funcx \ y -> type of s equals :: PRELAMB:def 1 the left_quotient of s . (x,y); coherence the left_quotient of s . (x,y) is type of s ; funcx /" y -> type of s equals :: PRELAMB:def 2 the right_quotient of s . (x,y); coherence the right_quotient of s . (x,y) is type of s ; funcx * y -> type of s equals :: PRELAMB:def 3 the inner_product of s . (x,y); coherence the inner_product of s . (x,y) is type of s ; end; :: deftheorem defines \ PRELAMB:def_1_:_ for s being non empty typealg for x, y being type of s holds x \ y = the left_quotient of s . (x,y); :: deftheorem defines /" PRELAMB:def_2_:_ for s being non empty typealg for x, y being type of s holds x /" y = the right_quotient of s . (x,y); :: deftheorem defines * PRELAMB:def_3_:_ for s being non empty typealg for x, y being type of s holds x * y = the inner_product of s . (x,y); definition let s be non empty typealg ; mode PreProof of s is finite DecoratedTree of [:[:( the carrier of s *), the carrier of s:],NAT:]; end; definition let s be non empty typealg ; let Tr be PreProof of s; let v be Element of dom Tr; attrv is correct means :Def4: :: PRELAMB:def 4 ( branchdeg v = 0 & ex x being type of s st (Tr . v) `1 = [<*x*>,x] ) if (Tr . v) `2 = 0 ( branchdeg v = 1 & ex T being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [T,(x /" y)] & (Tr . (v ^ <*0*>)) `1 = [(T ^ <*y*>),x] ) ) if (Tr . v) `2 = 1 ( branchdeg v = 1 & ex T being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [T,(y \ x)] & (Tr . (v ^ <*0*>)) `1 = [(<*y*> ^ T),x] ) ) if (Tr . v) `2 = 2 ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( (Tr . v) `1 = [(((X ^ <*(x /" y)*>) ^ T) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*x*>) ^ Y),z] ) ) if (Tr . v) `2 = 3 ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( (Tr . v) `1 = [(((X ^ T) ^ <*(y \ x)*>) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*x*>) ^ Y),z] ) ) if (Tr . v) `2 = 4 for z being type of s holds ( branchdeg v = 1 & ex X being FinSequence of s ex x, y being type of s ex Y being FinSequence of s st ( (Tr . v) `1 = [((X ^ <*(x * y)*>) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [(((X ^ <*x*>) ^ <*y*>) ^ Y),z] ) ) if (Tr . v) `2 = 5 ( branchdeg v = 2 & ex X, Y being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [(X ^ Y),(x * y)] & (Tr . (v ^ <*0*>)) `1 = [X,x] & (Tr . (v ^ <*1*>)) `1 = [Y,y] ) ) if (Tr . v) `2 = 6 ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex y, z being type of s st ( (Tr . v) `1 = [((X ^ T) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*y*>) ^ Y),z] ) ) if (Tr . v) `2 = 7 otherwise contradiction; correctness consistency ( ( (Tr . v) `2 = 0 & (Tr . v) `2 = 1 implies ( branchdeg v = 0 & ex x being type of s st (Tr . v) `1 = [<*x*>,x] iff ( branchdeg v = 1 & ex T being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [T,(x /" y)] & (Tr . (v ^ <*0*>)) `1 = [(T ^ <*y*>),x] ) ) ) ) & ( (Tr . v) `2 = 0 & (Tr . v) `2 = 2 implies ( branchdeg v = 0 & ex x being type of s st (Tr . v) `1 = [<*x*>,x] iff ( branchdeg v = 1 & ex T being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [T,(y \ x)] & (Tr . (v ^ <*0*>)) `1 = [(<*y*> ^ T),x] ) ) ) ) & ( (Tr . v) `2 = 0 & (Tr . v) `2 = 3 implies ( branchdeg v = 0 & ex x being type of s st (Tr . v) `1 = [<*x*>,x] iff ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( (Tr . v) `1 = [(((X ^ <*(x /" y)*>) ^ T) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*x*>) ^ Y),z] ) ) ) ) & ( (Tr . v) `2 = 0 & (Tr . v) `2 = 4 implies ( branchdeg v = 0 & ex x being type of s st (Tr . v) `1 = [<*x*>,x] iff ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( (Tr . v) `1 = [(((X ^ T) ^ <*(y \ x)*>) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*x*>) ^ Y),z] ) ) ) ) & ( (Tr . v) `2 = 0 & (Tr . v) `2 = 5 implies ( ( branchdeg v = 0 & ex x being type of s st (Tr . v) `1 = [<*x*>,x] ) iff for z being type of s holds ( branchdeg v = 1 & ex X being FinSequence of s ex x, y being type of s ex Y being FinSequence of s st ( (Tr . v) `1 = [((X ^ <*(x * y)*>) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [(((X ^ <*x*>) ^ <*y*>) ^ Y),z] ) ) ) ) & ( (Tr . v) `2 = 0 & (Tr . v) `2 = 6 implies ( branchdeg v = 0 & ex x being type of s st (Tr . v) `1 = [<*x*>,x] iff ( branchdeg v = 2 & ex X, Y being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [(X ^ Y),(x * y)] & (Tr . (v ^ <*0*>)) `1 = [X,x] & (Tr . (v ^ <*1*>)) `1 = [Y,y] ) ) ) ) & ( (Tr . v) `2 = 0 & (Tr . v) `2 = 7 implies ( branchdeg v = 0 & ex x being type of s st (Tr . v) `1 = [<*x*>,x] iff ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex y, z being type of s st ( (Tr . v) `1 = [((X ^ T) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*y*>) ^ Y),z] ) ) ) ) & ( (Tr . v) `2 = 1 & (Tr . v) `2 = 2 implies ( branchdeg v = 1 & ex T being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [T,(x /" y)] & (Tr . (v ^ <*0*>)) `1 = [(T ^ <*y*>),x] ) iff ( branchdeg v = 1 & ex T being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [T,(y \ x)] & (Tr . (v ^ <*0*>)) `1 = [(<*y*> ^ T),x] ) ) ) ) & ( (Tr . v) `2 = 1 & (Tr . v) `2 = 3 implies ( branchdeg v = 1 & ex T being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [T,(x /" y)] & (Tr . (v ^ <*0*>)) `1 = [(T ^ <*y*>),x] ) iff ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( (Tr . v) `1 = [(((X ^ <*(x /" y)*>) ^ T) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*x*>) ^ Y),z] ) ) ) ) & ( (Tr . v) `2 = 1 & (Tr . v) `2 = 4 implies ( branchdeg v = 1 & ex T being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [T,(x /" y)] & (Tr . (v ^ <*0*>)) `1 = [(T ^ <*y*>),x] ) iff ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( (Tr . v) `1 = [(((X ^ T) ^ <*(y \ x)*>) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*x*>) ^ Y),z] ) ) ) ) & ( (Tr . v) `2 = 1 & (Tr . v) `2 = 5 implies ( ( branchdeg v = 1 & ex T being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [T,(x /" y)] & (Tr . (v ^ <*0*>)) `1 = [(T ^ <*y*>),x] ) ) iff for z being type of s holds ( branchdeg v = 1 & ex X being FinSequence of s ex x, y being type of s ex Y being FinSequence of s st ( (Tr . v) `1 = [((X ^ <*(x * y)*>) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [(((X ^ <*x*>) ^ <*y*>) ^ Y),z] ) ) ) ) & ( (Tr . v) `2 = 1 & (Tr . v) `2 = 6 implies ( branchdeg v = 1 & ex T being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [T,(x /" y)] & (Tr . (v ^ <*0*>)) `1 = [(T ^ <*y*>),x] ) iff ( branchdeg v = 2 & ex X, Y being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [(X ^ Y),(x * y)] & (Tr . (v ^ <*0*>)) `1 = [X,x] & (Tr . (v ^ <*1*>)) `1 = [Y,y] ) ) ) ) & ( (Tr . v) `2 = 1 & (Tr . v) `2 = 7 implies ( branchdeg v = 1 & ex T being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [T,(x /" y)] & (Tr . (v ^ <*0*>)) `1 = [(T ^ <*y*>),x] ) iff ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex y, z being type of s st ( (Tr . v) `1 = [((X ^ T) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*y*>) ^ Y),z] ) ) ) ) & ( (Tr . v) `2 = 2 & (Tr . v) `2 = 3 implies ( branchdeg v = 1 & ex T being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [T,(y \ x)] & (Tr . (v ^ <*0*>)) `1 = [(<*y*> ^ T),x] ) iff ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( (Tr . v) `1 = [(((X ^ <*(x /" y)*>) ^ T) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*x*>) ^ Y),z] ) ) ) ) & ( (Tr . v) `2 = 2 & (Tr . v) `2 = 4 implies ( branchdeg v = 1 & ex T being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [T,(y \ x)] & (Tr . (v ^ <*0*>)) `1 = [(<*y*> ^ T),x] ) iff ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( (Tr . v) `1 = [(((X ^ T) ^ <*(y \ x)*>) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*x*>) ^ Y),z] ) ) ) ) & ( (Tr . v) `2 = 2 & (Tr . v) `2 = 5 implies ( ( branchdeg v = 1 & ex T being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [T,(y \ x)] & (Tr . (v ^ <*0*>)) `1 = [(<*y*> ^ T),x] ) ) iff for z being type of s holds ( branchdeg v = 1 & ex X being FinSequence of s ex x, y being type of s ex Y being FinSequence of s st ( (Tr . v) `1 = [((X ^ <*(x * y)*>) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [(((X ^ <*x*>) ^ <*y*>) ^ Y),z] ) ) ) ) & ( (Tr . v) `2 = 2 & (Tr . v) `2 = 6 implies ( branchdeg v = 1 & ex T being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [T,(y \ x)] & (Tr . (v ^ <*0*>)) `1 = [(<*y*> ^ T),x] ) iff ( branchdeg v = 2 & ex X, Y being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [(X ^ Y),(x * y)] & (Tr . (v ^ <*0*>)) `1 = [X,x] & (Tr . (v ^ <*1*>)) `1 = [Y,y] ) ) ) ) & ( (Tr . v) `2 = 2 & (Tr . v) `2 = 7 implies ( branchdeg v = 1 & ex T being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [T,(y \ x)] & (Tr . (v ^ <*0*>)) `1 = [(<*y*> ^ T),x] ) iff ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex y, z being type of s st ( (Tr . v) `1 = [((X ^ T) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*y*>) ^ Y),z] ) ) ) ) & ( (Tr . v) `2 = 3 & (Tr . v) `2 = 4 implies ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( (Tr . v) `1 = [(((X ^ <*(x /" y)*>) ^ T) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*x*>) ^ Y),z] ) iff ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( (Tr . v) `1 = [(((X ^ T) ^ <*(y \ x)*>) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*x*>) ^ Y),z] ) ) ) ) & ( (Tr . v) `2 = 3 & (Tr . v) `2 = 5 implies ( ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( (Tr . v) `1 = [(((X ^ <*(x /" y)*>) ^ T) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*x*>) ^ Y),z] ) ) iff for z being type of s holds ( branchdeg v = 1 & ex X being FinSequence of s ex x, y being type of s ex Y being FinSequence of s st ( (Tr . v) `1 = [((X ^ <*(x * y)*>) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [(((X ^ <*x*>) ^ <*y*>) ^ Y),z] ) ) ) ) & ( (Tr . v) `2 = 3 & (Tr . v) `2 = 6 implies ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( (Tr . v) `1 = [(((X ^ <*(x /" y)*>) ^ T) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*x*>) ^ Y),z] ) iff ( branchdeg v = 2 & ex X, Y being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [(X ^ Y),(x * y)] & (Tr . (v ^ <*0*>)) `1 = [X,x] & (Tr . (v ^ <*1*>)) `1 = [Y,y] ) ) ) ) & ( (Tr . v) `2 = 3 & (Tr . v) `2 = 7 implies ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( (Tr . v) `1 = [(((X ^ <*(x /" y)*>) ^ T) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*x*>) ^ Y),z] ) iff ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex y, z being type of s st ( (Tr . v) `1 = [((X ^ T) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*y*>) ^ Y),z] ) ) ) ) & ( (Tr . v) `2 = 4 & (Tr . v) `2 = 5 implies ( ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( (Tr . v) `1 = [(((X ^ T) ^ <*(y \ x)*>) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*x*>) ^ Y),z] ) ) iff for z being type of s holds ( branchdeg v = 1 & ex X being FinSequence of s ex x, y being type of s ex Y being FinSequence of s st ( (Tr . v) `1 = [((X ^ <*(x * y)*>) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [(((X ^ <*x*>) ^ <*y*>) ^ Y),z] ) ) ) ) & ( (Tr . v) `2 = 4 & (Tr . v) `2 = 6 implies ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( (Tr . v) `1 = [(((X ^ T) ^ <*(y \ x)*>) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*x*>) ^ Y),z] ) iff ( branchdeg v = 2 & ex X, Y being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [(X ^ Y),(x * y)] & (Tr . (v ^ <*0*>)) `1 = [X,x] & (Tr . (v ^ <*1*>)) `1 = [Y,y] ) ) ) ) & ( (Tr . v) `2 = 4 & (Tr . v) `2 = 7 implies ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( (Tr . v) `1 = [(((X ^ T) ^ <*(y \ x)*>) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*x*>) ^ Y),z] ) iff ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex y, z being type of s st ( (Tr . v) `1 = [((X ^ T) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*y*>) ^ Y),z] ) ) ) ) & ( (Tr . v) `2 = 5 & (Tr . v) `2 = 6 implies ( ( for z being type of s holds ( branchdeg v = 1 & ex X being FinSequence of s ex x, y being type of s ex Y being FinSequence of s st ( (Tr . v) `1 = [((X ^ <*(x * y)*>) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [(((X ^ <*x*>) ^ <*y*>) ^ Y),z] ) ) ) iff ( branchdeg v = 2 & ex X, Y being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [(X ^ Y),(x * y)] & (Tr . (v ^ <*0*>)) `1 = [X,x] & (Tr . (v ^ <*1*>)) `1 = [Y,y] ) ) ) ) & ( (Tr . v) `2 = 5 & (Tr . v) `2 = 7 implies ( ( for z being type of s holds ( branchdeg v = 1 & ex X being FinSequence of s ex x, y being type of s ex Y being FinSequence of s st ( (Tr . v) `1 = [((X ^ <*(x * y)*>) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [(((X ^ <*x*>) ^ <*y*>) ^ Y),z] ) ) ) iff ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex y, z being type of s st ( (Tr . v) `1 = [((X ^ T) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*y*>) ^ Y),z] ) ) ) ) & ( (Tr . v) `2 = 6 & (Tr . v) `2 = 7 implies ( branchdeg v = 2 & ex X, Y being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [(X ^ Y),(x * y)] & (Tr . (v ^ <*0*>)) `1 = [X,x] & (Tr . (v ^ <*1*>)) `1 = [Y,y] ) iff ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex y, z being type of s st ( (Tr . v) `1 = [((X ^ T) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*y*>) ^ Y),z] ) ) ) ) ); ; end; :: deftheorem Def4 defines correct PRELAMB:def_4_:_ for s being non empty typealg for Tr being PreProof of s for v being Element of dom Tr holds ( ( (Tr . v) `2 = 0 implies ( v is correct iff ( branchdeg v = 0 & ex x being type of s st (Tr . v) `1 = [<*x*>,x] ) ) ) & ( (Tr . v) `2 = 1 implies ( v is correct iff ( branchdeg v = 1 & ex T being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [T,(x /" y)] & (Tr . (v ^ <*0*>)) `1 = [(T ^ <*y*>),x] ) ) ) ) & ( (Tr . v) `2 = 2 implies ( v is correct iff ( branchdeg v = 1 & ex T being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [T,(y \ x)] & (Tr . (v ^ <*0*>)) `1 = [(<*y*> ^ T),x] ) ) ) ) & ( (Tr . v) `2 = 3 implies ( v is correct iff ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( (Tr . v) `1 = [(((X ^ <*(x /" y)*>) ^ T) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*x*>) ^ Y),z] ) ) ) ) & ( (Tr . v) `2 = 4 implies ( v is correct iff ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( (Tr . v) `1 = [(((X ^ T) ^ <*(y \ x)*>) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*x*>) ^ Y),z] ) ) ) ) & ( (Tr . v) `2 = 5 implies ( v is correct iff for z being type of s holds ( branchdeg v = 1 & ex X being FinSequence of s ex x, y being type of s ex Y being FinSequence of s st ( (Tr . v) `1 = [((X ^ <*(x * y)*>) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [(((X ^ <*x*>) ^ <*y*>) ^ Y),z] ) ) ) ) & ( (Tr . v) `2 = 6 implies ( v is correct iff ( branchdeg v = 2 & ex X, Y being FinSequence of s ex x, y being type of s st ( (Tr . v) `1 = [(X ^ Y),(x * y)] & (Tr . (v ^ <*0*>)) `1 = [X,x] & (Tr . (v ^ <*1*>)) `1 = [Y,y] ) ) ) ) & ( (Tr . v) `2 = 7 implies ( v is correct iff ( branchdeg v = 2 & ex T, X, Y being FinSequence of s ex y, z being type of s st ( (Tr . v) `1 = [((X ^ T) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*y*>) ^ Y),z] ) ) ) ) & ( not (Tr . v) `2 = 0 & not (Tr . v) `2 = 1 & not (Tr . v) `2 = 2 & not (Tr . v) `2 = 3 & not (Tr . v) `2 = 4 & not (Tr . v) `2 = 5 & not (Tr . v) `2 = 6 & not (Tr . v) `2 = 7 implies ( v is correct iff contradiction ) ) ); definition let s be non empty typealg ; let IT be type of s; attrIT is left means :: PRELAMB:def 5 ex x, y being type of s st IT = x \ y; attrIT is right means :: PRELAMB:def 6 ex x, y being type of s st IT = x /" y; attrIT is middle means :: PRELAMB:def 7 ex x, y being type of s st IT = x * y; end; :: deftheorem defines left PRELAMB:def_5_:_ for s being non empty typealg for IT being type of s holds ( IT is left iff ex x, y being type of s st IT = x \ y ); :: deftheorem defines right PRELAMB:def_6_:_ for s being non empty typealg for IT being type of s holds ( IT is right iff ex x, y being type of s st IT = x /" y ); :: deftheorem defines middle PRELAMB:def_7_:_ for s being non empty typealg for IT being type of s holds ( IT is middle iff ex x, y being type of s st IT = x * y ); definition let s be non empty typealg ; let IT be type of s; attrIT is primitive means :: PRELAMB:def 8 ( not IT is left & not IT is right & not IT is middle ); end; :: deftheorem defines primitive PRELAMB:def_8_:_ for s being non empty typealg for IT being type of s holds ( IT is primitive iff ( not IT is left & not IT is right & not IT is middle ) ); definition let s be non empty typealg ; let Tr be finite DecoratedTree of the carrier of s; let v be Element of dom Tr; :: original: . redefine funcTr . v -> type of s; coherence Tr . v is type of s proof reconsider Tr = Tr as DecoratedTree of the carrier of s ; reconsider v = v as Element of dom Tr ; Tr . v is type of s ; hence Tr . v is type of s ; ::_thesis: verum end; end; definition let s be non empty typealg ; let Tr be finite DecoratedTree of the carrier of s; let x be type of s; predTr represents x means :: PRELAMB:def 9 ( dom Tr is finite & ( for v being Element of dom Tr holds ( ( branchdeg v = 0 or branchdeg v = 2 ) & ( branchdeg v = 0 implies Tr . v is primitive ) & ( branchdeg v = 2 implies ex y, z being type of s st ( ( Tr . v = y /" z or Tr . v = y \ z or Tr . v = y * z ) & Tr . (v ^ <*0*>) = y & Tr . (v ^ <*1*>) = z ) ) ) ) ); end; :: deftheorem defines represents PRELAMB:def_9_:_ for s being non empty typealg for Tr being finite DecoratedTree of the carrier of s for x being type of s holds ( Tr represents x iff ( dom Tr is finite & ( for v being Element of dom Tr holds ( ( branchdeg v = 0 or branchdeg v = 2 ) & ( branchdeg v = 0 implies Tr . v is primitive ) & ( branchdeg v = 2 implies ex y, z being type of s st ( ( Tr . v = y /" z or Tr . v = y \ z or Tr . v = y * z ) & Tr . (v ^ <*0*>) = y & Tr . (v ^ <*1*>) = z ) ) ) ) ) ); notation let s be non empty typealg ; let Tr be finite DecoratedTree of the carrier of s; let x be type of s; antonym Tr does_not_represent x for Tr represents x; end; definition let IT be non empty typealg ; attrIT is free means :Def10: :: PRELAMB:def 10 ( ( for x being type of IT holds ( not ( x is left & x is right ) & not ( x is left & x is middle ) & not ( x is right & x is middle ) ) ) & ( for x being type of IT ex Tr being finite DecoratedTree of the carrier of IT st for Tr1 being finite DecoratedTree of the carrier of IT holds ( Tr1 represents x iff Tr = Tr1 ) ) ); end; :: deftheorem Def10 defines free PRELAMB:def_10_:_ for IT being non empty typealg holds ( IT is free iff ( ( for x being type of IT holds ( not ( x is left & x is right ) & not ( x is left & x is middle ) & not ( x is right & x is middle ) ) ) & ( for x being type of IT ex Tr being finite DecoratedTree of the carrier of IT st for Tr1 being finite DecoratedTree of the carrier of IT holds ( Tr1 represents x iff Tr = Tr1 ) ) ) ); definition let s be non empty typealg ; let x be type of s; assume A1: s is free ; func repr_of x -> finite DecoratedTree of the carrier of s means :: PRELAMB:def 11 for Tr being finite DecoratedTree of the carrier of s holds ( Tr represents x iff it = Tr ); existence ex b1 being finite DecoratedTree of the carrier of s st for Tr being finite DecoratedTree of the carrier of s holds ( Tr represents x iff b1 = Tr ) by A1, Def10; uniqueness for b1, b2 being finite DecoratedTree of the carrier of s st ( for Tr being finite DecoratedTree of the carrier of s holds ( Tr represents x iff b1 = Tr ) ) & ( for Tr being finite DecoratedTree of the carrier of s holds ( Tr represents x iff b2 = Tr ) ) holds b1 = b2 proof let tr1, tr2 be finite DecoratedTree of the carrier of s; ::_thesis: ( ( for Tr being finite DecoratedTree of the carrier of s holds ( Tr represents x iff tr1 = Tr ) ) & ( for Tr being finite DecoratedTree of the carrier of s holds ( Tr represents x iff tr2 = Tr ) ) implies tr1 = tr2 ) assume that A1: for Tr being finite DecoratedTree of the carrier of s holds ( Tr represents x iff tr1 = Tr ) and A2: for Tr being finite DecoratedTree of the carrier of s holds ( Tr represents x iff tr2 = Tr ) ; ::_thesis: tr1 = tr2 tr1 represents x by A1; hence tr1 = tr2 by A2; ::_thesis: verum end; end; :: deftheorem defines repr_of PRELAMB:def_11_:_ for s being non empty typealg for x being type of s st s is free holds for b3 being finite DecoratedTree of the carrier of s holds ( b3 = repr_of x iff for Tr being finite DecoratedTree of the carrier of s holds ( Tr represents x iff b3 = Tr ) ); deffunc H1( typealg ) -> set = [:( the carrier of $1 *), the carrier of $1:]; definition let s be non empty typealg ; let f be FinSequence of s; let t be type of s; :: original: [ redefine func[f,t] -> Element of [:( the carrier of s *), the carrier of s:]; coherence [f,t] is Element of [:( the carrier of s *), the carrier of s:] proof f in the carrier of s * by FINSEQ_1:def_11; hence [f,t] is Element of [:( the carrier of s *), the carrier of s:] by ZFMISC_1:87; ::_thesis: verum end; end; definition let s be non empty typealg ; mode Proof of s -> PreProof of s means :Def12: :: PRELAMB:def 12 ( dom it is finite & ( for v being Element of dom it holds v is correct ) ); existence ex b1 being PreProof of s st ( dom b1 is finite & ( for v being Element of dom b1 holds v is correct ) ) proof set x = the type of s; set Tr = {{}} --> [[<* the type of s*>, the type of s],0]; A1: dom ({{}} --> [[<* the type of s*>, the type of s],0]) = {{}} by FUNCOP_1:13; reconsider Tr = {{}} --> [[<* the type of s*>, the type of s],0] as finite DecoratedTree by TREES_1:23; A2: [[<* the type of s*>, the type of s],0] in [:H1(s),NAT:] by ZFMISC_1:87; {[[<* the type of s*>, the type of s],0]} = rng Tr by FUNCOP_1:8; then rng Tr c= [:H1(s),NAT:] by A2, ZFMISC_1:31; then reconsider Tr = Tr as PreProof of s by RELAT_1:def_19; take Tr ; ::_thesis: ( dom Tr is finite & ( for v being Element of dom Tr holds v is correct ) ) thus dom Tr is finite ; ::_thesis: for v being Element of dom Tr holds v is correct let v be Element of dom Tr; ::_thesis: v is correct A3: v = {} by A1, TARSKI:def_1; A4: now__::_thesis:_not_(dom_Tr)_-level_1_<>_{} set x = the Element of (dom Tr) -level 1; assume (dom Tr) -level 1 <> {} ; ::_thesis: contradiction then the Element of (dom Tr) -level 1 in (dom Tr) -level 1 ; then the Element of (dom Tr) -level 1 in { w where w is Element of dom Tr : len w = 1 } by TREES_2:def_6; then ex w being Element of dom Tr st ( the Element of (dom Tr) -level 1 = w & len w = 1 ) ; hence contradiction by A1, CARD_1:27, TARSKI:def_1; ::_thesis: verum end; A5: branchdeg v = card (succ v) by TREES_2:def_12 .= 0 by A3, A4, CARD_1:27, TREES_2:13 ; A6: Tr . v = [[<* the type of s*>, the type of s],0] by A1, FUNCOP_1:7; then A7: (Tr . v) `1 = [<* the type of s*>, the type of s] by MCART_1:7; (Tr . v) `2 = 0 by A6, MCART_1:7; hence v is correct by A5, A7, Def4; ::_thesis: verum end; end; :: deftheorem Def12 defines Proof PRELAMB:def_12_:_ for s being non empty typealg for b2 being PreProof of s holds ( b2 is Proof of s iff ( dom b2 is finite & ( for v being Element of dom b2 holds v is correct ) ) ); theorem Th1: :: PRELAMB:1 for s being non empty typealg for p being Proof of s for v being Element of dom p st branchdeg v = 1 holds v ^ <*0*> in dom p proof let s be non empty typealg ; ::_thesis: for p being Proof of s for v being Element of dom p st branchdeg v = 1 holds v ^ <*0*> in dom p let p be Proof of s; ::_thesis: for v being Element of dom p st branchdeg v = 1 holds v ^ <*0*> in dom p let v be Element of dom p; ::_thesis: ( branchdeg v = 1 implies v ^ <*0*> in dom p ) assume branchdeg v = 1 ; ::_thesis: v ^ <*0*> in dom p then A1: succ v <> {} by CARD_1:27, TREES_2:def_12; set x = the Element of succ v; the Element of succ v in succ v by A1; then the Element of succ v in { (v ^ <*n*>) where n is Element of NAT : v ^ <*n*> in dom p } by TREES_2:def_5; then consider n being Element of NAT such that the Element of succ v = v ^ <*n*> and A2: v ^ <*n*> in dom p ; 0 <= n by NAT_1:2; hence v ^ <*0*> in dom p by A2, TREES_1:def_3; ::_thesis: verum end; theorem Th2: :: PRELAMB:2 for s being non empty typealg for p being Proof of s for v being Element of dom p st branchdeg v = 2 holds ( v ^ <*0*> in dom p & v ^ <*1*> in dom p ) proof let s be non empty typealg ; ::_thesis: for p being Proof of s for v being Element of dom p st branchdeg v = 2 holds ( v ^ <*0*> in dom p & v ^ <*1*> in dom p ) let p be Proof of s; ::_thesis: for v being Element of dom p st branchdeg v = 2 holds ( v ^ <*0*> in dom p & v ^ <*1*> in dom p ) let v be Element of dom p; ::_thesis: ( branchdeg v = 2 implies ( v ^ <*0*> in dom p & v ^ <*1*> in dom p ) ) A1: succ v = { (v ^ <*n*>) where n is Element of NAT : v ^ <*n*> in dom p } by TREES_2:def_5; assume branchdeg v = 2 ; ::_thesis: ( v ^ <*0*> in dom p & v ^ <*1*> in dom p ) then card (succ v) = 2 by TREES_2:def_12; then consider x, y being set such that A2: x <> y and A3: succ v = {x,y} by CARD_2:60; x in succ v by A3, TARSKI:def_2; then consider n being Element of NAT such that A4: x = v ^ <*n*> and A5: v ^ <*n*> in dom p by A1; y in succ v by A3, TARSKI:def_2; then consider k being Element of NAT such that A6: y = v ^ <*k*> and A7: v ^ <*k*> in dom p by A1; ( n <> 0 or k <> 0 ) by A2, A4, A6; then A8: ( n > 0 or k > 0 ) by NAT_1:3; hence v ^ <*0*> in dom p by A5, A7, TREES_1:def_3; ::_thesis: v ^ <*1*> in dom p ( n >= 0 + 1 or k >= 0 + 1 ) by A8, NAT_1:13; hence v ^ <*1*> in dom p by A5, A7, TREES_1:def_3; ::_thesis: verum end; theorem :: PRELAMB:3 for s being non empty typealg for p being Proof of s for v being Element of dom p st (p . v) `2 = 0 holds ex x being type of s st (p . v) `1 = [<*x*>,x] proof let s be non empty typealg ; ::_thesis: for p being Proof of s for v being Element of dom p st (p . v) `2 = 0 holds ex x being type of s st (p . v) `1 = [<*x*>,x] let p be Proof of s; ::_thesis: for v being Element of dom p st (p . v) `2 = 0 holds ex x being type of s st (p . v) `1 = [<*x*>,x] let v be Element of dom p; ::_thesis: ( (p . v) `2 = 0 implies ex x being type of s st (p . v) `1 = [<*x*>,x] ) v is correct by Def12; hence ( (p . v) `2 = 0 implies ex x being type of s st (p . v) `1 = [<*x*>,x] ) by Def4; ::_thesis: verum end; theorem :: PRELAMB:4 for s being non empty typealg for p being Proof of s for v being Element of dom p st (p . v) `2 = 1 holds ex w being Element of dom p ex T being FinSequence of s ex x, y being type of s st ( w = v ^ <*0*> & (p . v) `1 = [T,(x /" y)] & (p . w) `1 = [(T ^ <*y*>),x] ) proof let s be non empty typealg ; ::_thesis: for p being Proof of s for v being Element of dom p st (p . v) `2 = 1 holds ex w being Element of dom p ex T being FinSequence of s ex x, y being type of s st ( w = v ^ <*0*> & (p . v) `1 = [T,(x /" y)] & (p . w) `1 = [(T ^ <*y*>),x] ) let p be Proof of s; ::_thesis: for v being Element of dom p st (p . v) `2 = 1 holds ex w being Element of dom p ex T being FinSequence of s ex x, y being type of s st ( w = v ^ <*0*> & (p . v) `1 = [T,(x /" y)] & (p . w) `1 = [(T ^ <*y*>),x] ) let v be Element of dom p; ::_thesis: ( (p . v) `2 = 1 implies ex w being Element of dom p ex T being FinSequence of s ex x, y being type of s st ( w = v ^ <*0*> & (p . v) `1 = [T,(x /" y)] & (p . w) `1 = [(T ^ <*y*>),x] ) ) A1: v is correct by Def12; assume A2: (p . v) `2 = 1 ; ::_thesis: ex w being Element of dom p ex T being FinSequence of s ex x, y being type of s st ( w = v ^ <*0*> & (p . v) `1 = [T,(x /" y)] & (p . w) `1 = [(T ^ <*y*>),x] ) then A3: ex T being FinSequence of s ex x, y being type of s st ( (p . v) `1 = [T,(x /" y)] & (p . (v ^ <*0*>)) `1 = [(T ^ <*y*>),x] ) by A1, Def4; branchdeg v = 1 by A1, A2, Def4; then v ^ <*0*> in dom p by Th1; hence ex w being Element of dom p ex T being FinSequence of s ex x, y being type of s st ( w = v ^ <*0*> & (p . v) `1 = [T,(x /" y)] & (p . w) `1 = [(T ^ <*y*>),x] ) by A3; ::_thesis: verum end; theorem :: PRELAMB:5 for s being non empty typealg for p being Proof of s for v being Element of dom p st (p . v) `2 = 2 holds ex w being Element of dom p ex T being FinSequence of s ex x, y being type of s st ( w = v ^ <*0*> & (p . v) `1 = [T,(y \ x)] & (p . w) `1 = [(<*y*> ^ T),x] ) proof let s be non empty typealg ; ::_thesis: for p being Proof of s for v being Element of dom p st (p . v) `2 = 2 holds ex w being Element of dom p ex T being FinSequence of s ex x, y being type of s st ( w = v ^ <*0*> & (p . v) `1 = [T,(y \ x)] & (p . w) `1 = [(<*y*> ^ T),x] ) let p be Proof of s; ::_thesis: for v being Element of dom p st (p . v) `2 = 2 holds ex w being Element of dom p ex T being FinSequence of s ex x, y being type of s st ( w = v ^ <*0*> & (p . v) `1 = [T,(y \ x)] & (p . w) `1 = [(<*y*> ^ T),x] ) let v be Element of dom p; ::_thesis: ( (p . v) `2 = 2 implies ex w being Element of dom p ex T being FinSequence of s ex x, y being type of s st ( w = v ^ <*0*> & (p . v) `1 = [T,(y \ x)] & (p . w) `1 = [(<*y*> ^ T),x] ) ) A1: v is correct by Def12; assume A2: (p . v) `2 = 2 ; ::_thesis: ex w being Element of dom p ex T being FinSequence of s ex x, y being type of s st ( w = v ^ <*0*> & (p . v) `1 = [T,(y \ x)] & (p . w) `1 = [(<*y*> ^ T),x] ) then A3: ex T being FinSequence of s ex x, y being type of s st ( (p . v) `1 = [T,(y \ x)] & (p . (v ^ <*0*>)) `1 = [(<*y*> ^ T),x] ) by A1, Def4; branchdeg v = 1 by A1, A2, Def4; then v ^ <*0*> in dom p by Th1; hence ex w being Element of dom p ex T being FinSequence of s ex x, y being type of s st ( w = v ^ <*0*> & (p . v) `1 = [T,(y \ x)] & (p . w) `1 = [(<*y*> ^ T),x] ) by A3; ::_thesis: verum end; theorem :: PRELAMB:6 for s being non empty typealg for p being Proof of s for v being Element of dom p st (p . v) `2 = 3 holds ex w, u being Element of dom p ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( w = v ^ <*0*> & u = v ^ <*1*> & (p . v) `1 = [(((X ^ <*(x /" y)*>) ^ T) ^ Y),z] & (p . w) `1 = [T,y] & (p . u) `1 = [((X ^ <*x*>) ^ Y),z] ) proof let s be non empty typealg ; ::_thesis: for p being Proof of s for v being Element of dom p st (p . v) `2 = 3 holds ex w, u being Element of dom p ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( w = v ^ <*0*> & u = v ^ <*1*> & (p . v) `1 = [(((X ^ <*(x /" y)*>) ^ T) ^ Y),z] & (p . w) `1 = [T,y] & (p . u) `1 = [((X ^ <*x*>) ^ Y),z] ) let p be Proof of s; ::_thesis: for v being Element of dom p st (p . v) `2 = 3 holds ex w, u being Element of dom p ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( w = v ^ <*0*> & u = v ^ <*1*> & (p . v) `1 = [(((X ^ <*(x /" y)*>) ^ T) ^ Y),z] & (p . w) `1 = [T,y] & (p . u) `1 = [((X ^ <*x*>) ^ Y),z] ) let v be Element of dom p; ::_thesis: ( (p . v) `2 = 3 implies ex w, u being Element of dom p ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( w = v ^ <*0*> & u = v ^ <*1*> & (p . v) `1 = [(((X ^ <*(x /" y)*>) ^ T) ^ Y),z] & (p . w) `1 = [T,y] & (p . u) `1 = [((X ^ <*x*>) ^ Y),z] ) ) A1: v is correct by Def12; assume A2: (p . v) `2 = 3 ; ::_thesis: ex w, u being Element of dom p ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( w = v ^ <*0*> & u = v ^ <*1*> & (p . v) `1 = [(((X ^ <*(x /" y)*>) ^ T) ^ Y),z] & (p . w) `1 = [T,y] & (p . u) `1 = [((X ^ <*x*>) ^ Y),z] ) then A3: ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( (p . v) `1 = [(((X ^ <*(x /" y)*>) ^ T) ^ Y),z] & (p . (v ^ <*0*>)) `1 = [T,y] & (p . (v ^ <*1*>)) `1 = [((X ^ <*x*>) ^ Y),z] ) by A1, Def4; A4: branchdeg v = 2 by A1, A2, Def4; then A5: v ^ <*0*> in dom p by Th2; v ^ <*1*> in dom p by A4, Th2; hence ex w, u being Element of dom p ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( w = v ^ <*0*> & u = v ^ <*1*> & (p . v) `1 = [(((X ^ <*(x /" y)*>) ^ T) ^ Y),z] & (p . w) `1 = [T,y] & (p . u) `1 = [((X ^ <*x*>) ^ Y),z] ) by A3, A5; ::_thesis: verum end; theorem :: PRELAMB:7 for s being non empty typealg for p being Proof of s for v being Element of dom p st (p . v) `2 = 4 holds ex w, u being Element of dom p ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( w = v ^ <*0*> & u = v ^ <*1*> & (p . v) `1 = [(((X ^ T) ^ <*(y \ x)*>) ^ Y),z] & (p . w) `1 = [T,y] & (p . u) `1 = [((X ^ <*x*>) ^ Y),z] ) proof let s be non empty typealg ; ::_thesis: for p being Proof of s for v being Element of dom p st (p . v) `2 = 4 holds ex w, u being Element of dom p ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( w = v ^ <*0*> & u = v ^ <*1*> & (p . v) `1 = [(((X ^ T) ^ <*(y \ x)*>) ^ Y),z] & (p . w) `1 = [T,y] & (p . u) `1 = [((X ^ <*x*>) ^ Y),z] ) let p be Proof of s; ::_thesis: for v being Element of dom p st (p . v) `2 = 4 holds ex w, u being Element of dom p ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( w = v ^ <*0*> & u = v ^ <*1*> & (p . v) `1 = [(((X ^ T) ^ <*(y \ x)*>) ^ Y),z] & (p . w) `1 = [T,y] & (p . u) `1 = [((X ^ <*x*>) ^ Y),z] ) let v be Element of dom p; ::_thesis: ( (p . v) `2 = 4 implies ex w, u being Element of dom p ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( w = v ^ <*0*> & u = v ^ <*1*> & (p . v) `1 = [(((X ^ T) ^ <*(y \ x)*>) ^ Y),z] & (p . w) `1 = [T,y] & (p . u) `1 = [((X ^ <*x*>) ^ Y),z] ) ) A1: v is correct by Def12; assume A2: (p . v) `2 = 4 ; ::_thesis: ex w, u being Element of dom p ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( w = v ^ <*0*> & u = v ^ <*1*> & (p . v) `1 = [(((X ^ T) ^ <*(y \ x)*>) ^ Y),z] & (p . w) `1 = [T,y] & (p . u) `1 = [((X ^ <*x*>) ^ Y),z] ) then A3: ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( (p . v) `1 = [(((X ^ T) ^ <*(y \ x)*>) ^ Y),z] & (p . (v ^ <*0*>)) `1 = [T,y] & (p . (v ^ <*1*>)) `1 = [((X ^ <*x*>) ^ Y),z] ) by A1, Def4; A4: branchdeg v = 2 by A1, A2, Def4; then A5: v ^ <*0*> in dom p by Th2; v ^ <*1*> in dom p by A4, Th2; hence ex w, u being Element of dom p ex T, X, Y being FinSequence of s ex x, y, z being type of s st ( w = v ^ <*0*> & u = v ^ <*1*> & (p . v) `1 = [(((X ^ T) ^ <*(y \ x)*>) ^ Y),z] & (p . w) `1 = [T,y] & (p . u) `1 = [((X ^ <*x*>) ^ Y),z] ) by A3, A5; ::_thesis: verum end; theorem :: PRELAMB:8 for s being non empty typealg for z being type of s for p being Proof of s for v being Element of dom p st (p . v) `2 = 5 holds ex w being Element of dom p ex X being FinSequence of s ex x, y being type of s ex Y being FinSequence of s st ( w = v ^ <*0*> & (p . v) `1 = [((X ^ <*(x * y)*>) ^ Y),z] & (p . w) `1 = [(((X ^ <*x*>) ^ <*y*>) ^ Y),z] ) proof let s be non empty typealg ; ::_thesis: for z being type of s for p being Proof of s for v being Element of dom p st (p . v) `2 = 5 holds ex w being Element of dom p ex X being FinSequence of s ex x, y being type of s ex Y being FinSequence of s st ( w = v ^ <*0*> & (p . v) `1 = [((X ^ <*(x * y)*>) ^ Y),z] & (p . w) `1 = [(((X ^ <*x*>) ^ <*y*>) ^ Y),z] ) let z be type of s; ::_thesis: for p being Proof of s for v being Element of dom p st (p . v) `2 = 5 holds ex w being Element of dom p ex X being FinSequence of s ex x, y being type of s ex Y being FinSequence of s st ( w = v ^ <*0*> & (p . v) `1 = [((X ^ <*(x * y)*>) ^ Y),z] & (p . w) `1 = [(((X ^ <*x*>) ^ <*y*>) ^ Y),z] ) let p be Proof of s; ::_thesis: for v being Element of dom p st (p . v) `2 = 5 holds ex w being Element of dom p ex X being FinSequence of s ex x, y being type of s ex Y being FinSequence of s st ( w = v ^ <*0*> & (p . v) `1 = [((X ^ <*(x * y)*>) ^ Y),z] & (p . w) `1 = [(((X ^ <*x*>) ^ <*y*>) ^ Y),z] ) let v be Element of dom p; ::_thesis: ( (p . v) `2 = 5 implies ex w being Element of dom p ex X being FinSequence of s ex x, y being type of s ex Y being FinSequence of s st ( w = v ^ <*0*> & (p . v) `1 = [((X ^ <*(x * y)*>) ^ Y),z] & (p . w) `1 = [(((X ^ <*x*>) ^ <*y*>) ^ Y),z] ) ) A1: v is correct by Def12; assume A2: (p . v) `2 = 5 ; ::_thesis: ex w being Element of dom p ex X being FinSequence of s ex x, y being type of s ex Y being FinSequence of s st ( w = v ^ <*0*> & (p . v) `1 = [((X ^ <*(x * y)*>) ^ Y),z] & (p . w) `1 = [(((X ^ <*x*>) ^ <*y*>) ^ Y),z] ) then A3: ex X being FinSequence of s ex x, y being type of s ex Y being FinSequence of s st ( (p . v) `1 = [((X ^ <*(x * y)*>) ^ Y),z] & (p . (v ^ <*0*>)) `1 = [(((X ^ <*x*>) ^ <*y*>) ^ Y),z] ) by A1, Def4; branchdeg v = 1 by A1, A2, Def4; then v ^ <*0*> in dom p by Th1; hence ex w being Element of dom p ex X being FinSequence of s ex x, y being type of s ex Y being FinSequence of s st ( w = v ^ <*0*> & (p . v) `1 = [((X ^ <*(x * y)*>) ^ Y),z] & (p . w) `1 = [(((X ^ <*x*>) ^ <*y*>) ^ Y),z] ) by A3; ::_thesis: verum end; theorem :: PRELAMB:9 for s being non empty typealg for p being Proof of s for v being Element of dom p st (p . v) `2 = 6 holds ex w, u being Element of dom p ex X, Y being FinSequence of s ex x, y being type of s st ( w = v ^ <*0*> & u = v ^ <*1*> & (p . v) `1 = [(X ^ Y),(x * y)] & (p . w) `1 = [X,x] & (p . u) `1 = [Y,y] ) proof let s be non empty typealg ; ::_thesis: for p being Proof of s for v being Element of dom p st (p . v) `2 = 6 holds ex w, u being Element of dom p ex X, Y being FinSequence of s ex x, y being type of s st ( w = v ^ <*0*> & u = v ^ <*1*> & (p . v) `1 = [(X ^ Y),(x * y)] & (p . w) `1 = [X,x] & (p . u) `1 = [Y,y] ) let p be Proof of s; ::_thesis: for v being Element of dom p st (p . v) `2 = 6 holds ex w, u being Element of dom p ex X, Y being FinSequence of s ex x, y being type of s st ( w = v ^ <*0*> & u = v ^ <*1*> & (p . v) `1 = [(X ^ Y),(x * y)] & (p . w) `1 = [X,x] & (p . u) `1 = [Y,y] ) let v be Element of dom p; ::_thesis: ( (p . v) `2 = 6 implies ex w, u being Element of dom p ex X, Y being FinSequence of s ex x, y being type of s st ( w = v ^ <*0*> & u = v ^ <*1*> & (p . v) `1 = [(X ^ Y),(x * y)] & (p . w) `1 = [X,x] & (p . u) `1 = [Y,y] ) ) A1: v is correct by Def12; assume A2: (p . v) `2 = 6 ; ::_thesis: ex w, u being Element of dom p ex X, Y being FinSequence of s ex x, y being type of s st ( w = v ^ <*0*> & u = v ^ <*1*> & (p . v) `1 = [(X ^ Y),(x * y)] & (p . w) `1 = [X,x] & (p . u) `1 = [Y,y] ) then A3: ex X, Y being FinSequence of s ex x, y being type of s st ( (p . v) `1 = [(X ^ Y),(x * y)] & (p . (v ^ <*0*>)) `1 = [X,x] & (p . (v ^ <*1*>)) `1 = [Y,y] ) by A1, Def4; A4: branchdeg v = 2 by A1, A2, Def4; then A5: v ^ <*0*> in dom p by Th2; v ^ <*1*> in dom p by A4, Th2; hence ex w, u being Element of dom p ex X, Y being FinSequence of s ex x, y being type of s st ( w = v ^ <*0*> & u = v ^ <*1*> & (p . v) `1 = [(X ^ Y),(x * y)] & (p . w) `1 = [X,x] & (p . u) `1 = [Y,y] ) by A3, A5; ::_thesis: verum end; theorem Th10: :: PRELAMB:10 for s being non empty typealg for p being Proof of s for v being Element of dom p st (p . v) `2 = 7 holds ex w, u being Element of dom p ex T, X, Y being FinSequence of s ex y, z being type of s st ( w = v ^ <*0*> & u = v ^ <*1*> & (p . v) `1 = [((X ^ T) ^ Y),z] & (p . w) `1 = [T,y] & (p . u) `1 = [((X ^ <*y*>) ^ Y),z] ) proof let s be non empty typealg ; ::_thesis: for p being Proof of s for v being Element of dom p st (p . v) `2 = 7 holds ex w, u being Element of dom p ex T, X, Y being FinSequence of s ex y, z being type of s st ( w = v ^ <*0*> & u = v ^ <*1*> & (p . v) `1 = [((X ^ T) ^ Y),z] & (p . w) `1 = [T,y] & (p . u) `1 = [((X ^ <*y*>) ^ Y),z] ) let p be Proof of s; ::_thesis: for v being Element of dom p st (p . v) `2 = 7 holds ex w, u being Element of dom p ex T, X, Y being FinSequence of s ex y, z being type of s st ( w = v ^ <*0*> & u = v ^ <*1*> & (p . v) `1 = [((X ^ T) ^ Y),z] & (p . w) `1 = [T,y] & (p . u) `1 = [((X ^ <*y*>) ^ Y),z] ) let v be Element of dom p; ::_thesis: ( (p . v) `2 = 7 implies ex w, u being Element of dom p ex T, X, Y being FinSequence of s ex y, z being type of s st ( w = v ^ <*0*> & u = v ^ <*1*> & (p . v) `1 = [((X ^ T) ^ Y),z] & (p . w) `1 = [T,y] & (p . u) `1 = [((X ^ <*y*>) ^ Y),z] ) ) A1: v is correct by Def12; assume A2: (p . v) `2 = 7 ; ::_thesis: ex w, u being Element of dom p ex T, X, Y being FinSequence of s ex y, z being type of s st ( w = v ^ <*0*> & u = v ^ <*1*> & (p . v) `1 = [((X ^ T) ^ Y),z] & (p . w) `1 = [T,y] & (p . u) `1 = [((X ^ <*y*>) ^ Y),z] ) then A3: ex T, X, Y being FinSequence of s ex y, z being type of s st ( (p . v) `1 = [((X ^ T) ^ Y),z] & (p . (v ^ <*0*>)) `1 = [T,y] & (p . (v ^ <*1*>)) `1 = [((X ^ <*y*>) ^ Y),z] ) by A1, Def4; A4: branchdeg v = 2 by A1, A2, Def4; then A5: v ^ <*0*> in dom p by Th2; v ^ <*1*> in dom p by A4, Th2; hence ex w, u being Element of dom p ex T, X, Y being FinSequence of s ex y, z being type of s st ( w = v ^ <*0*> & u = v ^ <*1*> & (p . v) `1 = [((X ^ T) ^ Y),z] & (p . w) `1 = [T,y] & (p . u) `1 = [((X ^ <*y*>) ^ Y),z] ) by A3, A5; ::_thesis: verum end; theorem :: PRELAMB:11 for s being non empty typealg for p being Proof of s for v being Element of dom p holds ( (p . v) `2 = 0 or (p . v) `2 = 1 or (p . v) `2 = 2 or (p . v) `2 = 3 or (p . v) `2 = 4 or (p . v) `2 = 5 or (p . v) `2 = 6 or (p . v) `2 = 7 ) proof let s be non empty typealg ; ::_thesis: for p being Proof of s for v being Element of dom p holds ( (p . v) `2 = 0 or (p . v) `2 = 1 or (p . v) `2 = 2 or (p . v) `2 = 3 or (p . v) `2 = 4 or (p . v) `2 = 5 or (p . v) `2 = 6 or (p . v) `2 = 7 ) let p be Proof of s; ::_thesis: for v being Element of dom p holds ( (p . v) `2 = 0 or (p . v) `2 = 1 or (p . v) `2 = 2 or (p . v) `2 = 3 or (p . v) `2 = 4 or (p . v) `2 = 5 or (p . v) `2 = 6 or (p . v) `2 = 7 ) let v be Element of dom p; ::_thesis: ( (p . v) `2 = 0 or (p . v) `2 = 1 or (p . v) `2 = 2 or (p . v) `2 = 3 or (p . v) `2 = 4 or (p . v) `2 = 5 or (p . v) `2 = 6 or (p . v) `2 = 7 ) v is correct by Def12; hence ( (p . v) `2 = 0 or (p . v) `2 = 1 or (p . v) `2 = 2 or (p . v) `2 = 3 or (p . v) `2 = 4 or (p . v) `2 = 5 or (p . v) `2 = 6 or (p . v) `2 = 7 ) by Def4; ::_thesis: verum end; definition let s be non empty typealg ; let IT be PreProof of s; attrIT is cut-free means :: PRELAMB:def 13 for v being Element of dom IT holds (IT . v) `2 <> 7; end; :: deftheorem defines cut-free PRELAMB:def_13_:_ for s being non empty typealg for IT being PreProof of s holds ( IT is cut-free iff for v being Element of dom IT holds (IT . v) `2 <> 7 ); definition let s be non empty typealg ; func size_w.r.t. s -> Function of the carrier of s,NAT means :: PRELAMB:def 14 for x being type of s holds it . x = card (dom (repr_of x)); existence ex b1 being Function of the carrier of s,NAT st for x being type of s holds b1 . x = card (dom (repr_of x)) proof deffunc H2( type of s) -> Element of NAT = card (dom (repr_of $1)); thus ex S being Function of the carrier of s,NAT st for x being type of s holds S . x = H2(x) from FUNCT_2:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being Function of the carrier of s,NAT st ( for x being type of s holds b1 . x = card (dom (repr_of x)) ) & ( for x being type of s holds b2 . x = card (dom (repr_of x)) ) holds b1 = b2 proof let f, g be Function of the carrier of s,NAT; ::_thesis: ( ( for x being type of s holds f . x = card (dom (repr_of x)) ) & ( for x being type of s holds g . x = card (dom (repr_of x)) ) implies f = g ) deffunc H2( type of s) -> Element of NAT = card (dom (repr_of $1)); assume that A1: for x being type of s holds f . x = H2(x) and A2: for x being type of s holds g . x = H2(x) ; ::_thesis: f = g now__::_thesis:_for_c_being_Element_of_s_holds_f_._c_=_g_._c let c be Element of s; ::_thesis: f . c = g . c thus f . c = H2(c) by A1 .= g . c by A2 ; ::_thesis: verum end; hence f = g by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem defines size_w.r.t. PRELAMB:def_14_:_ for s being non empty typealg for b2 being Function of the carrier of s,NAT holds ( b2 = size_w.r.t. s iff for x being type of s holds b2 . x = card (dom (repr_of x)) ); definition let D be non empty set ; let T be FinSequence of D; let f be Function of D,NAT; :: original: (#) redefine funcf * T -> FinSequence of REAL ; coherence T (#) f is FinSequence of REAL proof A1: f * T is FinSequence of NAT by FINSEQ_2:32; rng (f * T) c= REAL ; hence T (#) f is FinSequence of REAL by A1, FINSEQ_1:def_4; ::_thesis: verum end; end; Lm1: for D being non empty set for T being FinSequence of D for f being Function of D,NAT holds Sum (f * T) is Nat proof let D be non empty set ; ::_thesis: for T being FinSequence of D for f being Function of D,NAT holds Sum (f * T) is Nat let T be FinSequence of D; ::_thesis: for f being Function of D,NAT holds Sum (f * T) is Nat let f be Function of D,NAT; ::_thesis: Sum (f * T) is Nat defpred S1[ FinSequence of REAL ] means ( $1 is FinSequence of NAT implies Sum $1 is Nat ); A1: S1[ <*> REAL] by RVSUM_1:72; A2: for p being FinSequence of REAL for x being Real st S1[p] holds S1[p ^ <*x*>] proof let p be FinSequence of REAL ; ::_thesis: for x being Real st S1[p] holds S1[p ^ <*x*>] let x be Real; ::_thesis: ( S1[p] implies S1[p ^ <*x*>] ) assume A3: S1[p] ; ::_thesis: S1[p ^ <*x*>] assume p ^ <*x*> is FinSequence of NAT ; ::_thesis: Sum (p ^ <*x*>) is Nat then A4: rng (p ^ <*x*>) c= NAT by FINSEQ_1:def_4; rng p c= rng (p ^ <*x*>) by FINSEQ_1:29; then A5: rng p c= NAT by A4, XBOOLE_1:1; rng <*x*> c= rng (p ^ <*x*>) by FINSEQ_1:30; then A6: rng <*x*> c= NAT by A4, XBOOLE_1:1; rng <*x*> = {x} by FINSEQ_1:38; then reconsider n = x as Element of NAT by A6, ZFMISC_1:31; reconsider s = Sum p as Nat by A3, A5, FINSEQ_1:def_4; Sum (p ^ <*x*>) = s + n by RVSUM_1:74; hence Sum (p ^ <*x*>) is Nat ; ::_thesis: verum end; A7: for p being FinSequence of REAL holds S1[p] from FINSEQ_2:sch_2(A1, A2); f * T is FinSequence of NAT by FINSEQ_2:32; hence Sum (f * T) is Nat by A7; ::_thesis: verum end; definition let s be non empty typealg ; let p be Proof of s; func cutdeg p -> Nat means :: PRELAMB:def 15 ex T, X, Y being FinSequence of s ex y, z being type of s st ( (p . {}) `1 = [((X ^ T) ^ Y),z] & (p . <*0*>) `1 = [T,y] & (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] & it = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) if (p . {}) `2 = 7 otherwise it = 0 ; existence ( ( (p . {}) `2 = 7 implies ex b1 being Nat ex T, X, Y being FinSequence of s ex y, z being type of s st ( (p . {}) `1 = [((X ^ T) ^ Y),z] & (p . <*0*>) `1 = [T,y] & (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] & b1 = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) ) & ( not (p . {}) `2 = 7 implies ex b1 being Nat st b1 = 0 ) ) proof thus ( (p . {}) `2 = 7 implies ex r being Nat ex T, X, Y being FinSequence of s ex y, z being type of s st ( (p . {}) `1 = [((X ^ T) ^ Y),z] & (p . <*0*>) `1 = [T,y] & (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] & r = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) ) ::_thesis: ( not (p . {}) `2 = 7 implies ex b1 being Nat st b1 = 0 ) proof A1: {} ^ <*0*> = <*0*> by FINSEQ_1:34; A2: {} ^ <*1*> = <*1*> by FINSEQ_1:34; reconsider v = {} as Element of dom p by TREES_1:22; assume (p . {}) `2 = 7 ; ::_thesis: ex r being Nat ex T, X, Y being FinSequence of s ex y, z being type of s st ( (p . {}) `1 = [((X ^ T) ^ Y),z] & (p . <*0*>) `1 = [T,y] & (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] & r = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) then consider w, u being Element of dom p, T, X, Y being FinSequence of s, y, z being type of s such that A3: w = v ^ <*0*> and A4: u = v ^ <*1*> and A5: (p . v) `1 = [((X ^ T) ^ Y),z] and A6: (p . w) `1 = [T,y] and A7: (p . u) `1 = [((X ^ <*y*>) ^ Y),z] by Th10; reconsider a = Sum ((size_w.r.t. s) * ((X ^ T) ^ Y)) as Nat by Lm1; take (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + a ; ::_thesis: ex T, X, Y being FinSequence of s ex y, z being type of s st ( (p . {}) `1 = [((X ^ T) ^ Y),z] & (p . <*0*>) `1 = [T,y] & (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] & (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + a = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) thus ex T, X, Y being FinSequence of s ex y, z being type of s st ( (p . {}) `1 = [((X ^ T) ^ Y),z] & (p . <*0*>) `1 = [T,y] & (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] & (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + a = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) by A1, A2, A3, A4, A5, A6, A7; ::_thesis: verum end; thus ( not (p . {}) `2 = 7 implies ex b1 being Nat st b1 = 0 ) ; ::_thesis: verum end; uniqueness for b1, b2 being Nat holds ( ( (p . {}) `2 = 7 & ex T, X, Y being FinSequence of s ex y, z being type of s st ( (p . {}) `1 = [((X ^ T) ^ Y),z] & (p . <*0*>) `1 = [T,y] & (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] & b1 = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) & ex T, X, Y being FinSequence of s ex y, z being type of s st ( (p . {}) `1 = [((X ^ T) ^ Y),z] & (p . <*0*>) `1 = [T,y] & (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] & b2 = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) implies b1 = b2 ) & ( not (p . {}) `2 = 7 & b1 = 0 & b2 = 0 implies b1 = b2 ) ) proof let r1, r2 be Nat; ::_thesis: ( ( (p . {}) `2 = 7 & ex T, X, Y being FinSequence of s ex y, z being type of s st ( (p . {}) `1 = [((X ^ T) ^ Y),z] & (p . <*0*>) `1 = [T,y] & (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] & r1 = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) & ex T, X, Y being FinSequence of s ex y, z being type of s st ( (p . {}) `1 = [((X ^ T) ^ Y),z] & (p . <*0*>) `1 = [T,y] & (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] & r2 = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) implies r1 = r2 ) & ( not (p . {}) `2 = 7 & r1 = 0 & r2 = 0 implies r1 = r2 ) ) thus ( (p . {}) `2 = 7 & ex T, X, Y being FinSequence of s ex y, z being type of s st ( (p . {}) `1 = [((X ^ T) ^ Y),z] & (p . <*0*>) `1 = [T,y] & (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] & r1 = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) & ex T, X, Y being FinSequence of s ex y, z being type of s st ( (p . {}) `1 = [((X ^ T) ^ Y),z] & (p . <*0*>) `1 = [T,y] & (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] & r2 = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) implies r1 = r2 ) ::_thesis: ( not (p . {}) `2 = 7 & r1 = 0 & r2 = 0 implies r1 = r2 ) proof assume (p . {}) `2 = 7 ; ::_thesis: ( for T, X, Y being FinSequence of s for y, z being type of s holds ( not (p . {}) `1 = [((X ^ T) ^ Y),z] or not (p . <*0*>) `1 = [T,y] or not (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] or not r1 = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) or for T, X, Y being FinSequence of s for y, z being type of s holds ( not (p . {}) `1 = [((X ^ T) ^ Y),z] or not (p . <*0*>) `1 = [T,y] or not (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] or not r2 = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) or r1 = r2 ) given T, X, Y being FinSequence of s, y, z being type of s such that A8: (p . {}) `1 = [((X ^ T) ^ Y),z] and A9: (p . <*0*>) `1 = [T,y] and (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] and A10: r1 = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ; ::_thesis: ( for T, X, Y being FinSequence of s for y, z being type of s holds ( not (p . {}) `1 = [((X ^ T) ^ Y),z] or not (p . <*0*>) `1 = [T,y] or not (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] or not r2 = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) or r1 = r2 ) given T9, X9, Y9 being FinSequence of s, y9, z9 being type of s such that A11: (p . {}) `1 = [((X9 ^ T9) ^ Y9),z9] and A12: (p . <*0*>) `1 = [T9,y9] and (p . <*1*>) `1 = [((X9 ^ <*y9*>) ^ Y9),z9] and A13: r2 = (((size_w.r.t. s) . y9) + ((size_w.r.t. s) . z9)) + (Sum ((size_w.r.t. s) * ((X9 ^ T9) ^ Y9))) ; ::_thesis: r1 = r2 A14: (X ^ T) ^ Y = [((X ^ T) ^ Y),z] `1 .= (X9 ^ T9) ^ Y9 by A8, A11, MCART_1:7 ; A15: y = [T,y] `2 .= y9 by A9, A12, MCART_1:7 ; z = [((X ^ T) ^ Y),z] `2 .= z9 by A8, A11, MCART_1:7 ; hence r1 = r2 by A10, A13, A14, A15; ::_thesis: verum end; thus ( not (p . {}) `2 = 7 & r1 = 0 & r2 = 0 implies r1 = r2 ) ; ::_thesis: verum end; consistency for b1 being Nat holds verum ; end; :: deftheorem defines cutdeg PRELAMB:def_15_:_ for s being non empty typealg for p being Proof of s for b3 being Nat holds ( ( (p . {}) `2 = 7 implies ( b3 = cutdeg p iff ex T, X, Y being FinSequence of s ex y, z being type of s st ( (p . {}) `1 = [((X ^ T) ^ Y),z] & (p . <*0*>) `1 = [T,y] & (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] & b3 = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) ) ) & ( not (p . {}) `2 = 7 implies ( b3 = cutdeg p iff b3 = 0 ) ) ); definition let s be non empty typealg ; let A be non empty set ; mode Model of s,A -> Function of the carrier of s,(bool (A *)) means :: PRELAMB:def 16 for x, y being type of s holds ( it . (x * y) = { (a ^ b) where a, b is Element of A * : ( a in it . x & b in it . y ) } & it . (x /" y) = { a1 where a1 is Element of A * : for b being Element of A * st b in it . y holds a1 ^ b in it . x } & it . (y \ x) = { a2 where a2 is Element of A * : for b being Element of A * st b in it . y holds b ^ a2 in it . x } ); existence ex b1 being Function of the carrier of s,(bool (A *)) st for x, y being type of s holds ( b1 . (x * y) = { (a ^ b) where a, b is Element of A * : ( a in b1 . x & b in b1 . y ) } & b1 . (x /" y) = { a1 where a1 is Element of A * : for b being Element of A * st b in b1 . y holds a1 ^ b in b1 . x } & b1 . (y \ x) = { a2 where a2 is Element of A * : for b being Element of A * st b in b1 . y holds b ^ a2 in b1 . x } ) proof {} in A * by FINSEQ_1:49; then {{}} c= A * by ZFMISC_1:31; then reconsider f = the carrier of s --> {{}} as Function of the carrier of s,(bool (A *)) by FUNCOP_1:45; A1: for x being type of s for t being set st t in f . x holds t = {} proof let x be type of s; ::_thesis: for t being set st t in f . x holds t = {} let t be set ; ::_thesis: ( t in f . x implies t = {} ) assume t in f . x ; ::_thesis: t = {} then t in {{}} by FUNCOP_1:7; hence t = {} by TARSKI:def_1; ::_thesis: verum end; A2: for x being type of s holds {} in f . x proof let x be type of s; ::_thesis: {} in f . x f . x = {{}} by FUNCOP_1:7; hence {} in f . x by TARSKI:def_1; ::_thesis: verum end; A3: {} is Element of A * by FINSEQ_1:49; take f ; ::_thesis: for x, y being type of s holds ( f . (x * y) = { (a ^ b) where a, b is Element of A * : ( a in f . x & b in f . y ) } & f . (x /" y) = { a1 where a1 is Element of A * : for b being Element of A * st b in f . y holds a1 ^ b in f . x } & f . (y \ x) = { a2 where a2 is Element of A * : for b being Element of A * st b in f . y holds b ^ a2 in f . x } ) let x, y be type of s; ::_thesis: ( f . (x * y) = { (a ^ b) where a, b is Element of A * : ( a in f . x & b in f . y ) } & f . (x /" y) = { a1 where a1 is Element of A * : for b being Element of A * st b in f . y holds a1 ^ b in f . x } & f . (y \ x) = { a2 where a2 is Element of A * : for b being Element of A * st b in f . y holds b ^ a2 in f . x } ) thus f . (x * y) = { (a ^ b) where a, b is Element of A * : ( a in f . x & b in f . y ) } ::_thesis: ( f . (x /" y) = { a1 where a1 is Element of A * : for b being Element of A * st b in f . y holds a1 ^ b in f . x } & f . (y \ x) = { a2 where a2 is Element of A * : for b being Element of A * st b in f . y holds b ^ a2 in f . x } ) proof thus f . (x * y) c= { (a ^ b) where a, b is Element of A * : ( a in f . x & b in f . y ) } :: according to XBOOLE_0:def_10 ::_thesis: { (a ^ b) where a, b is Element of A * : ( a in f . x & b in f . y ) } c= f . (x * y) proof let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in f . (x * y) or t in { (a ^ b) where a, b is Element of A * : ( a in f . x & b in f . y ) } ) assume t in f . (x * y) ; ::_thesis: t in { (a ^ b) where a, b is Element of A * : ( a in f . x & b in f . y ) } then A4: t = {} by A1; A5: {} ^ {} = {} by FINSEQ_1:34; A6: t = {} ^ {} by A4, A5; A7: {} in f . x by A2; {} in f . y by A2; hence t in { (a ^ b) where a, b is Element of A * : ( a in f . x & b in f . y ) } by A6, A7; ::_thesis: verum end; let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in { (a ^ b) where a, b is Element of A * : ( a in f . x & b in f . y ) } or t in f . (x * y) ) assume t in { (a ^ b) where a, b is Element of A * : ( a in f . x & b in f . y ) } ; ::_thesis: t in f . (x * y) then consider a, b being Element of A * such that A8: t = a ^ b and A9: a in f . x and A10: b in f . y ; A11: a = {} by A1, A9; b = {} by A1, A10; then a ^ b = {} by A11, FINSEQ_1:34; hence t in f . (x * y) by A2, A8; ::_thesis: verum end; thus f . (x /" y) = { a where a is Element of A * : for b being Element of A * st b in f . y holds a ^ b in f . x } ::_thesis: f . (y \ x) = { a2 where a2 is Element of A * : for b being Element of A * st b in f . y holds b ^ a2 in f . x } proof thus f . (x /" y) c= { a where a is Element of A * : for b being Element of A * st b in f . y holds a ^ b in f . x } :: according to XBOOLE_0:def_10 ::_thesis: { a where a is Element of A * : for b being Element of A * st b in f . y holds a ^ b in f . x } c= f . (x /" y) proof let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in f . (x /" y) or t in { a where a is Element of A * : for b being Element of A * st b in f . y holds a ^ b in f . x } ) assume t in f . (x /" y) ; ::_thesis: t in { a where a is Element of A * : for b being Element of A * st b in f . y holds a ^ b in f . x } then A12: t = {} by A1; now__::_thesis:_for_b_being_Element_of_A_*_st_b_in_f_._y_holds_ {}_^_b_in_f_._x let b be Element of A * ; ::_thesis: ( b in f . y implies {} ^ b in f . x ) assume b in f . y ; ::_thesis: {} ^ b in f . x then b = {} by A1; then {} ^ b = {} by FINSEQ_1:34; hence {} ^ b in f . x by A2; ::_thesis: verum end; hence t in { a where a is Element of A * : for b being Element of A * st b in f . y holds a ^ b in f . x } by A3, A12; ::_thesis: verum end; let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in { a where a is Element of A * : for b being Element of A * st b in f . y holds a ^ b in f . x } or t in f . (x /" y) ) assume t in { a where a is Element of A * : for b being Element of A * st b in f . y holds a ^ b in f . x } ; ::_thesis: t in f . (x /" y) then consider a being Element of A * such that A13: t = a and A14: for b being Element of A * st b in f . y holds a ^ b in f . x ; {} in f . y by A2; then a ^ {} in f . x by A14; then a = {} by A1; hence t in f . (x /" y) by A2, A13; ::_thesis: verum end; thus f . (y \ x) = { a where a is Element of A * : for b being Element of A * st b in f . y holds b ^ a in f . x } ::_thesis: verum proof thus f . (y \ x) c= { a where a is Element of A * : for b being Element of A * st b in f . y holds b ^ a in f . x } :: according to XBOOLE_0:def_10 ::_thesis: { a where a is Element of A * : for b being Element of A * st b in f . y holds b ^ a in f . x } c= f . (y \ x) proof let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in f . (y \ x) or t in { a where a is Element of A * : for b being Element of A * st b in f . y holds b ^ a in f . x } ) assume t in f . (y \ x) ; ::_thesis: t in { a where a is Element of A * : for b being Element of A * st b in f . y holds b ^ a in f . x } then A15: t = {} by A1; now__::_thesis:_for_b_being_Element_of_A_*_st_b_in_f_._y_holds_ b_^_{}_in_f_._x let b be Element of A * ; ::_thesis: ( b in f . y implies b ^ {} in f . x ) assume b in f . y ; ::_thesis: b ^ {} in f . x then b = {} by A1; then b ^ {} = {} by FINSEQ_1:34; hence b ^ {} in f . x by A2; ::_thesis: verum end; hence t in { a where a is Element of A * : for b being Element of A * st b in f . y holds b ^ a in f . x } by A3, A15; ::_thesis: verum end; let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in { a where a is Element of A * : for b being Element of A * st b in f . y holds b ^ a in f . x } or t in f . (y \ x) ) assume t in { a where a is Element of A * : for b being Element of A * st b in f . y holds b ^ a in f . x } ; ::_thesis: t in f . (y \ x) then consider a being Element of A * such that A16: t = a and A17: for b being Element of A * st b in f . y holds b ^ a in f . x ; {} in f . y by A2; then {} ^ a in f . x by A17; then a = {} by A1; hence t in f . (y \ x) by A2, A16; ::_thesis: verum end; end; end; :: deftheorem defines Model PRELAMB:def_16_:_ for s being non empty typealg for A being non empty set for b3 being Function of the carrier of s,(bool (A *)) holds ( b3 is Model of s,A iff for x, y being type of s holds ( b3 . (x * y) = { (a ^ b) where a, b is Element of A * : ( a in b3 . x & b in b3 . y ) } & b3 . (x /" y) = { a1 where a1 is Element of A * : for b being Element of A * st b in b3 . y holds a1 ^ b in b3 . x } & b3 . (y \ x) = { a2 where a2 is Element of A * : for b being Element of A * st b in b3 . y holds b ^ a2 in b3 . x } ) ); definition attrc1 is strict ; struct typestr -> typealg ; aggrtypestr(# carrier, left_quotient, right_quotient, inner_product, derivability #) -> typestr ; sel derivability c1 -> Relation of ( the carrier of c1 *), the carrier of c1; end; registration cluster non empty strict for typestr ; existence ex b1 being typestr st ( not b1 is empty & b1 is strict ) proof set l = the BinOp of {{}}; set d = the Relation of ({{}} *),{{}}; take typestr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}}, the Relation of ({{}} *),{{}} #) ; ::_thesis: ( not typestr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}}, the Relation of ({{}} *),{{}} #) is empty & typestr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}}, the Relation of ({{}} *),{{}} #) is strict ) thus not the carrier of typestr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}}, the Relation of ({{}} *),{{}} #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: typestr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}}, the Relation of ({{}} *),{{}} #) is strict thus typestr(# {{}}, the BinOp of {{}}, the BinOp of {{}}, the BinOp of {{}}, the Relation of ({{}} *),{{}} #) is strict ; ::_thesis: verum end; end; definition let s be non empty typestr ; let f be FinSequence of s; let x be type of s; predf ==>. x means :Def17: :: PRELAMB:def 17 [f,x] in the derivability of s; end; :: deftheorem Def17 defines ==>. PRELAMB:def_17_:_ for s being non empty typestr for f being FinSequence of s for x being type of s holds ( f ==>. x iff [f,x] in the derivability of s ); definition let IT be non empty typestr ; attrIT is SynTypes_Calculus-like means :Def18: :: PRELAMB:def 18 ( ( for x being type of IT holds <*x*> ==>. x ) & ( for T being FinSequence of IT for x, y being type of IT st T ^ <*y*> ==>. x holds T ==>. x /" y ) & ( for T being FinSequence of IT for x, y being type of IT st <*y*> ^ T ==>. x holds T ==>. y \ x ) & ( for T, X, Y being FinSequence of IT for x, y, z being type of IT st T ==>. y & (X ^ <*x*>) ^ Y ==>. z holds ((X ^ <*(x /" y)*>) ^ T) ^ Y ==>. z ) & ( for T, X, Y being FinSequence of IT for x, y, z being type of IT st T ==>. y & (X ^ <*x*>) ^ Y ==>. z holds ((X ^ T) ^ <*(y \ x)*>) ^ Y ==>. z ) & ( for X, Y being FinSequence of IT for x, y, z being type of IT st ((X ^ <*x*>) ^ <*y*>) ^ Y ==>. z holds (X ^ <*(x * y)*>) ^ Y ==>. z ) & ( for X, Y being FinSequence of IT for x, y being type of IT st X ==>. x & Y ==>. y holds X ^ Y ==>. x * y ) ); end; :: deftheorem Def18 defines SynTypes_Calculus-like PRELAMB:def_18_:_ for IT being non empty typestr holds ( IT is SynTypes_Calculus-like iff ( ( for x being type of IT holds <*x*> ==>. x ) & ( for T being FinSequence of IT for x, y being type of IT st T ^ <*y*> ==>. x holds T ==>. x /" y ) & ( for T being FinSequence of IT for x, y being type of IT st <*y*> ^ T ==>. x holds T ==>. y \ x ) & ( for T, X, Y being FinSequence of IT for x, y, z being type of IT st T ==>. y & (X ^ <*x*>) ^ Y ==>. z holds ((X ^ <*(x /" y)*>) ^ T) ^ Y ==>. z ) & ( for T, X, Y being FinSequence of IT for x, y, z being type of IT st T ==>. y & (X ^ <*x*>) ^ Y ==>. z holds ((X ^ T) ^ <*(y \ x)*>) ^ Y ==>. z ) & ( for X, Y being FinSequence of IT for x, y, z being type of IT st ((X ^ <*x*>) ^ <*y*>) ^ Y ==>. z holds (X ^ <*(x * y)*>) ^ Y ==>. z ) & ( for X, Y being FinSequence of IT for x, y being type of IT st X ==>. x & Y ==>. y holds X ^ Y ==>. x * y ) ) ); registration cluster non empty SynTypes_Calculus-like for typestr ; existence ex b1 being non empty typestr st b1 is SynTypes_Calculus-like proof [:(1 *),1:] c= [:(1 *),1:] ; then reconsider DER = [:(1 *),1:] as non empty Relation of (1 *),1 ; reconsider EM = typestr(# 1,op2,op2,op2,DER #) as non empty typestr ; take EM ; ::_thesis: EM is SynTypes_Calculus-like A1: for x being type of EM for X being FinSequence of EM holds X ==>. x proof let x be type of EM; ::_thesis: for X being FinSequence of EM holds X ==>. x let X be FinSequence of EM; ::_thesis: X ==>. x [X,x] in [:(1 *),1:] ; hence X ==>. x by Def17; ::_thesis: verum end; hence for x being type of EM holds <*x*> ==>. x ; :: according to PRELAMB:def_18 ::_thesis: ( ( for T being FinSequence of EM for x, y being type of EM st T ^ <*y*> ==>. x holds T ==>. x /" y ) & ( for T being FinSequence of EM for x, y being type of EM st <*y*> ^ T ==>. x holds T ==>. y \ x ) & ( for T, X, Y being FinSequence of EM for x, y, z being type of EM st T ==>. y & (X ^ <*x*>) ^ Y ==>. z holds ((X ^ <*(x /" y)*>) ^ T) ^ Y ==>. z ) & ( for T, X, Y being FinSequence of EM for x, y, z being type of EM st T ==>. y & (X ^ <*x*>) ^ Y ==>. z holds ((X ^ T) ^ <*(y \ x)*>) ^ Y ==>. z ) & ( for X, Y being FinSequence of EM for x, y, z being type of EM st ((X ^ <*x*>) ^ <*y*>) ^ Y ==>. z holds (X ^ <*(x * y)*>) ^ Y ==>. z ) & ( for X, Y being FinSequence of EM for x, y being type of EM st X ==>. x & Y ==>. y holds X ^ Y ==>. x * y ) ) thus ( ( for T being FinSequence of EM for x, y being type of EM st T ^ <*y*> ==>. x holds T ==>. x /" y ) & ( for T being FinSequence of EM for x, y being type of EM st <*y*> ^ T ==>. x holds T ==>. y \ x ) & ( for T, X, Y being FinSequence of EM for x, y, z being type of EM st T ==>. y & (X ^ <*x*>) ^ Y ==>. z holds ((X ^ <*(x /" y)*>) ^ T) ^ Y ==>. z ) & ( for T, X, Y being FinSequence of EM for x, y, z being type of EM st T ==>. y & (X ^ <*x*>) ^ Y ==>. z holds ((X ^ T) ^ <*(y \ x)*>) ^ Y ==>. z ) & ( for X, Y being FinSequence of EM for x, y, z being type of EM st ((X ^ <*x*>) ^ <*y*>) ^ Y ==>. z holds (X ^ <*(x * y)*>) ^ Y ==>. z ) & ( for X, Y being FinSequence of EM for x, y being type of EM st X ==>. x & Y ==>. y holds X ^ Y ==>. x * y ) ) by A1; ::_thesis: verum end; end; definition mode SynTypes_Calculus is non empty SynTypes_Calculus-like typestr ; end; deffunc H2( typestr ) -> FinSequence of the carrier of $1 = <*> the carrier of $1; Lm2: for s being SynTypes_Calculus for T, X being FinSequence of s for y, x, z being type of s st T ==>. y & X ^ <*x*> ==>. z holds (X ^ <*(x /" y)*>) ^ T ==>. z proof let s be SynTypes_Calculus; ::_thesis: for T, X being FinSequence of s for y, x, z being type of s st T ==>. y & X ^ <*x*> ==>. z holds (X ^ <*(x /" y)*>) ^ T ==>. z let T, X be FinSequence of s; ::_thesis: for y, x, z being type of s st T ==>. y & X ^ <*x*> ==>. z holds (X ^ <*(x /" y)*>) ^ T ==>. z let y, x, z be type of s; ::_thesis: ( T ==>. y & X ^ <*x*> ==>. z implies (X ^ <*(x /" y)*>) ^ T ==>. z ) assume that A1: T ==>. y and A2: X ^ <*x*> ==>. z ; ::_thesis: (X ^ <*(x /" y)*>) ^ T ==>. z (X ^ <*x*>) ^ H2(s) ==>. z by A2, FINSEQ_1:34; then ((X ^ <*(x /" y)*>) ^ T) ^ H2(s) ==>. z by A1, Def18; hence (X ^ <*(x /" y)*>) ^ T ==>. z by FINSEQ_1:34; ::_thesis: verum end; Lm3: for s being SynTypes_Calculus for T, Y being FinSequence of s for y, x, z being type of s st T ==>. y & <*x*> ^ Y ==>. z holds (<*(x /" y)*> ^ T) ^ Y ==>. z proof let s be SynTypes_Calculus; ::_thesis: for T, Y being FinSequence of s for y, x, z being type of s st T ==>. y & <*x*> ^ Y ==>. z holds (<*(x /" y)*> ^ T) ^ Y ==>. z let T, Y be FinSequence of s; ::_thesis: for y, x, z being type of s st T ==>. y & <*x*> ^ Y ==>. z holds (<*(x /" y)*> ^ T) ^ Y ==>. z let y, x, z be type of s; ::_thesis: ( T ==>. y & <*x*> ^ Y ==>. z implies (<*(x /" y)*> ^ T) ^ Y ==>. z ) assume that A1: T ==>. y and A2: <*x*> ^ Y ==>. z ; ::_thesis: (<*(x /" y)*> ^ T) ^ Y ==>. z (H2(s) ^ <*x*>) ^ Y ==>. z by A2, FINSEQ_1:34; then ((H2(s) ^ <*(x /" y)*>) ^ T) ^ Y ==>. z by A1, Def18; hence (<*(x /" y)*> ^ T) ^ Y ==>. z by FINSEQ_1:34; ::_thesis: verum end; Lm4: for s being SynTypes_Calculus for T being FinSequence of s for y, x, z being type of s st T ==>. y & <*x*> ==>. z holds <*(x /" y)*> ^ T ==>. z proof let s be SynTypes_Calculus; ::_thesis: for T being FinSequence of s for y, x, z being type of s st T ==>. y & <*x*> ==>. z holds <*(x /" y)*> ^ T ==>. z let T be FinSequence of s; ::_thesis: for y, x, z being type of s st T ==>. y & <*x*> ==>. z holds <*(x /" y)*> ^ T ==>. z let y, x, z be type of s; ::_thesis: ( T ==>. y & <*x*> ==>. z implies <*(x /" y)*> ^ T ==>. z ) assume that A1: T ==>. y and A2: <*x*> ==>. z ; ::_thesis: <*(x /" y)*> ^ T ==>. z H2(s) ^ <*x*> ==>. z by A2, FINSEQ_1:34; then (H2(s) ^ <*(x /" y)*>) ^ T ==>. z by A1, Lm2; hence <*(x /" y)*> ^ T ==>. z by FINSEQ_1:34; ::_thesis: verum end; Lm5: for s being SynTypes_Calculus for T, X being FinSequence of s for y, x, z being type of s st T ==>. y & X ^ <*x*> ==>. z holds (X ^ T) ^ <*(y \ x)*> ==>. z proof let s be SynTypes_Calculus; ::_thesis: for T, X being FinSequence of s for y, x, z being type of s st T ==>. y & X ^ <*x*> ==>. z holds (X ^ T) ^ <*(y \ x)*> ==>. z let T, X be FinSequence of s; ::_thesis: for y, x, z being type of s st T ==>. y & X ^ <*x*> ==>. z holds (X ^ T) ^ <*(y \ x)*> ==>. z let y, x, z be type of s; ::_thesis: ( T ==>. y & X ^ <*x*> ==>. z implies (X ^ T) ^ <*(y \ x)*> ==>. z ) assume that A1: T ==>. y and A2: X ^ <*x*> ==>. z ; ::_thesis: (X ^ T) ^ <*(y \ x)*> ==>. z (X ^ <*x*>) ^ H2(s) ==>. z by A2, FINSEQ_1:34; then ((X ^ T) ^ <*(y \ x)*>) ^ H2(s) ==>. z by A1, Def18; hence (X ^ T) ^ <*(y \ x)*> ==>. z by FINSEQ_1:34; ::_thesis: verum end; Lm6: for s being SynTypes_Calculus for T, Y being FinSequence of s for y, x, z being type of s st T ==>. y & <*x*> ^ Y ==>. z holds (T ^ <*(y \ x)*>) ^ Y ==>. z proof let s be SynTypes_Calculus; ::_thesis: for T, Y being FinSequence of s for y, x, z being type of s st T ==>. y & <*x*> ^ Y ==>. z holds (T ^ <*(y \ x)*>) ^ Y ==>. z let T, Y be FinSequence of s; ::_thesis: for y, x, z being type of s st T ==>. y & <*x*> ^ Y ==>. z holds (T ^ <*(y \ x)*>) ^ Y ==>. z let y, x, z be type of s; ::_thesis: ( T ==>. y & <*x*> ^ Y ==>. z implies (T ^ <*(y \ x)*>) ^ Y ==>. z ) assume that A1: T ==>. y and A2: <*x*> ^ Y ==>. z ; ::_thesis: (T ^ <*(y \ x)*>) ^ Y ==>. z (H2(s) ^ <*x*>) ^ Y ==>. z by A2, FINSEQ_1:34; then ((H2(s) ^ T) ^ <*(y \ x)*>) ^ Y ==>. z by A1, Def18; hence (T ^ <*(y \ x)*>) ^ Y ==>. z by FINSEQ_1:34; ::_thesis: verum end; Lm7: for s being SynTypes_Calculus for T being FinSequence of s for y, x, z being type of s st T ==>. y & <*x*> ==>. z holds T ^ <*(y \ x)*> ==>. z proof let s be SynTypes_Calculus; ::_thesis: for T being FinSequence of s for y, x, z being type of s st T ==>. y & <*x*> ==>. z holds T ^ <*(y \ x)*> ==>. z let T be FinSequence of s; ::_thesis: for y, x, z being type of s st T ==>. y & <*x*> ==>. z holds T ^ <*(y \ x)*> ==>. z let y, x, z be type of s; ::_thesis: ( T ==>. y & <*x*> ==>. z implies T ^ <*(y \ x)*> ==>. z ) assume that A1: T ==>. y and A2: <*x*> ==>. z ; ::_thesis: T ^ <*(y \ x)*> ==>. z H2(s) ^ <*x*> ==>. z by A2, FINSEQ_1:34; then (H2(s) ^ T) ^ <*(y \ x)*> ==>. z by A1, Lm5; hence T ^ <*(y \ x)*> ==>. z by FINSEQ_1:34; ::_thesis: verum end; Lm8: for s being SynTypes_Calculus for Y being FinSequence of s for x, y, z being type of s st (<*x*> ^ <*y*>) ^ Y ==>. z holds <*(x * y)*> ^ Y ==>. z proof let s be SynTypes_Calculus; ::_thesis: for Y being FinSequence of s for x, y, z being type of s st (<*x*> ^ <*y*>) ^ Y ==>. z holds <*(x * y)*> ^ Y ==>. z let Y be FinSequence of s; ::_thesis: for x, y, z being type of s st (<*x*> ^ <*y*>) ^ Y ==>. z holds <*(x * y)*> ^ Y ==>. z let x, y, z be type of s; ::_thesis: ( (<*x*> ^ <*y*>) ^ Y ==>. z implies <*(x * y)*> ^ Y ==>. z ) assume (<*x*> ^ <*y*>) ^ Y ==>. z ; ::_thesis: <*(x * y)*> ^ Y ==>. z then ((H2(s) ^ <*x*>) ^ <*y*>) ^ Y ==>. z by FINSEQ_1:34; then (H2(s) ^ <*(x * y)*>) ^ Y ==>. z by Def18; hence <*(x * y)*> ^ Y ==>. z by FINSEQ_1:34; ::_thesis: verum end; Lm9: for s being SynTypes_Calculus for X being FinSequence of s for x, y, z being type of s st (X ^ <*x*>) ^ <*y*> ==>. z holds X ^ <*(x * y)*> ==>. z proof let s be SynTypes_Calculus; ::_thesis: for X being FinSequence of s for x, y, z being type of s st (X ^ <*x*>) ^ <*y*> ==>. z holds X ^ <*(x * y)*> ==>. z let X be FinSequence of s; ::_thesis: for x, y, z being type of s st (X ^ <*x*>) ^ <*y*> ==>. z holds X ^ <*(x * y)*> ==>. z let x, y, z be type of s; ::_thesis: ( (X ^ <*x*>) ^ <*y*> ==>. z implies X ^ <*(x * y)*> ==>. z ) assume (X ^ <*x*>) ^ <*y*> ==>. z ; ::_thesis: X ^ <*(x * y)*> ==>. z then ((X ^ <*x*>) ^ <*y*>) ^ H2(s) ==>. z by FINSEQ_1:34; then (X ^ <*(x * y)*>) ^ H2(s) ==>. z by Def18; hence X ^ <*(x * y)*> ==>. z by FINSEQ_1:34; ::_thesis: verum end; Lm10: for s being SynTypes_Calculus for x, y, z being type of s st <*x*> ^ <*y*> ==>. z holds <*(x * y)*> ==>. z proof let s be SynTypes_Calculus; ::_thesis: for x, y, z being type of s st <*x*> ^ <*y*> ==>. z holds <*(x * y)*> ==>. z let x, y, z be type of s; ::_thesis: ( <*x*> ^ <*y*> ==>. z implies <*(x * y)*> ==>. z ) assume <*x*> ^ <*y*> ==>. z ; ::_thesis: <*(x * y)*> ==>. z then (H2(s) ^ <*x*>) ^ <*y*> ==>. z by FINSEQ_1:34; then H2(s) ^ <*(x * y)*> ==>. z by Lm9; hence <*(x * y)*> ==>. z by FINSEQ_1:34; ::_thesis: verum end; theorem Th12: :: PRELAMB:12 for s being SynTypes_Calculus for x, y being type of s holds ( <*(x /" y)*> ^ <*y*> ==>. x & <*y*> ^ <*(y \ x)*> ==>. x ) proof let s be SynTypes_Calculus; ::_thesis: for x, y being type of s holds ( <*(x /" y)*> ^ <*y*> ==>. x & <*y*> ^ <*(y \ x)*> ==>. x ) let x, y be type of s; ::_thesis: ( <*(x /" y)*> ^ <*y*> ==>. x & <*y*> ^ <*(y \ x)*> ==>. x ) A1: <*x*> ==>. x by Def18; <*y*> ==>. y by Def18; hence ( <*(x /" y)*> ^ <*y*> ==>. x & <*y*> ^ <*(y \ x)*> ==>. x ) by A1, Lm4, Lm7; ::_thesis: verum end; theorem Th13: :: PRELAMB:13 for s being SynTypes_Calculus for x, y being type of s holds ( <*x*> ==>. y /" (x \ y) & <*x*> ==>. (y /" x) \ y ) proof let s be SynTypes_Calculus; ::_thesis: for x, y being type of s holds ( <*x*> ==>. y /" (x \ y) & <*x*> ==>. (y /" x) \ y ) let x, y be type of s; ::_thesis: ( <*x*> ==>. y /" (x \ y) & <*x*> ==>. (y /" x) \ y ) A1: <*(y /" x)*> ^ <*x*> ==>. y by Th12; <*x*> ^ <*(x \ y)*> ==>. y by Th12; hence ( <*x*> ==>. y /" (x \ y) & <*x*> ==>. (y /" x) \ y ) by A1, Def18; ::_thesis: verum end; theorem Th14: :: PRELAMB:14 for s being SynTypes_Calculus for x, y, z being type of s holds <*(x /" y)*> ==>. (x /" z) /" (y /" z) proof let s be SynTypes_Calculus; ::_thesis: for x, y, z being type of s holds <*(x /" y)*> ==>. (x /" z) /" (y /" z) let x, y, z be type of s; ::_thesis: <*(x /" y)*> ==>. (x /" z) /" (y /" z) A1: <*(x /" y)*> ^ <*y*> ==>. x by Th12; <*z*> ==>. z by Def18; then (<*(x /" y)*> ^ <*(y /" z)*>) ^ <*z*> ==>. x by A1, Lm2; then <*(x /" y)*> ^ <*(y /" z)*> ==>. x /" z by Def18; hence <*(x /" y)*> ==>. (x /" z) /" (y /" z) by Def18; ::_thesis: verum end; theorem Th15: :: PRELAMB:15 for s being SynTypes_Calculus for y, x, z being type of s holds <*(y \ x)*> ==>. (z \ y) \ (z \ x) proof let s be SynTypes_Calculus; ::_thesis: for y, x, z being type of s holds <*(y \ x)*> ==>. (z \ y) \ (z \ x) let y, x, z be type of s; ::_thesis: <*(y \ x)*> ==>. (z \ y) \ (z \ x) A1: <*y*> ^ <*(y \ x)*> ==>. x by Th12; <*z*> ==>. z by Def18; then (<*z*> ^ <*(z \ y)*>) ^ <*(y \ x)*> ==>. x by A1, Lm6; then <*z*> ^ (<*(z \ y)*> ^ <*(y \ x)*>) ==>. x by FINSEQ_1:32; then <*(z \ y)*> ^ <*(y \ x)*> ==>. z \ x by Def18; hence <*(y \ x)*> ==>. (z \ y) \ (z \ x) by Def18; ::_thesis: verum end; theorem :: PRELAMB:16 for s being SynTypes_Calculus for x, y, z being type of s st <*x*> ==>. y holds ( <*(x /" z)*> ==>. y /" z & <*(z \ x)*> ==>. z \ y ) proof let s be SynTypes_Calculus; ::_thesis: for x, y, z being type of s st <*x*> ==>. y holds ( <*(x /" z)*> ==>. y /" z & <*(z \ x)*> ==>. z \ y ) let x, y, z be type of s; ::_thesis: ( <*x*> ==>. y implies ( <*(x /" z)*> ==>. y /" z & <*(z \ x)*> ==>. z \ y ) ) assume A1: <*x*> ==>. y ; ::_thesis: ( <*(x /" z)*> ==>. y /" z & <*(z \ x)*> ==>. z \ y ) A2: <*z*> ==>. z by Def18; then A3: <*(x /" z)*> ^ <*z*> ==>. y by A1, Lm4; <*z*> ^ <*(z \ x)*> ==>. y by A1, A2, Lm7; hence ( <*(x /" z)*> ==>. y /" z & <*(z \ x)*> ==>. z \ y ) by A3, Def18; ::_thesis: verum end; theorem Th17: :: PRELAMB:17 for s being SynTypes_Calculus for x, y, z being type of s st <*x*> ==>. y holds ( <*(z /" y)*> ==>. z /" x & <*(y \ z)*> ==>. x \ z ) proof let s be SynTypes_Calculus; ::_thesis: for x, y, z being type of s st <*x*> ==>. y holds ( <*(z /" y)*> ==>. z /" x & <*(y \ z)*> ==>. x \ z ) let x, y, z be type of s; ::_thesis: ( <*x*> ==>. y implies ( <*(z /" y)*> ==>. z /" x & <*(y \ z)*> ==>. x \ z ) ) assume A1: <*x*> ==>. y ; ::_thesis: ( <*(z /" y)*> ==>. z /" x & <*(y \ z)*> ==>. x \ z ) A2: <*z*> ==>. z by Def18; then A3: <*(z /" y)*> ^ <*x*> ==>. z by A1, Lm4; <*x*> ^ <*(y \ z)*> ==>. z by A1, A2, Lm7; hence ( <*(z /" y)*> ==>. z /" x & <*(y \ z)*> ==>. x \ z ) by A3, Def18; ::_thesis: verum end; theorem Th18: :: PRELAMB:18 for s being SynTypes_Calculus for y, x being type of s holds <*(y /" ((y /" x) \ y))*> ==>. y /" x proof let s be SynTypes_Calculus; ::_thesis: for y, x being type of s holds <*(y /" ((y /" x) \ y))*> ==>. y /" x let y, x be type of s; ::_thesis: <*(y /" ((y /" x) \ y))*> ==>. y /" x <*x*> ==>. (y /" x) \ y by Th13; hence <*(y /" ((y /" x) \ y))*> ==>. y /" x by Th17; ::_thesis: verum end; theorem Th19: :: PRELAMB:19 for s being SynTypes_Calculus for x, y being type of s st <*x*> ==>. y holds ( <*> the carrier of s ==>. y /" x & <*> the carrier of s ==>. x \ y ) proof let s be SynTypes_Calculus; ::_thesis: for x, y being type of s st <*x*> ==>. y holds ( <*> the carrier of s ==>. y /" x & <*> the carrier of s ==>. x \ y ) let x, y be type of s; ::_thesis: ( <*x*> ==>. y implies ( <*> the carrier of s ==>. y /" x & <*> the carrier of s ==>. x \ y ) ) assume A1: <*x*> ==>. y ; ::_thesis: ( <*> the carrier of s ==>. y /" x & <*> the carrier of s ==>. x \ y ) A2: H2(s) ^ <*x*> = <*x*> by FINSEQ_1:34; <*x*> ^ H2(s) = <*x*> by FINSEQ_1:34; hence ( <*> the carrier of s ==>. y /" x & <*> the carrier of s ==>. x \ y ) by A1, A2, Def18; ::_thesis: verum end; theorem Th20: :: PRELAMB:20 for s being SynTypes_Calculus for x being type of s holds ( <*> the carrier of s ==>. x /" x & <*> the carrier of s ==>. x \ x ) proof let s be SynTypes_Calculus; ::_thesis: for x being type of s holds ( <*> the carrier of s ==>. x /" x & <*> the carrier of s ==>. x \ x ) let x be type of s; ::_thesis: ( <*> the carrier of s ==>. x /" x & <*> the carrier of s ==>. x \ x ) <*x*> ==>. x by Def18; hence ( <*> the carrier of s ==>. x /" x & <*> the carrier of s ==>. x \ x ) by Th19; ::_thesis: verum end; theorem :: PRELAMB:21 for s being SynTypes_Calculus for y, x being type of s holds ( <*> the carrier of s ==>. (y /" (x \ y)) /" x & <*> the carrier of s ==>. x \ ((y /" x) \ y) ) proof let s be SynTypes_Calculus; ::_thesis: for y, x being type of s holds ( <*> the carrier of s ==>. (y /" (x \ y)) /" x & <*> the carrier of s ==>. x \ ((y /" x) \ y) ) let y, x be type of s; ::_thesis: ( <*> the carrier of s ==>. (y /" (x \ y)) /" x & <*> the carrier of s ==>. x \ ((y /" x) \ y) ) A1: <*x*> ==>. y /" (x \ y) by Th13; <*x*> ==>. (y /" x) \ y by Th13; hence ( <*> the carrier of s ==>. (y /" (x \ y)) /" x & <*> the carrier of s ==>. x \ ((y /" x) \ y) ) by A1, Th19; ::_thesis: verum end; theorem :: PRELAMB:22 for s being SynTypes_Calculus for x, z, y being type of s holds ( <*> the carrier of s ==>. ((x /" z) /" (y /" z)) /" (x /" y) & <*> the carrier of s ==>. (y \ x) \ ((z \ y) \ (z \ x)) ) proof let s be SynTypes_Calculus; ::_thesis: for x, z, y being type of s holds ( <*> the carrier of s ==>. ((x /" z) /" (y /" z)) /" (x /" y) & <*> the carrier of s ==>. (y \ x) \ ((z \ y) \ (z \ x)) ) let x, z, y be type of s; ::_thesis: ( <*> the carrier of s ==>. ((x /" z) /" (y /" z)) /" (x /" y) & <*> the carrier of s ==>. (y \ x) \ ((z \ y) \ (z \ x)) ) A1: <*(x /" y)*> ==>. (x /" z) /" (y /" z) by Th14; <*(y \ x)*> ==>. (z \ y) \ (z \ x) by Th15; hence ( <*> the carrier of s ==>. ((x /" z) /" (y /" z)) /" (x /" y) & <*> the carrier of s ==>. (y \ x) \ ((z \ y) \ (z \ x)) ) by A1, Th19; ::_thesis: verum end; theorem :: PRELAMB:23 for s being SynTypes_Calculus for x, y being type of s st <*> the carrier of s ==>. x holds ( <*> the carrier of s ==>. y /" (y /" x) & <*> the carrier of s ==>. (x \ y) \ y ) proof let s be SynTypes_Calculus; ::_thesis: for x, y being type of s st <*> the carrier of s ==>. x holds ( <*> the carrier of s ==>. y /" (y /" x) & <*> the carrier of s ==>. (x \ y) \ y ) let x, y be type of s; ::_thesis: ( <*> the carrier of s ==>. x implies ( <*> the carrier of s ==>. y /" (y /" x) & <*> the carrier of s ==>. (x \ y) \ y ) ) A1: <*y*> ==>. y by Def18; then A2: H2(s) ^ <*y*> ==>. y by FINSEQ_1:34; A3: <*y*> ^ H2(s) ==>. y by A1, FINSEQ_1:34; assume A4: H2(s) ==>. x ; ::_thesis: ( <*> the carrier of s ==>. y /" (y /" x) & <*> the carrier of s ==>. (x \ y) \ y ) then A5: (H2(s) ^ <*(y /" x)*>) ^ H2(s) ==>. y by A2, Lm2; A6: (H2(s) ^ <*(x \ y)*>) ^ H2(s) ==>. y by A3, A4, Lm6; A7: H2(s) ^ <*(y /" x)*> ==>. y by A5, FINSEQ_1:34; <*(x \ y)*> ^ H2(s) ==>. y by A6, FINSEQ_1:34; hence ( <*> the carrier of s ==>. y /" (y /" x) & <*> the carrier of s ==>. (x \ y) \ y ) by A7, Def18; ::_thesis: verum end; theorem :: PRELAMB:24 for s being SynTypes_Calculus for x, y being type of s holds <*(x /" (y /" y))*> ==>. x proof let s be SynTypes_Calculus; ::_thesis: for x, y being type of s holds <*(x /" (y /" y))*> ==>. x let x, y be type of s; ::_thesis: <*(x /" (y /" y))*> ==>. x <*x*> ==>. x by Def18; then <*(x /" (y /" y))*> ^ H2(s) ==>. x by Lm4, Th20; hence <*(x /" (y /" y))*> ==>. x by FINSEQ_1:34; ::_thesis: verum end; definition let s be SynTypes_Calculus; let x, y be type of s; predx <==>. y means :Def19: :: PRELAMB:def 19 ( <*x*> ==>. y & <*y*> ==>. x ); reflexivity for x being type of s holds ( <*x*> ==>. x & <*x*> ==>. x ) by Def18; symmetry for x, y being type of s st <*x*> ==>. y & <*y*> ==>. x holds ( <*y*> ==>. x & <*x*> ==>. y ) ; end; :: deftheorem Def19 defines <==>. PRELAMB:def_19_:_ for s being SynTypes_Calculus for x, y being type of s holds ( x <==>. y iff ( <*x*> ==>. y & <*y*> ==>. x ) ); theorem :: PRELAMB:25 for s being SynTypes_Calculus for x, y being type of s holds x /" y <==>. x /" ((x /" y) \ x) proof let s be SynTypes_Calculus; ::_thesis: for x, y being type of s holds x /" y <==>. x /" ((x /" y) \ x) let x, y be type of s; ::_thesis: x /" y <==>. x /" ((x /" y) \ x) A1: <*(x /" y)*> ==>. x /" ((x /" y) \ x) by Th13; <*(x /" ((x /" y) \ x))*> ==>. x /" y by Th18; hence x /" y <==>. x /" ((x /" y) \ x) by A1, Def19; ::_thesis: verum end; theorem :: PRELAMB:26 for s being SynTypes_Calculus for x, z, y being type of s holds x /" (z * y) <==>. (x /" y) /" z proof let s be SynTypes_Calculus; ::_thesis: for x, z, y being type of s holds x /" (z * y) <==>. (x /" y) /" z let x, z, y be type of s; ::_thesis: x /" (z * y) <==>. (x /" y) /" z A1: <*z*> ==>. z by Def18; A2: <*y*> ==>. y by Def18; A3: <*x*> ==>. x by Def18; <*z*> ^ <*y*> ==>. z * y by A1, A2, Def18; then <*(x /" (z * y))*> ^ (<*z*> ^ <*y*>) ==>. x by A3, Lm4; then (<*(x /" (z * y))*> ^ <*z*>) ^ <*y*> ==>. x by FINSEQ_1:32; then <*(x /" (z * y))*> ^ <*z*> ==>. x /" y by Def18; then A4: <*(x /" (z * y))*> ==>. (x /" y) /" z by Def18; <*(x /" y)*> ^ <*y*> ==>. x by A2, A3, Lm4; then (<*((x /" y) /" z)*> ^ <*z*>) ^ <*y*> ==>. x by A1, Lm3; then <*((x /" y) /" z)*> ^ <*(z * y)*> ==>. x by Lm9; then <*((x /" y) /" z)*> ==>. x /" (z * y) by Def18; hence x /" (z * y) <==>. (x /" y) /" z by A4, Def19; ::_thesis: verum end; theorem :: PRELAMB:27 for s being SynTypes_Calculus for x, y, z being type of s holds <*(x * (y /" z))*> ==>. (x * y) /" z proof let s be SynTypes_Calculus; ::_thesis: for x, y, z being type of s holds <*(x * (y /" z))*> ==>. (x * y) /" z let x, y, z be type of s; ::_thesis: <*(x * (y /" z))*> ==>. (x * y) /" z A1: <*x*> ==>. x by Def18; <*y*> ==>. y by Def18; then A2: <*x*> ^ <*y*> ==>. x * y by A1, Def18; <*z*> ==>. z by Def18; then (<*x*> ^ <*(y /" z)*>) ^ <*z*> ==>. x * y by A2, Lm2; then <*(x * (y /" z))*> ^ <*z*> ==>. x * y by Lm8; hence <*(x * (y /" z))*> ==>. (x * y) /" z by Def18; ::_thesis: verum end; theorem :: PRELAMB:28 for s being SynTypes_Calculus for x, y being type of s holds ( <*x*> ==>. (x * y) /" y & <*x*> ==>. y \ (y * x) ) proof let s be SynTypes_Calculus; ::_thesis: for x, y being type of s holds ( <*x*> ==>. (x * y) /" y & <*x*> ==>. y \ (y * x) ) let x, y be type of s; ::_thesis: ( <*x*> ==>. (x * y) /" y & <*x*> ==>. y \ (y * x) ) A1: <*x*> ==>. x by Def18; A2: <*y*> ==>. y by Def18; then A3: <*x*> ^ <*y*> ==>. x * y by A1, Def18; <*y*> ^ <*x*> ==>. y * x by A1, A2, Def18; hence ( <*x*> ==>. (x * y) /" y & <*x*> ==>. y \ (y * x) ) by A3, Def18; ::_thesis: verum end; theorem :: PRELAMB:29 for s being SynTypes_Calculus for x, y, z being type of s holds (x * y) * z <==>. x * (y * z) proof let s be SynTypes_Calculus; ::_thesis: for x, y, z being type of s holds (x * y) * z <==>. x * (y * z) let x, y, z be type of s; ::_thesis: (x * y) * z <==>. x * (y * z) A1: <*x*> ==>. x by Def18; A2: <*y*> ==>. y by Def18; A3: <*z*> ==>. z by Def18; <*x*> ^ <*y*> ==>. x * y by A1, A2, Def18; then (<*x*> ^ <*y*>) ^ <*z*> ==>. (x * y) * z by A3, Def18; then <*x*> ^ <*(y * z)*> ==>. (x * y) * z by Lm9; then A4: <*(x * (y * z))*> ==>. (x * y) * z by Lm10; <*y*> ^ <*z*> ==>. y * z by A2, A3, Def18; then <*x*> ^ (<*y*> ^ <*z*>) ==>. x * (y * z) by A1, Def18; then (<*x*> ^ <*y*>) ^ <*z*> ==>. x * (y * z) by FINSEQ_1:32; then <*(x * y)*> ^ <*z*> ==>. x * (y * z) by Lm8; then <*((x * y) * z)*> ==>. x * (y * z) by Lm10; hence (x * y) * z <==>. x * (y * z) by A4, Def19; ::_thesis: verum end;