-- ======================================================
-- the code written again
-- ======================================================

-- ======================================================
-- set
-- ======================================================

mod* ID {
[Id]
op _=_ : Id Id -> Bool {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
 op _in_ : Id Set -> Bool .
 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'
 op _<s_ : Set Set -> Bool
 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
 op _=_ : Set Set -> Bool {comm}
 eq[1]: (S = S) = true .
}

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

mod* VERTEX {
[Vertex]
op _=_ : Vertex Vertex -> Bool {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){
inc(INT)
inc(SET(V{sort Id -> Vertex})*{sort Set -> VtxSet})
inc(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 .


op nocycle : Graph -> Bool
 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 .
}
-- ======================================================
-- Exercise (solution for the first exercise)
-- ======================================================
mod* EX{
inc(SFOREST)
op _=_ : Edge Edge -> Bool {comm}
vars A B C D : Vertex .
var E : Edge . 
eq (E = E) = true .
ceq < A,B > = < C,D > if (A = C and B = D) .
ceq < A,B > = < C,D > if (A = D and B = C) .
op _in_ : Edge Graph -> Bool .
var G : Graph
vars E E' : Edge 
eq E in nil = false .
ceq E in E' ; G = true if (E = E') .
ceq E in E' ; G = E in G if not(E = E') .
}

-- (E:Edge in G:Graph) = true if (E in mktree(G)) .
-- We make the proof by induction on the structure of G

-- (IB) (forall G:Graph). (forall E:Edge). (E in nil) = true if (E in mktree(nil)) 
-- (IB) (forall G:Graph). (forall E:Edge).(E in G:Graph) = true if (E in mktree(G)) 
--      implies
--      (forall E1:Edge).(forall E_2:Edge).(E1 in E2;G) = true if (E1 in mktree(E2;G))

-- proof for (IB)
open EX
red E in mktree(nil) implies E in nil .
close  


-- proof for (IS)  
mod* INV{
inc(EX)
op g : -> Graph
vars E : Edge .
ceq [IH]: (E in g) = true if (E in mktree(g)) .
-- we need to prove 
-- (forall E1:Edge).(forall E_2:Edge).(E1 in E2;g) = true if (E1 in mktree(E2;g))
-- we use induction on the structure of E1 and E2
ops a b a' b' : -> Vertex .
-- our goal restated:
-- (< a', b' > in < a,b > ; g) = true if (< a',b' > in mktree(< a,b > ; G))
-- using the rule of implications we add  
eq [II]: < a',b' > in  mktree(< a,b > ; g) = true .   
} 


-- We use Case Analysis 
-- mcc(a,g) = mcc(b,g), < a,b > = < a',b' > 
open INV
eq mcc(a,g) = mcc(b,g) .
red mktree(< a,b > ; g)  .
eq < a',b' > = < a,b > .
red < a',b' > in < a,b > ; g .
close


-- mcc(a,g) = mcc(b,g), ~ < a,b > = < a',b' > 
open INV
eq mcc(a,g) = mcc(b,g) .                  -- subcase hypothesis
eq (< a',b' > = < a,b >) = false .        --  subcase hypothesis
red < a',b' > in mktree(< a,b > ; g)  .   **>  < a',b' > in mktree(g)
eq [II']: < a',b' > in mktree(g) = true . --  consequence of II 
red < a',b' > in < a,b > ; g .
close

-- ~ mcc(a,g) = mcc(b,g), < a,b > = < a',b' > 
open INV
eq (mcc(a,g) = mcc(b,g)) = false .      -- subcase hypothesis 
eq < a',b' > = < a,b > .                -- subcase hypothesis
red < a',b' > in < a,b > ; g .
close

-- ~ mcc(a,g) = mcc(b,g), ~ < a,b > = < a',b' > 
open INV
eq (mcc(a,g) = mcc(b,g)) = false .        -- subcase hypothesis
eq (< a',b' > = < a,b >) = false .        -- subcase hypothesis 
red < a',b' > in mktree(< a,b > ; g) .    **> < a',b' > in mktree(g) 
eq [II']: < a',b' > in mktree(g) = true . --  consequence of II 
red < a',b' > in < a,b > ; g .
close