:: Preliminaries to the Lambek Calculus :: by Wojciech Zielonka :: :: Received February 13, 1991 :: Copyright (c) 1991-2012 Association of Mizar Users 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 ) proofend; 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 proofend; 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 proofend; 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:] proofend; 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 ) ) proofend; 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 proofend; 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 ) proofend; 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] proofend; 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] ) proofend; 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] ) proofend; 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] ) proofend; 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] ) proofend; 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] ) proofend; 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] ) proofend; 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] ) proofend; 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 ) proofend; 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)) proofend; 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 proofend; 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 proofend; 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 proofend; 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 ) ) proofend; 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 ) ) proofend; 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 } ) proofend; 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 } ) ); :: Axioms, rules, and some of their consequences 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 ) proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; Lm10: for s being SynTypes_Calculus for x, y, z being type of s st <*x*> ^ <*y*> ==>. z holds <*(x * y)*> ==>. z proofend; 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 ) proofend; 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 ) proofend; theorem Th14: :: PRELAMB:14 for s being SynTypes_Calculus for x, y, z being type of s holds <*(x /" y)*> ==>. (x /" z) /" (y /" z) proofend; theorem Th15: :: PRELAMB:15 for s being SynTypes_Calculus for y, x, z being type of s holds <*(y \ x)*> ==>. (z \ y) \ (z \ x) proofend; 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 ) proofend; 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 ) proofend; theorem Th18: :: PRELAMB:18 for s being SynTypes_Calculus for y, x being type of s holds <*(y /" ((y /" x) \ y))*> ==>. y /" x proofend; 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 ) proofend; 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 ) proofend; 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) ) proofend; 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)) ) proofend; 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 ) proofend; theorem :: PRELAMB:24 for s being SynTypes_Calculus for x, y being type of s holds <*(x /" (y /" y))*> ==>. x proofend; 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) proofend; theorem :: PRELAMB:26 for s being SynTypes_Calculus for x, z, y being type of s holds x /" (z * y) <==>. (x /" y) /" z proofend; theorem :: PRELAMB:27 for s being SynTypes_Calculus for x, y, z being type of s holds <*(x * (y /" z))*> ==>. (x * y) /" z proofend; theorem :: PRELAMB:28 for s being SynTypes_Calculus for x, y being type of s holds ( <*x*> ==>. (x * y) /" y & <*x*> ==>. y \ (y * x) ) proofend; theorem :: PRELAMB:29 for s being SynTypes_Calculus for x, y, z being type of s holds (x * y) * z <==>. x * (y * z) proofend;