Library Exercise_3_3_1_9


Require Import Utf8.
Require Import Peano_dec.
Require Import Common Graph.

Set Implicit Arguments.

Generalizable All Variables.


Exercise 3.3.1.9

Section Exercise_3_3_1_9.
  Example Exercise_3_3_1_9' : Graph' :=
    {| Vertex' := × ;
       Arrow' := { nmn'm' : ( × ) × ( × )
                 | let n := fst (fst nmn'm') in
                   let m := snd (fst nmn'm') in
                   let n' := fst (snd nmn'm') in
                   let m' := snd (snd nmn'm') in
                   (n = n' m + 1 = m') (m = m' n + 1 = n') };
       Graph'Source := (fun x fst (proj1_sig x));
       Graph'Target := (fun x snd (proj1_sig x)) |}.

  Local Infix "=" := eq_nat_dec : nat_scope.

  Example Exercise_3_3_1_9 : Graph :=
    {| Vertex := × ;
       Edge := (fun nm n'm' let n := fst nm in
                               let m := snd nm in
                               let n' := fst n'm' in
                               let m' := snd n'm' in
                               if (((n = n') && (m + 1 = m'))
                                     || ((m = m') && (n + 1 = n')))%bool
                               then unit
                               else ∅) |}.
End Exercise_3_3_1_9.