:: PRELAMB semantic presentation

definition
attr a1 is strict;
struct typealg -> 1-sorted ;
aggr typealg(# carrier, left_quotient, right_quotient, inner_product #) -> typealg ;
sel left_quotient c1 -> BinOp of the carrier of a1;
sel right_quotient c1 -> BinOp of the carrier of a1;
sel inner_product c1 -> BinOp of the carrier of a1;
end;

registration
cluster non empty strict typealg ;
existence
ex b1 being typealg st
( not b1 is empty & b1 is strict )
proof end;
end;

definition
let c1 be non empty typealg ;
mode type of a1 is Element of a1;
end;

definition
let c1 be non empty typealg ;
let c2, c3 be type of c1;
func c2 \ c3 -> type of a1 equals :: PRELAMB:def 1
the left_quotient of a1 . a2,a3;
correctness
coherence
the left_quotient of c1 . c2,c3 is type of c1;
;
func c2 /" c3 -> type of a1 equals :: PRELAMB:def 2
the right_quotient of a1 . a2,a3;
correctness
coherence
the right_quotient of c1 . c2,c3 is type of c1;
;
func c2 * c3 -> type of a1 equals :: PRELAMB:def 3
the inner_product of a1 . a2,a3;
correctness
coherence
the inner_product of c1 . c2,c3 is type of c1;
;
end;

:: deftheorem Def1 defines \ PRELAMB:def 1 :
for b1 being non empty typealg
for b2, b3 being type of b1 holds b2 \ b3 = the left_quotient of b1 . b2,b3;

:: deftheorem Def2 defines /" PRELAMB:def 2 :
for b1 being non empty typealg
for b2, b3 being type of b1 holds b2 /" b3 = the right_quotient of b1 . b2,b3;

:: deftheorem Def3 defines * PRELAMB:def 3 :
for b1 being non empty typealg
for b2, b3 being type of b1 holds b2 * b3 = the inner_product of b1 . b2,b3;

Lemma1: for b1 being Function holds (pr1 (dom b1),(rng b1)) .: b1 = dom b1
proof end;

Lemma2: for b1 being Function holds
( dom b1 is finite iff b1 is finite )
proof end;

definition
let c1 be non empty typealg ;
mode PreProof of a1 is finite DecoratedTree of [:[:(the carrier of a1 * ),the carrier of a1:],NAT :];
end;

definition
let c1 be non empty typealg ;
let c2 be PreProof of c1;
let c3 be Element of dom c2;
canceled;
attr a3 is correct means :Def5: :: PRELAMB:def 5
( branchdeg a3 = 0 & ex b1 being type of a1 st (a2 . a3) `1 = [<*b1*>,b1] ) if (a2 . a3) `2 = 0
( branchdeg a3 = 1 & ex b1 being FinSequence of the carrier of a1ex b2, b3 being type of a1 st
( (a2 . a3) `1 = [b1,(b2 /" b3)] & (a2 . (a3 ^ <*0*>)) `1 = [(b1 ^ <*b3*>),b2] ) ) if (a2 . a3) `2 = 1
( branchdeg a3 = 1 & ex b1 being FinSequence of the carrier of a1ex b2, b3 being type of a1 st
( (a2 . a3) `1 = [b1,(b3 \ b2)] & (a2 . (a3 ^ <*0*>)) `1 = [(<*b3*> ^ b1),b2] ) ) if (a2 . a3) `2 = 2
( branchdeg a3 = 2 & ex b1, b2, b3 being FinSequence of the carrier of a1ex b4, b5, b6 being type of a1 st
( (a2 . a3) `1 = [(((b2 ^ <*(b4 /" b5)*>) ^ b1) ^ b3),b6] & (a2 . (a3 ^ <*0*>)) `1 = [b1,b5] & (a2 . (a3 ^ <*1*>)) `1 = [((b2 ^ <*b4*>) ^ b3),b6] ) ) if (a2 . a3) `2 = 3
( branchdeg a3 = 2 & ex b1, b2, b3 being FinSequence of the carrier of a1ex b4, b5, b6 being type of a1 st
( (a2 . a3) `1 = [(((b2 ^ b1) ^ <*(b5 \ b4)*>) ^ b3),b6] & (a2 . (a3 ^ <*0*>)) `1 = [b1,b5] & (a2 . (a3 ^ <*1*>)) `1 = [((b2 ^ <*b4*>) ^ b3),b6] ) ) if (a2 . a3) `2 = 4
for b1 being type of a1 holds
( branchdeg a3 = 1 & ex b2 being FinSequence of the carrier of a1ex b3, b4 being type of a1ex b5 being FinSequence of the carrier of a1 st
( (a2 . a3) `1 = [((b2 ^ <*(b3 * b4)*>) ^ b5),b1] & (a2 . (a3 ^ <*0*>)) `1 = [(((b2 ^ <*b3*>) ^ <*b4*>) ^ b5),b1] ) ) if (a2 . a3) `2 = 5
( branchdeg a3 = 2 & ex b1, b2 being FinSequence of the carrier of a1ex b3, b4 being type of a1 st
( (a2 . a3) `1 = [(b1 ^ b2),(b3 * b4)] & (a2 . (a3 ^ <*0*>)) `1 = [b1,b3] & (a2 . (a3 ^ <*1*>)) `1 = [b2,b4] ) ) if (a2 . a3) `2 = 6
( branchdeg a3 = 2 & ex b1, b2, b3 being FinSequence of the carrier of a1ex b4, b5 being type of a1 st
( (a2 . a3) `1 = [((b2 ^ b1) ^ b3),b5] & (a2 . (a3 ^ <*0*>)) `1 = [b1,b4] & (a2 . (a3 ^ <*1*>)) `1 = [((b2 ^ <*b4*>) ^ b3),b5] ) ) if (a2 . a3) `2 = 7
otherwise contradiction;
correctness
consistency
( ( (c2 . c3) `2 = 0 & (c2 . c3) `2 = 1 implies ( branchdeg c3 = 0 & ex b1 being type of c1 st (c2 . c3) `1 = [<*b1*>,b1] iff ( branchdeg c3 = 1 & ex b1 being FinSequence of the carrier of c1ex b2, b3 being type of c1 st
( (c2 . c3) `1 = [b1,(b2 /" b3)] & (c2 . (c3 ^ <*0*>)) `1 = [(b1 ^ <*b3*>),b2] ) ) ) ) & ( (c2 . c3) `2 = 0 & (c2 . c3) `2 = 2 implies ( branchdeg c3 = 0 & ex b1 being type of c1 st (c2 . c3) `1 = [<*b1*>,b1] iff ( branchdeg c3 = 1 & ex b1 being FinSequence of the carrier of c1ex b2, b3 being type of c1 st
( (c2 . c3) `1 = [b1,(b3 \ b2)] & (c2 . (c3 ^ <*0*>)) `1 = [(<*b3*> ^ b1),b2] ) ) ) ) & ( (c2 . c3) `2 = 0 & (c2 . c3) `2 = 3 implies ( branchdeg c3 = 0 & ex b1 being type of c1 st (c2 . c3) `1 = [<*b1*>,b1] iff ( branchdeg c3 = 2 & ex b1, b2, b3 being FinSequence of the carrier of c1ex b4, b5, b6 being type of c1 st
( (c2 . c3) `1 = [(((b2 ^ <*(b4 /" b5)*>) ^ b1) ^ b3),b6] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b5] & (c2 . (c3 ^ <*1*>)) `1 = [((b2 ^ <*b4*>) ^ b3),b6] ) ) ) ) & ( (c2 . c3) `2 = 0 & (c2 . c3) `2 = 4 implies ( branchdeg c3 = 0 & ex b1 being type of c1 st (c2 . c3) `1 = [<*b1*>,b1] iff ( branchdeg c3 = 2 & ex b1, b2, b3 being FinSequence of the carrier of c1ex b4, b5, b6 being type of c1 st
( (c2 . c3) `1 = [(((b2 ^ b1) ^ <*(b5 \ b4)*>) ^ b3),b6] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b5] & (c2 . (c3 ^ <*1*>)) `1 = [((b2 ^ <*b4*>) ^ b3),b6] ) ) ) ) & ( (c2 . c3) `2 = 0 & (c2 . c3) `2 = 5 implies ( ( branchdeg c3 = 0 & ex b1 being type of c1 st (c2 . c3) `1 = [<*b1*>,b1] ) iff for b1 being type of c1 holds
( branchdeg c3 = 1 & ex b2 being FinSequence of the carrier of c1ex b3, b4 being type of c1ex b5 being FinSequence of the carrier of c1 st
( (c2 . c3) `1 = [((b2 ^ <*(b3 * b4)*>) ^ b5),b1] & (c2 . (c3 ^ <*0*>)) `1 = [(((b2 ^ <*b3*>) ^ <*b4*>) ^ b5),b1] ) ) ) ) & ( (c2 . c3) `2 = 0 & (c2 . c3) `2 = 6 implies ( branchdeg c3 = 0 & ex b1 being type of c1 st (c2 . c3) `1 = [<*b1*>,b1] iff ( branchdeg c3 = 2 & ex b1, b2 being FinSequence of the carrier of c1ex b3, b4 being type of c1 st
( (c2 . c3) `1 = [(b1 ^ b2),(b3 * b4)] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b3] & (c2 . (c3 ^ <*1*>)) `1 = [b2,b4] ) ) ) ) & ( (c2 . c3) `2 = 0 & (c2 . c3) `2 = 7 implies ( branchdeg c3 = 0 & ex b1 being type of c1 st (c2 . c3) `1 = [<*b1*>,b1] iff ( branchdeg c3 = 2 & ex b1, b2, b3 being FinSequence of the carrier of c1ex b4, b5 being type of c1 st
( (c2 . c3) `1 = [((b2 ^ b1) ^ b3),b5] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b4] & (c2 . (c3 ^ <*1*>)) `1 = [((b2 ^ <*b4*>) ^ b3),b5] ) ) ) ) & ( (c2 . c3) `2 = 1 & (c2 . c3) `2 = 2 implies ( branchdeg c3 = 1 & ex b1 being FinSequence of the carrier of c1ex b2, b3 being type of c1 st
( (c2 . c3) `1 = [b1,(b2 /" b3)] & (c2 . (c3 ^ <*0*>)) `1 = [(b1 ^ <*b3*>),b2] ) iff ( branchdeg c3 = 1 & ex b1 being FinSequence of the carrier of c1ex b2, b3 being type of c1 st
( (c2 . c3) `1 = [b1,(b3 \ b2)] & (c2 . (c3 ^ <*0*>)) `1 = [(<*b3*> ^ b1),b2] ) ) ) ) & ( (c2 . c3) `2 = 1 & (c2 . c3) `2 = 3 implies ( branchdeg c3 = 1 & ex b1 being FinSequence of the carrier of c1ex b2, b3 being type of c1 st
( (c2 . c3) `1 = [b1,(b2 /" b3)] & (c2 . (c3 ^ <*0*>)) `1 = [(b1 ^ <*b3*>),b2] ) iff ( branchdeg c3 = 2 & ex b1, b2, b3 being FinSequence of the carrier of c1ex b4, b5, b6 being type of c1 st
( (c2 . c3) `1 = [(((b2 ^ <*(b4 /" b5)*>) ^ b1) ^ b3),b6] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b5] & (c2 . (c3 ^ <*1*>)) `1 = [((b2 ^ <*b4*>) ^ b3),b6] ) ) ) ) & ( (c2 . c3) `2 = 1 & (c2 . c3) `2 = 4 implies ( branchdeg c3 = 1 & ex b1 being FinSequence of the carrier of c1ex b2, b3 being type of c1 st
( (c2 . c3) `1 = [b1,(b2 /" b3)] & (c2 . (c3 ^ <*0*>)) `1 = [(b1 ^ <*b3*>),b2] ) iff ( branchdeg c3 = 2 & ex b1, b2, b3 being FinSequence of the carrier of c1ex b4, b5, b6 being type of c1 st
( (c2 . c3) `1 = [(((b2 ^ b1) ^ <*(b5 \ b4)*>) ^ b3),b6] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b5] & (c2 . (c3 ^ <*1*>)) `1 = [((b2 ^ <*b4*>) ^ b3),b6] ) ) ) ) & ( (c2 . c3) `2 = 1 & (c2 . c3) `2 = 5 implies ( ( branchdeg c3 = 1 & ex b1 being FinSequence of the carrier of c1ex b2, b3 being type of c1 st
( (c2 . c3) `1 = [b1,(b2 /" b3)] & (c2 . (c3 ^ <*0*>)) `1 = [(b1 ^ <*b3*>),b2] ) ) iff for b1 being type of c1 holds
( branchdeg c3 = 1 & ex b2 being FinSequence of the carrier of c1ex b3, b4 being type of c1ex b5 being FinSequence of the carrier of c1 st
( (c2 . c3) `1 = [((b2 ^ <*(b3 * b4)*>) ^ b5),b1] & (c2 . (c3 ^ <*0*>)) `1 = [(((b2 ^ <*b3*>) ^ <*b4*>) ^ b5),b1] ) ) ) ) & ( (c2 . c3) `2 = 1 & (c2 . c3) `2 = 6 implies ( branchdeg c3 = 1 & ex b1 being FinSequence of the carrier of c1ex b2, b3 being type of c1 st
( (c2 . c3) `1 = [b1,(b2 /" b3)] & (c2 . (c3 ^ <*0*>)) `1 = [(b1 ^ <*b3*>),b2] ) iff ( branchdeg c3 = 2 & ex b1, b2 being FinSequence of the carrier of c1ex b3, b4 being type of c1 st
( (c2 . c3) `1 = [(b1 ^ b2),(b3 * b4)] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b3] & (c2 . (c3 ^ <*1*>)) `1 = [b2,b4] ) ) ) ) & ( (c2 . c3) `2 = 1 & (c2 . c3) `2 = 7 implies ( branchdeg c3 = 1 & ex b1 being FinSequence of the carrier of c1ex b2, b3 being type of c1 st
( (c2 . c3) `1 = [b1,(b2 /" b3)] & (c2 . (c3 ^ <*0*>)) `1 = [(b1 ^ <*b3*>),b2] ) iff ( branchdeg c3 = 2 & ex b1, b2, b3 being FinSequence of the carrier of c1ex b4, b5 being type of c1 st
( (c2 . c3) `1 = [((b2 ^ b1) ^ b3),b5] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b4] & (c2 . (c3 ^ <*1*>)) `1 = [((b2 ^ <*b4*>) ^ b3),b5] ) ) ) ) & ( (c2 . c3) `2 = 2 & (c2 . c3) `2 = 3 implies ( branchdeg c3 = 1 & ex b1 being FinSequence of the carrier of c1ex b2, b3 being type of c1 st
( (c2 . c3) `1 = [b1,(b3 \ b2)] & (c2 . (c3 ^ <*0*>)) `1 = [(<*b3*> ^ b1),b2] ) iff ( branchdeg c3 = 2 & ex b1, b2, b3 being FinSequence of the carrier of c1ex b4, b5, b6 being type of c1 st
( (c2 . c3) `1 = [(((b2 ^ <*(b4 /" b5)*>) ^ b1) ^ b3),b6] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b5] & (c2 . (c3 ^ <*1*>)) `1 = [((b2 ^ <*b4*>) ^ b3),b6] ) ) ) ) & ( (c2 . c3) `2 = 2 & (c2 . c3) `2 = 4 implies ( branchdeg c3 = 1 & ex b1 being FinSequence of the carrier of c1ex b2, b3 being type of c1 st
( (c2 . c3) `1 = [b1,(b3 \ b2)] & (c2 . (c3 ^ <*0*>)) `1 = [(<*b3*> ^ b1),b2] ) iff ( branchdeg c3 = 2 & ex b1, b2, b3 being FinSequence of the carrier of c1ex b4, b5, b6 being type of c1 st
( (c2 . c3) `1 = [(((b2 ^ b1) ^ <*(b5 \ b4)*>) ^ b3),b6] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b5] & (c2 . (c3 ^ <*1*>)) `1 = [((b2 ^ <*b4*>) ^ b3),b6] ) ) ) ) & ( (c2 . c3) `2 = 2 & (c2 . c3) `2 = 5 implies ( ( branchdeg c3 = 1 & ex b1 being FinSequence of the carrier of c1ex b2, b3 being type of c1 st
( (c2 . c3) `1 = [b1,(b3 \ b2)] & (c2 . (c3 ^ <*0*>)) `1 = [(<*b3*> ^ b1),b2] ) ) iff for b1 being type of c1 holds
( branchdeg c3 = 1 & ex b2 being FinSequence of the carrier of c1ex b3, b4 being type of c1ex b5 being FinSequence of the carrier of c1 st
( (c2 . c3) `1 = [((b2 ^ <*(b3 * b4)*>) ^ b5),b1] & (c2 . (c3 ^ <*0*>)) `1 = [(((b2 ^ <*b3*>) ^ <*b4*>) ^ b5),b1] ) ) ) ) & ( (c2 . c3) `2 = 2 & (c2 . c3) `2 = 6 implies ( branchdeg c3 = 1 & ex b1 being FinSequence of the carrier of c1ex b2, b3 being type of c1 st
( (c2 . c3) `1 = [b1,(b3 \ b2)] & (c2 . (c3 ^ <*0*>)) `1 = [(<*b3*> ^ b1),b2] ) iff ( branchdeg c3 = 2 & ex b1, b2 being FinSequence of the carrier of c1ex b3, b4 being type of c1 st
( (c2 . c3) `1 = [(b1 ^ b2),(b3 * b4)] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b3] & (c2 . (c3 ^ <*1*>)) `1 = [b2,b4] ) ) ) ) & ( (c2 . c3) `2 = 2 & (c2 . c3) `2 = 7 implies ( branchdeg c3 = 1 & ex b1 being FinSequence of the carrier of c1ex b2, b3 being type of c1 st
( (c2 . c3) `1 = [b1,(b3 \ b2)] & (c2 . (c3 ^ <*0*>)) `1 = [(<*b3*> ^ b1),b2] ) iff ( branchdeg c3 = 2 & ex b1, b2, b3 being FinSequence of the carrier of c1ex b4, b5 being type of c1 st
( (c2 . c3) `1 = [((b2 ^ b1) ^ b3),b5] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b4] & (c2 . (c3 ^ <*1*>)) `1 = [((b2 ^ <*b4*>) ^ b3),b5] ) ) ) ) & ( (c2 . c3) `2 = 3 & (c2 . c3) `2 = 4 implies ( branchdeg c3 = 2 & ex b1, b2, b3 being FinSequence of the carrier of c1ex b4, b5, b6 being type of c1 st
( (c2 . c3) `1 = [(((b2 ^ <*(b4 /" b5)*>) ^ b1) ^ b3),b6] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b5] & (c2 . (c3 ^ <*1*>)) `1 = [((b2 ^ <*b4*>) ^ b3),b6] ) iff ( branchdeg c3 = 2 & ex b1, b2, b3 being FinSequence of the carrier of c1ex b4, b5, b6 being type of c1 st
( (c2 . c3) `1 = [(((b2 ^ b1) ^ <*(b5 \ b4)*>) ^ b3),b6] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b5] & (c2 . (c3 ^ <*1*>)) `1 = [((b2 ^ <*b4*>) ^ b3),b6] ) ) ) ) & ( (c2 . c3) `2 = 3 & (c2 . c3) `2 = 5 implies ( ( branchdeg c3 = 2 & ex b1, b2, b3 being FinSequence of the carrier of c1ex b4, b5, b6 being type of c1 st
( (c2 . c3) `1 = [(((b2 ^ <*(b4 /" b5)*>) ^ b1) ^ b3),b6] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b5] & (c2 . (c3 ^ <*1*>)) `1 = [((b2 ^ <*b4*>) ^ b3),b6] ) ) iff for b1 being type of c1 holds
( branchdeg c3 = 1 & ex b2 being FinSequence of the carrier of c1ex b3, b4 being type of c1ex b5 being FinSequence of the carrier of c1 st
( (c2 . c3) `1 = [((b2 ^ <*(b3 * b4)*>) ^ b5),b1] & (c2 . (c3 ^ <*0*>)) `1 = [(((b2 ^ <*b3*>) ^ <*b4*>) ^ b5),b1] ) ) ) ) & ( (c2 . c3) `2 = 3 & (c2 . c3) `2 = 6 implies ( branchdeg c3 = 2 & ex b1, b2, b3 being FinSequence of the carrier of c1ex b4, b5, b6 being type of c1 st
( (c2 . c3) `1 = [(((b2 ^ <*(b4 /" b5)*>) ^ b1) ^ b3),b6] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b5] & (c2 . (c3 ^ <*1*>)) `1 = [((b2 ^ <*b4*>) ^ b3),b6] ) iff ( branchdeg c3 = 2 & ex b1, b2 being FinSequence of the carrier of c1ex b3, b4 being type of c1 st
( (c2 . c3) `1 = [(b1 ^ b2),(b3 * b4)] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b3] & (c2 . (c3 ^ <*1*>)) `1 = [b2,b4] ) ) ) ) & ( (c2 . c3) `2 = 3 & (c2 . c3) `2 = 7 implies ( branchdeg c3 = 2 & ex b1, b2, b3 being FinSequence of the carrier of c1ex b4, b5, b6 being type of c1 st
( (c2 . c3) `1 = [(((b2 ^ <*(b4 /" b5)*>) ^ b1) ^ b3),b6] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b5] & (c2 . (c3 ^ <*1*>)) `1 = [((b2 ^ <*b4*>) ^ b3),b6] ) iff ( branchdeg c3 = 2 & ex b1, b2, b3 being FinSequence of the carrier of c1ex b4, b5 being type of c1 st
( (c2 . c3) `1 = [((b2 ^ b1) ^ b3),b5] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b4] & (c2 . (c3 ^ <*1*>)) `1 = [((b2 ^ <*b4*>) ^ b3),b5] ) ) ) ) & ( (c2 . c3) `2 = 4 & (c2 . c3) `2 = 5 implies ( ( branchdeg c3 = 2 & ex b1, b2, b3 being FinSequence of the carrier of c1ex b4, b5, b6 being type of c1 st
( (c2 . c3) `1 = [(((b2 ^ b1) ^ <*(b5 \ b4)*>) ^ b3),b6] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b5] & (c2 . (c3 ^ <*1*>)) `1 = [((b2 ^ <*b4*>) ^ b3),b6] ) ) iff for b1 being type of c1 holds
( branchdeg c3 = 1 & ex b2 being FinSequence of the carrier of c1ex b3, b4 being type of c1ex b5 being FinSequence of the carrier of c1 st
( (c2 . c3) `1 = [((b2 ^ <*(b3 * b4)*>) ^ b5),b1] & (c2 . (c3 ^ <*0*>)) `1 = [(((b2 ^ <*b3*>) ^ <*b4*>) ^ b5),b1] ) ) ) ) & ( (c2 . c3) `2 = 4 & (c2 . c3) `2 = 6 implies ( branchdeg c3 = 2 & ex b1, b2, b3 being FinSequence of the carrier of c1ex b4, b5, b6 being type of c1 st
( (c2 . c3) `1 = [(((b2 ^ b1) ^ <*(b5 \ b4)*>) ^ b3),b6] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b5] & (c2 . (c3 ^ <*1*>)) `1 = [((b2 ^ <*b4*>) ^ b3),b6] ) iff ( branchdeg c3 = 2 & ex b1, b2 being FinSequence of the carrier of c1ex b3, b4 being type of c1 st
( (c2 . c3) `1 = [(b1 ^ b2),(b3 * b4)] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b3] & (c2 . (c3 ^ <*1*>)) `1 = [b2,b4] ) ) ) ) & ( (c2 . c3) `2 = 4 & (c2 . c3) `2 = 7 implies ( branchdeg c3 = 2 & ex b1, b2, b3 being FinSequence of the carrier of c1ex b4, b5, b6 being type of c1 st
( (c2 . c3) `1 = [(((b2 ^ b1) ^ <*(b5 \ b4)*>) ^ b3),b6] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b5] & (c2 . (c3 ^ <*1*>)) `1 = [((b2 ^ <*b4*>) ^ b3),b6] ) iff ( branchdeg c3 = 2 & ex b1, b2, b3 being FinSequence of the carrier of c1ex b4, b5 being type of c1 st
( (c2 . c3) `1 = [((b2 ^ b1) ^ b3),b5] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b4] & (c2 . (c3 ^ <*1*>)) `1 = [((b2 ^ <*b4*>) ^ b3),b5] ) ) ) ) & ( (c2 . c3) `2 = 5 & (c2 . c3) `2 = 6 implies ( ( for b1 being type of c1 holds
( branchdeg c3 = 1 & ex b2 being FinSequence of the carrier of c1ex b3, b4 being type of c1ex b5 being FinSequence of the carrier of c1 st
( (c2 . c3) `1 = [((b2 ^ <*(b3 * b4)*>) ^ b5),b1] & (c2 . (c3 ^ <*0*>)) `1 = [(((b2 ^ <*b3*>) ^ <*b4*>) ^ b5),b1] ) ) ) iff ( branchdeg c3 = 2 & ex b1, b2 being FinSequence of the carrier of c1ex b3, b4 being type of c1 st
( (c2 . c3) `1 = [(b1 ^ b2),(b3 * b4)] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b3] & (c2 . (c3 ^ <*1*>)) `1 = [b2,b4] ) ) ) ) & ( (c2 . c3) `2 = 5 & (c2 . c3) `2 = 7 implies ( ( for b1 being type of c1 holds
( branchdeg c3 = 1 & ex b2 being FinSequence of the carrier of c1ex b3, b4 being type of c1ex b5 being FinSequence of the carrier of c1 st
( (c2 . c3) `1 = [((b2 ^ <*(b3 * b4)*>) ^ b5),b1] & (c2 . (c3 ^ <*0*>)) `1 = [(((b2 ^ <*b3*>) ^ <*b4*>) ^ b5),b1] ) ) ) iff ( branchdeg c3 = 2 & ex b1, b2, b3 being FinSequence of the carrier of c1ex b4, b5 being type of c1 st
( (c2 . c3) `1 = [((b2 ^ b1) ^ b3),b5] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b4] & (c2 . (c3 ^ <*1*>)) `1 = [((b2 ^ <*b4*>) ^ b3),b5] ) ) ) ) & ( (c2 . c3) `2 = 6 & (c2 . c3) `2 = 7 implies ( branchdeg c3 = 2 & ex b1, b2 being FinSequence of the carrier of c1ex b3, b4 being type of c1 st
( (c2 . c3) `1 = [(b1 ^ b2),(b3 * b4)] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b3] & (c2 . (c3 ^ <*1*>)) `1 = [b2,b4] ) iff ( branchdeg c3 = 2 & ex b1, b2, b3 being FinSequence of the carrier of c1ex b4, b5 being type of c1 st
( (c2 . c3) `1 = [((b2 ^ b1) ^ b3),b5] & (c2 . (c3 ^ <*0*>)) `1 = [b1,b4] & (c2 . (c3 ^ <*1*>)) `1 = [((b2 ^ <*b4*>) ^ b3),b5] ) ) ) ) );
;
end;

:: deftheorem Def4 PRELAMB:def 4 :
canceled;

:: deftheorem Def5 defines correct PRELAMB:def 5 :
for b1 being non empty typealg
for b2 being PreProof of b1
for b3 being Element of dom b2 holds
( ( (b2 . b3) `2 = 0 implies ( b3 is correct iff ( branchdeg b3 = 0 & ex b4 being type of b1 st (b2 . b3) `1 = [<*b4*>,b4] ) ) ) & ( (b2 . b3) `2 = 1 implies ( b3 is correct iff ( branchdeg b3 = 1 & ex b4 being FinSequence of the carrier of b1ex b5, b6 being type of b1 st
( (b2 . b3) `1 = [b4,(b5 /" b6)] & (b2 . (b3 ^ <*0*>)) `1 = [(b4 ^ <*b6*>),b5] ) ) ) ) & ( (b2 . b3) `2 = 2 implies ( b3 is correct iff ( branchdeg b3 = 1 & ex b4 being FinSequence of the carrier of b1ex b5, b6 being type of b1 st
( (b2 . b3) `1 = [b4,(b6 \ b5)] & (b2 . (b3 ^ <*0*>)) `1 = [(<*b6*> ^ b4),b5] ) ) ) ) & ( (b2 . b3) `2 = 3 implies ( b3 is correct iff ( branchdeg b3 = 2 & ex b4, b5, b6 being FinSequence of the carrier of b1ex b7, b8, b9 being type of b1 st
( (b2 . b3) `1 = [(((b5 ^ <*(b7 /" b8)*>) ^ b4) ^ b6),b9] & (b2 . (b3 ^ <*0*>)) `1 = [b4,b8] & (b2 . (b3 ^ <*1*>)) `1 = [((b5 ^ <*b7*>) ^ b6),b9] ) ) ) ) & ( (b2 . b3) `2 = 4 implies ( b3 is correct iff ( branchdeg b3 = 2 & ex b4, b5, b6 being FinSequence of the carrier of b1ex b7, b8, b9 being type of b1 st
( (b2 . b3) `1 = [(((b5 ^ b4) ^ <*(b8 \ b7)*>) ^ b6),b9] & (b2 . (b3 ^ <*0*>)) `1 = [b4,b8] & (b2 . (b3 ^ <*1*>)) `1 = [((b5 ^ <*b7*>) ^ b6),b9] ) ) ) ) & ( (b2 . b3) `2 = 5 implies ( b3 is correct iff for b4 being type of b1 holds
( branchdeg b3 = 1 & ex b5 being FinSequence of the carrier of b1ex b6, b7 being type of b1ex b8 being FinSequence of the carrier of b1 st
( (b2 . b3) `1 = [((b5 ^ <*(b6 * b7)*>) ^ b8),b4] & (b2 . (b3 ^ <*0*>)) `1 = [(((b5 ^ <*b6*>) ^ <*b7*>) ^ b8),b4] ) ) ) ) & ( (b2 . b3) `2 = 6 implies ( b3 is correct iff ( branchdeg b3 = 2 & ex b4, b5 being FinSequence of the carrier of b1ex b6, b7 being type of b1 st
( (b2 . b3) `1 = [(b4 ^ b5),(b6 * b7)] & (b2 . (b3 ^ <*0*>)) `1 = [b4,b6] & (b2 . (b3 ^ <*1*>)) `1 = [b5,b7] ) ) ) ) & ( (b2 . b3) `2 = 7 implies ( b3 is correct iff ( branchdeg b3 = 2 & ex b4, b5, b6 being FinSequence of the carrier of b1ex b7, b8 being type of b1 st
( (b2 . b3) `1 = [((b5 ^ b4) ^ b6),b8] & (b2 . (b3 ^ <*0*>)) `1 = [b4,b7] & (b2 . (b3 ^ <*1*>)) `1 = [((b5 ^ <*b7*>) ^ b6),b8] ) ) ) ) & ( not (b2 . b3) `2 = 0 & not (b2 . b3) `2 = 1 & not (b2 . b3) `2 = 2 & not (b2 . b3) `2 = 3 & not (b2 . b3) `2 = 4 & not (b2 . b3) `2 = 5 & not (b2 . b3) `2 = 6 & not (b2 . b3) `2 = 7 implies ( b3 is correct iff contradiction ) ) );

definition
let c1 be non empty typealg ;
let c2 be type of c1;
attr a2 is left means :: PRELAMB:def 6
ex b1, b2 being type of a1 st a2 = b1 \ b2;
attr a2 is right means :: PRELAMB:def 7
ex b1, b2 being type of a1 st a2 = b1 /" b2;
attr a2 is middle means :: PRELAMB:def 8
ex b1, b2 being type of a1 st a2 = b1 * b2;
end;

:: deftheorem Def6 defines left PRELAMB:def 6 :
for b1 being non empty typealg
for b2 being type of b1 holds
( b2 is left iff ex b3, b4 being type of b1 st b2 = b3 \ b4 );

:: deftheorem Def7 defines right PRELAMB:def 7 :
for b1 being non empty typealg
for b2 being type of b1 holds
( b2 is right iff ex b3, b4 being type of b1 st b2 = b3 /" b4 );

:: deftheorem Def8 defines middle PRELAMB:def 8 :
for b1 being non empty typealg
for b2 being type of b1 holds
( b2 is middle iff ex b3, b4 being type of b1 st b2 = b3 * b4 );

definition
let c1 be non empty typealg ;
let c2 be type of c1;
attr a2 is primitive means :: PRELAMB:def 9
( not a2 is left & not a2 is right & not a2 is middle );
end;

:: deftheorem Def9 defines primitive PRELAMB:def 9 :
for b1 being non empty typealg
for b2 being type of b1 holds
( b2 is primitive iff ( not b2 is left & not b2 is right & not b2 is middle ) );

definition
let c1 be non empty typealg ;
let c2 be finite DecoratedTree of the carrier of c1;
let c3 be Element of dom c2;
redefine func . as c2 . c3 -> type of a1;
coherence
c2 . c3 is type of c1
proof end;
end;

definition
let c1 be non empty typealg ;
let c2 be finite DecoratedTree of the carrier of c1;
let c3 be type of c1;
pred c2 represents c3 means :: PRELAMB:def 10
( dom a2 is finite & ( for b1 being Element of dom a2 holds
( ( branchdeg b1 = 0 or branchdeg b1 = 2 ) & ( branchdeg b1 = 0 implies a2 . b1 is primitive ) & ( branchdeg b1 = 2 implies ex b2, b3 being type of a1 st
( ( a2 . b1 = b2 /" b3 or a2 . b1 = b2 \ b3 or a2 . b1 = b2 * b3 ) & a2 . (b1 ^ <*0*>) = b2 & a2 . (b1 ^ <*1*>) = b3 ) ) ) ) );
end;

:: deftheorem Def10 defines represents PRELAMB:def 10 :
for b1 being non empty typealg
for b2 being finite DecoratedTree of the carrier of b1
for b3 being type of b1 holds
( b2 represents b3 iff ( dom b2 is finite & ( for b4 being Element of dom b2 holds
( ( branchdeg b4 = 0 or branchdeg b4 = 2 ) & ( branchdeg b4 = 0 implies b2 . b4 is primitive ) & ( branchdeg b4 = 2 implies ex b5, b6 being type of b1 st
( ( b2 . b4 = b5 /" b6 or b2 . b4 = b5 \ b6 or b2 . b4 = b5 * b6 ) & b2 . (b4 ^ <*0*>) = b5 & b2 . (b4 ^ <*1*>) = b6 ) ) ) ) ) );

notation
let c1 be non empty typealg ;
let c2 be finite DecoratedTree of the carrier of c1;
let c3 be type of c1;
antonym c2 does_not_represent c3 for c2 represents c3;
end;

definition
let c1 be non empty typealg ;
attr a1 is free means :Def11: :: PRELAMB:def 11
( ( for b1 being type of a1 holds
( not ( b1 is left & b1 is right ) & not ( b1 is left & b1 is middle ) & not ( b1 is right & b1 is middle ) ) ) & ( for b1 being type of a1 ex b2 being finite DecoratedTree of the carrier of a1 st
for b3 being finite DecoratedTree of the carrier of a1 holds
( b3 represents b1 iff b2 = b3 ) ) );
end;

:: deftheorem Def11 defines free PRELAMB:def 11 :
for b1 being non empty typealg holds
( b1 is free iff ( ( for b2 being type of b1 holds
( not ( b2 is left & b2 is right ) & not ( b2 is left & b2 is middle ) & not ( b2 is right & b2 is middle ) ) ) & ( for b2 being type of b1 ex b3 being finite DecoratedTree of the carrier of b1 st
for b4 being finite DecoratedTree of the carrier of b1 holds
( b4 represents b2 iff b3 = b4 ) ) ) );

definition
let c1 be non empty typealg ;
let c2 be type of c1;
assume E5: c1 is free ;
func repr_of c2 -> finite DecoratedTree of the carrier of a1 means :: PRELAMB:def 12
for b1 being finite DecoratedTree of the carrier of a1 holds
( b1 represents a2 iff a3 = b1 );
existence
ex b1 being finite DecoratedTree of the carrier of c1 st
for b2 being finite DecoratedTree of the carrier of c1 holds
( b2 represents c2 iff b1 = b2 ) by E5, Def11;
uniqueness
for b1, b2 being finite DecoratedTree of the carrier of c1 st ( for b3 being finite DecoratedTree of the carrier of c1 holds
( b3 represents c2 iff b1 = b3 ) ) & ( for b3 being finite DecoratedTree of the carrier of c1 holds
( b3 represents c2 iff b2 = b3 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines repr_of PRELAMB:def 12 :
for b1 being non empty typealg
for b2 being type of b1 st b1 is free holds
for b3 being finite DecoratedTree of the carrier of b1 holds
( b3 = repr_of b2 iff for b4 being finite DecoratedTree of the carrier of b1 holds
( b4 represents b2 iff b3 = b4 ) );

deffunc H1( typealg ) -> set = [:(the carrier of a1 * ),the carrier of a1:];

definition
let c1 be non empty typealg ;
let c2 be FinSequence of the carrier of c1;
let c3 be type of c1;
redefine func [ as [c2,c3] -> Element of [:(the carrier of a1 * ),the carrier of a1:];
coherence
[c2,c3] is Element of [:(the carrier of c1 * ),the carrier of c1:]
proof end;
end;

definition
let c1 be non empty typealg ;
mode Proof of c1 -> PreProof of a1 means :Def13: :: PRELAMB:def 13
( dom a2 is finite & ( for b1 being Element of dom a2 holds b1 is correct ) );
existence
ex b1 being PreProof of c1 st
( dom b1 is finite & ( for b2 being Element of dom b1 holds b2 is correct ) )
proof end;
end;

:: deftheorem Def13 defines Proof PRELAMB:def 13 :
for b1 being non empty typealg
for b2 being PreProof of b1 holds
( b2 is Proof of b1 iff ( dom b2 is finite & ( for b3 being Element of dom b2 holds b3 is correct ) ) );

theorem Th1: :: PRELAMB:1
for b1 being non empty typealg
for b2 being Proof of b1
for b3 being Element of dom b2 st branchdeg b3 = 1 holds
b3 ^ <*0*> in dom b2
proof end;

theorem Th2: :: PRELAMB:2
for b1 being non empty typealg
for b2 being Proof of b1
for b3 being Element of dom b2 st branchdeg b3 = 2 holds
( b3 ^ <*0*> in dom b2 & b3 ^ <*1*> in dom b2 )
proof end;

theorem Th3: :: PRELAMB:3
for b1 being non empty typealg
for b2 being Proof of b1
for b3 being Element of dom b2 st (b2 . b3) `2 = 0 holds
ex b4 being type of b1 st (b2 . b3) `1 = [<*b4*>,b4]
proof end;

theorem Th4: :: PRELAMB:4
for b1 being non empty typealg
for b2 being Proof of b1
for b3 being Element of dom b2 st (b2 . b3) `2 = 1 holds
ex b4 being Element of dom b2ex b5 being FinSequence of the carrier of b1ex b6, b7 being type of b1 st
( b4 = b3 ^ <*0*> & (b2 . b3) `1 = [b5,(b6 /" b7)] & (b2 . b4) `1 = [(b5 ^ <*b7*>),b6] )
proof end;

theorem Th5: :: PRELAMB:5
for b1 being non empty typealg
for b2 being Proof of b1
for b3 being Element of dom b2 st (b2 . b3) `2 = 2 holds
ex b4 being Element of dom b2ex b5 being FinSequence of the carrier of b1ex b6, b7 being type of b1 st
( b4 = b3 ^ <*0*> & (b2 . b3) `1 = [b5,(b7 \ b6)] & (b2 . b4) `1 = [(<*b7*> ^ b5),b6] )
proof end;

theorem Th6: :: PRELAMB:6
for b1 being non empty typealg
for b2 being Proof of b1
for b3 being Element of dom b2 st (b2 . b3) `2 = 3 holds
ex b4, b5 being Element of dom b2ex b6, b7, b8 being FinSequence of the carrier of b1ex b9, b10, b11 being type of b1 st
( b4 = b3 ^ <*0*> & b5 = b3 ^ <*1*> & (b2 . b3) `1 = [(((b7 ^ <*(b9 /" b10)*>) ^ b6) ^ b8),b11] & (b2 . b4) `1 = [b6,b10] & (b2 . b5) `1 = [((b7 ^ <*b9*>) ^ b8),b11] )
proof end;

theorem Th7: :: PRELAMB:7
for b1 being non empty typealg
for b2 being Proof of b1
for b3 being Element of dom b2 st (b2 . b3) `2 = 4 holds
ex b4, b5 being Element of dom b2ex b6, b7, b8 being FinSequence of the carrier of b1ex b9, b10, b11 being type of b1 st
( b4 = b3 ^ <*0*> & b5 = b3 ^ <*1*> & (b2 . b3) `1 = [(((b7 ^ b6) ^ <*(b10 \ b9)*>) ^ b8),b11] & (b2 . b4) `1 = [b6,b10] & (b2 . b5) `1 = [((b7 ^ <*b9*>) ^ b8),b11] )
proof end;

theorem Th8: :: PRELAMB:8
for b1 being non empty typealg
for b2 being type of b1
for b3 being Proof of b1
for b4 being Element of dom b3 st (b3 . b4) `2 = 5 holds
ex b5 being Element of dom b3ex b6 being FinSequence of the carrier of b1ex b7, b8 being type of b1ex b9 being FinSequence of the carrier of b1 st
( b5 = b4 ^ <*0*> & (b3 . b4) `1 = [((b6 ^ <*(b7 * b8)*>) ^ b9),b2] & (b3 . b5) `1 = [(((b6 ^ <*b7*>) ^ <*b8*>) ^ b9),b2] )
proof end;

theorem Th9: :: PRELAMB:9
for b1 being non empty typealg
for b2 being Proof of b1
for b3 being Element of dom b2 st (b2 . b3) `2 = 6 holds
ex b4, b5 being Element of dom b2ex b6, b7 being FinSequence of the carrier of b1ex b8, b9 being type of b1 st
( b4 = b3 ^ <*0*> & b5 = b3 ^ <*1*> & (b2 . b3) `1 = [(b6 ^ b7),(b8 * b9)] & (b2 . b4) `1 = [b6,b8] & (b2 . b5) `1 = [b7,b9] )
proof end;

theorem Th10: :: PRELAMB:10
for b1 being non empty typealg
for b2 being Proof of b1
for b3 being Element of dom b2 st (b2 . b3) `2 = 7 holds
ex b4, b5 being Element of dom b2ex b6, b7, b8 being FinSequence of the carrier of b1ex b9, b10 being type of b1 st
( b4 = b3 ^ <*0*> & b5 = b3 ^ <*1*> & (b2 . b3) `1 = [((b7 ^ b6) ^ b8),b10] & (b2 . b4) `1 = [b6,b9] & (b2 . b5) `1 = [((b7 ^ <*b9*>) ^ b8),b10] )
proof end;

theorem Th11: :: PRELAMB:11
for b1 being non empty typealg
for b2 being Proof of b1
for b3 being Element of dom b2 holds
( (b2 . b3) `2 = 0 or (b2 . b3) `2 = 1 or (b2 . b3) `2 = 2 or (b2 . b3) `2 = 3 or (b2 . b3) `2 = 4 or (b2 . b3) `2 = 5 or (b2 . b3) `2 = 6 or (b2 . b3) `2 = 7 )
proof end;

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

:: deftheorem Def14 defines cut-free PRELAMB:def 14 :
for b1 being non empty typealg
for b2 being PreProof of b1 holds
( b2 is cut-free iff for b3 being Element of dom b2 holds (b2 . b3) `2 <> 7 );

definition
let c1 be non empty typealg ;
func size_w.r.t. c1 -> Function of the carrier of a1, NAT means :: PRELAMB:def 15
for b1 being type of a1 holds a2 . b1 = card (dom (repr_of b1));
existence
ex b1 being Function of the carrier of c1, NAT st
for b2 being type of c1 holds b1 . b2 = card (dom (repr_of b2))
proof end;
uniqueness
for b1, b2 being Function of the carrier of c1, NAT st ( for b3 being type of c1 holds b1 . b3 = card (dom (repr_of b3)) ) & ( for b3 being type of c1 holds b2 . b3 = card (dom (repr_of b3)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines size_w.r.t. PRELAMB:def 15 :
for b1 being non empty typealg
for b2 being Function of the carrier of b1, NAT holds
( b2 = size_w.r.t. b1 iff for b3 being type of b1 holds b2 . b3 = card (dom (repr_of b3)) );

Lemma9: for b1 being non empty set
for b2 being FinSequence of b1
for b3 being Function of b1, NAT holds b3 * b2 is FinSequence of NAT
proof end;

Lemma10: for b1 being non empty set
for b2 being FinSequence of b1
for b3 being Function of b1, NAT holds b3 * b2 is FinSequence of REAL
proof end;

definition
let c1 be non empty set ;
let c2 be FinSequence of c1;
let c3 be Function of c1, NAT ;
redefine func * as c3 * c2 -> FinSequence of REAL ;
coherence
c2 * c3 is FinSequence of REAL by Lemma10;
end;

Lemma11: for b1 being non empty set
for b2 being FinSequence of b1
for b3 being Function of b1, NAT holds Sum (b3 * b2) is Nat
proof end;

definition
let c1 be non empty typealg ;
let c2 be Proof of c1;
func cutdeg c2 -> Nat means :: PRELAMB:def 16
ex b1, b2, b3 being FinSequence of the carrier of a1ex b4, b5 being type of a1 st
( (a2 . {} ) `1 = [((b2 ^ b1) ^ b3),b5] & (a2 . <*0*>) `1 = [b1,b4] & (a2 . <*1*>) `1 = [((b2 ^ <*b4*>) ^ b3),b5] & a3 = (((size_w.r.t. a1) . b4) + ((size_w.r.t. a1) . b5)) + (Sum ((size_w.r.t. a1) * ((b2 ^ b1) ^ b3))) ) if (a2 . {} ) `2 = 7
otherwise a3 = 0;
existence
( ( (c2 . {} ) `2 = 7 implies ex b1 being Natex b2, b3, b4 being FinSequence of the carrier of c1ex b5, b6 being type of c1 st
( (c2 . {} ) `1 = [((b3 ^ b2) ^ b4),b6] & (c2 . <*0*>) `1 = [b2,b5] & (c2 . <*1*>) `1 = [((b3 ^ <*b5*>) ^ b4),b6] & b1 = (((size_w.r.t. c1) . b5) + ((size_w.r.t. c1) . b6)) + (Sum ((size_w.r.t. c1) * ((b3 ^ b2) ^ b4))) ) ) & ( not (c2 . {} ) `2 = 7 implies ex b1 being Nat st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being Nat holds
( ( (c2 . {} ) `2 = 7 & ex b3, b4, b5 being FinSequence of the carrier of c1ex b6, b7 being type of c1 st
( (c2 . {} ) `1 = [((b4 ^ b3) ^ b5),b7] & (c2 . <*0*>) `1 = [b3,b6] & (c2 . <*1*>) `1 = [((b4 ^ <*b6*>) ^ b5),b7] & b1 = (((size_w.r.t. c1) . b6) + ((size_w.r.t. c1) . b7)) + (Sum ((size_w.r.t. c1) * ((b4 ^ b3) ^ b5))) ) & ex b3, b4, b5 being FinSequence of the carrier of c1ex b6, b7 being type of c1 st
( (c2 . {} ) `1 = [((b4 ^ b3) ^ b5),b7] & (c2 . <*0*>) `1 = [b3,b6] & (c2 . <*1*>) `1 = [((b4 ^ <*b6*>) ^ b5),b7] & b2 = (((size_w.r.t. c1) . b6) + ((size_w.r.t. c1) . b7)) + (Sum ((size_w.r.t. c1) * ((b4 ^ b3) ^ b5))) ) implies b1 = b2 ) & ( not (c2 . {} ) `2 = 7 & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof end;
consistency
for b1 being Nat holds verum ;
end;

:: deftheorem Def16 defines cutdeg PRELAMB:def 16 :
for b1 being non empty typealg
for b2 being Proof of b1
for b3 being Nat holds
( ( (b2 . {} ) `2 = 7 implies ( b3 = cutdeg b2 iff ex b4, b5, b6 being FinSequence of the carrier of b1ex b7, b8 being type of b1 st
( (b2 . {} ) `1 = [((b5 ^ b4) ^ b6),b8] & (b2 . <*0*>) `1 = [b4,b7] & (b2 . <*1*>) `1 = [((b5 ^ <*b7*>) ^ b6),b8] & b3 = (((size_w.r.t. b1) . b7) + ((size_w.r.t. b1) . b8)) + (Sum ((size_w.r.t. b1) * ((b5 ^ b4) ^ b6))) ) ) ) & ( not (b2 . {} ) `2 = 7 implies ( b3 = cutdeg b2 iff b3 = 0 ) ) );

definition
let c1 be non empty typealg ;
let c2 be non empty set ;
mode Model of c1,c2 -> Function of the carrier of a1, bool (a2 * ) means :: PRELAMB:def 17
for b1, b2 being type of a1 holds
( a3 . (b1 * b2) = { (b3 ^ b4) where B is Element of a2 * , B is Element of a2 * : ( b3 in a3 . b1 & b4 in a3 . b2 ) } & a3 . (b1 /" b2) = { b3 where B is Element of a2 * : for b1 being Element of a2 * st b4 in a3 . b2 holds
b3 ^ b4 in a3 . b1 } & a3 . (b2 \ b1) = { b3 where B is Element of a2 * : for b1 being Element of a2 * st b4 in a3 . b2 holds
b4 ^ b3 in a3 . b1 } );
existence
ex b1 being Function of the carrier of c1, bool (c2 * ) st
for b2, b3 being type of c1 holds
( b1 . (b2 * b3) = { (b4 ^ b5) where B is Element of c2 * , B is Element of c2 * : ( b4 in b1 . b2 & b5 in b1 . b3 ) } & b1 . (b2 /" b3) = { b4 where B is Element of c2 * : for b1 being Element of c2 * st b5 in b1 . b3 holds
b4 ^ b5 in b1 . b2 } & b1 . (b3 \ b2) = { b4 where B is Element of c2 * : for b1 being Element of c2 * st b5 in b1 . b3 holds
b5 ^ b4 in b1 . b2 } )
proof end;
end;

:: deftheorem Def17 defines Model PRELAMB:def 17 :
for b1 being non empty typealg
for b2 being non empty set
for b3 being Function of the carrier of b1, bool (b2 * ) holds
( b3 is Model of b1,b2 iff for b4, b5 being type of b1 holds
( b3 . (b4 * b5) = { (b6 ^ b7) where B is Element of b2 * , B is Element of b2 * : ( b6 in b3 . b4 & b7 in b3 . b5 ) } & b3 . (b4 /" b5) = { b6 where B is Element of b2 * : for b1 being Element of b2 * st b7 in b3 . b5 holds
b6 ^ b7 in b3 . b4 } & b3 . (b5 \ b4) = { b6 where B is Element of b2 * : for b1 being Element of b2 * st b7 in b3 . b5 holds
b7 ^ b6 in b3 . b4 } ) );

definition
attr a1 is strict;
struct typestr -> typealg ;
aggr typestr(# carrier, left_quotient, right_quotient, inner_product, derivability #) -> typestr ;
sel derivability c1 -> Relation of the carrier of a1 * ,the carrier of a1;
end;

registration
cluster non empty strict typestr ;
existence
ex b1 being typestr st
( not b1 is empty & b1 is strict )
proof end;
end;

definition
let c1 be non empty typestr ;
let c2 be FinSequence of the carrier of c1;
let c3 be type of c1;
pred c2 ==>. c3 means :Def18: :: PRELAMB:def 18
[a2,a3] in the derivability of a1;
end;

:: deftheorem Def18 defines ==>. PRELAMB:def 18 :
for b1 being non empty typestr
for b2 being FinSequence of the carrier of b1
for b3 being type of b1 holds
( b2 ==>. b3 iff [b2,b3] in the derivability of b1 );

definition
let c1 be non empty typestr ;
attr a1 is SynTypes_Calculus-like means :Def19: :: PRELAMB:def 19
( ( for b1 being type of a1 holds <*b1*> ==>. b1 ) & ( for b1 being FinSequence of the carrier of a1
for b2, b3 being type of a1 st b1 ^ <*b3*> ==>. b2 holds
b1 ==>. b2 /" b3 ) & ( for b1 being FinSequence of the carrier of a1
for b2, b3 being type of a1 st <*b3*> ^ b1 ==>. b2 holds
b1 ==>. b3 \ b2 ) & ( for b1, b2, b3 being FinSequence of the carrier of a1
for b4, b5, b6 being type of a1 st b1 ==>. b5 & (b2 ^ <*b4*>) ^ b3 ==>. b6 holds
((b2 ^ <*(b4 /" b5)*>) ^ b1) ^ b3 ==>. b6 ) & ( for b1, b2, b3 being FinSequence of the carrier of a1
for b4, b5, b6 being type of a1 st b1 ==>. b5 & (b2 ^ <*b4*>) ^ b3 ==>. b6 holds
((b2 ^ b1) ^ <*(b5 \ b4)*>) ^ b3 ==>. b6 ) & ( for b1, b2 being FinSequence of the carrier of a1
for b3, b4, b5 being type of a1 st ((b1 ^ <*b3*>) ^ <*b4*>) ^ b2 ==>. b5 holds
(b1 ^ <*(b3 * b4)*>) ^ b2 ==>. b5 ) & ( for b1, b2 being FinSequence of the carrier of a1
for b3, b4 being type of a1 st b1 ==>. b3 & b2 ==>. b4 holds
b1 ^ b2 ==>. b3 * b4 ) );
end;

:: deftheorem Def19 defines SynTypes_Calculus-like PRELAMB:def 19 :
for b1 being non empty typestr holds
( b1 is SynTypes_Calculus-like iff ( ( for b2 being type of b1 holds <*b2*> ==>. b2 ) & ( for b2 being FinSequence of the carrier of b1
for b3, b4 being type of b1 st b2 ^ <*b4*> ==>. b3 holds
b2 ==>. b3 /" b4 ) & ( for b2 being FinSequence of the carrier of b1
for b3, b4 being type of b1 st <*b4*> ^ b2 ==>. b3 holds
b2 ==>. b4 \ b3 ) & ( for b2, b3, b4 being FinSequence of the carrier of b1
for b5, b6, b7 being type of b1 st b2 ==>. b6 & (b3 ^ <*b5*>) ^ b4 ==>. b7 holds
((b3 ^ <*(b5 /" b6)*>) ^ b2) ^ b4 ==>. b7 ) & ( for b2, b3, b4 being FinSequence of the carrier of b1
for b5, b6, b7 being type of b1 st b2 ==>. b6 & (b3 ^ <*b5*>) ^ b4 ==>. b7 holds
((b3 ^ b2) ^ <*(b6 \ b5)*>) ^ b4 ==>. b7 ) & ( for b2, b3 being FinSequence of the carrier of b1
for b4, b5, b6 being type of b1 st ((b2 ^ <*b4*>) ^ <*b5*>) ^ b3 ==>. b6 holds
(b2 ^ <*(b4 * b5)*>) ^ b3 ==>. b6 ) & ( for b2, b3 being FinSequence of the carrier of b1
for b4, b5 being type of b1 st b2 ==>. b4 & b3 ==>. b5 holds
b2 ^ b3 ==>. b4 * b5 ) ) );

registration
cluster non empty SynTypes_Calculus-like typestr ;
existence
ex b1 being non empty typestr st b1 is SynTypes_Calculus-like
proof end;
end;

definition
mode SynTypes_Calculus is non empty SynTypes_Calculus-like typestr ;
end;

deffunc H2( typestr ) -> FinSequence of the carrier of a1 = <*> the carrier of a1;

Lemma14: for b1 being SynTypes_Calculus
for b2, b3 being FinSequence of the carrier of b1
for b4, b5, b6 being type of b1 st b2 ==>. b4 & b3 ^ <*b5*> ==>. b6 holds
(b3 ^ <*(b5 /" b4)*>) ^ b2 ==>. b6
proof end;

Lemma15: for b1 being SynTypes_Calculus
for b2, b3 being FinSequence of the carrier of b1
for b4, b5, b6 being type of b1 st b2 ==>. b4 & <*b5*> ^ b3 ==>. b6 holds
(<*(b5 /" b4)*> ^ b2) ^ b3 ==>. b6
proof end;

Lemma16: for b1 being SynTypes_Calculus
for b2 being FinSequence of the carrier of b1
for b3, b4, b5 being type of b1 st b2 ==>. b3 & <*b4*> ==>. b5 holds
<*(b4 /" b3)*> ^ b2 ==>. b5
proof end;

Lemma17: for b1 being SynTypes_Calculus
for b2, b3 being FinSequence of the carrier of b1
for b4, b5, b6 being type of b1 st b2 ==>. b4 & b3 ^ <*b5*> ==>. b6 holds
(b3 ^ b2) ^ <*(b4 \ b5)*> ==>. b6
proof end;

Lemma18: for b1 being SynTypes_Calculus
for b2, b3 being FinSequence of the carrier of b1
for b4, b5, b6 being type of b1 st b2 ==>. b4 & <*b5*> ^ b3 ==>. b6 holds
(b2 ^ <*(b4 \ b5)*>) ^ b3 ==>. b6
proof end;

Lemma19: for b1 being SynTypes_Calculus
for b2 being FinSequence of the carrier of b1
for b3, b4, b5 being type of b1 st b2 ==>. b3 & <*b4*> ==>. b5 holds
b2 ^ <*(b3 \ b4)*> ==>. b5
proof end;

Lemma20: for b1 being SynTypes_Calculus
for b2 being FinSequence of the carrier of b1
for b3, b4, b5 being type of b1 st (<*b3*> ^ <*b4*>) ^ b2 ==>. b5 holds
<*(b3 * b4)*> ^ b2 ==>. b5
proof end;

Lemma21: for b1 being SynTypes_Calculus
for b2 being FinSequence of the carrier of b1
for b3, b4, b5 being type of b1 st (b2 ^ <*b3*>) ^ <*b4*> ==>. b5 holds
b2 ^ <*(b3 * b4)*> ==>. b5
proof end;

Lemma22: for b1 being SynTypes_Calculus
for b2, b3, b4 being type of b1 st <*b2*> ^ <*b3*> ==>. b4 holds
<*(b2 * b3)*> ==>. b4
proof end;

theorem Th12: :: PRELAMB:12
for b1 being SynTypes_Calculus
for b2, b3 being type of b1 holds
( <*(b2 /" b3)*> ^ <*b3*> ==>. b2 & <*b3*> ^ <*(b3 \ b2)*> ==>. b2 )
proof end;

theorem Th13: :: PRELAMB:13
for b1 being SynTypes_Calculus
for b2, b3 being type of b1 holds
( <*b2*> ==>. b3 /" (b2 \ b3) & <*b2*> ==>. (b3 /" b2) \ b3 )
proof end;

theorem Th14: :: PRELAMB:14
for b1 being SynTypes_Calculus
for b2, b3, b4 being type of b1 holds <*(b2 /" b3)*> ==>. (b2 /" b4) /" (b3 /" b4)
proof end;

theorem Th15: :: PRELAMB:15
for b1 being SynTypes_Calculus
for b2, b3, b4 being type of b1 holds <*(b2 \ b3)*> ==>. (b4 \ b2) \ (b4 \ b3)
proof end;

theorem Th16: :: PRELAMB:16
for b1 being SynTypes_Calculus
for b2, b3, b4 being type of b1 st <*b2*> ==>. b3 holds
( <*(b2 /" b4)*> ==>. b3 /" b4 & <*(b4 \ b2)*> ==>. b4 \ b3 )
proof end;

theorem Th17: :: PRELAMB:17
for b1 being SynTypes_Calculus
for b2, b3, b4 being type of b1 st <*b2*> ==>. b3 holds
( <*(b4 /" b3)*> ==>. b4 /" b2 & <*(b3 \ b4)*> ==>. b2 \ b4 )
proof end;

theorem Th18: :: PRELAMB:18
for b1 being SynTypes_Calculus
for b2, b3 being type of b1 holds <*(b2 /" ((b2 /" b3) \ b2))*> ==>. b2 /" b3
proof end;

theorem Th19: :: PRELAMB:19
for b1 being SynTypes_Calculus
for b2, b3 being type of b1 st <*b2*> ==>. b3 holds
( <*> the carrier of b1 ==>. b3 /" b2 & <*> the carrier of b1 ==>. b2 \ b3 )
proof end;

theorem Th20: :: PRELAMB:20
for b1 being SynTypes_Calculus
for b2 being type of b1 holds
( <*> the carrier of b1 ==>. b2 /" b2 & <*> the carrier of b1 ==>. b2 \ b2 )
proof end;

theorem Th21: :: PRELAMB:21
for b1 being SynTypes_Calculus
for b2, b3 being type of b1 holds
( <*> the carrier of b1 ==>. (b2 /" (b3 \ b2)) /" b3 & <*> the carrier of b1 ==>. b3 \ ((b2 /" b3) \ b2) )
proof end;

theorem Th22: :: PRELAMB:22
for b1 being SynTypes_Calculus
for b2, b3, b4 being type of b1 holds
( <*> the carrier of b1 ==>. ((b2 /" b3) /" (b4 /" b3)) /" (b2 /" b4) & <*> the carrier of b1 ==>. (b4 \ b2) \ ((b3 \ b4) \ (b3 \ b2)) )
proof end;

theorem Th23: :: PRELAMB:23
for b1 being SynTypes_Calculus
for b2, b3 being type of b1 st <*> the carrier of b1 ==>. b2 holds
( <*> the carrier of b1 ==>. b3 /" (b3 /" b2) & <*> the carrier of b1 ==>. (b2 \ b3) \ b3 )
proof end;

theorem Th24: :: PRELAMB:24
for b1 being SynTypes_Calculus
for b2, b3 being type of b1 holds <*(b2 /" (b3 /" b3))*> ==>. b2
proof end;

definition
let c1 be SynTypes_Calculus;
let c2, c3 be type of c1;
pred c2 <==>. c3 means :Def20: :: PRELAMB:def 20
( <*a2*> ==>. a3 & <*a3*> ==>. a2 );
end;

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

theorem Th25: :: PRELAMB:25
for b1 being SynTypes_Calculus
for b2 being type of b1 holds b2 <==>. b2
proof end;

theorem Th26: :: PRELAMB:26
for b1 being SynTypes_Calculus
for b2, b3 being type of b1 holds b2 /" b3 <==>. b2 /" ((b2 /" b3) \ b2)
proof end;

theorem Th27: :: PRELAMB:27
for b1 being SynTypes_Calculus
for b2, b3, b4 being type of b1 holds b2 /" (b3 * b4) <==>. (b2 /" b4) /" b3
proof end;

theorem Th28: :: PRELAMB:28
for b1 being SynTypes_Calculus
for b2, b3, b4 being type of b1 holds <*(b2 * (b3 /" b4))*> ==>. (b2 * b3) /" b4
proof end;

theorem Th29: :: PRELAMB:29
for b1 being SynTypes_Calculus
for b2, b3 being type of b1 holds
( <*b2*> ==>. (b2 * b3) /" b3 & <*b2*> ==>. b3 \ (b3 * b2) )
proof end;

theorem Th30: :: PRELAMB:30
for b1 being SynTypes_Calculus
for b2, b3, b4 being type of b1 holds (b2 * b3) * b4 <==>. b2 * (b3 * b4)
proof end;