:: Preliminaries to the Lambek Calculus
:: by Wojciech Zielonka
::
:: Received February 13, 1991
:: Copyright (c) 1991-2011 Association of Mizar Users


begin

definition
attr c1 is strict ;
struct typealg -> 1-sorted ;
aggr typealg(# 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 typealg ;
existence
ex b1 being typealg st
( not b1 is empty & b1 is strict )
proof 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;
func x \ 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 ;
func x /" 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 ;
func x * 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;
canceled;
attr v is correct means :Def5: :: PRELAMB:def 5
( 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 PRELAMB:def 4 :
canceled;

:: deftheorem Def5 defines correct PRELAMB:def 5 :
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;
attr IT is left means :: PRELAMB:def 6
 ex x, y being type of s st IT = x \ y;
attr IT is right means :: PRELAMB:def 7
 ex x, y being type of s st IT = x /" y;
attr IT is middle means :: PRELAMB:def 8
 ex x, y being type of s st IT = x * y;
end;

:: deftheorem defines left PRELAMB:def 6 :
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 7 :
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 8 :
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;
attr IT is primitive means :: PRELAMB:def 9
( not IT is left & not IT is right & not IT is middle );
end;

:: deftheorem defines primitive PRELAMB:def 9 :
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 func Tr . v -> type of s;
coherence
Tr . v is type of s
proof 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;
pred Tr represents x means :: PRELAMB:def 10
( 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 10 :
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 ;
attr IT is free means :Def11: :: PRELAMB:def 11
( ( 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 Def11 defines free PRELAMB:def 11 :
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 12
 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, Def11;
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 end;
end;

:: deftheorem defines repr_of PRELAMB:def 12 :
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 end;
end;

definition
let s be non empty typealg ;
mode Proof of s -> PreProof of s means :Def13: :: PRELAMB:def 13
( 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 end;
end;

:: deftheorem Def13 defines Proof PRELAMB:def 13 :
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 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 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 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 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 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 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 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 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 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 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 end;

definition
let s be non empty typealg ;
let IT be PreProof of s;
attr IT is cut-free means :: PRELAMB:def 14
 for v being Element of dom IT holds (IT . v) `2 <> 7;
end;

:: deftheorem defines cut-free PRELAMB:def 14 :
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 15
 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 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 end;
end;

:: deftheorem defines size_w.r.t. PRELAMB:def 15 :
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 func f * T -> FinSequence of REAL ;
coherence
T * f is FinSequence of REAL
proof 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 end;

definition
let s be non empty typealg ;
let p be Proof of s;
func cutdeg p -> Nat means :: PRELAMB:def 16
 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 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 end;
consistency
for b1 being Nat holds verum ;
end;

:: deftheorem defines cutdeg PRELAMB:def 16 :
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 17
 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 end;
end;

:: deftheorem defines Model PRELAMB:def 17 :
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
attr c1 is strict ;
struct typestr -> typealg ;
aggr typestr(# 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 typestr ;
existence
ex b1 being typestr st
( not b1 is empty & b1 is strict )
proof end;
end;

definition
let s be non empty typestr ;
let f be FinSequence of s;
let x be type of s;
pred f ==>. x means :Def18: :: PRELAMB:def 18
[f,x] in the derivability of s;
end;

:: deftheorem Def18 defines ==>. PRELAMB:def 18 :
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 ;
attr IT is SynTypes_Calculus-like means :Def19: :: PRELAMB:def 19
( ( 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 Def19 defines SynTypes_Calculus-like PRELAMB:def 19 :
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 typestr ;
existence
ex b1 being non empty typestr st b1 is SynTypes_Calculus-like
proof 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 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 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 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 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 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 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 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 end;

Lm10: for s being SynTypes_Calculus
for x, y, z being type of s st <*x*> ^ <*y*> ==>. z holds
<*(x * y)*> ==>. z
proof 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 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 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 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 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 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 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 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 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 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 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 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 end;

theorem :: PRELAMB:24
for s being SynTypes_Calculus
for x, y being type of s holds <*(x /" (y /" y))*> ==>. x
proof end;

definition
let s be SynTypes_Calculus;
let x, y be type of s;
pred x <==>. y means :Def20: :: PRELAMB:def 20
( <*x*> ==>. y & <*y*> ==>. x );
reflexivity
for x being type of s holds
( <*x*> ==>. x & <*x*> ==>. x ) by Def19;
symmetry
for x, y being type of s st <*x*> ==>. y & <*y*> ==>. x holds
( <*y*> ==>. x & <*x*> ==>. y ) ;
end;

:: deftheorem Def20 defines <==>. PRELAMB:def 20 :
for s being SynTypes_Calculus
for x, y being type of s holds
( x <==>. y iff ( <*x*> ==>. y & <*y*> ==>. x ) );

theorem :: PRELAMB:25
canceled;

theorem :: PRELAMB:26
for s being SynTypes_Calculus
for x, y being type of s holds x /" y <==>. x /" ((x /" y) \ x)
proof end;

theorem :: PRELAMB:27
for s being SynTypes_Calculus
for x, z, y being type of s holds x /" (z * y) <==>. (x /" y) /" z
proof end;

theorem :: PRELAMB:28
for s being SynTypes_Calculus
for x, y, z being type of s holds <*(x * (y /" z))*> ==>. (x * y) /" z
proof end;

theorem :: PRELAMB:29
for s being SynTypes_Calculus
for x, y being type of s holds
( <*x*> ==>. (x * y) /" y & <*x*> ==>. y \ (y * x) )
proof end;

theorem :: PRELAMB:30
for s being SynTypes_Calculus
for x, y, z being type of s holds (x * y) * z <==>. x * (y * z)
proof end;