:: by Wojciech Zielonka

::

:: Received February 13, 1991

:: Copyright (c) 1991-2017 Association of Mizar Users

definition

attr c_{1} is strict ;

struct typealg -> 1-sorted ;

aggr typealg(# carrier, left_quotient, right_quotient, inner_product #) -> typealg ;

sel left_quotient c_{1} -> BinOp of the carrier of c_{1};

sel right_quotient c_{1} -> BinOp of the carrier of c_{1};

sel inner_product c_{1} -> BinOp of the carrier of c_{1};

end;
struct typealg -> 1-sorted ;

aggr typealg(# carrier, left_quotient, right_quotient, inner_product #) -> typealg ;

sel left_quotient c

sel right_quotient c

sel inner_product c

registration
end;

definition

let s be non empty typealg ;

let x, y be type of s;

coherence

the left_quotient of s . (x,y) is type of s ;

coherence

the right_quotient of s . (x,y) is type of s ;

coherence

the inner_product of s . (x,y) is type of s ;

end;
let x, y be type of s;

coherence

the left_quotient of s . (x,y) is type of s ;

coherence

the right_quotient of s . (x,y) is type of s ;

coherence

the inner_product of s . (x,y) is type of s ;

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

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

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

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;
mode PreProof of s is finite DecoratedTree of [:[:( the carrier of s *), the carrier of s:],NAT:];

definition

let s be non empty typealg ;

let Tr be PreProof of s;

let v be Element of dom Tr;

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;
let Tr be PreProof of s;

let v be Element of dom Tr;

attr v 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 ( 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;

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] ) ) ) ) );

;

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

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

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

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

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

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

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

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

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

definition

let s be non empty typealg ;

let Tr be finite DecoratedTree of the carrier of s;

let x be type of s;

end;
let Tr be finite DecoratedTree of the carrier of s;

let x be type of s;

pred Tr 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 ) ) ) ) );

( 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 ) ) ) ) );

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

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

definition

let IT be non empty typealg ;

end;
attr IT is free means :: 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 ) ) );

( ( 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 ) ) );

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

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 ;

ex b_{1} being finite DecoratedTree of the carrier of s st

for Tr being finite DecoratedTree of the carrier of s holds

( Tr represents x iff b_{1} = Tr )
by A1;

uniqueness

for b_{1}, b_{2} being finite DecoratedTree of the carrier of s st ( for Tr being finite DecoratedTree of the carrier of s holds

( Tr represents x iff b_{1} = Tr ) ) & ( for Tr being finite DecoratedTree of the carrier of s holds

( Tr represents x iff b_{2} = Tr ) ) holds

b_{1} = b_{2}
;

end;
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 for Tr being finite DecoratedTree of the carrier of s holds

( Tr represents x iff it = Tr );

ex b

for Tr being finite DecoratedTree of the carrier of s holds

( Tr represents x iff b

uniqueness

for b

( Tr represents x iff b

( Tr represents x iff b

b

:: 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 b_{3} being finite DecoratedTree of the carrier of s holds

( b_{3} = repr_of x iff for Tr being finite DecoratedTree of the carrier of s holds

( Tr represents x iff b_{3} = Tr ) );

for s being non empty typealg

for x being type of s st s is free holds

for b

( b

( Tr represents x iff b

deffunc H

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

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

definition

let s be non empty typealg ;

ex b_{1} being PreProof of s st

( dom b_{1} is finite & ( for v being Element of dom b_{1} holds v is correct ) )

end;
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 ( dom it is finite & ( for v being Element of dom it holds v is correct ) );

ex b

( dom b

proof end;

:: deftheorem Def12 defines Proof PRELAMB:def 12 :

for s being non empty typealg

for b_{2} being PreProof of s holds

( b_{2} is Proof of s iff ( dom b_{2} is finite & ( for v being Element of dom b_{2} holds v is correct ) ) );

for s being non empty typealg

for b

( b

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

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 )

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]

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] )

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] )

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] )

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] )

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] )

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] )

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] )

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

not not (p . v) `2 = 0 & ... & not (p . v) `2 = 7

for p being Proof of s

for v being Element of dom p holds

not not (p . v) `2 = 0 & ... & not (p . v) `2 = 7

proof 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 );

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 ;

ex b_{1} being Function of the carrier of s,NAT st

for x being type of s holds b_{1} . x = card (dom (repr_of x))

for b_{1}, b_{2} being Function of the carrier of s,NAT st ( for x being type of s holds b_{1} . x = card (dom (repr_of x)) ) & ( for x being type of s holds b_{2} . x = card (dom (repr_of x)) ) holds

b_{1} = b_{2}

end;
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 for x being type of s holds it . x = card (dom (repr_of x));

ex b

for x being type of s holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines size_w.r.t. PRELAMB:def 14 :

for s being non empty typealg

for b_{2} being Function of the carrier of s,NAT holds

( b_{2} = size_w.r.t. s iff for x being type of s holds b_{2} . x = card (dom (repr_of x)) );

for s being non empty typealg

for b

( b

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

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

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;

( ( (p . {}) `2 = 7 implies ex b_{1} 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] & b_{1} = (((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 b_{1} being Nat st b_{1} = 0 ) )

for b_{1}, b_{2} 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] & b_{1} = (((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] & b_{2} = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) implies b_{1} = b_{2} ) & ( not (p . {}) `2 = 7 & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) )

for b_{1} being Nat holds verum
;

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

( ( (p . {}) `2 = 7 implies ex b

( (p . {}) `1 = [((X ^ T) ^ Y),z] & (p . <*0*>) `1 = [T,y] & (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] & b

proof end;

uniqueness for b

( ( (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] & b

( (p . {}) `1 = [((X ^ T) ^ Y),z] & (p . <*0*>) `1 = [T,y] & (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] & b

proof end;

consistency for b

:: deftheorem defines cutdeg PRELAMB:def 15 :

for s being non empty typealg

for p being Proof of s

for b_{3} being Nat holds

( ( (p . {}) `2 = 7 implies ( b_{3} = 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] & b_{3} = (((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 ( b_{3} = cutdeg p iff b_{3} = 0 ) ) );

for s being non empty typealg

for p being Proof of s

for b

( ( (p . {}) `2 = 7 implies ( b

( (p . {}) `1 = [((X ^ T) ^ Y),z] & (p . <*0*>) `1 = [T,y] & (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] & b

definition

let s be non empty typealg ;

let A be non empty set ;

ex b_{1} being Function of the carrier of s,(bool (A *)) st

for x, y being type of s holds

( b_{1} . (x * y) = { (a ^ b) where a, b is Element of A * : ( a in b_{1} . x & b in b_{1} . y ) } & b_{1} . (x /" y) = { a1 where a1 is Element of A * : for b being Element of A * st b in b_{1} . y holds

a1 ^ b in b_{1} . x } & b_{1} . (y \ x) = { a2 where a2 is Element of A * : for b being Element of A * st b in b_{1} . y holds

b ^ a2 in b_{1} . x } )

end;
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 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 } );

ex b

for x, y being type of s holds

( b

a1 ^ b in b

b ^ a2 in b

proof end;

:: deftheorem defines Model PRELAMB:def 16 :

for s being non empty typealg

for A being non empty set

for b_{3} being Function of the carrier of s,(bool (A *)) holds

( b_{3} is Model of s,A iff for x, y being type of s holds

( b_{3} . (x * y) = { (a ^ b) where a, b is Element of A * : ( a in b_{3} . x & b in b_{3} . y ) } & b_{3} . (x /" y) = { a1 where a1 is Element of A * : for b being Element of A * st b in b_{3} . y holds

a1 ^ b in b_{3} . x } & b_{3} . (y \ x) = { a2 where a2 is Element of A * : for b being Element of A * st b in b_{3} . y holds

b ^ a2 in b_{3} . x } ) );

for s being non empty typealg

for A being non empty set

for b

( b

( b

a1 ^ b in b

b ^ a2 in b

:: Axioms, rules, and some of their consequences

definition

attr c_{1} is strict ;

struct typestr -> typealg ;

aggr typestr(# carrier, left_quotient, right_quotient, inner_product, derivability #) -> typestr ;

sel derivability c_{1} -> Relation of ( the carrier of c_{1} *), the carrier of c_{1};

end;
struct typestr -> typealg ;

aggr typestr(# carrier, left_quotient, right_quotient, inner_product, derivability #) -> typestr ;

sel derivability c

registration
end;

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

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 ;

end;
attr IT 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 ) );

( ( 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 ) );

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

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

deffunc H

Lm2: for s being SynTypes_Calculus

for T, X being FinSequence of s

for x, y, 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 x, y, 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 x, y, 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 x, y, 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 x, y, 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 x, y, 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 )

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 )

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)

for x, y, z being type of s holds <*(x /" y)*> ==>. (x /" z) /" (y /" z)

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 )

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 )

for x, y, z being type of s st <*x*> ==>. y holds

( <*(z /" y)*> ==>. z /" x & <*(y \ z)*> ==>. x \ z )

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 )

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 )

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 x, y being type of s holds

( <*> the carrier of s ==>. (y /" (x \ y)) /" x & <*> the carrier of s ==>. x \ ((y /" x) \ y) )

for x, y 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, y, z 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)) )

for x, y, z 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 )

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;

definition

let s be SynTypes_Calculus;

let x, y be type of s;

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;
let x, y be type of s;

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

:: deftheorem defines <==>. PRELAMB:def 19 :

for s being SynTypes_Calculus

for x, y being type of s holds

( x <==>. y iff ( <*x*> ==>. y & <*y*> ==>. x ) );

for s being SynTypes_Calculus

for x, y being type of s holds

( x <==>. y iff ( <*x*> ==>. y & <*y*> ==>. x ) );

theorem :: PRELAMB:25

theorem :: PRELAMB:27

for s being SynTypes_Calculus

for x, y, z being type of s holds <*(x * (y /" z))*> ==>. (x * y) /" z

for x, y, z being type of s holds <*(x * (y /" z))*> ==>. (x * y) /" z

proof 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) )

for x, y being type of s holds

( <*x*> ==>. (x * y) /" y & <*x*> ==>. y \ (y * x) )

proof end;