#|
Copyright (C) 1994 by Yuan Yu.  All Rights Reserved.
This script is hereby placed in the public domain, and therefore unlimited
editing and redistribution is permitted.
NO WARRANTY
Yuan Yu PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT IS PROVIDED "AS IS"
WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING, BUT NOT
LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE
SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU ASSUME THE COST OF
ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
IN NO EVENT WILL Yuan Yu BE LIABLE TO YOU FOR ANY DAMAGES, ANY LOST PROFITS,
LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT
OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT NOT LIMITED TO LOSS
OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY THIRD
PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF SUCH DAMAGES, OR
FOR ANY CLAIM BY ANY OTHER PARTY.
|#
; Requires defn-sk.
#|
The following article is about this event file.
@article{Yu89,
       author="Yuan Yu",
       title="Computer Proofs in Group Theory",
       journal="Journal of Automated Reasoning",
       volume="6",
number="3",
       year=1990
}
|#

Event: Start with the initial thm theory.

; First, several concepts on SET.
; Set L has no duplicate element.

Definition: set-standard (l) = if listp (l) then (car (l) ∉ cdr (l)) ∧ set-standard (cdr (l))

else t endif

; L1-L2.

Definition: set-minus (l1 , l2 ) = if listp (l1 )

then if car (l1 ) ∈ l2 then set-minus (cdr (l1 ), l2 )

else cons (car (l1 ), set-minus (cdr (l1 ), l2 )) endif else l1 endif

; L1 and L2 are disjoint.

Definition: set-disjoint (l1 , l2 ) = if listp (l1 )

then if car (l1 ) ∈ l2 then f

else set-disjoint (cdr (l1 ), l2 ) endif else t endif

; remove the element x from L.

Definition: delete (x, l) = if listp (l)

then if x = car (l) then cdr (l)

else cons (car (l), delete (x, cdr (l))) endif else l endif

; L2 contains L1.

Definition: subset (l1 , l2 ) = if listp (l1 ) then (car (l1 ) ∈ l2 ) ∧ subset (cdr (l1 ), l2 )

else t endif

; The number of elements in L.

Definition: cardinal (l) = if listp (l) then 1 + cardinal (cdr (l))

else 0 endif

; Lemmas based on the above concepts.

Theorem: set-standard-lemma set-standard (a) → set-standard (set-minus (a, b))

Theorem: set-minus-lemma1 count (set-minus (s, s1 )) ≤ count (s)

Theorem: set-minus-lemma2 (c ∉ a) → (set-minus (a, cons (c, b)) = set-minus (a, b))

Theorem: set-minus-lemma3 (x ∈ set-minus (s, s1 )) = ((x ∈ s) ∧ (x ∉ s1 ))

Theorem: set-minus-lemma (listp (s) ∧ (x ∈ s) ∧ (x ∈ s1 )) → (count (set-minus (s, s1 )) < count (s))

Theorem: delete-lemma1 (x ∈ a) → (cardinal (a) = (1 + cardinal (delete (x, a))))

Theorem: delete-lemma2 ((y ∈ a) ∧ (x ≠ y)) → (y ∈ delete (x, a))

Theorem: delete-lemma3 ((x ∈ a) ∧ (x ∉ b) ∧ subset (b, a)) → subset (b, delete (x, a))

Theorem: subset-transitivity (subset (a, b) ∧ subset (b, c)) → subset (a, c)

Theorem: subset-lemma0 (subset (s1 , s) ∧ (x ∈ s1 )) → (x ∈ s)

Theorem: subset-lemma1 subset (a, b) → subset (a, cons (c, b))

Theorem: subset-lemma2 subset (a, b) → subset (set-minus (a, c), b)

Theorem: subset-reflexivity subset (a, a)

Theorem: cardinal-lemma (x ∈ s) → (1 ≤ cardinal (s))

Theorem: cardinal-equality (set-standard (a) ∧ (c ∉ b) ∧ (c ∈ a)) → (cardinal (set-minus (a, b)) = (1 + cardinal (set-minus (a, cons (c, b)))))

; Induction hint for CARDINAL-INEQUALITY-LEMMA

Definition: cardinal-inequality-induct (b, a) = if listp (b) then cardinal-inequality-induct (cdr (b), delete (car (b), a))

else t endif

Theorem: cardinal-inequality (set-standard (b) ∧ subset (b, a)) → (cardinal (b) ≤ cardinal (a))

Theorem: cardinal-subset (set-standard (a) ∧ set-standard (b) ∧ subset (b, a)) → (cardinal (set-minus (a, b)) = (cardinal (a) − cardinal (b)))

; we will introduce the axioms for definition of group with operation OP.

Event: Introduce the function symbol op of 2 arguments.

Definition: group-op (g) ↔ (∀ x, y (((x ∈ g) ∧ (y ∈ g)) → (op (x, y) ∈ g))

∧ ∀ x, y, z (((x ∈ g) ∧ (y ∈ g) ∧ (z ∈ g))

→ (op (op (x, y), z) = op (x, op (y, z))))

∧ ∃ id ((id ∈ g)

∧ ∀ x ((x ∈ g)
→ ((op (id, x) = x)
∧ (op (x, id) = x)
∧ ∃ inv ((inv ∈ g)

∧ (op (inv, x) = id) ∧ (op (x, inv)

= id))))))

; the group has the "closed" property.

Theorem: group-op-closed (group-op (g) ∧ (x ∈ g) ∧ (y ∈ g)) → (op (x, y) ∈ g)

; the group has the "associativity" property.

Theorem: group-op-associativity (group-op (g) ∧ (x ∈ g) ∧ (y ∈ g) ∧ (z ∈ g)) → (op (op (x, y), z) = op (x, op (y, z)))

Theorem: group-op-associativity1 (group-op (g) ∧ (x ∈ g) ∧ (y ∈ g) ∧ (z ∈ g)) → (op (x, op (y, z)) = op (op (x, y), z))

; the group has the "identity" property.

Theorem: group-op-identity group-op (g) → ((id (g) ∈ g)

∧ ((x ∈ g) → ((op (id (g), x) = x) ∧ (op (x, id (g)) = x))))

; the group has the "inverse" property.

Theorem: group-op-inverse (group-op (g) ∧ (x ∈ g)) → ((inv (g, x) ∈ g)

∧ (op (inv (g, x), x) = id (g)) ∧ (op (x, inv (g, x)) = id (g)))

; introduce the concept of coset.

Definition: right-coset (s, a) = if listp (s) then cons (op (car (s), a), right-coset (cdr (s), a))

else nil endif

Theorem: right-coset-cardinal cardinal (right-coset (s, a)) = cardinal (s)

Theorem: right-coset-nempty (group-op (g) ∧ (x ∈ g) ∧ subset (s, g) ∧ (id (g) ∈ s)) → (x ∈ right-coset (s, x))

; some simple equalities in group.
; EQUALITY1: x*a=y*b-->x=y*(b*(inv g a)).

Theorem: op-equality1 (group-op (g) ∧ (x ∈ g) ∧ (y ∈ g) ∧ (a ∈ g) ∧ (b ∈ g) ∧ (op (x, a) = op (y, b))) → (x = op (y, op (b, inv (g, a))))

; EQUALITY2: x*a=y*b-->a=((inv g x)*y)*b.

Theorem: op-equality2 (group-op (g) ∧ (x ∈ g) ∧ (y ∈ g) ∧ (a ∈ g) ∧ (b ∈ g) ∧ (op (x, a) = op (y, b))) → (a = op (op (inv (g, x), y), b))

; cancellation: xa=ya-->x=y.

Theorem: cancellation (group-op (g) ∧ (x ∈ g) ∧ (y ∈ g) ∧ (a ∈ g) ∧ (op (x, a) = op (y, a))) → (x = y)

; some further simple equalities.

Theorem: op-equality3 (group-op (g) ∧ (x ∈ g) ∧ (a ∈ g) ∧ (op (x, a) = id (g))) → (a = inv (g, x))

Theorem: op-equality4 (group-op (g) ∧ (x ∈ g) ∧ (op (x, x) = x)) → (x = id (g))

Definition: subgroup-op (h, g) = (group-op (g) ∧ group-op (h) ∧ subset (h, g))

; (id g)=(id h), if h is a subgroup of g.

Theorem: op-identity-same subgroup-op (h, g) → (id (g) = id (h))

Theorem: op-identity-in-subgroup subgroup-op (h, g) → (id (g) ∈ h)

; (inv g x)=(inv h x), if h is a subgroup of g.

Theorem: op-inverse-same (subgroup-op (h, g) ∧ (x ∈ h)) → (inv (h, x) = inv (g, x))

Theorem: op-inverse-in-subgroup (subgroup-op (h, g) ∧ (x ∈ h)) → (inv (g, x) ∈ h)

Theorem: group-op-order group-op (g) → (1 ≤ cardinal (g))

Event: Disable group-op.

Event: Disable group-op-associativity1.

; we will introduce the axioms for another group with operation OP1.

Event: Introduce the function symbol op1 of 2 arguments.

Definition: group-op1 (h) ↔ (∀ x, y (((x ∈ h) ∧ (y ∈ h)) → (op1 (x, y) ∈ h))

∧ ∀ x, y, z (((x ∈ h) ∧ (y ∈ h) ∧ (z ∈ h))

→ (op1 (op1 (x, y), z) = op1 (x, op1 (y, z))))

∧ ∃ id ((id ∈ h)

∧ ∀ x ((x ∈ h)
→ ((op1 (id, x) = x)
∧ (op1 (x, id) = x)
∧ ∃ inv ((inv ∈ h)

∧ (op1 (inv, x) = id) ∧ (op1 (x, inv) = id))))))

; the group has the "closed" property.

Theorem: group-op1-closed (group-op1 (h) ∧ (x ∈ h) ∧ (y ∈ h)) → (op1 (x, y) ∈ h)

; the group has the "associativity" property.

Theorem: group-op1-associativity (group-op1 (h) ∧ (x ∈ h) ∧ (y ∈ h) ∧ (z ∈ h)) → (op1 (op1 (x, y), z) = op1 (x, op1 (y, z)))

Theorem: group-op1-associativity1 (group-op1 (h) ∧ (x ∈ h) ∧ (y ∈ h) ∧ (z ∈ h)) → (op1 (x, op1 (y, z)) = op1 (op1 (x, y), z))

; the group has the "identity" property.

Theorem: group-op1-identity group-op1 (h) → ((id-1 (h) ∈ h)

∧ ((x ∈ h)

→ ((op1 (id-1 (h), x) = x) ∧ (op1 (x, id-1 (h)) = x))))

; the group has the "inverse" property.

Theorem: group-op1-inverse (group-op1 (h) ∧ (x ∈ h)) → ((inv-1 (h, x) ∈ h)

∧ (op1 (inv-1 (h, x), x) = id-1 (h)) ∧ (op1 (x, inv-1 (h, x)) = id-1 (h)))

; some simple equalities in group.
; OP1-EQUALITY1: x*a=y*b-->x=y*(b*(inv a)).

Theorem: op1-equality1 (group-op1 (h) ∧ (x ∈ h) ∧ (y ∈ h) ∧ (a ∈ h) ∧ (b ∈ h) ∧ (op1 (x, a) = op1 (y, b))) → (x = op1 (y, op1 (b, inv-1 (h, a))))

; EQUALITY2: x*a=y*b-->a=((inv x)*y)*b.

Theorem: op1-equality2 (group-op1 (h) ∧ (x ∈ h) ∧ (y ∈ h) ∧ (a ∈ h) ∧ (b ∈ h) ∧ (op1 (x, a) = op1 (y, b))) → (a = op1 (op1 (inv-1 (h, x), y), b))

Theorem: op1-equality3 (group-op1 (h) ∧ (x ∈ h) ∧ (a ∈ h) ∧ (op1 (x, a) = id-1 (h))) → (a = inv-1 (h, x))

Theorem: op1-equality4 (group-op1 (h) ∧ (x ∈ h) ∧ (op1 (x, x) = x)) → (x = id-1 (h))

; cancellation: xa=ya-->x=y.

Theorem: op1-cancellation (group-op1 (h) ∧ (x ∈ h) ∧ (y ∈ h) ∧ (a ∈ h) ∧ (op1 (x, a) = op1 (y, a))) → (x = y)

; we start to prove the kernel of a group homomorphism is a normal subgroup.
; Introduce homomorphisms.

Event: Introduce the function symbol phi of one argument.

Definition: homo-phi (g, h) ↔ ∀ x, y (((x ∈ g) ∧ (y ∈ g))

→ ((phi (x) ∈ h) ∧ (phi (y) ∈ h) ∧ (phi (op (x, y)) = op1 (phi (x), phi (y)))))

Theorem: homomorphism-phi (homo-phi (g, h) ∧ (x ∈ g) ∧ (y ∈ g)) → ((phi (x) ∈ h)

∧ (phi (y) ∈ h)

∧ (phi (op (x, y)) = op1 (phi (x), phi (y))))

Definition: phi-inv (g, a) = if listp (g)

then if phi (car (g)) = a then cons (car (g), phi-inv (cdr (g), a))

else phi-inv (cdr (g), a) endif else nil endif

Theorem: basic-mapping1 ((x ∈ g) ∧ (phi (x) = a)) → (x ∈ phi-inv (g, a))

Theorem: basic-mapping2 (x ∈ phi-inv (g, a)) → (phi (x) = a)

Theorem: phi-inv-subset subset (phi-inv (g, a), g)

Theorem: id-to-id (group-op (g) ∧ group-op1 (h) ∧ homo-phi (g, h)) → (phi (id (g)) = id-1 (h))

Theorem: inv-to-inv (group-op (g) ∧ group-op1 (h) ∧ homo-phi (g, h) ∧ (x ∈ g)) → (phi (inv (g, x)) = inv-1 (h, phi (x)))

Theorem: ker-closed (group-op (g) ∧ group-op1 (h) ∧ homo-phi (g, h) ∧ (x ∈ phi-inv (g, id-1 (h))) ∧ (y ∈ phi-inv (g, id-1 (h)))) → (op (x, y) ∈ phi-inv (g, id-1 (h)))

Theorem: ker-associativity (group-op (g) ∧ (x ∈ phi-inv (g, a)) ∧ (y ∈ phi-inv (g, a)) ∧ (z ∈ phi-inv (g, a))) → (op (op (x, y), z) = op (x, op (y, z)))

Theorem: ker-identity (group-op (g) ∧ group-op1 (h) ∧ homo-phi (g, h)) → (id (g) ∈ phi-inv (g, id-1 (h)))

Theorem: id-inv-id group-op1 (h) → (inv-1 (h, id-1 (h)) = id-1 (h))

Theorem: ker-inverse (group-op (g) ∧ group-op1 (h) ∧ homo-phi (g, h) ∧ (x ∈ phi-inv (g, id-1 (h)))) → (inv (g, x) ∈ phi-inv (g, id-1 (h)))

Theorem: ker-identity-inverse (group-op (g) ∧ group-op1 (h) ∧ homo-phi (g, h)) → ((x ∈ phi-inv (g, id-1 (h)))

→ ((op (id (g), x) = x) ∧ (op (x, id (g)) = x) ∧ (inv (g, x) ∈ phi-inv (g, id-1 (h))) ∧ (op (inv (g, x), x) = id (g)) ∧ (op (x, inv (g, x)) = id (g))))

Theorem: ker-subgroup (group-op (g) ∧ group-op1 (h) ∧ homo-phi (g, h)) → group-op (phi-inv (g, id-1 (h)))

Definition: op-normalp (g, n) ↔ ∀ x, y (((x ∈ g) ∧ (y ∈ n)) → (op (op (x, y), inv (g, x)) ∈ n))

Definition: normal-subgroup-op (g, n) = (group-op (g) ∧ group-op (n) ∧ subset (n, g) ∧ op-normalp (g, n))

Theorem: normal-lemma (group-op (g) ∧ group-op1 (h) ∧ homo-phi (g, h) ∧ (x ∈ g) ∧ (y ∈ phi-inv (g, id-1 (h)))) → (op (op (x, y), inv (g, x)) ∈ phi-inv (g, id-1 (h)))

Theorem: ker-normal (group-op (g) ∧ group-op1 (h) ∧ homo-phi (g, h)) → op-normalp (g, phi-inv (g, id-1 (h)))

Theorem: ker-normal-subgroup (group-op (g) ∧ group-op1 (h) ∧ homo-phi (g, h)) → normal-subgroup-op (g, phi-inv (g, id-1 (h)))

Event: Enable group-op-associativity1.

; Now back to the proof of Lagrange Theorem.
; Every coset of s in a group is "set-standard".

Theorem: right-coset-standard-1 (group-op (g) ∧ subset (s, g) ∧ (a ∈ g) ∧ (x ∈ g) ∧ (x ∉ s)) → (op (x, a) ∉ right-coset (s, a))

Theorem: right-coset-standard-2 (group-op (g) ∧ subset (s, g) ∧ set-standard (s) ∧ (a ∈ g)) → set-standard (right-coset (s, a))

Theorem: right-coset-standard (subgroup-op (h, g) ∧ set-standard (h) ∧ (a ∈ g)) → set-standard (right-coset (h, a))

; different cosets are disjoint.

Theorem: right-coset-disjoint-lemma (group-op (g)

∧ subset (s, g) ∧ (x ∈ g) ∧ (y ∈ g) ∧ (a ∈ g) ∧ (b ∈ g) ∧ (op (inv (g, x), y) ∈ s) ∧ (a ∉ right-coset (s, b))) → (op (x, a) ≠ op (y, b))

Theorem: right-coset-disjoint-1 (subgroup-op (h, g) ∧ subset (s, h) ∧ (x ∈ h) ∧ (a ∈ g) ∧ (b ∈ g) ∧ (a ∉ right-coset (h, b))) → (op (x, a) ∉ right-coset (s, b))

Theorem: right-coset-disjoint-2 (subgroup-op (h, g) ∧ (x ∈ h) ∧ (a ∈ g) ∧ (b ∈ g) ∧ (a ∉ right-coset (h, b))) → (op (x, a) ∉ right-coset (h, b))

Theorem: right-coset-disjoint-3 (subgroup-op (h, g) ∧ subset (s, h) ∧ (a ∈ g) ∧ (b ∈ g) ∧ (a ∉ right-coset (h, b))) → set-disjoint (right-coset (s, a), right-coset (h, b))

Theorem: right-coset-disjoint (subgroup-op (h, g) ∧ (a ∈ g) ∧ (b ∈ g) ∧ (a ∉ right-coset (h, b))) → set-disjoint (right-coset (h, a), right-coset (h, b))

; Now the Lagrange Theorem will be attacked.
; First, we still need some lemmas.
; first, disable GROUP.

Event: Disable group-op.

Definition: op-closed (s1 , s2 ) ↔ ∀ x, y (((x ∈ s1 ) ∧ (y ∈ s2 )) → (op (x, y) ∈ s2 ))

Theorem: la-lemma1 ((b ∈ s) ∧ subset (h1 , h) ∧ op-closed (h, s)) → subset (right-coset (h1 , b), s)

Theorem: la-lemma2 (subgroup-op (h, g) ∧ subset (s, g) ∧ (b ∈ g) ∧ op-closed (h, s)) → (((x ∈ h) ∧ (a ∈ set-minus (s, right-coset (h, b))))

→ (op (x, a) ∈ set-minus (s, right-coset (h, b))))

Theorem: la-lemma3 (subgroup-op (h, g) ∧ subset (s, g) ∧ (b ∈ g) ∧ op-closed (h, s)) → op-closed (h, set-minus (s, right-coset (h, b)))

Theorem: lagrange-induct-measure (group-op (g) ∧ group-op (h) ∧ subset (h, g) ∧ subset (s, g) ∧ listp (s)) → (count (set-minus (s, right-coset (h, car (s)))) < count (s))

Theorem: la-lemma4 ((y ≤ x) ∧ (1 ≤ y) ∧ (((x − y) mod y) = 0)) → ((x mod y) = 0)

Theorem: la-lemma5 (subgroup-op (h, g) ∧ set-standard (h) ∧ subset (s, g) ∧ set-standard (s) ∧ op-closed (h, s) ∧ ((cardinal (set-minus (s, right-coset (h, car (s)))) mod cardinal (h))

= 0)) → ((cardinal (s) mod cardinal (h)) = 0)

Definition: lagrange-induct (g, h, s) = if subgroup-op (h, g) ∧ subset (s, g) ∧ listp (s)

then lagrange-induct (g, h, set-minus (s, right-coset (h, car (s)))) else t endif

Theorem: lagrange-generalized (subgroup-op (h, g) ∧ set-standard (h) ∧ subset (s, g) ∧ set-standard (s) ∧ op-closed (h, s)) → ((cardinal (s) mod cardinal (h)) = 0)

Definition: divides (m, n) = ((n mod m) = 0)

Theorem: subset-op-closed (group-op (g) ∧ subset (h, g)) → op-closed (h, g)

Theorem: lagrange (subgroup-op (h, g) ∧ set-standard (g) ∧ set-standard (h)) → divides (cardinal (h), cardinal (g))

Index

basic-mapping1, 9 basic-mapping2, 9

cancellation, 6 cardinal, 3–5, 7, 13, 14 cardinal-equality, 4 cardinal-inequality, 4 cardinal-inequality-induct, 4 cardinal-lemma, 4 cardinal-subset, 4

delete, 2–4 delete-lemma1, 3 delete-lemma2, 3 delete-lemma3, 3 divides, 14

exists, 4, 7

forall, 4, 7, 9, 11, 13

group-op, 4–7, 9–11, 13, 14 group-op-associativity, 5 group-op-associativity1, 5 group-op-closed, 4 group-op-identity, 5 group-op-inverse, 5 group-op-order, 7 group-op1, 7–11 group-op1-associativity, 7 group-op1-associativity1, 7 group-op1-closed, 7 group-op1-identity, 8 group-op1-inverse, 8

homo-phi, 9–11 homomorphism-phi, 9

id, 5, 6, 9, 10 id-1, 8–11 id-inv-id, 10 id-to-id, 9 inv, 5–7, 10–12 inv-1, 8, 10 inv-to-inv, 10

ker-associativity, 10 ker-closed, 10 ker-identity, 10 ker-identity-inverse, 10 ker-inverse, 10 ker-normal, 11 ker-normal-subgroup, 11 ker-subgroup, 10

la-lemma1, 13 la-lemma2, 13 la-lemma3, 13 la-lemma4, 13 la-lemma5, 13 lagrange, 14 lagrange-generalized, 13 lagrange-induct, 13 lagrange-induct-measure, 13

normal-lemma, 11 normal-subgroup-op, 11

op, 4–6, 9–13 op-closed, 12–14 op-equality1, 5 op-equality2, 6 op-equality3, 6 op-equality4, 6 op-identity-in-subgroup, 6 op-identity-same, 6 op-inverse-in-subgroup, 7 op-inverse-same, 6 op-normalp, 11 op1, 7–9 op1-cancellation, 9 op1-equality1, 8 op1-equality2, 8 op1-equality3, 8 op1-equality4, 8

phi, 9, 10 phi-inv, 9–11 phi-inv-subset, 9

right-coset, 5, 11–13 right-coset-cardinal, 5 right-coset-disjoint, 12 right-coset-disjoint-1, 12 right-coset-disjoint-2, 12 right-coset-disjoint-3, 12 right-coset-disjoint-lemma, 11 right-coset-nempty, 5 right-coset-standard, 11 right-coset-standard-1, 11 right-coset-standard-2, 11

set-disjoint, 2, 12 set-minus, 2–4, 13 set-minus-lemma, 3 set-minus-lemma1, 3 set-minus-lemma2, 3 set-minus-lemma3, 3 set-standard, 2–4, 11, 13, 14 set-standard-lemma, 3 subgroup-op, 6, 7, 11–14 subset, 2–6, 9, 11–14 subset-lemma0, 3 subset-lemma1, 3 subset-lemma2, 3 subset-op-closed, 14 subset-reflexivity, 3 subset-transitivity, 3