:: 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;