```(def-language graph-language
(embedded-language the-kernel-theory)
(base-types vertices edges)
(constants
(endpoints "[edges -> sets[vertices]]")))
```

```
(def-theory graphs
(language graph-language)
(component-theories h-o-real-arithmetic)
(axioms
(edges-have-two-endpoints
"forall(e:edges, forsome(v_1,v_2: vertices,
endpoints(e) = singleton{v_1} union singleton{v_2}))")))
```

```
(def-theorem endpoints-is-total
"total_q{endpoints,[edges -> sets[vertices]]}"
(usages d-r-convergence)
(theory graphs)
(proof
(
insistent-direct-inference
(instantiate-theorem edges-have-two-endpoints ("x_0"))
)))
```

```
(def-constant loop
"lambda(e:edges, singleton{endpoints(e)})"
(theory graphs))
```

```
(def-constant parallel
"lambda(e_1,e_2:edges, endpoints(e_1) = endpoints(e_2))"
(theory graphs))
```

```
"lambda(v_1,v_2:vertices, forsome(e:edges,
endpoints(e) = singleton{v_1} union singleton{v_2}))"
(theory graphs))
```

```
"lambda(e_1,e_2:edges, forsome(v:vertices,
v in endpoints(e_1)  and v in endpoints(e_2)))"
(theory graphs))
```

```
(def-constant vertex%incidence%set
"lambda(v:vertices, indic{e:edges, v in endpoints(e)})"
(theory graphs))
```

```
(def-constant degree
"lambda(v:vertices, f_card{vertex%incidence%set(v)})"
(theory graphs))
```

```
(def-constant isolated
"lambda(v:vertices, degree(v) = 0)"
(theory graphs))
```