top :
top 1 :
top 1 1 :
top 1 1 1 :
top 1 1 1 1 :
top 1 2 :
top 1 2 1 :
top 1 2 1 1 :
top 1 2 1 1 1 :
top 1 2 1 1 1 1 :
(TCC)
r2_TCC1:
OBLIGATION
FORALL
(G:Graph[T])
:
is
finite[T](LET
(v0:(vert(G))
)
=
choose[T](vert(G))
IN
{(n:T)
|
vert(G)(n)
AND
(n
/=
v0)
AND
(NOT
edge?[T](G)(v0,
n))})
Subproof Addresses (10 steps)
top :
top 1 :
top 1 1 :
top 1 1 1 :
top 1 1 1 1 :
top 1 2 :
top 1 2 1 :
top 1 2 1 1 :
top 1 2 1 1 1 :
top 1 2 1 1 1 1 :