l,x. if P(x)
[x / l] else l fi),nil)
t:GraphObject(the_graph), T:Type. t.vacc 
(T
VT)TTA:Type, B:(AType), p:(a:A
B(a)). 2of(p) B(1of(p))A:Type, B:(AType), p:(a:AB(a)). 1of(p) A| Who Cites vertex-subset? | |
| vertex-subset | Def vertex-subset(the_obj;x.P(x)) == the_obj.vacc((l,x. if P(x) [x / l] else l fi),nil) |
| gro_vacc | Def t.vacc == 1of(2of(2of(2of(2of(t))))) |
| Thm* For any graph
t:GraphObject(the_graph), T:Type. t.vacc (TVT)TT | |
| pi2 | Def 2of(t) == t.2 |
| Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p) B(1of(p)) | |
| pi1 | Def 1of(t) == t.1 |
| Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A |
| Syntax: | vertex-subset(the_obj;x.P(x)) | has structure: | vertex-subset(the_obj; x.P(x)) |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |
 |