converse -> ^-1
authornipkow
Tue Jun 17 09:01:56 1997 +0200 (1997-06-17)
changeset 343954785105178c
parent 3438 8d63ff01d37e
child 3440 22db7a9cbb52
converse -> ^-1
src/HOL/Finite.ML
src/HOL/IMP/Transition.ML
src/HOL/Integ/Equiv.ML
src/HOL/Lambda/Commutation.ML
src/HOL/Lambda/Commutation.thy
src/HOL/Relation.ML
src/HOL/Relation.thy
src/HOL/Trancl.ML
src/HOL/WF.ML
src/HOL/ex/mesontest2.ML
     1.1 --- a/src/HOL/Finite.ML	Mon Jun 16 14:25:33 1997 +0200
     1.2 +++ b/src/HOL/Finite.ML	Tue Jun 17 09:01:56 1997 +0200
     1.3 @@ -174,22 +174,22 @@
     1.4  qed "finite_Pow_iff";
     1.5  AddIffs [finite_Pow_iff];
     1.6  
     1.7 -goal Finite.thy "finite(converse r) = finite r";
     1.8 -by(subgoal_tac "converse r = (%(x,y).(y,x))``r" 1);
     1.9 +goal Finite.thy "finite(r^-1) = finite r";
    1.10 +by(subgoal_tac "r^-1 = (%(x,y).(y,x))``r" 1);
    1.11   by(Asm_simp_tac 1);
    1.12   br iffI 1;
    1.13    be (rewrite_rule [inj_onto_def] finite_imageD) 1;
    1.14    by(simp_tac (!simpset setloop (split_tac[expand_split])) 1);
    1.15   be finite_imageI 1;
    1.16 -by(simp_tac (!simpset addsimps [converse_def,image_def]) 1);
    1.17 +by(simp_tac (!simpset addsimps [inverse_def,image_def]) 1);
    1.18  by(Auto_tac());
    1.19   br bexI 1;
    1.20   ba 2;
    1.21   by(Simp_tac 1);
    1.22  by(split_all_tac 1);
    1.23  by(Asm_full_simp_tac 1);
    1.24 -qed "finite_converse";
    1.25 -AddIffs [finite_converse];
    1.26 +qed "finite_inverse";
    1.27 +AddIffs [finite_inverse];
    1.28  
    1.29  section "Finite cardinality -- 'card'";
    1.30  
     2.1 --- a/src/HOL/IMP/Transition.ML	Mon Jun 16 14:25:33 1997 +0200
     2.2 +++ b/src/HOL/IMP/Transition.ML	Tue Jun 17 09:01:56 1997 +0200
     2.3 @@ -128,7 +128,7 @@
     2.4  goal Transition.thy
     2.5   "!!c1. (c1,s1) -*-> (SKIP,s2) ==> \
     2.6  \ (c2,s2) -*-> cs3 --> (c1;c2,s1) -*-> cs3";
     2.7 -by (etac converse_rtrancl_induct2 1);
     2.8 +by (etac inverse_rtrancl_induct2 1);
     2.9  by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
    2.10  by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
    2.11  qed_spec_mp "my_lemma1";
     3.1 --- a/src/HOL/Integ/Equiv.ML	Mon Jun 16 14:25:33 1997 +0200
     3.2 +++ b/src/HOL/Integ/Equiv.ML	Tue Jun 17 09:01:56 1997 +0200
     3.3 @@ -12,22 +12,22 @@
     3.4  
     3.5  Delrules [equalityI];
     3.6  
     3.7 -(*** Suppes, Theorem 70: r is an equiv relation iff converse(r) O r = r ***)
     3.8 +(*** Suppes, Theorem 70: r is an equiv relation iff r^-1 O r = r ***)
     3.9  
    3.10 -(** first half: equiv A r ==> converse(r) O r = r **)
    3.11 +(** first half: equiv A r ==> r^-1 O r = r **)
    3.12  
    3.13 -goalw Equiv.thy [trans_def,sym_def,converse_def]
    3.14 -    "!!r. [| sym(r); trans(r) |] ==> converse(r) O r <= r";
    3.15 -by (fast_tac (!claset addSEs [converseD]) 1);
    3.16 +goalw Equiv.thy [trans_def,sym_def,inverse_def]
    3.17 +    "!!r. [| sym(r); trans(r) |] ==> r^-1 O r <= r";
    3.18 +by (fast_tac (!claset addSEs [inverseD]) 1);
    3.19  qed "sym_trans_comp_subset";
    3.20  
    3.21  goalw Equiv.thy [refl_def]
    3.22 -    "!!A r. refl A r ==> r <= converse(r) O r";
    3.23 +    "!!A r. refl A r ==> r <= r^-1 O r";
    3.24  by (fast_tac (!claset addIs [compI]) 1);
    3.25  qed "refl_comp_subset";
    3.26  
    3.27  goalw Equiv.thy [equiv_def]
    3.28 -    "!!A r. equiv A r ==> converse(r) O r = r";
    3.29 +    "!!A r. equiv A r ==> r^-1 O r = r";
    3.30  by (rtac equalityI 1);
    3.31  by (REPEAT (ares_tac [sym_trans_comp_subset, refl_comp_subset] 1
    3.32       ORELSE etac conjE 1));
    3.33 @@ -35,7 +35,7 @@
    3.34  
    3.35  (*second half*)
    3.36  goalw Equiv.thy [equiv_def,refl_def,sym_def,trans_def]
    3.37 -    "!!A r. [| converse(r) O r = r;  Domain(r) = A |] ==> equiv A r";
    3.38 +    "!!A r. [| r^-1 O r = r;  Domain(r) = A |] ==> equiv A r";
    3.39  by (etac equalityE 1);
    3.40  by (subgoal_tac "ALL x y. (x,y) : r --> (y,x) : r" 1);
    3.41  by (Step_tac 1);
     4.1 --- a/src/HOL/Lambda/Commutation.ML	Mon Jun 16 14:25:33 1997 +0200
     4.2 +++ b/src/HOL/Lambda/Commutation.ML	Tue Jun 17 09:01:56 1997 +0200
     4.3 @@ -91,7 +91,7 @@
     4.4  by (safe_tac HOL_cs);
     4.5   by (blast_tac (HOL_cs addIs
     4.6        [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
     4.7 -       rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
     4.8 +       rtrancl_inverseI, inverseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
     4.9  by (etac rtrancl_induct 1);
    4.10   by (Blast_tac 1);
    4.11  by (Blast.depth_tac (!claset delrules [rtrancl_refl] 
     5.1 --- a/src/HOL/Lambda/Commutation.thy	Mon Jun 16 14:25:33 1997 +0200
     5.2 +++ b/src/HOL/Lambda/Commutation.thy	Tue Jun 17 09:01:56 1997 +0200
     5.3 @@ -21,7 +21,7 @@
     5.4    diamond_def "diamond R   == commute R R"
     5.5  
     5.6    Church_Rosser_def "Church_Rosser(R) ==   
     5.7 -  !x y. (x,y) : (R Un converse(R))^* --> (? z. (x,z) : R^* & (y,z) : R^*)"
     5.8 +  !x y. (x,y) : (R Un R^-1)^* --> (? z. (x,z) : R^* & (y,z) : R^*)"
     5.9  
    5.10  translations
    5.11    "confluent R" == "diamond(R^*)"
     6.1 --- a/src/HOL/Relation.ML	Mon Jun 16 14:25:33 1997 +0200
     6.2 +++ b/src/HOL/Relation.ML	Tue Jun 17 09:01:56 1997 +0200
     6.3 @@ -75,25 +75,25 @@
     6.4  by (Blast_tac 1);
     6.5  qed "transD";
     6.6  
     6.7 -(** Natural deduction for converse(r) **)
     6.8 +(** Natural deduction for r^-1 **)
     6.9  
    6.10 -goalw Relation.thy [converse_def] "!!a b r. ((a,b):converse r) = ((b,a):r)";
    6.11 +goalw Relation.thy [inverse_def] "!!a b r. ((a,b): r^-1) = ((b,a):r)";
    6.12  by (Simp_tac 1);
    6.13 -qed "converse_iff";
    6.14 +qed "inverse_iff";
    6.15  
    6.16 -AddIffs [converse_iff];
    6.17 +AddIffs [inverse_iff];
    6.18  
    6.19 -goalw Relation.thy [converse_def] "!!a b r. (a,b):r ==> (b,a):converse(r)";
    6.20 +goalw Relation.thy [inverse_def] "!!a b r. (a,b):r ==> (b,a): r^-1";
    6.21  by (Simp_tac 1);
    6.22 -qed "converseI";
    6.23 +qed "inverseI";
    6.24  
    6.25 -goalw Relation.thy [converse_def] "!!a b r. (a,b) : converse(r) ==> (b,a) : r";
    6.26 +goalw Relation.thy [inverse_def] "!!a b r. (a,b) : r^-1 ==> (b,a) : r";
    6.27  by (Blast_tac 1);
    6.28 -qed "converseD";
    6.29 +qed "inverseD";
    6.30  
    6.31 -(*More general than converseD, as it "splits" the member of the relation*)
    6.32 -qed_goalw "converseE" Relation.thy [converse_def]
    6.33 -    "[| yx : converse(r);  \
    6.34 +(*More general than inverseD, as it "splits" the member of the relation*)
    6.35 +qed_goalw "inverseE" Relation.thy [inverse_def]
    6.36 +    "[| yx : r^-1;  \
    6.37  \       !!x y. [| yx=(y,x);  (x,y):r |] ==> P \
    6.38  \    |] ==> P"
    6.39   (fn [major,minor]=>
    6.40 @@ -101,16 +101,16 @@
    6.41      (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1)),
    6.42      (assume_tac 1) ]);
    6.43  
    6.44 -AddSEs [converseE];
    6.45 +AddSEs [inverseE];
    6.46  
    6.47 -goalw Relation.thy [converse_def] "converse(converse R) = R";
    6.48 +goalw Relation.thy [inverse_def] "(r^-1)^-1 = r";
    6.49  by (Blast_tac 1);
    6.50 -qed "converse_converse";
    6.51 -Addsimps [converse_converse];
    6.52 +qed "inverse_inverse";
    6.53 +Addsimps [inverse_inverse];
    6.54  
    6.55 -goal Relation.thy "converse(r O s) = converse s O converse r";
    6.56 +goal Relation.thy "(r O s)^-1 = s^-1 O r^-1";
    6.57  by(Blast_tac 1);
    6.58 -qed "converse_comp";
    6.59 +qed "inverse_comp";
    6.60  
    6.61  (** Domain **)
    6.62  
    6.63 @@ -133,14 +133,14 @@
    6.64  (** Range **)
    6.65  
    6.66  qed_goalw "RangeI" Relation.thy [Range_def] "!!a b r.(a,b): r ==> b : Range(r)"
    6.67 - (fn _ => [ (etac (converseI RS DomainI) 1) ]);
    6.68 + (fn _ => [ (etac (inverseI RS DomainI) 1) ]);
    6.69  
    6.70  qed_goalw "RangeE" Relation.thy [Range_def]
    6.71      "[| b : Range(r);  !!x. (x,b): r ==> P |] ==> P"
    6.72   (fn major::prems=>
    6.73    [ (rtac (major RS DomainE) 1),
    6.74      (resolve_tac prems 1),
    6.75 -    (etac converseD 1) ]);
    6.76 +    (etac inverseD 1) ]);
    6.77  
    6.78  AddIs  [RangeI];
    6.79  AddSEs [RangeE];
     7.1 --- a/src/HOL/Relation.thy	Mon Jun 16 14:25:33 1997 +0200
     7.2 +++ b/src/HOL/Relation.thy	Tue Jun 17 09:01:56 1997 +0200
     7.3 @@ -9,7 +9,7 @@
     7.4      id          :: "('a * 'a)set"               (*the identity relation*)
     7.5      O           :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60)
     7.6      trans       :: "('a * 'a)set => bool"       (*transitivity predicate*)
     7.7 -    converse    :: "('a*'b) set => ('b*'a) set"
     7.8 +    inverse    :: "('a*'b) set => ('b*'a) set"     ("(_^-1)" [1000] 1000)
     7.9      "^^"        :: "[('a*'b) set,'a set] => 'b set" (infixl 90)
    7.10      Domain      :: "('a*'b) set => 'a set"
    7.11      Range       :: "('a*'b) set => 'b set"
    7.12 @@ -17,8 +17,8 @@
    7.13      id_def        "id == {p. ? x. p = (x,x)}"
    7.14      comp_def      "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
    7.15      trans_def     "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)"
    7.16 -    converse_def  "converse(r) == {(y,x). (x,y):r}"
    7.17 +    inverse_def   "r^-1 == {(y,x). (x,y):r}"
    7.18      Domain_def    "Domain(r) == {x. ? y. (x,y):r}"
    7.19 -    Range_def     "Range(r) == Domain(converse(r))"
    7.20 +    Range_def     "Range(r) == Domain(r^-1)"
    7.21      Image_def     "r ^^ s == {y. ? x:s. (x,y):r}"
    7.22  end
     8.1 --- a/src/HOL/Trancl.ML	Mon Jun 16 14:25:33 1997 +0200
     8.2 +++ b/src/HOL/Trancl.ML	Tue Jun 17 09:01:56 1997 +0200
     8.3 @@ -138,49 +138,49 @@
     8.4  qed "rtrancl_reflcl";
     8.5  Addsimps [rtrancl_reflcl];
     8.6  
     8.7 -goal Trancl.thy "!!r. (x,y) : (converse r)^* ==> (x,y) : converse(r^*)";
     8.8 -by (rtac converseI 1);
     8.9 +goal Trancl.thy "!!r. (x,y) : (r^-1)^* ==> (x,y) : (r^*)^-1";
    8.10 +by (rtac inverseI 1);
    8.11  by (etac rtrancl_induct 1);
    8.12  by (rtac rtrancl_refl 1);
    8.13  by (blast_tac (!claset addIs [r_into_rtrancl,rtrancl_trans]) 1);
    8.14 -qed "rtrancl_converseD";
    8.15 +qed "rtrancl_inverseD";
    8.16  
    8.17 -goal Trancl.thy "!!r. (x,y) : converse(r^*) ==> (x,y) : (converse r)^*";
    8.18 -by (dtac converseD 1);
    8.19 +goal Trancl.thy "!!r. (x,y) : (r^*)^-1 ==> (x,y) : (r^-1)^*";
    8.20 +by (dtac inverseD 1);
    8.21  by (etac rtrancl_induct 1);
    8.22  by (rtac rtrancl_refl 1);
    8.23  by (blast_tac (!claset addIs [r_into_rtrancl,rtrancl_trans]) 1);
    8.24 -qed "rtrancl_converseI";
    8.25 +qed "rtrancl_inverseI";
    8.26  
    8.27 -goal Trancl.thy "(converse r)^* = converse(r^*)";
    8.28 -by (safe_tac (!claset addSIs [rtrancl_converseI]));
    8.29 +goal Trancl.thy "(r^-1)^* = (r^*)^-1";
    8.30 +by (safe_tac (!claset addSIs [rtrancl_inverseI]));
    8.31  by (res_inst_tac [("p","x")] PairE 1);
    8.32  by (hyp_subst_tac 1);
    8.33 -by (etac rtrancl_converseD 1);
    8.34 -qed "rtrancl_converse";
    8.35 +by (etac rtrancl_inverseD 1);
    8.36 +qed "rtrancl_inverse";
    8.37  
    8.38  val major::prems = goal Trancl.thy
    8.39      "[| (a,b) : r^*; P(b); \
    8.40  \       !!y z.[| (y,z) : r;  (z,b) : r^*;  P(z) |] ==> P(y) |]  \
    8.41  \     ==> P(a)";
    8.42 -by (rtac ((major RS converseI RS rtrancl_converseI) RS rtrancl_induct) 1);
    8.43 +by (rtac ((major RS inverseI RS rtrancl_inverseI) RS rtrancl_induct) 1);
    8.44  by (resolve_tac prems 1);
    8.45 -by (blast_tac (!claset addIs prems addSDs[rtrancl_converseD])1);
    8.46 -qed "converse_rtrancl_induct";
    8.47 +by (blast_tac (!claset addIs prems addSDs[rtrancl_inverseD])1);
    8.48 +qed "inverse_rtrancl_induct";
    8.49  
    8.50  val prems = goal Trancl.thy
    8.51   "[| ((a,b),(c,d)) : r^*; P c d; \
    8.52  \    !!x y z u.[| ((x,y),(z,u)) : r;  ((z,u),(c,d)) : r^*;  P z u |] ==> P x y\
    8.53  \ |] ==> P a b";
    8.54  by (res_inst_tac[("R","P")]splitD 1);
    8.55 -by (res_inst_tac[("P","split P")]converse_rtrancl_induct 1);
    8.56 +by (res_inst_tac[("P","split P")]inverse_rtrancl_induct 1);
    8.57  by (resolve_tac prems 1);
    8.58  by (Simp_tac 1);
    8.59  by (resolve_tac prems 1);
    8.60  by (split_all_tac 1);
    8.61  by (Asm_full_simp_tac 1);
    8.62  by (REPEAT(ares_tac prems 1));
    8.63 -qed "converse_rtrancl_induct2";
    8.64 +qed "inverse_rtrancl_induct2";
    8.65  
    8.66  val major::prems = goal Trancl.thy
    8.67   "[| (x,z):r^*; \
    8.68 @@ -188,7 +188,7 @@
    8.69  \    !!y. [| (x,y):r; (y,z):r^* |] ==> P \
    8.70  \ |] ==> P";
    8.71  by (subgoal_tac "x = z  | (? y. (x,y) : r & (y,z) : r^*)" 1);
    8.72 -by (rtac (major RS converse_rtrancl_induct) 2);
    8.73 +by (rtac (major RS inverse_rtrancl_induct) 2);
    8.74  by (blast_tac (!claset addIs prems) 2);
    8.75  by (blast_tac (!claset addIs prems) 2);
    8.76  by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
    8.77 @@ -304,10 +304,10 @@
    8.78        impOfSubs rtrancl_mono, trancl_mono]) 1);
    8.79  qed "trancl_insert";
    8.80  
    8.81 -goalw Trancl.thy [trancl_def] "(converse r)^+ = converse(r^+)";
    8.82 -by(simp_tac (!simpset addsimps [rtrancl_converse,converse_comp]) 1);
    8.83 -by(simp_tac (!simpset addsimps [rtrancl_converse RS sym,r_comp_rtrancl_eq]) 1);
    8.84 -qed "trancl_converse";
    8.85 +goalw Trancl.thy [trancl_def] "(r^-1)^+ = (r^+)^-1";
    8.86 +by(simp_tac (!simpset addsimps [rtrancl_inverse,inverse_comp]) 1);
    8.87 +by(simp_tac (!simpset addsimps [rtrancl_inverse RS sym,r_comp_rtrancl_eq]) 1);
    8.88 +qed "trancl_inverse";
    8.89  
    8.90  
    8.91  val major::prems = goal Trancl.thy
     9.1 --- a/src/HOL/WF.ML	Mon Jun 16 14:25:33 1997 +0200
     9.2 +++ b/src/HOL/WF.ML	Tue Jun 17 09:01:56 1997 +0200
     9.3 @@ -141,9 +141,9 @@
     9.4  qed "acyclic_insert";
     9.5  AddIffs [acyclic_insert];
     9.6  
     9.7 -goalw WF.thy [acyclic_def] "acyclic(converse r) = acyclic r";
     9.8 -by(simp_tac (!simpset addsimps [trancl_converse]) 1);
     9.9 -qed "acyclic_converse";
    9.10 +goalw WF.thy [acyclic_def] "acyclic(r^-1) = acyclic r";
    9.11 +by(simp_tac (!simpset addsimps [trancl_inverse]) 1);
    9.12 +qed "acyclic_inverse";
    9.13  
    9.14  (** cut **)
    9.15  
    10.1 --- a/src/HOL/ex/mesontest2.ML	Mon Jun 16 14:25:33 1997 +0200
    10.2 +++ b/src/HOL/ex/mesontest2.ML	Tue Jun 17 09:01:56 1997 +0200
    10.3 @@ -2986,9 +2986,9 @@
    10.4  \  (! Y Z X. member(Z::'a,cross_product(X::'a,Y)) --> member(first(Z),X)) &     \
    10.5  \  (! X Z Y. member(Z::'a,cross_product(X::'a,Y)) --> member(second(Z),Y)) &    \
    10.6  \  (! X Z Y. little_set(Z) & ordered_pair_predicate(Z) & member(first(Z),X) & member(second(Z),Y) --> member(Z::'a,cross_product(X::'a,Y))) &   \
    10.7 -\  (! X Z. member(Z::'a,converse(X)) --> ordered_pair_predicate(Z)) &       \
    10.8 -\  (! Z X. member(Z::'a,converse(X)) --> member(ordered_pair(second(Z),first(Z)),X)) &      \
    10.9 -\  (! Z X. little_set(Z) & ordered_pair_predicate(Z) & member(ordered_pair(second(Z),first(Z)),X) --> member(Z::'a,converse(X))) &  \
   10.10 +\  (! X Z. member(Z::'a,X^-1) --> ordered_pair_predicate(Z)) &       \
   10.11 +\  (! Z X. member(Z::'a,X^-1) --> member(ordered_pair(second(Z),first(Z)),X)) &      \
   10.12 +\  (! Z X. little_set(Z) & ordered_pair_predicate(Z) & member(ordered_pair(second(Z),first(Z)),X) --> member(Z::'a,X^-1)) &  \
   10.13  \  (! Z X. member(Z::'a,rotate_right(X)) --> little_set(f9(Z::'a,X))) & \
   10.14  \  (! Z X. member(Z::'a,rotate_right(X)) --> little_set(f10(Z::'a,X))) &        \
   10.15  \  (! Z X. member(Z::'a,rotate_right(X)) --> little_set(f11(Z::'a,X))) &        \
   10.16 @@ -3056,8 +3056,8 @@
   10.17  \  (! Z. little_set(Z) & ordered_pair_predicate(Z) & equal(first(Z),second(Z)) --> member(Z::'a,identity_relation)) &       \
   10.18  \  (! X Y. equal(restrict(X::'a,Y),intersection(X::'a,cross_product(Y::'a,universal_set)))) &       \
   10.19  \  (! Xf. one_to_one_function(Xf) --> function(Xf)) &   \
   10.20 -\  (! Xf. one_to_one_function(Xf) --> function(converse(Xf))) & \
   10.21 -\  (! Xf. function(Xf) & function(converse(Xf)) --> one_to_one_function(Xf)) &  \
   10.22 +\  (! Xf. one_to_one_function(Xf) --> function(Xf^-1)) & \
   10.23 +\  (! Xf. function(Xf) & function(Xf^-1) --> one_to_one_function(Xf)) &  \
   10.24  \  (! Z Xf Y. member(Z::'a,apply(Xf::'a,Y)) --> ordered_pair_predicate(f28(Z::'a,Xf,Y))) &  \
   10.25  \  (! Z Y Xf. member(Z::'a,apply(Xf::'a,Y)) --> member(f28(Z::'a,Xf,Y),Xf)) &       \
   10.26  \  (! Z Xf Y. member(Z::'a,apply(Xf::'a,Y)) --> equal(first(f28(Z::'a,Xf,Y)),Y)) &  \
   10.27 @@ -3159,7 +3159,7 @@
   10.28  \  (! S' T'. equal(S'::'a,T') --> equal(complement(S'),complement(T'))) &   \
   10.29  \  (! U V W. equal(U::'a,V) --> equal(composition(U::'a,W),composition(V::'a,W))) & \
   10.30  \  (! X Z Y. equal(X::'a,Y) --> equal(composition(Z::'a,X),composition(Z::'a,Y))) & \
   10.31 -\  (! A1 B1. equal(A1::'a,B1) --> equal(converse(A1),converse(B1))) &       \
   10.32 +\  (! A1 B1. equal(A1::'a,B1) --> equal(A1^-1,B1^-1)) &       \
   10.33  \  (! C1 D1 E1. equal(C1::'a,D1) --> equal(cross_product(C1::'a,E1),cross_product(D1::'a,E1))) &    \
   10.34  \  (! F1 H1 G1. equal(F1::'a,G1) --> equal(cross_product(H1::'a,F1),cross_product(H1::'a,G1))) &    \
   10.35  \  (! I1 J1. equal(I1::'a,J1) --> equal(domain_of(I1),domain_of(J1))) &     \