theorem TBALemma:
for
T being non
empty TBAStruct st ( for
v4,
v3,
v2,
v1,
v0 being
Element of
T holds
Tern (
(Tern (v0,v1,v2)),
v3,
(Tern (v0,v1,v4)))
= Tern (
v0,
v1,
(Tern (v2,v3,v4))) ) & ( for
v1,
v0 being
Element of
T holds
Tern (
v0,
v1,
v1)
= v1 ) & ( for
v1,
v0 being
Element of
T holds
Tern (
v0,
v1,
(v1 `))
= v0 ) & ( for
v1,
v0 being
Element of
T holds
Tern (
v0,
v0,
v1)
= v0 ) holds
for
x,
y,
z,
u,
v,
v6,
w being
Element of
T holds
Tern (
(Tern (x,(x `),y)),
((Tern ((Tern (z,u,v)),w,(Tern (z,u,v6)))) `),
(Tern (u,(Tern (v6,w,v)),z)))
= y