Wikimedia.ml

open Mat
open Nat
open Path

type coq_Node =
| TC
| SK
| KW
| MR
| LG
| CB
| HC
| JSR
| PL
| JG
| JF
| FSS
| GM
| MP
| EZ
| WHD
| UW
| TM

(** val coq_Node_rect :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> coq_Node -> 'a1 **)

let coq_Node_rect f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 = function
| TC -> f
| SK -> f0
| KW -> f1
| MR -> f2
| LG -> f3
| CB -> f4
| HC -> f5
| JSR -> f6
| PL -> f7
| JG -> f8
| JF -> f9
| FSS -> f10
| GM -> f11
| MP -> f12
| EZ -> f13
| WHD -> f14
| UW -> f15
| TM -> f16

(** val coq_Node_rec :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> coq_Node -> 'a1 **)

let coq_Node_rec f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 = function
| TC -> f
| SK -> f0
| KW -> f1
| MR -> f2
| LG -> f3
| CB -> f4
| HC -> f5
| JSR -> f6
| PL -> f7
| JG -> f8
| JF -> f9
| FSS -> f10
| GM -> f11
| MP -> f12
| EZ -> f13
| WHD -> f14
| UW -> f15
| TM -> f16

(** val eqN : coq_Node -> coq_Node -> bool **)

let eqN x y =
  match x with
  | TC -> (match y with
           | TC -> true
           | _ -> false)
  | SK -> (match y with
           | SK -> true
           | _ -> false)
  | KW -> (match y with
           | KW -> true
           | _ -> false)
  | MR -> (match y with
           | MR -> true
           | _ -> false)
  | LG -> (match y with
           | LG -> true
           | _ -> false)
  | CB -> (match y with
           | CB -> true
           | _ -> false)
  | HC -> (match y with
           | HC -> true
           | _ -> false)
  | JSR -> (match y with
            | JSR -> true
            | _ -> false)
  | PL -> (match y with
           | PL -> true
           | _ -> false)
  | JG -> (match y with
           | JG -> true
           | _ -> false)
  | JF -> (match y with
           | JF -> true
           | _ -> false)
  | FSS -> (match y with
            | FSS -> true
            | _ -> false)
  | GM -> (match y with
           | GM -> true
           | _ -> false)
  | MP -> (match y with
           | MP -> true
           | _ -> false)
  | EZ -> (match y with
           | EZ -> true
           | _ -> false)
  | WHD -> (match y with
            | WHD -> true
            | _ -> false)
  | UW -> (match y with
           | UW -> true
           | _ -> false)
  | TM -> (match y with
           | TM -> true
           | _ -> false)

type coq_R =
| Left of int
| Infinity

(** val coq_R_rect : (int -> 'a1) -> 'a1 -> coq_R -> 'a1 **)

let coq_R_rect f f0 = function
| Left n -> f n
| Infinity -> f0

(** val coq_R_rec : (int -> 'a1) -> 'a1 -> coq_R -> 'a1 **)

let coq_R_rec f f0 = function
| Left n -> f n
| Infinity -> f0

(** val eqR : coq_R -> coq_R -> bool **)

let eqR u v =
  match u with
  | Left x -> (match v with
               | Left y -> eqb x y
               | Infinity -> false)
  | Infinity -> (match v with
                 | Left _ -> false
                 | Infinity -> true)

(** val zeroR : coq_R **)

let zeroR =
  Left 0

(** val oneR : coq_R **)

let oneR =
  Infinity

(** val plusR : coq_R -> coq_R -> coq_R **)

let plusR u v =
  match u with
  | Left x -> (match v with
               | Left y -> Left (max x y)
               | Infinity -> Infinity)
  | Infinity -> Infinity

(** val mulR : coq_R -> coq_R -> coq_R **)

let mulR u v =
  match u with
  | Left x -> (match v with
               | Left y -> Left (min x y)
               | Infinity -> Left x)
  | Infinity -> v

(** val finN : coq_Node list **)

let finN =
  TC::(SK::(KW::(MR::(LG::(CB::(HC::(JSR::(PL::(JG::(JF::(FSS::(GM::(MP::(EZ::(WHD::(UW::(TM::[])))))))))))))))))

(** val wikimedia :
    (coq_Node, coq_R) coq_Matrix -> (coq_Node, coq_R) coq_Matrix **)

let wikimedia m =
  matrix_exp_binary eqN finN zeroR oneR plusR mulR m ((fun p->2*p)
    ((fun p->1+2*p) ((fun p->2*p) 1)))