meson/test/selftest.sml

2949    (!Z X. member(Z,second(X)) ==> little_set(f6(Z,X))) /\
2951    (!Z X. member(Z,second(X)) ==> equal(X,ordered_pair(f6(Z,X),f7(Z,X)))) /\
3079    (!A8 B8 C8. equal(A8,B8) ==> equal(f6(A8,C8),f6(B8,C8))) /\
3080    (!D8 F8 E8. equal(D8,E8) ==> equal(f6(F8,D8),f6(F8,E8))) /\
3309    (!X Vf Y Vb1 Vb2. basis(X,Vf) /\ element_of_set(Y,X) /\ element_of_collection(Vb1,Vf) /\ element_of_collection(Vb2,Vf) /\ element_of_set(Y,intersection_of_sets(Vb1,Vb2)) ==> element_of_set(Y,f6(X,Vf,Y,Vb1,Vb2))) /\
3310    (!X Y Vb1 Vb2 Vf. basis(X,Vf) /\ element_of_set(Y,X) /\ element_of_collection(Vb1,Vf) /\ element_of_collection(Vb2,Vf) /\ element_of_set(Y,intersection_of_sets(Vb1,Vb2)) ==> element_of_collection(f6(X,Vf,Y,Vb1,Vb2),Vf)) /\
3311    (!X Vf Y Vb1 Vb2. basis(X,Vf) /\ element_of_set(Y,X) /\ element_of_collection(Vb1,Vf) /\ element_of_collection(Vb2,Vf) /\ element_of_set(Y,intersection_of_sets(Vb1,Vb2)) ==> subset_sets(f6(X,Vf,Y,Vb1,Vb2),intersection_of_sets(Vb1,Vb2))) /\
3402    (!X Vf Y Vb1 Vb2. basis(X,Vf) /\ element_of_set(Y,X) /\ element_of_collection(Vb1,Vf) /\ element_of_collection(Vb2,Vf) /\ element_of_set(Y,intersection_of_sets(Vb1,Vb2)) ==> element_of_set(Y,f6(X,Vf,Y,Vb1,Vb2))) /\
3403    (!X Y Vb1 Vb2 Vf. basis(X,Vf) /\ element_of_set(Y,X) /\ element_of_collection(Vb1,Vf) /\ element_of_collection(Vb2,Vf) /\ element_of_set(Y,intersection_of_sets(Vb1,Vb2)) ==> element_of_collection(f6(X,Vf,Y,Vb1,Vb2),Vf)) /\
3404    (!X Vf Y Vb1 Vb2. basis(X,Vf) /\ element_of_set(Y,X) /\ element_of_collection(Vb1,Vf) /\ element_of_collection(Vb2,Vf) /\ element_of_set(Y,intersection_of_sets(Vb1,Vb2)) ==> subset_sets(f6(X,Vf,Y,Vb1,Vb2),intersection_of_sets(Vb1,Vb2))) /\