Theory CoCallImplTTree

theory CoCallImplTTree
imports TTreeAnalysisSig "Env-Set-Cpo" CoCallAritySig "CoCallGraph-TTree"
begin

context CoCallArity
begin
  definition Texp :: "exp ⇒ Arity → var ttree"
    where "Texp e = (Λ a. ccTTree (edom (Aexp e ⋅a)) (ccExp e⋅a))"
  
  lemma Texp_simp: "Texp e⋅a = ccTTree (edom (Aexp e ⋅a)) (ccExp e⋅a)"
    unfolding Texp_def
    by simp

  sublocale TTreeAnalysis Texp.
end



end