|- (getBLOCK z (H_BLOCK y) = y) ∧ (getBLOCK z H_EMP = z) ∧
   (getBLOCK z (H_REF v2) = z)

|- ∀a b. a =+ b = (λf c. if a = c then b else f c)

|- (rel_move (H_DATA x,j,m,b,e,b2,e2) = (H_DATA x,j,m)) ∧
   (rel_move (H_ADDR a,j,m,b,e,b2,e2) =
    case m a of
      H_EMP => (H_ADDR j,j,m)
    | H_REF i => (H_ADDR i,j,m)
    | H_BLOCK (xs,n,d) =>
        (let m = (a =+ H_REF j) m in
         let m = (j =+ H_BLOCK (xs,n,d)) m
         in
           (H_ADDR j,j + n + 1,m)))

|- (∀m j e2 e b2 b. rel_move_list ([],j,m,b,e,b2,e2) = ([],j,m)) ∧
   ∀xs x m j e2 e b2 b.
     rel_move_list (x::xs,j,m,b,e,b2,e2) =
     (let (x',j',m') = rel_move (x,j,m,b,e,b2,e2) in
      let (xs',j'',m'') = rel_move_list (xs,j',m',b,e,b2,e2)
      in
        (x'::xs',j'',m''))

|- ∀z i j m b e b2 e2.
     rel_gc_step z (i,j,m,b,e,b2,e2) =
     (let (xs,n,d) = getBLOCK z (m i) in
      let (ys,j,m) = rel_move_list (xs,j,m,b,e,b2,e2) in
      let m = (i =+ H_BLOCK (ys,n,d)) m in
      let i = i + n + 1
      in
        (i,j,m))

|- rel_gc_loop z (i,j,m,b,e,b2,e2) =
   if i = j then
     (i,m)
   else if ¬(i < j ∧ j ≤ e) then
     (i,m)
   else
     (let (i',j',m') = rel_gc_step z (i,j,m,b,e,b2,e2) in
      let (i'',m'') = rel_gc_loop z (i',j',m',b,e,b2,e2)
      in
        (i'',m''))

|- ∀i j k. RANGE (i,j) k ⇔ i ≤ k ∧ k < j

|- ∀i j m. CUT (i,j) m = (λk. if RANGE (i,j) k then m k else H_EMP)

|- ∀z b e b2 e2 roots m.
     rel_gc z (b,e,b2,e2,roots,m) =
     (let (b2,e2,b,e) = (b,e,b2,e2) in
      let (roots,j,m) = rel_move_list (roots,b,m,b,e,b2,e2) in
      let (i,m) = rel_gc_loop z (b,j,m,b,e,b2,e2) in
      let m = CUT (b,i) m
      in
        (b,i,e,b2,e2,roots,m))