src/HOL/ex/mesontest2.ML

 \  (\\<forall>X. siblings(left_child_of(X),right_child_of(X))) &        \
 \  (\\<forall>D E. equal(D::'a,E) --> equal(left_child_of(D),left_child_of(E))) &   \
 \  (\\<forall>F' G. equal(F'::'a,G) --> equal(negate(F'),negate(G))) &      \
 \  (\\<forall>H I' J. equal(H::'a,I') --> equal(or(H::'a,J),or(I'::'a,J))) &        \
 \  (\\<forall>K' M L. equal(K'::'a,L) --> equal(or(M::'a,K'),or(M::'a,L))) &        \
-\  (\\<forall>N O_ P. equal(N::'a,O_) --> equal(parent_of(N::'a,P),parent_of(O_::'a,P))) &     \
+\  (\\<forall>N O' P. equal(N::'a,O') --> equal(parent_of(N::'a,P),parent_of(O'::'a,P))) &     \
 \  (\\<forall>Q S' R. equal(Q::'a,R) --> equal(parent_of(S'::'a,Q),parent_of(S'::'a,R))) &  \
 \  (\\<forall>T' U. equal(T'::'a,U) --> equal(right_child_of(T'),right_child_of(U))) &      \
 \  (\\<forall>V W X. equal(V::'a,W) & contradictory(V::'a,X) --> contradictory(W::'a,X)) &  \
 \  (\\<forall>Y A1 Z. equal(Y::'a,Z) & contradictory(A1::'a,Y) --> contradictory(A1::'a,Z)) &       \
 \  (\\<forall>B1 C1 D1. equal(B1::'a,C1) & failure_node(B1::'a,D1) --> failure_node(C1::'a,D1)) &   \

 \  (\\<forall>X V1 V2 Y V3 V4. equal(X::'a,Y) --> equal(outer_pasch(V1::'a,V2,X,V3,V4),outer_pasch(V1::'a,V2,Y,V3,V4))) &   \
 \  (\\<forall>X V1 V2 V3 Y V4. equal(X::'a,Y) --> equal(outer_pasch(V1::'a,V2,V3,X,V4),outer_pasch(V1::'a,V2,V3,Y,V4))) &   \
 \  (\\<forall>X V1 V2 V3 V4 Y. equal(X::'a,Y) --> equal(outer_pasch(V1::'a,V2,V3,V4,X),outer_pasch(V1::'a,V2,V3,V4,Y))) &   \
 \  (\\<forall>A B C D E F'. equal(A::'a,B) --> equal(euclid1(A::'a,C,D,E,F'),euclid1(B::'a,C,D,E,F'))) &    \
 \  (\\<forall>G I' H J K' L. equal(G::'a,H) --> equal(euclid1(I'::'a,G,J,K',L),euclid1(I'::'a,H,J,K',L))) & \
-\  (\\<forall>M O_ P N Q R. equal(M::'a,N) --> equal(euclid1(O_::'a,P,M,Q,R),euclid1(O_::'a,P,N,Q,R))) &       \
+\  (\\<forall>M O' P N Q R. equal(M::'a,N) --> equal(euclid1(O'::'a,P,M,Q,R),euclid1(O'::'a,P,N,Q,R))) &       \
 \  (\\<forall>S' U V W T' X. equal(S'::'a,T') --> equal(euclid1(U::'a,V,W,S',X),euclid1(U::'a,V,W,T',X))) & \
 \  (\\<forall>Y A1 B1 C1 D1 Z. equal(Y::'a,Z) --> equal(euclid1(A1::'a,B1,C1,D1,Y),euclid1(A1::'a,B1,C1,D1,Z))) &   \
 \  (\\<forall>E1 F1 G1 H1 I1 J1. equal(E1::'a,F1) --> equal(euclid2(E1::'a,G1,H1,I1,J1),euclid2(F1::'a,G1,H1,I1,J1))) &     \
 \  (\\<forall>K1 M1 L1 N1 O1 P1. equal(K1::'a,L1) --> equal(euclid2(M1::'a,K1,N1,O1,P1),euclid2(M1::'a,L1,N1,O1,P1))) &     \
 \  (\\<forall>Q1 S1 T1 R1 U1 V1. equal(Q1::'a,R1) --> equal(euclid2(S1::'a,T1,Q1,U1,V1),euclid2(S1::'a,T1,R1,U1,V1))) &     \

 \  (\\<forall>X V1 V2 Y V3 V4. equal(X::'a,Y) --> equal(inner_pasch(V1::'a,V2,X,V3,V4),inner_pasch(V1::'a,V2,Y,V3,V4))) &   \
 \  (\\<forall>X V1 V2 V3 Y V4. equal(X::'a,Y) --> equal(inner_pasch(V1::'a,V2,V3,X,V4),inner_pasch(V1::'a,V2,V3,Y,V4))) &   \
 \  (\\<forall>X V1 V2 V3 V4 Y. equal(X::'a,Y) --> equal(inner_pasch(V1::'a,V2,V3,V4,X),inner_pasch(V1::'a,V2,V3,V4,Y))) &   \
 \  (\\<forall>A B C D E F'. equal(A::'a,B) --> equal(euclid1(A::'a,C,D,E,F'),euclid1(B::'a,C,D,E,F'))) &    \
 \  (\\<forall>G I' H J K' L. equal(G::'a,H) --> equal(euclid1(I'::'a,G,J,K',L),euclid1(I'::'a,H,J,K',L))) & \
-\  (\\<forall>M O_ P N Q R. equal(M::'a,N) --> equal(euclid1(O_::'a,P,M,Q,R),euclid1(O_::'a,P,N,Q,R))) &       \
+\  (\\<forall>M O' P N Q R. equal(M::'a,N) --> equal(euclid1(O'::'a,P,M,Q,R),euclid1(O'::'a,P,N,Q,R))) &       \
 \  (\\<forall>S' U V W T' X. equal(S'::'a,T') --> equal(euclid1(U::'a,V,W,S',X),euclid1(U::'a,V,W,T',X))) & \
 \  (\\<forall>Y A1 B1 C1 D1 Z. equal(Y::'a,Z) --> equal(euclid1(A1::'a,B1,C1,D1,Y),euclid1(A1::'a,B1,C1,D1,Z))) &   \
 \  (\\<forall>E1 F1 G1 H1 I1 J1. equal(E1::'a,F1) --> equal(euclid2(E1::'a,G1,H1,I1,J1),euclid2(F1::'a,G1,H1,I1,J1))) &     \
 \  (\\<forall>K1 M1 L1 N1 O1 P1. equal(K1::'a,L1) --> equal(euclid2(M1::'a,K1,N1,O1,P1),euclid2(M1::'a,L1,N1,O1,P1))) &     \
 \  (\\<forall>Q1 S1 T1 R1 U1 V1. equal(Q1::'a,R1) --> equal(euclid2(S1::'a,T1,Q1,U1,V1),euclid2(S1::'a,T1,R1,U1,V1))) &     \

 \  (\\<forall>X Y. equal(implies(X,Y),true) --> ordered(X,Y)) & \
 \  (\\<forall>A B C. equal(A,B) --> equal(big_V(A,C),big_V(B,C))) &     \
 \  (\\<forall>D F' E. equal(D,E) --> equal(big_V(F',D),big_V(F',E))) &  \
 \  (\\<forall>G H I'. equal(G,H) --> equal(big_hat(G,I'),big_hat(H,I'))) &      \
 \  (\\<forall>J L K'. equal(J,K') --> equal(big_hat(L,J),big_hat(L,K'))) &      \
-\  (\\<forall>M N O_. equal(M,N) & ordered(M,O_) --> ordered(N,O_)) &      \
+\  (\\<forall>M N O'. equal(M,N) & ordered(M,O') --> ordered(N,O')) &      \
 \  (\\<forall>P R Q. equal(P,Q) & ordered(R,P) --> ordered(R,Q)) &      \
 \  (ordered(x,y)) &     \
 \  (~ordered(implies(z,x),implies(z,y))) --> False",
   meson_tac 1);
 

 val SET004_0_eq =
   "(\\<forall>D E F'. equal(D::'a,E) --> equal(apply(D::'a,F'),apply(E::'a,F'))) &  \
 \  (\\<forall>G I' H. equal(G::'a,H) --> equal(apply(I'::'a,G),apply(I'::'a,H))) &  \
 \  (\\<forall>J K'. equal(J::'a,K') --> equal(cantor(J),cantor(K'))) &      \
 \  (\\<forall>L M. equal(L::'a,M) --> equal(complement(L),complement(M))) & \
-\  (\\<forall>N O_ P. equal(N::'a,O_) --> equal(compos(N::'a,P),compos(O_::'a,P))) & \
+\  (\\<forall>N O' P. equal(N::'a,O') --> equal(compos(N::'a,P),compos(O'::'a,P))) & \
 \  (\\<forall>Q S' R. equal(Q::'a,R) --> equal(compos(S'::'a,Q),compos(S'::'a,R))) &      \
 \  (\\<forall>T' U V. equal(T'::'a,U) --> equal(cross_product(T'::'a,V),cross_product(U::'a,V))) &  \
 \  (\\<forall>W Y X. equal(W::'a,X) --> equal(cross_product(Y::'a,W),cross_product(Y::'a,X))) &     \
 \  (\\<forall>Z A1. equal(Z::'a,A1) --> equal(diagonalise(Z),diagonalise(A1))) &    \
 \  (\\<forall>B1 C1 D1. equal(B1::'a,C1) --> equal(difference(B1::'a,D1),difference(C1::'a,D1))) &  \

 val NUM004_0_eq =
   "(\\<forall>D E. equal(D::'a,E) --> equal(integer_of(D),integer_of(E))) & \
 \  (\\<forall>F' G H. equal(F'::'a,G) --> equal(least(F'::'a,H),least(G::'a,H))) &  \
 \  (\\<forall>I' K' J. equal(I'::'a,J) --> equal(least(K'::'a,I'),least(K'::'a,J))) &       \
 \  (\\<forall>L M N. equal(L::'a,M) --> equal(not_well_ordering(L::'a,N),not_well_ordering(M::'a,N))) &     \
-\  (\\<forall>O_ Q P. equal(O_::'a,P) --> equal(not_well_ordering(Q::'a,O_),not_well_ordering(Q::'a,P))) &     \
+\  (\\<forall>O' Q P. equal(O'::'a,P) --> equal(not_well_ordering(Q::'a,O'),not_well_ordering(Q::'a,P))) &     \
 \  (\\<forall>R S' T'. equal(R::'a,S') --> equal(ordinal_add(R::'a,T'),ordinal_add(S'::'a,T'))) &   \
 \  (\\<forall>U W V. equal(U::'a,V) --> equal(ordinal_add(W::'a,U),ordinal_add(W::'a,V))) & \
 \  (\\<forall>X Y Z. equal(X::'a,Y) --> equal(ordinal_multiply(X::'a,Z),ordinal_multiply(Y::'a,Z))) &       \
 \  (\\<forall>A1 C1 B1. equal(A1::'a,B1) --> equal(ordinal_multiply(C1::'a,A1),ordinal_multiply(C1::'a,B1))) &      \
 \  (\\<forall>F1 G1 H1 I1. equal(F1::'a,G1) --> equal(recursion(F1::'a,H1,I1),recursion(G1::'a,H1,I1))) &   \

 \  (\\<forall>I' J K'. equal(I'::'a,J) --> equal(multiply(I'::'a,K'),multiply(J::'a,K'))) & \
 \  (\\<forall>L N M. equal(L::'a,M) --> equal(multiply(N::'a,L),multiply(N::'a,M))) &       \
 \  (\\<forall>A B C D. equal(A::'a,B) --> equal(associator(A::'a,C,D),associator(B::'a,C,D))) &     \
 \  (\\<forall>E G F' H. equal(E::'a,F') --> equal(associator(G::'a,E,H),associator(G::'a,F',H))) &  \
 \  (\\<forall>I' K' L J. equal(I'::'a,J) --> equal(associator(K'::'a,L,I'),associator(K'::'a,L,J))) &       \
-\  (\\<forall>M N O_. equal(M::'a,N) --> equal(commutator(M::'a,O_),commutator(N::'a,O_))) &   \
+\  (\\<forall>M N O'. equal(M::'a,N) --> equal(commutator(M::'a,O'),commutator(N::'a,O'))) &   \
 \  (\\<forall>P R Q. equal(P::'a,Q) --> equal(commutator(R::'a,P),commutator(R::'a,Q))) &   \
 \  (\\<forall>Y X. equal(add(X::'a,Y),add(Y::'a,X))) &  \
 \  (\\<forall>X Y Z. equal(add(add(X::'a,Y),Z),add(X::'a,add(Y::'a,Z)))) &  \
 \  (\\<forall>X. equal(add(X::'a,additive_identity),X)) &   \
 \  (\\<forall>X. equal(add(additive_identity::'a,X),X)) &   \

 \  (\\<forall>X Y Z. equal(associator(X::'a,Y,Z),add(multiply(multiply(X::'a,Y),Z),additive_inverse(multiply(X::'a,multiply(Y::'a,Z)))))) &     \
 \  (\\<forall>X Y. equal(commutator(X::'a,Y),add(multiply(Y::'a,X),additive_inverse(multiply(X::'a,Y))))) & \
 \  (\\<forall>D E F'. equal(D::'a,E) --> equal(add(D::'a,F'),add(E::'a,F'))) &      \
 \  (\\<forall>G I' H. equal(G::'a,H) --> equal(add(I'::'a,G),add(I'::'a,H))) &      \
 \  (\\<forall>J K'. equal(J::'a,K') --> equal(additive_inverse(J),additive_inverse(K'))) &  \
-\  (\\<forall>L M N O_. equal(L::'a,M) --> equal(associator(L::'a,N,O_),associator(M::'a,N,O_))) &     \
+\  (\\<forall>L M N O'. equal(L::'a,M) --> equal(associator(L::'a,N,O'),associator(M::'a,N,O'))) &     \
 \  (\\<forall>P R Q S'. equal(P::'a,Q) --> equal(associator(R::'a,P,S'),associator(R::'a,Q,S'))) &  \
 \  (\\<forall>T' V W U. equal(T'::'a,U) --> equal(associator(V::'a,W,T'),associator(V::'a,W,U))) &  \
 \  (\\<forall>X Y Z. equal(X::'a,Y) --> equal(commutator(X::'a,Z),commutator(Y::'a,Z))) &   \
 \  (\\<forall>A1 C1 B1. equal(A1::'a,B1) --> equal(commutator(C1::'a,A1),commutator(C1::'a,B1))) &  \
 \  (\\<forall>D1 E1 F1. equal(D1::'a,E1) --> equal(multiply(D1::'a,F1),multiply(E1::'a,F1))) &      \

 \  (\\<forall>G I' H. equal(G::'a,H) --> equal(add(I'::'a,G),add(I'::'a,H))) &      \
 \  (\\<forall>J K'. equal(J::'a,K') --> equal(additive_inverse(J),additive_inverse(K'))) &  \
 \  (\\<forall>D1 E1 F1. equal(D1::'a,E1) --> equal(multiply(D1::'a,F1),multiply(E1::'a,F1))) &      \
 \  (\\<forall>G1 I1 H1. equal(G1::'a,H1) --> equal(multiply(I1::'a,G1),multiply(I1::'a,H1))) &      \
 \  (\\<forall>X Y Z. equal(associator(X::'a,Y,Z),add(multiply(multiply(X::'a,Y),Z),additive_inverse(multiply(X::'a,multiply(Y::'a,Z)))))) &     \
-\  (\\<forall>L M N O_. equal(L::'a,M) --> equal(associator(L::'a,N,O_),associator(M::'a,N,O_))) &     \
+\  (\\<forall>L M N O'. equal(L::'a,M) --> equal(associator(L::'a,N,O'),associator(M::'a,N,O'))) &     \
 \  (\\<forall>P R Q S'. equal(P::'a,Q) --> equal(associator(R::'a,P,S'),associator(R::'a,Q,S'))) &  \
 \  (\\<forall>T' V W U. equal(T'::'a,U) --> equal(associator(V::'a,W,T'),associator(V::'a,W,U))) &  \
 \  (\\<forall>X Y. ~equal(multiply(multiply(Y::'a,X),Y),multiply(Y::'a,multiply(X::'a,Y)))) &       \
 \  (\\<forall>X Y Z. ~equal(associator(Y::'a,X,Z),additive_inverse(associator(X::'a,Y,Z)))) &   \
 \  (\\<forall>X Y Z. ~equal(associator(Z::'a,Y,X),additive_inverse(associator(X::'a,Y,Z)))) &   \

 \  (\\<forall>Y X. equal(negate(add(negate(add(X::'a,Y)),negate(add(X::'a,negate(Y))))),X)) &   \
 \  (\\<forall>A B C. equal(A::'a,B) --> equal(add(A::'a,C),add(B::'a,C))) & \
 \  (\\<forall>D F' E. equal(D::'a,E) --> equal(add(F'::'a,D),add(F'::'a,E))) &      \
 \  (\\<forall>G H. equal(G::'a,H) --> equal(negate(G),negate(H))) & \
 \  (\\<forall>J K' L. equal(J::'a,K') --> equal(multiply(J::'a,L),multiply(K'::'a,L))) &    \
-\  (\\<forall>M O_ N. equal(M::'a,N) --> equal(multiply(O_::'a,M),multiply(O_::'a,N))) &       \
+\  (\\<forall>M O' N. equal(M::'a,N) --> equal(multiply(O'::'a,M),multiply(O'::'a,N))) &       \
 \  (\\<forall>P Q. equal(P::'a,Q) --> equal(successor(P),successor(Q))) &   \
 \  (\\<forall>R S'. equal(R::'a,S') & positive_integer(R) --> positive_integer(S')) &       \
 \  (\\<forall>X. equal(multiply(One::'a,X),X)) &    \
 \  (\\<forall>V X. positive_integer(X) --> equal(multiply(successor(V),X),add(X::'a,multiply(V::'a,X)))) &      \
 \  (positive_integer(One)) &    \

 \  (\\<forall>P8 R8 Q8. equal(P8::'a,Q8) --> equal(f8(R8::'a,P8),f8(R8::'a,Q8))) &  \
 \  (\\<forall>S8 T8 U8. equal(S8::'a,T8) --> equal(f9(S8::'a,U8),f9(T8::'a,U8))) &  \
 \  (\\<forall>V8 X8 W8. equal(V8::'a,W8) --> equal(f9(X8::'a,V8),f9(X8::'a,W8))) &  \
 \  (\\<forall>G H I'. equal(G::'a,H) --> equal(f10(G::'a,I'),f10(H::'a,I'))) &      \
 \  (\\<forall>J L K'. equal(J::'a,K') --> equal(f10(L::'a,J),f10(L::'a,K'))) &      \
-\  (\\<forall>M N O_. equal(M::'a,N) --> equal(f11(M::'a,O_),f11(N::'a,O_))) & \
+\  (\\<forall>M N O'. equal(M::'a,N) --> equal(f11(M::'a,O'),f11(N::'a,O'))) & \
 \  (\\<forall>P R Q. equal(P::'a,Q) --> equal(f11(R::'a,P),f11(R::'a,Q))) & \
 \  (\\<forall>S' T' U. equal(S'::'a,T') --> equal(f12(S'::'a,U),f12(T'::'a,U))) &   \
 \  (\\<forall>V X W. equal(V::'a,W) --> equal(f12(X::'a,V),f12(X::'a,W))) & \
 \  (\\<forall>Y Z A1. equal(Y::'a,Z) --> equal(f13(Y::'a,A1),f13(Z::'a,A1))) &      \
 \  (\\<forall>B1 D1 C1. equal(B1::'a,C1) --> equal(f13(D1::'a,B1),f13(D1::'a,C1))) &        \

 \  (\\<forall>I7 K7 L7 M7 N7 J7. equal(I7::'a,J7) --> equal(f33(K7::'a,L7,M7,N7,I7),f33(K7::'a,L7,M7,N7,J7))) &     \
 \  (\\<forall>A B C. equal(A::'a,B) --> equal(apply(A::'a,C),apply(B::'a,C))) &     \
 \  (\\<forall>D F' E. equal(D::'a,E) --> equal(apply(F'::'a,D),apply(F'::'a,E))) &  \
 \  (\\<forall>G H I' J. equal(G::'a,H) --> equal(apply_to_two_arguments(G::'a,I',J),apply_to_two_arguments(H::'a,I',J))) &  \
 \  (\\<forall>K' M L N. equal(K'::'a,L) --> equal(apply_to_two_arguments(M::'a,K',N),apply_to_two_arguments(M::'a,L,N))) &  \
-\  (\\<forall>O_ Q R P. equal(O_::'a,P) --> equal(apply_to_two_arguments(Q::'a,R,O_),apply_to_two_arguments(Q::'a,R,P))) &     \
+\  (\\<forall>O' Q R P. equal(O'::'a,P) --> equal(apply_to_two_arguments(Q::'a,R,O'),apply_to_two_arguments(Q::'a,R,P))) &     \
 \  (\\<forall>S' T'. equal(S'::'a,T') --> equal(complement(S'),complement(T'))) &   \
 \  (\\<forall>U V W. equal(U::'a,V) --> equal(composition(U::'a,W),composition(V::'a,W))) & \
 \  (\\<forall>X Z Y. equal(X::'a,Y) --> equal(composition(Z::'a,X),composition(Z::'a,Y))) & \
 \  (\\<forall>A1 B1. equal(A1::'a,B1) --> equal(inv1 A1,inv1 B1)) &       \
 \  (\\<forall>C1 D1 E1. equal(C1::'a,D1) --> equal(cross_product(C1::'a,E1),cross_product(D1::'a,E1))) &    \