| DISP | lang_rel_df | Rl== Rl |
| ABS | lang_rel | Rl ==  x,y. z:A List. L (z @ x)    L (z @ y) |
| THM | lang_rel_wf | A: . L:L(A). Rl  A List   A List  |
| THM | lang_rel_refl | A:. L:L(A). Refl(A List;x,y.x Rl y) |
| THM | lang_rel_symm | A:. L:L(A). Sym(A List;x,y.x Rl y) |
| THM | lang_rel_tran | A:. L:L(A). Trans(A List;x,y.x Rl y) |
| THM | lang_rel_equi | A:. L:L(A). EquivRel(A List;x,y.x Rl y) |
| DISP | mn_quo_append_df | <z:z:*>@ <x:x:*>== <z>@<x> |
| ABS | mn_quo_append | z@x == z @ x |
| THM | mn_quo_append_wf | A:. R:A List A List .
EquivRel(A List;x,y.x R y)
(x,y,z:A List. x R y (z @ x) R (z @ y))
(z:A List. y:x,y:(A List)//(x R y).
z@y x,y:(A List)//(x R y)) |
| THM | mn_quo_append_assoc | Alph:. R:Alph List Alph List .
EquivRel(Alph List;x,y.x R y)
(x,y,z:Alph List. x R y (z @ x) R (z @ y))
(z1,z2:Alph List. y:x,y:(Alph List)//(x R y).
z1 @ z2@y = z1@z2@y) |
| DISP | lquo_rel_df | Rg== Rg |
| ABS | lquo_rel | Rg == x,y.z:A List.  (g z@x) (g z@y) |
| THM | lquo_rel_wf | A:. R:A List A List .
EquivRel(A List;x,y.x R y)
(x,y,z:A List. x R y (z @ x) R (z @ y))
(g:x,y:(A List)//(x R y) 
Rg x,y:(A List)//(x R y) x,y:(A List)//(x R y) ) |
| THM | lquo_rel_refl | A:. R:A List A List .
EquivRel(A List;x,y.x R y)
(x,y,z:A List. x R y (z @ x) R (z @ y))
(g:x,y:(A List)//(x R y)
Refl(x,y:(A List)//(x R y);u,v.u Rg v)) |
| THM | lquo_rel_symm | A:. R:A List A List .
EquivRel(A List;x,y.x R y)
(x,y,z:A List. x R y (z @ x) R (z @ y))
(g:x,y:(A List)//(x R y)
Sym(x,y:(A List)//(x R y);u,v.u Rg v)) |
| THM | lquo_rel_tran | A:. R:A List A List .
EquivRel(A List;x,y.x R y)
(x,y,z:A List. x R y (z @ x) R (z @ y))
(g:x,y:(A List)//(x R y)
Trans(x,y:(A List)//(x R y);u,v.u Rg v)) |
| THM | lquo_rel_equi | A:. R:A List A List .
EquivRel(A List;x,y.x R y)
(x,y,z:A List. x R y (z @ x) R (z @ y))
(g:x,y:(A List)//(x R y)
EquivRel(x,y:(A List)//(x R y);u,v.u Rg v)) |
| THM | Rl_iff_Rg | A:. R:A List A List .
EquivRel(A List;x,y.x R y)
(x,y,z:A List. x R y (z @ x) R (z @ y))
(g:x,y:(A List)//(x R y) . L:L(A).
(l:A List. L l (g l))
(x,y:A List. x Rl y x Rg y)) |
| THM | mn_23_refinment | Alph:. L:L(Alph). R:Alph List Alph List .
EquivRel(Alph List;x,y.x R y)
( g:x,y:(Alph List)//(x R y) . l:Alph List. L l (g l))
 (x,y,z:Alph List. x R y (z @ x) R (z @ y))
(x,y:Alph List. x R y x Rl y) |
| THM | assert_iff_eq | a,b:. (a b) a = b |
| THM | mn_23_lem_0 | P: . n:.
(k:{n...}. P k (i:k. P i)) (m:. P m) (m:n. P m) |
| THM | nxn_plus_1_ge_0 | n:. n * n + 1 |
| THM | mn_23_lem_1 | Alph:. L:L(Alph). R:Alph List Alph List .
Fin(Alph)
EquivRel(Alph List;x,y.x R y)
Fin(x,y:(Alph List)//(x R y))
(x,y,z:Alph List. x R y (z @ x) R (z @ y))
(g:x,y:(Alph List)//(x R y)
(l:Alph List. L l (g l))
(x,y:x,y:(Alph List)//(x R y). Dec(x Rg y))) |
| THM | mn_23_Rl_equal_Rg | Alph:. L:L(Alph). R:Alph List Alph List .
EquivRel(Alph List;x,y.x R y)
(x,y,z:Alph List. x R y (z @ x) R (z @ y))
(g:x,y:(Alph List)//(x R y)
(l:Alph List. L l (g l))
x,y:(Alph List)//(x Rl y) = x,y:(Alph List)//(x Rg y)) |
| THM | mn_23 | n:{1...}. A:. L:L(A). R:A List A List .
Fin(A)
EquivRel(A List;x,y.x R y)
1-1-Corresp(n;x,y:(A List)//(x R y))
(x,y,z:A List. x R y (z @ x) R (z @ y))
(g:x,y:(A List)//(x R y) . l:A List. L l (g l))
(m:. 1-1-Corresp(m;x,y:(A List)//(x Rl y)))
(l:A List. Dec(L l)) |