Lines Matching refs:g1
260 ``!G H g1 g2 h1 h2.
261 gop (prod_group G H) (g1, h1) (g2, h2) = (gop G g1 g2, gop H h1 h2)``,
504 ``!G :: group. !H :: subgroup G. !g1 g2 :: gset G.
505 (lcoset G g1 H = lcoset G g2 H)
506 \/ DISJOINT (lcoset G g1 H) (lcoset G g2 H)``,
509 (Cases_on `?g. g IN lcoset G g1 H
517 ++ Suff `!v. v IN lcoset G g1 H = v IN lcoset G g2 H`
523 ++ Q.SPEC_TAC (`g1`, `g1`)
524 ++ Suff `!g1 g2 :: gset G.
525 g IN lcoset G g1 H /\
528 v IN lcoset G g1 H ==>
538 ++ Suff `gop G g1 x'' = gop G (gop G (gop G g2 x') (ginv G x)) x''`