let T be non empty TBAStruct ; :: thesis: ( ( 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 ) implies 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 )
assume A2: 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))) ; :: thesis: ( ex v1, v0 being Element of T st not Tern (v0,v1,v1) = v1 or ex v1, v0 being Element of T st not Tern (v0,v1,(v1 `)) = v0 or ex v1, v0 being Element of T st not Tern (v0,v0,v1) = v0 or 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 )
assume A3: for v1, v0 being Element of T holds Tern (v0,v1,v1) = v1 ; :: thesis: ( ex v1, v0 being Element of T st not Tern (v0,v1,(v1 `)) = v0 or ex v1, v0 being Element of T st not Tern (v0,v0,v1) = v0 or 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 )
assume A4: for v1, v0 being Element of T holds Tern (v0,v1,(v1 `)) = v0 ; :: thesis: ( ex v1, v0 being Element of T st not Tern (v0,v0,v1) = v0 or 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 )
assume A5: for v1, v0 being Element of T holds Tern (v0,v0,v1) = v0 ; :: thesis: 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
A11: for v103, v104, v102, v100 being Element of T holds Tern (v102,v103,(Tern (v100,v102,v104))) = Tern (v100,v102,(Tern (v102,v103,v104)))
proof
let v103, v104, v102, v100 be Element of T; :: thesis: Tern (v102,v103,(Tern (v100,v102,v104))) = Tern (v100,v102,(Tern (v102,v103,v104)))
Tern (v100,v102,v102) = v102 by A3;
hence Tern (v102,v103,(Tern (v100,v102,v104))) = Tern (v100,v102,(Tern (v102,v103,v104))) by A2; :: thesis: verum
end;
A15: for v103, v102, v104, v100 being Element of T holds Tern ((Tern (v100,v104,v102)),v103,v104) = Tern (v100,v104,(Tern (v102,v103,v104)))
proof
let v103, v102, v104, v100 be Element of T; :: thesis: Tern ((Tern (v100,v104,v102)),v103,v104) = Tern (v100,v104,(Tern (v102,v103,v104)))
Tern (v100,v104,v104) = v104 by A3;
hence Tern ((Tern (v100,v104,v102)),v103,v104) = Tern (v100,v104,(Tern (v102,v103,v104))) by A2; :: thesis: verum
end;
A19: for v103, v104, v101, v100 being Element of T holds Tern (v100,v103,(Tern (v100,v101,v104))) = Tern (v100,v101,(Tern ((v101 `),v103,v104)))
proof
let v103, v104, v101, v100 be Element of T; :: thesis: Tern (v100,v103,(Tern (v100,v101,v104))) = Tern (v100,v101,(Tern ((v101 `),v103,v104)))
Tern (v100,v101,(v101 `)) = v100 by A4;
hence Tern (v100,v103,(Tern (v100,v101,v104))) = Tern (v100,v101,(Tern ((v101 `),v103,v104))) by A2; :: thesis: verum
end;
A25: for v103, v100, v102 being Element of T holds Tern (v100,v103,(Tern (v102,v100,v103))) = Tern (v102,v100,v103)
proof
let v103, v100, v102 be Element of T; :: thesis: Tern (v100,v103,(Tern (v102,v100,v103))) = Tern (v102,v100,v103)
Tern (v100,v103,v103) = v103 by A3;
hence Tern (v100,v103,(Tern (v102,v100,v103))) = Tern (v102,v100,v103) by A11; :: thesis: verum
end;
A29: for v102, v101, v100 being Element of T holds Tern (v100,v101,v102) = Tern (v102,v100,(Tern (v100,v101,(v100 `))))
proof
let v102, v101, v100 be Element of T; :: thesis: Tern (v100,v101,v102) = Tern (v102,v100,(Tern (v100,v101,(v100 `))))
Tern (v102,v100,(v100 `)) = v102 by A4;
hence Tern (v100,v101,v102) = Tern (v102,v100,(Tern (v100,v101,(v100 `)))) by A11; :: thesis: verum
end;
A35: for v102, v100 being Element of T holds Tern (v100,(v100 `),v102) = Tern (v102,v100,(v100 `))
proof
let v102, v100 be Element of T; :: thesis: Tern (v100,(v100 `),v102) = Tern (v102,v100,(v100 `))
Tern (v102,v100,(v100 `)) = v102 by A4;
hence Tern (v100,(v100 `),v102) = Tern (v102,v100,(v100 `)) by A25; :: thesis: verum
end;
A38: for v1, v0 being Element of T holds Tern (v0,(v0 `),v1) = v1
proof
let v1, v0 be Element of T; :: thesis: Tern (v0,(v0 `),v1) = v1
Tern (v1,v0,(v0 `)) = v1 by A4;
hence Tern (v0,(v0 `),v1) = v1 by A35; :: thesis: verum
end;
A43: for v101, v103, v100 being Element of T holds Tern (v100,v103,v101) = Tern (v100,v101,(Tern ((v101 `),v103,v101)))
proof
let v101, v103, v100 be Element of T; :: thesis: Tern (v100,v103,v101) = Tern (v100,v101,(Tern ((v101 `),v103,v101)))
Tern (v100,v101,(v101 `)) = v100 by A4;
hence Tern (v100,v103,v101) = Tern (v100,v101,(Tern ((v101 `),v103,v101))) by A15; :: thesis: verum
end;
A49: for v101, v100 being Element of T holds Tern (v100,v100,(Tern (v100,v101,v101))) = Tern ((v101 `),v100,v101)
proof
let v101, v100 be Element of T; :: thesis: Tern (v100,v100,(Tern (v100,v101,v101))) = Tern ((v101 `),v100,v101)
Tern (v100,v101,(Tern ((v101 `),v100,v101))) = Tern (v100,v100,(Tern (v100,v101,v101))) by A19;
hence Tern (v100,v100,(Tern (v100,v101,v101))) = Tern ((v101 `),v100,v101) by A25; :: thesis: verum
end;
A52: for v1, v0 being Element of T holds Tern (v0,v0,v1) = Tern ((v1 `),v0,v1)
proof
let v1, v0 be Element of T; :: thesis: Tern (v0,v0,v1) = Tern ((v1 `),v0,v1)
Tern (v0,v1,v1) = v1 by A3;
hence Tern (v0,v0,v1) = Tern ((v1 `),v0,v1) by A49; :: thesis: verum
end;
A54: for v0, v1 being Element of T holds v0 = Tern ((v1 `),v0,v1)
proof
let v0, v1 be Element of T; :: thesis: v0 = Tern ((v1 `),v0,v1)
Tern (v0,v0,v1) = v0 by A5;
hence v0 = Tern ((v1 `),v0,v1) by A52; :: thesis: verum
end;
A58: for v2, v1, v0 being Element of T holds Tern (v0,v1,v2) = Tern (v0,v2,v1)
proof
let v2, v1, v0 be Element of T; :: thesis: Tern (v0,v1,v2) = Tern (v0,v2,v1)
Tern ((v1 `),v2,v1) = v2 by A54;
hence Tern (v0,v1,v2) = Tern (v0,v2,v1) by A43; :: thesis: verum
end;
A64: for v1, v0 being Element of T holds Tern (v0,v1,(v0 `)) = v1
proof
let v1, v0 be Element of T; :: thesis: Tern (v0,v1,(v0 `)) = v1
Tern (v0,(v0 `),v1) = Tern (v0,v1,(v0 `)) by A58;
hence Tern (v0,v1,(v0 `)) = v1 by A38; :: thesis: verum
end;
A66: for v2, v1, v0 being Element of T holds Tern (v0,v1,v2) = Tern (v1,v2,v0)
proof
let v2, v1, v0 be Element of T; :: thesis: Tern (v0,v1,v2) = Tern (v1,v2,v0)
Tern (v1,v2,(v1 `)) = v2 by A64;
hence Tern (v0,v1,v2) = Tern (v1,v2,v0) by A29; :: thesis: verum
end;
let x, y, z, u, v, v6, w be Element of T; :: thesis: Tern ((Tern (x,(x `),y)),((Tern ((Tern (z,u,v)),w,(Tern (z,u,v6)))) `),(Tern (u,(Tern (v6,w,v)),z))) = y
Tern (v,w,v6) = Tern (w,v6,v) by A66
.= Tern (w,v,v6) by A58
.= Tern (v6,w,v) by A66 ;
then VV: Tern (z,u,(Tern (v6,w,v))) = Tern ((Tern (z,u,v)),w,(Tern (z,u,v6))) by A2;
Tern ((Tern (x,(x `),y)),((Tern ((Tern (z,u,v)),w,(Tern (z,u,v6)))) `),(Tern (u,(Tern (v6,w,v)),z))) = Tern (y,((Tern ((Tern (z,u,v)),w,(Tern (z,u,v6)))) `),(Tern (u,(Tern (v6,w,v)),z))) by A38
.= Tern (y,((Tern ((Tern (z,u,v)),w,(Tern (z,u,v6)))) `),(Tern (z,u,(Tern (v6,w,v))))) by A66
.= Tern (y,(Tern (z,u,(Tern (v6,w,v)))),((Tern ((Tern (z,u,v)),w,(Tern (z,u,v6)))) `)) by A58
.= Tern ((Tern (z,u,(Tern (v6,w,v)))),((Tern ((Tern (z,u,v)),w,(Tern (z,u,v6)))) `),y) by A66
.= y by A38, VV ;
hence Tern ((Tern (x,(x `),y)),((Tern ((Tern (z,u,v)),w,(Tern (z,u,v6)))) `),(Tern (u,(Tern (v6,w,v)),z))) = y ; :: thesis: verum