From Undecidability.L.Tactics Require Import LTactics.
From Undecidability.L.Datatypes Require Import LNat LTerm LBool LProd List.List_enc LOptions.


Instance term_nat_enc : computableTime' (enc (X:= nat)) (fun n _ => (n * 14 + 12,tt)).
Proof.
  unfold enc;cbn. extract. solverec.
Qed.


Instance term_term_enc : computableTime' (enc (X:=term)) (fun s _ => (size s * 30,tt)).
Proof.
  unfold enc;cbn. extract. solverec.
Qed.

Instance bool_enc :computableTime' (enc (X:=bool)) (fun l _ => (12,tt)).
Proof.
  unfold enc;cbn. extract. solverec.
Qed.


Instance term_prod_enc X Y (R1:encodable X) (R2:encodable Y) t__X t__Y
         `{computableTime' (@enc X _) t__X} `{computableTime' (@enc Y _) t__Y}
  :computableTime' (enc (X:=X*Y)) (fun w _ => (let '(x,y):= w in fst (t__X x tt) + fst (t__Y y tt) + 15,tt)).
Proof.
  unfold enc;cbn.
  extract. solverec.
Qed.

Instance term_list_enc X (R:encodable X) t__X
         `{computableTime' (@enc X _) t__X}
  :computableTime' (enc (X:=list X)) (fun l _ => (sumn (map (fun x => fst (t__X x tt) + 17) l) + 12,tt)).
Proof.
  unfold enc;cbn.
  extract. solverec.
Qed.

Import LOptions.

Instance term_option_enc X (R:encodable X) t__X
         `{computableTime' (@enc X _) t__X}
  :computableTime' (enc (X:=option X)) (fun x _ => (match x with Some x => fst (t__X x tt) | _ => 0 end + 15,tt)).
Proof.
  unfold enc;cbn.
  extract. solverec.
Qed.