- PAIR_MAP_I
-
|- I ## I = I
- PAIR_REL_THM
-
|- ∀R1 R2 a b c d. (R1 ### R2) (a,b) (c,d) ⇔ R1 a c ∧ R2 b d
- PAIR_REL_EQ
-
|- $= ### $= = $=
- PAIR_REL_REFL
-
|- ∀R1 R2.
(∀x y. R1 x y ⇔ (R1 x = R1 y)) ∧ (∀x y. R2 x y ⇔ (R2 x = R2 y)) ⇒
∀x. (R1 ### R2) x x
- PAIR_EQUIV
-
|- ∀R1 R2. EQUIV R1 ⇒ EQUIV R2 ⇒ EQUIV (R1 ### R2)
- PAIR_QUOTIENT
-
|- ∀R1 abs1 rep1.
QUOTIENT R1 abs1 rep1 ⇒
∀R2 abs2 rep2.
QUOTIENT R2 abs2 rep2 ⇒
QUOTIENT (R1 ### R2) (abs1 ## abs2) (rep1 ## rep2)
- FST_PRS
-
|- ∀R1 abs1 rep1.
QUOTIENT R1 abs1 rep1 ⇒
∀R2 abs2 rep2.
QUOTIENT R2 abs2 rep2 ⇒ ∀p. FST p = abs1 (FST ((rep1 ## rep2) p))
- FST_RSP
-
|- ∀R1 abs1 rep1.
QUOTIENT R1 abs1 rep1 ⇒
∀R2 abs2 rep2.
QUOTIENT R2 abs2 rep2 ⇒
∀p1 p2. (R1 ### R2) p1 p2 ⇒ R1 (FST p1) (FST p2)
- SND_PRS
-
|- ∀R1 abs1 rep1.
QUOTIENT R1 abs1 rep1 ⇒
∀R2 abs2 rep2.
QUOTIENT R2 abs2 rep2 ⇒ ∀p. SND p = abs2 (SND ((rep1 ## rep2) p))
- SND_RSP
-
|- ∀R1 abs1 rep1.
QUOTIENT R1 abs1 rep1 ⇒
∀R2 abs2 rep2.
QUOTIENT R2 abs2 rep2 ⇒
∀p1 p2. (R1 ### R2) p1 p2 ⇒ R2 (SND p1) (SND p2)
- COMMA_PRS
-
|- ∀R1 abs1 rep1.
QUOTIENT R1 abs1 rep1 ⇒
∀R2 abs2 rep2.
QUOTIENT R2 abs2 rep2 ⇒ ∀a b. (a,b) = (abs1 ## abs2) (rep1 a,rep2 b)
- COMMA_RSP
-
|- ∀R1 abs1 rep1.
QUOTIENT R1 abs1 rep1 ⇒
∀R2 abs2 rep2.
QUOTIENT R2 abs2 rep2 ⇒
∀a1 a2 b1 b2. R1 a1 b1 ∧ R2 a2 b2 ⇒ (R1 ### R2) (a1,a2) (b1,b2)
- CURRY_PRS
-
|- ∀R1 abs1 rep1.
QUOTIENT R1 abs1 rep1 ⇒
∀R2 abs2 rep2.
QUOTIENT R2 abs2 rep2 ⇒
∀R3 abs3 rep3.
QUOTIENT R3 abs3 rep3 ⇒
∀f a b.
CURRY f a b =
abs3 (CURRY (((abs1 ## abs2) --> rep3) f) (rep1 a) (rep2 b))
- CURRY_RSP
-
|- ∀R1 abs1 rep1.
QUOTIENT R1 abs1 rep1 ⇒
∀R2 abs2 rep2.
QUOTIENT R2 abs2 rep2 ⇒
∀R3 abs3 rep3.
QUOTIENT R3 abs3 rep3 ⇒
∀f1 f2.
((R1 ### R2) ===> R3) f1 f2 ⇒
(R1 ===> R2 ===> R3) (CURRY f1) (CURRY f2)
- UNCURRY_PRS
-
|- ∀R1 abs1 rep1.
QUOTIENT R1 abs1 rep1 ⇒
∀R2 abs2 rep2.
QUOTIENT R2 abs2 rep2 ⇒
∀R3 abs3 rep3.
QUOTIENT R3 abs3 rep3 ⇒
∀f p.
UNCURRY f p =
abs3 (UNCURRY ((abs1 --> abs2 --> rep3) f) ((rep1 ## rep2) p))
- UNCURRY_RSP
-
|- ∀R1 abs1 rep1.
QUOTIENT R1 abs1 rep1 ⇒
∀R2 abs2 rep2.
QUOTIENT R2 abs2 rep2 ⇒
∀R3 abs3 rep3.
QUOTIENT R3 abs3 rep3 ⇒
∀f1 f2.
(R1 ===> R2 ===> R3) f1 f2 ⇒
((R1 ### R2) ===> R3) (UNCURRY f1) (UNCURRY f2)
- PAIR_MAP_PRS
-
|- ∀R1 abs1 rep1.
QUOTIENT R1 abs1 rep1 ⇒
∀R2 abs2 rep2.
QUOTIENT R2 abs2 rep2 ⇒
∀R3 abs3 rep3.
QUOTIENT R3 abs3 rep3 ⇒
∀R4 abs4 rep4.
QUOTIENT R4 abs4 rep4 ⇒
∀f g.
f ## g =
((rep1 ## rep3) --> (abs2 ## abs4))
((abs1 --> rep2) f ## (abs3 --> rep4) g)
- PAIR_MAP_RSP
-
|- ∀R1 abs1 rep1.
QUOTIENT R1 abs1 rep1 ⇒
∀R2 abs2 rep2.
QUOTIENT R2 abs2 rep2 ⇒
∀R3 abs3 rep3.
QUOTIENT R3 abs3 rep3 ⇒
∀R4 abs4 rep4.
QUOTIENT R4 abs4 rep4 ⇒
∀f1 f2 g1 g2.
(R1 ===> R2) f1 f2 ∧ (R3 ===> R4) g1 g2 ⇒
((R1 ### R3) ===> R2 ### R4) (f1 ## g1) (f2 ## g2)