mod* ID {
[Id]
pred _=_ : Id Id {comm}
eq (I:Id = I) = true .
}

-- set
mod* SET(I :: ID){
 [Id < Set]
 op empty : -> Set {constr}
 op (_U_) : Set Set -> Set {constr assoc comm}
 eq (S:Set U S) = S .

 vars I I' : Id
 vars S S' : Set

 -- (I in S) indicates whether I is an element of S
 pred _in_ : Id Set .
 eq I in empty = false .
 eq I in I' = if I = I' then true else false fi .
 eq I in I' U S = if I = I' then true else I in S fi .

 -- (S <s S') indicates whether S is subset of S'
 pred _<s_ : Set Set
 eq empty <s S = true .
 eq I <s S = if I in S then true else false fi .
 eq I U S <s S' = if I in S' then S <s S' else false fi .

 -- equality on Set
 pred _=_ : Set Set {comm}
 eq[1]: (S = S) = true .
 eq[2]: (S = S') = (S <s S') and (S' <s S) .
}

-- ======================================================
-- graph and spanning forest
-- ======================================================

mod* VERTEX {
[Vertex]
pred _=_ : Vertex Vertex {comm}
eq (A:Vertex = A) = true .
}

mod* GRAPH(V :: VERTEX){
[Edge]
[Graph]

op <_,_> : Vertex Vertex -> Edge {constr}
op nil : -> Graph {constr}
op _;_ :  Edge Graph -> Graph {constr}
}

mod* SFOREST (V :: VERTEX){
us(INT)
us(SET(V{sort Id -> Vertex})*{sort Set -> VtxSet})
us(GRAPH(V))

vars A B C : Vertex
var G : Graph

op mcc : Vertex Graph -> VtxSet
eq mcc(A,nil) = A .
eq mcc(A, < B,C > ; G) =
     if mcc(A,G) = mcc(B,G) or mcc(A,G) = mcc(C,G)
     then (mcc(B,G) U mcc(C,G)) else mcc(A,G) fi .


pred nocycle : Graph
 eq nocycle(nil) = true .
 eq nocycle(< A,B > ; G) = if mcc(A,G) = mcc(B,G) then false
                       else nocycle(G) fi .

op #cc : Graph -> Int .
op #vertexes : -> Nat .
 eq #cc(nil) = #vertexes .
 eq #cc(< A,B > ; G) = if mcc(A,G) = mcc(B,G) then #cc(G)
                   else #cc(G) - 1 fi .

-- mktree(G) returns the spanning forest of G
 op mktree : Graph -> Graph
 eq mktree(nil) = nil .
 eq mktree(< A,B > ; G) = if mcc(A,G) = mcc(B,G) then mktree(G)
                      else < A,B > ; mktree(G) fi .
}

-- Lemma 1 : mcc(A,mktree(G)) = mcc(A,G)

-- base case 
open SFOREST
op a : -> Vertex .
red mcc(a,mktree(nil)) = mcc(a,nil) .
close

-- induction step: inv(a , < b,c > ; g) 
-- subcase: mcc(b,g) = mcc(c,g), mcc(a,g) = mcc(c,g)
open SFOREST
ops a b c : -> Vertex .
op g : -> Graph .
var A : Vertex .
eq mcc(A,mktree(g)) = mcc(A,g) .   -- IH
eq mcc(b,g) = mcc(c,g) .           -- subcase hypothesis
eq mcc(a,g) = mcc(c,g) .           -- subcase hypothesis
red mcc(a,mktree(< b,c > ; g)) = mcc(a, < b,c > ; g) . 
close


-- subcase: mcc(b,g) = mcc(c,g) , ~ mcc(a,g) = mcc(c,g)
open SFOREST
ops a b c : -> Vertex .
op g : -> Graph .
var A : Vertex .
eq mcc(A,mktree(g)) = mcc(A,g) .    -- IH 
eq mcc(b,g) = mcc(c,g) .            -- subcase hypothesis
eq (mcc(a,g) = mcc(c,g)) = false .  -- subcase hypothesis
red mcc(a,mktree(< b,c > ; g)) = mcc(a, < b,c > ; g) . 
close

-- subcase: ~ mcc(b,g) = mcc(c,g) ,  mcc(a,g) = mcc(b,g)
open SFOREST
ops a b c : -> Vertex .
op g : -> Graph .
var A : Vertex
eq mcc(A,mktree(g)) = mcc(A,g) .     -- IH
eq (mcc(b,g) = mcc(c,g)) = false .   -- subcase hypothesis
eq mcc(a,g) = mcc(b,g) .             -- subcase hypothesis
red mcc(a,mktree(< b,c > ; g)) = mcc(a, < b,c > ; g) . 
close

-- subcase: ~ mcc(b,g) = mcc(c,g) , mcc(a,g) = mcc(c,g)
open SFOREST
ops a b c : -> Vertex .
op g : -> Graph .
var A : Vertex
eq mcc(A,mktree(g)) = mcc(A,g) .    -- IH
eq (mcc(b,g) = mcc(c,g)) = false .  -- subcase hypothesis
eq mcc(a,g) = mcc(c,g) .            -- subcase hypothesis
red mcc(a,mktree(< b,c > ; g)) = mcc(a, < b,c > ; g) . 
close

-- subcase: ~ mcc(b,g) = mcc(c,g) , ~ mcc(a,g) = mcc(b,g) , ~ mcc(a,g) = mcc(c,g)
open SFOREST
ops a b c : -> Vertex .
op g : -> Graph .
var A : Vertex 
eq mcc(A,mktree(g)) = mcc(A,g) .     -- IH
eq (mcc(b,g) = mcc(c,g)) = false .   -- subcase hypothesis
eq (mcc(a,g) = mcc(b,g)) = false .   -- subcase hypothesis
eq (mcc(a,g) = mcc(c,g)) = false .   -- subcase hypothesis
red mcc(a,mktree(< b,c > ; g)) = mcc(a, < b,c > ; g) . 
close


-- Theorem 1 :  #cc(mktree(G)) = #cc(G) . 

-- base case 
open SFOREST + EQL
red #cc(mktree(nil)) = #cc(nil) .
close



-- induction step: #cc(< a,b> ; g) = #cc(mktree(< a,b> ; g))
-- subcase: mcc(a,g) = mcc(b,g)
open SFOREST + EQL 
ops a b : -> Vertex .
op g : -> Graph .
eq [IH] : #cc(mktree(g)) = #cc(g) .   -- IH
eq mcc(a,g) = mcc(b,g) .            -- subcase hypothesis
red  #cc(mktree(< a,b > ; g)) = #cc(< a,b > ; g) . 
close

-- subcase:  ~ (mcc(a,g) = mcc(b,g))
open SFOREST + EQL
ops a b : -> Vertex .
op g : -> Graph .
var A : Vertex .
var G : Graph .
eq [IH] : #cc(mktree(g)) = #cc(g) .    -- IH
eq (mcc(a,g) = mcc(b,g)) = false .   -- subcase hypothesis
eq mcc(A,mktree(G)) = mcc(A,G) .  
red #cc(mktree(< a,b > ; g)) = #cc(< a,b > ; g) . 
close






-- Theorem 2 : nocycle(mktree(G)) = true 

-- base case 
open SFOREST
red nocycle(mktree(nil)) .
close

-- the induction step: < a,b > ; g
-- subcase: mcc(a,g) = mcc(b,g)
open SFOREST
ops a b : -> Vertex .
op g : -> Graph .
eq [IH] : nocycle(mktree(g)) = true .  -- IH
eq mcc(a,g) = mcc(b,g) .               -- subcase hypothesis
red nocycle(mktree(< a,b > ; g)) .
close

-- subcase: ~ mcc(a,g) = mcc(b,g)
open SFOREST
ops a b : -> Vertex .
op g : -> Graph .
var A : Vertex .
var G : Graph .
eq [IH] : nocycle(mktree(g)) = true . -- IH
eq (mcc(a,g) = mcc(b,g)) = false .    -- subcase hypothsis
eq mcc(A,mktree(G)) = mcc(A,G) .  
red nocycle(mktree(< a,b > ; g)) .
close