:: PRELAMB semantic presentation :: Showing IDV graph ... (Click the Palm Trees again to close it)
:: deftheorem defines \ PRELAMB:def 1 :
:: deftheorem defines /" PRELAMB:def 2 :
:: deftheorem defines * PRELAMB:def 3 :
Lm1:
for f being Function holds (pr1 (dom f),(rng f)) .: f = dom f
Lm2:
for f being Function holds
( dom f is finite iff f is finite )
definition
let s be non
empty typealg ;
let Tr be
PreProof of
s;
let v be
Element of
dom Tr;
canceled;attr v is
correct means :
Def5:
:: PRELAMB:def 5
(
branchdeg v = 0 & ex
x being
type of
s st
(Tr . v) `1 = [<*x*>,x] )
if (Tr . v) `2 = 0
(
branchdeg v = 1 & ex
T being
FinSequence of the
carrier 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 the
carrier 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 the
carrier 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 the
carrier 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 the
carrier of
s ex
x,
y being
type of
s ex
Y being
FinSequence of the
carrier 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 the
carrier 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 the
carrier of
s ex
y,
z being
type of
s st
(
(Tr . v) `1 = [((X ^ T) ^ Y),z] &
(Tr . (v ^ <*0*>)) `1 = [T,y] &
(Tr . (v ^ <*1*>)) `1 = [((X ^ <*y*>) ^ Y),z] ) )
if (Tr . v) `2 = 7
otherwise contradiction;
correctness
consistency
( ( (Tr . v) `2 = 0 & (Tr . v) `2 = 1 implies ( branchdeg v = 0 & ex x being type of s st (Tr . v) `1 = [<*x*>,x] iff ( branchdeg v = 1 & ex T being FinSequence of the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier of s ex x, y being type of s ex Y being FinSequence of the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier of s ex x, y being type of s ex Y being FinSequence of the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier of s ex x, y being type of s ex Y being FinSequence of the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier of s ex x, y being type of s ex Y being FinSequence of the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier of s ex x, y being type of s ex Y being FinSequence of the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier 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 the carrier of s ex x, y being type of s ex Y being FinSequence of the carrier 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 the carrier 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 the carrier of s ex x, y being type of s ex Y being FinSequence of the carrier 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 the carrier 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 the carrier 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 the carrier of s ex y, z being type of s st
( (Tr . v) `1 = [((X ^ T) ^ Y),z] & (Tr . (v ^ <*0*>)) `1 = [T,y] & (Tr . (v ^ <*1*>)) `1 = [((X ^ <*y*>) ^ Y),z] ) ) ) ) );
;
end;
:: deftheorem PRELAMB:def 4 :
canceled;
:: deftheorem Def5 defines correct PRELAMB:def 5 :
for
s being non
empty typealg for
Tr being
PreProof of
s for
v being
Element of
dom Tr holds
( (
(Tr . v) `2 = 0 implies (
v is
correct iff (
branchdeg v = 0 & ex
x being
type of
s st
(Tr . v) `1 = [<*x*>,x] ) ) ) & (
(Tr . v) `2 = 1 implies (
v is
correct iff (
branchdeg v = 1 & ex
T being
FinSequence of the
carrier 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 the
carrier 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 the
carrier 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 the
carrier 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 the
carrier of
s ex
x,
y being
type of
s ex
Y being
FinSequence of the
carrier 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 the
carrier 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 the
carrier 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 6 :
:: deftheorem defines right PRELAMB:def 7 :
:: deftheorem defines middle PRELAMB:def 8 :
:: deftheorem defines primitive PRELAMB:def 9 :
:: deftheorem defines represents PRELAMB:def 10 :
:: deftheorem Def11 defines free PRELAMB:def 11 :
:: deftheorem defines repr_of PRELAMB:def 12 :
deffunc H1( typealg ) -> set = [:(the carrier of $1 * ),the carrier of $1:];
:: deftheorem Def13 defines Proof PRELAMB:def 13 :
theorem Th1: :: PRELAMB:1 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th2: :: PRELAMB:2 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: PRELAMB:3 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: PRELAMB:4 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: PRELAMB:5 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: PRELAMB:6 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: PRELAMB:7 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: PRELAMB:8 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: PRELAMB:9 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th10: :: PRELAMB:10 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: PRELAMB:11 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem defines cut-free PRELAMB:def 14 :
:: deftheorem defines size_w.r.t. PRELAMB:def 15 :
Lm3:
for D being non empty set
for T being FinSequence of D
for f being Function of D, NAT holds f * T is FinSequence of NAT
Lm4:
for D being non empty set
for T being FinSequence of D
for f being Function of D, NAT holds f * T is FinSequence of REAL
Lm5:
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
definition
let s be non
empty typealg ;
let p be
Proof of
s;
func cutdeg p -> Nat means :: PRELAMB:def 16
ex
T,
X,
Y being
FinSequence of the
carrier of
s ex
y,
z being
type of
s st
(
(p . {} ) `1 = [((X ^ T) ^ Y),z] &
(p . <*0*>) `1 = [T,y] &
(p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] &
it = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) )
if (p . {} ) `2 = 7
otherwise it = 0;
existence
( ( (p . {} ) `2 = 7 implies ex b1 being Nat ex T, X, Y being FinSequence of the carrier of s ex y, z being type of s st
( (p . {} ) `1 = [((X ^ T) ^ Y),z] & (p . <*0*>) `1 = [T,y] & (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] & b1 = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) ) & ( not (p . {} ) `2 = 7 implies ex b1 being Nat st b1 = 0 ) )
uniqueness
for b1, b2 being Nat holds
( ( (p . {} ) `2 = 7 & ex T, X, Y being FinSequence of the carrier of s ex y, z being type of s st
( (p . {} ) `1 = [((X ^ T) ^ Y),z] & (p . <*0*>) `1 = [T,y] & (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] & b1 = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) & ex T, X, Y being FinSequence of the carrier of s ex y, z being type of s st
( (p . {} ) `1 = [((X ^ T) ^ Y),z] & (p . <*0*>) `1 = [T,y] & (p . <*1*>) `1 = [((X ^ <*y*>) ^ Y),z] & b2 = (((size_w.r.t. s) . y) + ((size_w.r.t. s) . z)) + (Sum ((size_w.r.t. s) * ((X ^ T) ^ Y))) ) implies b1 = b2 ) & ( not (p . {} ) `2 = 7 & b1 = 0 & b2 = 0 implies b1 = b2 ) )
consistency
for b1 being Nat holds verum
;
end;
:: deftheorem defines cutdeg PRELAMB:def 16 :
:: deftheorem defines Model PRELAMB:def 17 :
:: deftheorem Def18 defines ==>. PRELAMB:def 18 :
definition
let IT be non
empty typestr ;
attr IT is
SynTypes_Calculus-like means :
Def19:
:: PRELAMB:def 19
( ( for
x being
type of
IT holds
<*x*> ==>. x ) & ( for
T being
FinSequence of the
carrier of
IT for
x,
y being
type of
IT st
T ^ <*y*> ==>. x holds
T ==>. x /" y ) & ( for
T being
FinSequence of the
carrier of
IT for
x,
y being
type of
IT st
<*y*> ^ T ==>. x holds
T ==>. y \ x ) & ( for
T,
X,
Y being
FinSequence of the
carrier 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 the
carrier 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 the
carrier 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 the
carrier of
IT for
x,
y being
type of
IT st
X ==>. x &
Y ==>. y holds
X ^ Y ==>. x * y ) );
end;
:: deftheorem Def19 defines SynTypes_Calculus-like PRELAMB:def 19 :
for
IT being non
empty typestr holds
(
IT is
SynTypes_Calculus-like iff ( ( for
x being
type of
IT holds
<*x*> ==>. x ) & ( for
T being
FinSequence of the
carrier of
IT for
x,
y being
type of
IT st
T ^ <*y*> ==>. x holds
T ==>. x /" y ) & ( for
T being
FinSequence of the
carrier of
IT for
x,
y being
type of
IT st
<*y*> ^ T ==>. x holds
T ==>. y \ x ) & ( for
T,
X,
Y being
FinSequence of the
carrier 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 the
carrier 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 the
carrier 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 the
carrier of
IT for
x,
y being
type of
IT st
X ==>. x &
Y ==>. y holds
X ^ Y ==>. x * y ) ) );
deffunc H2( typestr ) -> FinSequence of the carrier of $1 = <*> the carrier of $1;
Lm6:
for s being SynTypes_Calculus
for T, X being FinSequence of the carrier of s
for y, x, z being type of s st T ==>. y & X ^ <*x*> ==>. z holds
(X ^ <*(x /" y)*>) ^ T ==>. z
Lm7:
for s being SynTypes_Calculus
for T, Y being FinSequence of the carrier of s
for y, x, z being type of s st T ==>. y & <*x*> ^ Y ==>. z holds
(<*(x /" y)*> ^ T) ^ Y ==>. z
Lm8:
for s being SynTypes_Calculus
for T being FinSequence of the carrier of s
for y, x, z being type of s st T ==>. y & <*x*> ==>. z holds
<*(x /" y)*> ^ T ==>. z
Lm9:
for s being SynTypes_Calculus
for T, X being FinSequence of the carrier of s
for y, x, z being type of s st T ==>. y & X ^ <*x*> ==>. z holds
(X ^ T) ^ <*(y \ x)*> ==>. z
Lm10:
for s being SynTypes_Calculus
for T, Y being FinSequence of the carrier of s
for y, x, z being type of s st T ==>. y & <*x*> ^ Y ==>. z holds
(T ^ <*(y \ x)*>) ^ Y ==>. z
Lm11:
for s being SynTypes_Calculus
for T being FinSequence of the carrier of s
for y, x, z being type of s st T ==>. y & <*x*> ==>. z holds
T ^ <*(y \ x)*> ==>. z
Lm12:
for s being SynTypes_Calculus
for Y being FinSequence of the carrier of s
for x, y, z being type of s st (<*x*> ^ <*y*>) ^ Y ==>. z holds
<*(x * y)*> ^ Y ==>. z
Lm13:
for s being SynTypes_Calculus
for X being FinSequence of the carrier of s
for x, y, z being type of s st (X ^ <*x*>) ^ <*y*> ==>. z holds
X ^ <*(x * y)*> ==>. z
Lm14:
for s being SynTypes_Calculus
for x, y, z being type of s st <*x*> ^ <*y*> ==>. z holds
<*(x * y)*> ==>. z
theorem Th12: :: PRELAMB:12 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th13: :: PRELAMB:13 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th14: :: PRELAMB:14 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th15: :: PRELAMB:15 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: PRELAMB:16 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th17: :: PRELAMB:17 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th18: :: PRELAMB:18 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th19: :: PRELAMB:19 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem Th20: :: PRELAMB:20 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: PRELAMB:21 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: PRELAMB:22 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: PRELAMB:23 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: PRELAMB:24 :: Showing IDV graph ... (Click the Palm Tree again to close it)
:: deftheorem Def20 defines <==>. PRELAMB:def 20 :
theorem :: PRELAMB:25 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: PRELAMB:26 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: PRELAMB:27 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: PRELAMB:28 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: PRELAMB:29 :: Showing IDV graph ... (Click the Palm Tree again to close it)
theorem :: PRELAMB:30 :: Showing IDV graph ... (Click the Palm Tree again to close it)