meson/test/selftest.sml

789    (!X Y W V. between(X,Y,extension(X,Y,W,V))) /\
790    (!X Y W V. equidistant(Y,extension(X,Y,W,V),W,V)) /\
819    (!X Y V1 V2 V3. equal(X,Y) ==> equal(extension(X,V1,V2,V3),extension(Y,V1,V2,V3))) /\
820    (!X V1 Y V2 V3. equal(X,Y) ==> equal(extension(V1,X,V2,V3),extension(V1,Y,V2,V3))) /\
821    (!X V1 V2 Y V3. equal(X,Y) ==> equal(extension(V1,V2,X,V3),extension(V1,V2,Y,V3))) /\
822    (!X V1 V2 V3 Y. equal(X,Y) ==> equal(extension(V1,V2,V3,X),extension(V1,V2,V3,Y))) /\
839    (!X Y W V. between(X,Y,extension(X,Y,W,V))) /\
840    (!X Y W V. equidistant(Y,extension(X,Y,W,V),W,V)) /\
876    (!X Y V1 V2 V3. equal(X,Y) ==> equal(extension(X,V1,V2,V3),extension(Y,V1,V2,V3))) /\
877    (!X V1 Y V2 V3. equal(X,Y) ==> equal(extension(V1,X,V2,V3),extension(V1,Y,V2,V3))) /\
878    (!X V1 V2 Y V3. equal(X,Y) ==> equal(extension(V1,V2,X,V3),extension(V1,V2,Y,V3))) /\
879    (!X V1 V2 V3 Y. equal(X,Y) ==> equal(extension(V1,V2,V3,X),extension(V1,V2,V3,Y))) /\
897    (!X Y W V. between(X,Y,extension(X,Y,W,V))) /\
898    (!X Y W V. equidistant(Y,extension(X,Y,W,V),W,V)) /\
934    (!X Y V1 V2 V3. equal(X,Y) ==> equal(extension(X,V1,V2,V3),extension(Y,V1,V2,V3))) /\
935    (!X V1 Y V2 V3. equal(X,Y) ==> equal(extension(V1,X,V2,V3),extension(V1,Y,V2,V3))) /\
936    (!X V1 V2 Y V3. equal(X,Y) ==> equal(extension(V1,V2,X,V3),extension(V1,V2,Y,V3))) /\
937    (!X V1 V2 V3 Y. equal(X,Y) ==> equal(extension(V1,V2,V3,X),extension(V1,V2,V3,Y))) /\
944    (!U V. equal(reflection(U,V),extension(U,V,U,V))) /\
956    (!U V W. equal(V,extension(U,V,W,W))) /\
957    (!W X U V Y. equal(Y,extension(U,V,W,X)) ==> between(U,V,Y)) /\
968    (~equal(w,extension(u,v,v,w))) ==> F���;
978    (!X Y W V. between(X,Y,extension(X,Y,W,V))) /\
979    (!X Y W V. equidistant(Y,extension(X,Y,W,V),W,V)) /\
1015    (!X Y V1 V2 V3. equal(X,Y) ==> equal(extension(X,V1,V2,V3),extension(Y,V1,V2,V3))) /\
1016    (!X V1 Y V2 V3. equal(X,Y) ==> equal(extension(V1,X,V2,V3),extension(V1,Y,V2,V3))) /\
1017    (!X V1 V2 Y V3. equal(X,Y) ==> equal(extension(V1,V2,X,V3),extension(V1,V2,Y,V3))) /\
1018    (!X V1 V2 V3 Y. equal(X,Y) ==> equal(extension(V1,V2,V3,X),extension(V1,V2,V3,Y))) /\
1025    (!U V. equal(reflection(U,V),extension(U,V,U,V))) /\