The file 'group.v' as Latin-1 characters
1 V a r i a b l e ␣ G ␣ : ␣ S e t . EOL()
2 V a r i a b l e ␣ o p e r a t i o n ␣ : ␣ G ␣ - > ␣ G ␣ - > ␣ G . EOL()
3 V a r i a b l e ␣ e ␣ : ␣ G . EOL()
4 V a r i a b l e ␣ i n v ␣ : ␣ G ␣ - > ␣ G . EOL()
5 EOL()
6 I n f i x ␣ " " ␣ : = ␣ o p e r a t i o n ␣ ( a t ␣ l e v e l ␣ 5 0 , ␣ l e f t ␣ a s s o c i a t i v i t y ) . EOL()
7 EOL()
8 H y p o t h e s i s ␣ a s s o c i a t i v i t y ␣ : ␣ f o r a l l ␣ x ␣ y ␣ z ␣ : ␣ G , ␣ ( x ␣ ␣ y ) ␣ ␣ z ␣ = ␣ x ␣ ␣ ( y ␣ ␣ z ) . EOL()
9 H y p o t h e s i s ␣ i d e n t i t y ␣ : ␣ f o r a l l ␣ x ␣ : ␣ G , ␣ ( x ␣ ␣ e ) ␣ = ␣ e ␣ / \ ␣ e ␣ ␣ x ␣ = ␣ x . EOL()
10 H y p o t h e s i s ␣ i n v e r s e ␣ : ␣ f o r a l l ␣ x ␣ : ␣ G , ␣ ( x ␣ ␣ i n v ␣ x ) ␣ = ␣ e ␣ / \ ␣ i n v ␣ x ␣ ␣ x ␣ = ␣ x . EOL()
11 EOL()
12 T h e o r e m ␣ l a t i n _ s q u a r e _ p r o p e r t y ␣ : ␣ f o r a l l ␣ a ␣ b ␣ : ␣ G , ␣ e x i s t s ␣ x ␣ : ␣ G , ␣ a ␣ ␣ x ␣ = ␣ b . EOL()
13 ␣ ␣ i n t r o s ␣ a ␣ b . EOL()
14 ␣ ␣ e x i s t s ␣ ( i n v ␣ a ␣ ␣ b ) . EOL()
15 ␣ ␣ r e w r i t e ␣ < - ␣ a s s o c i a t i v i t y . EOL()
16 ␣ ␣ d e s t r u c t ␣ i n v e r s e ␣ w i t h ␣ ( x : = a ) ␣ a s ␣ [ H ␣ _ ] . EOL()
17 ␣ ␣ r e w r i t e ␣ H . EOL()
18 ␣ ␣ d e s t r u c t ␣ i d e n t i t y ␣ w i t h ␣ ( x : = b ) ␣ a s ␣ [ _ ␣ H ' ] . EOL()
19 ␣ ␣ t r i v i a l . EOL()
20 Q e d . EOL()