fun_signature.sats

fun_signature.sats

(* Normal Function *)
fun{a:vt0p}
list_vt_reverse_append
  {m,n:int} .<m>. (
  list_vt (INV(a), m), list_vt (a, n)
) : list_vt (a, m+n)

(* Mixed Function *)
fun{a:vt0p}
gflist_vt_revapp
  {xs1,xs2:ilist} .<xs1>. (
  xs1: gflist_vt (INV(a), xs1), xs2: gflist_vt (a, xs2)
) : [res:ilist] (REVAPP (xs1, xs2, res) | gflist_vt (a, res))

(* Proof Function *)
prfun
lemma_revapp_length
  {xs,ys,zs:ilist}{m,n:int} .<xs>. (
  pf: REVAPP (xs, ys, zs), pf1len: LENGTH (xs, m), pf2len: LENGTH (ys, n)
) : LENGTH (zs, m+n)