Theory TTreeImplCardinalitySafe

theory TTreeImplCardinalitySafe
imports TTreeImplCardinality TTreeAnalysisSpec CardinalityAnalysisSpec
begin

lemma pathsCard_paths_nxt:  "pathsCard (paths (nxt f x)) ⊑ record_call x⋅(pathsCard (paths f))"
  apply transfer
  apply (rule pathsCard_below)
  apply auto
  apply (erule below_trans[OF _ monofun_cfun_arg[OF paths_Card_above], rotated]) back
  apply (auto intro: fun_belowI simp add: record_call_simp two_pred_two_add_once)
  done

lemma pathsCards_none: "pathsCard (paths t) x = none ⟹ x ∉ carrier t"
  by transfer (auto dest: pathCards_noneD)

lemma const_on_edom_disj: "const_on f S empty ⟷ edom f ∩ S = {}"
  by (auto simp add: empty_is_bottom edom_def)

context TTreeAnalysisCarrier
begin
  lemma carrier_Fstack: "carrier (Fstack as S) ⊆ fv S"
    by (induction S rule: Fstack.induct)
       (auto simp add: empty_is_bottom[symmetric] carrier_Fexp dest!: subsetD[OF Aexp_edom])

  lemma carrier_FBinds: "carrier ((FBinds Γ⋅ae) x) ⊆ fv Γ"
  apply (simp add: Texp.AnalBinds_lookup)
  apply (auto split: option.split simp add: empty_is_bottom[symmetric] )
  apply (case_tac "ae x")
  apply (auto simp add: empty_is_bottom[symmetric] carrier_Fexp dest!: subsetD[OF Aexp_edom])
  by (metis (poly_guards_query) contra_subsetD domA_from_set map_of_fv_subset map_of_SomeD option.sel)
end

context TTreeAnalysisSafe
begin

  sublocale CardinalityPrognosisShape prognosis
  proof
    fix Γ :: heap and ae ae' :: AEnv and u e S as
    assume "ae f|` domA Γ = ae' f|` domA Γ"
    from Texp.AnalBinds_cong[OF this]
    show "prognosis ae as u (Γ, e, S) = prognosis ae' as u (Γ, e, S)" by simp
  next
    fix ae as a Γ e S
    show "const_on (prognosis ae as a (Γ, e, S)) (ap S) many"
    proof
      fix x
      assume "x ∈ ap S"
      hence "[x,x] ∈ paths (Fstack as S)"
        by (induction S rule: Fstack.induct)
           (auto 4 4 intro: subsetD[OF both_contains_arg1] subsetD[OF both_contains_arg2] paths_Cons_nxt)
      hence "[x,x] ∈ paths (Texp e⋅a ⊗⊗ Fstack as S)"
        by (rule subsetD[OF both_contains_arg2])
      hence "[x,x] ∈ paths (substitute (FBinds Γ⋅ae) (thunks Γ) (Texp e⋅a ⊗⊗ Fstack as S))" 
        by (rule subsetD[OF substitute_contains_arg])
      hence "pathCard [x,x] x ⊑ pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks Γ) (Texp e⋅a ⊗⊗ Fstack as S))) x"
        by (metis fun_belowD paths_Card_above)
      also have "pathCard [x,x] x = many"  by (auto simp add: pathCard_def)
      finally
      show "prognosis ae as a (Γ, e, S) x = many"
        by (auto intro: below_antisym)
    qed
  next
    fix Γ Δ :: heap and e :: exp and ae :: AEnv and as u S
    assume "map_of Γ = map_of Δ"
    hence "FBinds Γ = FBinds Δ" and "thunks Γ = thunks Δ" by (auto intro!: cfun_eqI  thunks_cong simp add: Texp.AnalBinds_lookup)
    thus "prognosis ae as u (Γ, e, S) = prognosis ae as u (Δ, e, S)"  by simp
  next
    fix Γ :: heap and e :: exp and ae :: AEnv and as u S x
    show "prognosis ae as u (Γ, e, S) ⊑ prognosis ae as u (Γ, e, Upd x # S)" by simp
  next
  fix Γ :: heap and e :: exp and ae :: AEnv and as a S x
  assume "ae x = ⊥"

  hence "FBinds (delete x Γ)⋅ae = FBinds Γ⋅ae" by (rule Texp.AnalBinds_delete_bot)
  moreover
  hence "((FBinds Γ⋅ae) x) = ⊥" by (metis Texp.AnalBinds_delete_lookup)
  ultimately
  show "prognosis ae as a (Γ, e, S) ⊑ prognosis ae as a (delete x Γ, e, S)"
    by (simp add: substitute_T_delete empty_is_bottom)
  next
    fix ae as a Γ x S
    have "once ⊑ (pathCard [x]) x" by (simp add: two_add_simp)
    also have "pathCard [x] ⊑ pathsCard ({[],[x]})"
      by (rule paths_Card_above) simp
    also have "… = pathsCard (paths (single x))" by simp
    also have "single x ⊑ (Texp (Var x)⋅a)" by (rule Texp_Var)
    also have "… ⊑ Texp (Var x)⋅a ⊗⊗ Fstack as S" by (rule both_above_arg1)
    also have "… ⊑ substitute  (FBinds Γ⋅ae) (thunks Γ) (Texp (Var x)⋅a ⊗⊗ Fstack as S)" by (rule substitute_above_arg)
    also have "pathsCard (paths …) x = prognosis ae as a (Γ, Var x, S) x" by simp
    finally
    show "once ⊑ prognosis ae as a (Γ, Var x, S) x"
      by this (rule cont2cont_fun, intro cont2cont)+
  qed

  sublocale CardinalityPrognosisApp prognosis
  proof
    fix ae as a Γ e x S
    have "Texp e⋅(inc⋅a)  ⊗⊗ many_calls x ⊗⊗ Fstack as S = many_calls x  ⊗⊗ (Texp e)⋅(inc⋅a) ⊗⊗ Fstack as S"
      by (metis both_assoc both_comm)
    thus "prognosis ae as (inc⋅a) (Γ, e, Arg x # S) ⊑ prognosis ae as a (Γ, App e x, S)"
      by simp (intro pathsCard_mono' paths_mono substitute_mono2' both_mono1' Texp_App)
  qed

  sublocale CardinalityPrognosisLam prognosis
  proof
    fix ae as a Γ e y x S
    have "Texp e[y::=x]⋅(pred⋅a) ⊑ many_calls x  ⊗⊗ Texp (Lam [y]. e)⋅a"
      by (rule below_trans[OF Texp_subst both_mono2'[OF Texp_Lam]])
    moreover have "Texp (Lam [y]. e)⋅a ⊗⊗ many_calls x ⊗⊗ Fstack as S = many_calls x  ⊗⊗ Texp (Lam [y]. e)⋅a ⊗⊗ Fstack as S"
      by (metis both_assoc both_comm)
    ultimately  
    show "prognosis ae as (pred⋅a) (Γ, e[y::=x], S) ⊑ prognosis ae as a (Γ, Lam [y]. e, Arg x # S)"
      by simp (intro pathsCard_mono' paths_mono substitute_mono2' both_mono1')
  qed

  sublocale CardinalityPrognosisVar prognosis
  proof
    fix Γ :: heap and e :: exp and x :: var and ae :: AEnv and as u a S
    assume "map_of Γ x = Some e"
    assume "ae x = up⋅u"

    assume "isVal e"
    hence "x ∉ thunks Γ" using ‹map_of Γ x = Some e› by (metis thunksE)
    hence [simp]: "f_nxt (FBinds Γ⋅ae) (thunks Γ) x = FBinds Γ⋅ae" by (auto simp add: f_nxt_def)

    have "prognosis ae as u (Γ, e, S) = pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks Γ) (Texp e⋅u ⊗⊗ Fstack as S)))"
      by simp
    also have "… = pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks Γ) (nxt (single x) x ⊗⊗ Texp e⋅u  ⊗⊗ Fstack as S)))"
      by simp
    also have "… = pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks Γ) ((nxt (single x) x ⊗⊗ Fstack as S) ⊗⊗ Texp e⋅u )))"
      by (metis both_assoc both_comm)
    also have "… ⊑ pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks Γ) (nxt (single x ⊗⊗ Fstack as S) x ⊗⊗ Texp e⋅u)))"
      by (intro pathsCard_mono' paths_mono substitute_mono2' both_mono1'  nxt_both_left) simp
    also have "… = pathsCard (paths (nxt (substitute (FBinds Γ⋅ae) (thunks Γ) (single x ⊗⊗ Fstack as S)) x))"
      using ‹map_of Γ x = Some e› ‹ae x = up⋅u› by (simp add: Texp.AnalBinds_lookup)
    also have "… ⊑ record_call x ⋅(pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks Γ) (single x ⊗⊗ Fstack as S))))"
      by (rule pathsCard_paths_nxt)
    also have "… ⊑ record_call x ⋅(pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks Γ) ((Texp (Var x)⋅a) ⊗⊗ Fstack as S))))"
      by (intro monofun_cfun_arg pathsCard_mono' paths_mono substitute_mono2' both_mono1' Texp_Var)
    also have "… = record_call x ⋅(prognosis ae as a (Γ, Var x, S))"
      by simp
    finally
    show "prognosis ae as u (Γ, e, S) ⊑ record_call x⋅(prognosis ae as a (Γ, Var x, S))" by this simp_all
  next
    fix Γ :: heap and e :: exp and x :: var and ae :: AEnv and as u a S
    assume "map_of Γ x = Some e"
    assume "ae x = up⋅u"
    assume "¬ isVal e"
    hence "x ∈ thunks Γ" using ‹map_of Γ x = Some e› by (metis thunksI)
    hence [simp]: "f_nxt (FBinds Γ⋅ae) (thunks Γ) x = FBinds (delete x Γ)⋅ae" 
      by (auto simp add: f_nxt_def Texp.AnalBinds_delete_to_fun_upd empty_is_bottom)

    have "prognosis ae as u (delete x Γ, e, Upd x # S) = pathsCard (paths (substitute (FBinds (delete x Γ)⋅ae) (thunks (delete x Γ)) (Texp e⋅u ⊗⊗ Fstack as S)))"
      by simp
    also have "… = pathsCard (paths (substitute (FBinds (delete x Γ)⋅ae) (thunks Γ) (Texp e⋅u ⊗⊗ Fstack as S)))"
       by (rule arg_cong[OF substitute_cong_T]) (auto simp add: empty_is_bottom)
    also have "… = pathsCard (paths (substitute (FBinds (delete x Γ)⋅ae) (thunks Γ) (nxt (single x) x ⊗⊗ Texp e⋅u  ⊗⊗ Fstack as S)))"
      by simp
    also have "… = pathsCard (paths (substitute (FBinds (delete x Γ)⋅ae) (thunks Γ) ((nxt (single x) x ⊗⊗ Fstack as S) ⊗⊗ Texp e⋅u )))"
      by (metis both_assoc both_comm)
    also have "… ⊑ pathsCard (paths (substitute (FBinds (delete x Γ)⋅ae) (thunks Γ) (nxt (single x ⊗⊗ Fstack as S) x  ⊗⊗ Texp e⋅u)))"
      by (intro pathsCard_mono' paths_mono substitute_mono2' both_mono1'  nxt_both_left) simp
    also have "… = pathsCard (paths (nxt (substitute (FBinds Γ⋅ae) (thunks Γ) (single x ⊗⊗ Fstack as S)) x))"
      using ‹map_of Γ x = Some e› ‹ae x = up⋅u› by (simp add: Texp.AnalBinds_lookup)
    also have "… ⊑ record_call x ⋅(pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks Γ) (single x ⊗⊗ Fstack as S))))"
      by (rule pathsCard_paths_nxt)
    also have "… ⊑ record_call x ⋅(pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks Γ) ((Texp (Var x)⋅a) ⊗⊗ Fstack as S))))"
      by (intro monofun_cfun_arg pathsCard_mono' paths_mono substitute_mono2' both_mono1' Texp_Var)
    also have "… = record_call x ⋅(prognosis ae as a (Γ, Var x, S))"
      by simp
    finally
    show "prognosis ae as u (delete x Γ, e, Upd x # S) ⊑ record_call x⋅(prognosis ae as a (Γ, Var x, S))" by this simp_all
  next
    fix Γ :: heap and e :: exp and ae :: AEnv and  x :: var and as S
    assume "isVal e"
    hence "repeatable (Texp e⋅0)" by (rule Fun_repeatable)

    assume [simp]: "x ∉ domA Γ"

    have [simp]: "thunks ((x, e) # Γ) = thunks Γ" 
      using ‹isVal e›
      by (auto simp add: thunks_Cons dest: subsetD[OF thunks_domA])

    have "fup⋅(Texp e)⋅(ae x) ⊑ Texp e⋅0" by (metis fup2 monofun_cfun_arg up_zero_top)
    hence "substitute ((FBinds Γ⋅ae)(x := fup⋅(Texp e)⋅(ae x))) (thunks Γ) (Texp e⋅0 ⊗⊗ Fstack as S) ⊑ substitute ((FBinds Γ⋅ae)(x := Texp e⋅0)) (thunks Γ) (Texp e⋅0 ⊗⊗ Fstack as S)"
      by (intro substitute_mono1' fun_upd_mono below_refl monofun_cfun_arg)
    also have "… = substitute (((FBinds Γ⋅ae)(x := Texp e⋅0))(x := empty)) (thunks Γ) (Texp e⋅0 ⊗⊗ Fstack as S)"
      using ‹repeatable (Texp e⋅0)› by (rule substitute_remove_anyways, simp)
    also have "((FBinds Γ⋅ae)(x := Texp e⋅0))(x := empty) = FBinds Γ⋅ae"
      by (simp add: fun_upd_idem Texp.AnalBinds_not_there empty_is_bottom)
    finally
    show "prognosis ae as 0 ((x, e) # Γ, e, S) ⊑ prognosis ae as 0 (Γ, e, Upd x # S)"
      by (simp, intro pathsCard_mono' paths_mono)
  qed

  sublocale CardinalityPrognosisIfThenElse prognosis
  proof
    fix ae as Γ scrut e1 e2 S a
    have "Texp scrut⋅0 ⊗⊗ (Texp e1⋅a ⊕⊕ Texp e2⋅a) ⊑ Texp (scrut ? e1 : e2)⋅a"
      by (rule Texp_IfThenElse)
    hence "substitute (FBinds Γ⋅ae) (thunks Γ) (Texp scrut⋅0 ⊗⊗ (Texp e1⋅a ⊕⊕ Texp e2⋅a) ⊗⊗ Fstack as S) ⊑ substitute (FBinds Γ⋅ae) (thunks Γ) (Texp (scrut ? e1 : e2)⋅a ⊗⊗ Fstack as S)"
      by (rule substitute_mono2'[OF both_mono1'])
    thus "prognosis ae (a#as) 0 (Γ, scrut, Alts e1 e2 # S) ⊑ prognosis ae as a (Γ, scrut ? e1 : e2, S)"
      by (simp, intro pathsCard_mono' paths_mono)
  next
    fix ae as a Γ b e1 e2 S
    have "Texp (if b then e1 else e2)⋅a ⊑ Texp e1⋅a ⊕⊕ Texp e2⋅a"
      by (auto simp add: either_above_arg1 either_above_arg2)
    hence "substitute (FBinds Γ⋅ae) (thunks Γ) (Texp (if b then e1 else e2)⋅a ⊗⊗ Fstack as S) ⊑ substitute (FBinds Γ⋅ae) (thunks Γ) (Texp (Bool b)⋅0 ⊗⊗ (Texp e1⋅a ⊕⊕ Texp e2⋅a) ⊗⊗ Fstack as S)"
      by (rule substitute_mono2'[OF both_mono1'[OF below_trans[OF _ both_above_arg2]]])
    thus "prognosis ae as a (Γ, if b then e1 else e2, S) ⊑ prognosis ae (a#as) 0 (Γ, Bool b, Alts e1 e2 # S)"
      by (auto intro!: pathsCard_mono' paths_mono)
  qed

end

context TTreeAnalysisCardinalityHeap
begin

  definition cHeap where
    "cHeap Γ e = (Λ a. pathsCard (paths (Theap Γ e⋅a)))"

  lemma cHeap_simp: "(cHeap Γ e)⋅a = pathsCard (paths (Theap Γ e⋅a))"
    unfolding cHeap_def  by (rule beta_cfun) (intro cont2cont)
  
  sublocale CardinalityHeap cHeap.
 
  sublocale CardinalityHeapSafe cHeap Aheap
  proof
    fix x Γ e a
    assume "x ∈ thunks Γ"
    moreover
    assume "many ⊑ (cHeap Γ e⋅a) x"
    hence "many ⊑ pathsCard (paths (Theap Γ e ⋅a)) x" unfolding cHeap_def by simp
    hence "∃p∈ (paths (Theap Γ e⋅a)). ¬ (one_call_in_path x p)" unfolding pathsCard_def
      by (auto split: if_splits)
    ultimately
    show "(Aheap Γ e⋅a) x = up⋅0"
      by (metis Theap_thunk)
  next
    fix Γ e a
    show "edom (cHeap Γ e⋅a) = edom (Aheap Γ e⋅a)"
    by (simp add: cHeap_def Union_paths_carrier carrier_Fheap)
  qed

  sublocale CardinalityPrognosisEdom prognosis 
  proof
    fix ae as a Γ e S
    show "edom (prognosis ae as a (Γ, e, S)) ⊆ fv Γ ∪ fv e ∪ fv S"
      apply (simp add: Union_paths_carrier)
      apply (rule carrier_substitute_below)
      apply (auto simp add: carrier_Fexp dest: subsetD[OF Aexp_edom] subsetD[OF carrier_Fstack] subsetD[OF ap_fv_subset] subsetD[OF carrier_FBinds])
      done
  qed
  
  sublocale CardinalityPrognosisLet prognosis cHeap
  proof
    fix Δ Γ :: heap and e :: exp and S :: stack and  ae :: AEnv and a :: Arity and as
    assume "atom ` domA Δ ♯* Γ"
    assume "atom ` domA Δ ♯* S"
    assume "edom ae ⊆ domA Γ ∪ upds S"

    have "domA Δ ∩ edom ae = {}"
      using fresh_distinct[OF ‹atom ` domA Δ ♯* Γ›] fresh_distinct_fv[OF ‹atom ` domA Δ ♯* S›] 
            ‹edom ae ⊆ domA Γ ∪ upds S› ups_fv_subset[of S]
      by auto

    have const_on1:  "⋀ x. const_on (FBinds Δ⋅(Aheap Δ e⋅a)) (carrier ((FBinds Γ⋅ae) x)) empty"
      unfolding const_on_edom_disj using fresh_distinct_fv[OF ‹atom ` domA Δ ♯* Γ›]
      by (auto dest!: subsetD[OF carrier_FBinds] subsetD[OF Texp.edom_AnalBinds])
    have const_on2:  "const_on (FBinds Δ⋅(Aheap Δ e⋅a)) (carrier (Fstack as S)) empty"
      unfolding const_on_edom_disj using fresh_distinct_fv[OF ‹atom ` domA Δ ♯* S›]
      by (auto dest!: subsetD[OF carrier_FBinds] subsetD[OF carrier_Fstack] subsetD[OF Texp.edom_AnalBinds] subsetD[OF ap_fv_subset ])
    have  const_on3: "const_on (FBinds Γ⋅ae) (- (- domA Δ)) TTree.empty"
      and const_on4: "const_on (FBinds Δ⋅(Aheap Δ e⋅a)) (domA Γ) TTree.empty"
      unfolding const_on_edom_disj using fresh_distinct[OF ‹atom ` domA Δ ♯* Γ›]
      by (auto dest!:  subsetD[OF Texp.edom_AnalBinds])

    have disj1: "⋀ x. carrier ((FBinds Γ⋅ae) x) ∩ domA Δ = {}"
      using fresh_distinct_fv[OF ‹atom ` domA Δ ♯* Γ›]
      by (auto dest: subsetD[OF carrier_FBinds])
    hence disj1': "⋀ x. carrier ((FBinds Γ⋅ae) x) ⊆ - domA Δ" by auto
    have disj2: "⋀ x. carrier (Fstack as S) ∩ domA Δ = {}"
      using fresh_distinct_fv[OF ‹atom ` domA Δ ♯* S›] by (auto dest!: subsetD[OF carrier_Fstack])
    hence disj2': "carrier (Fstack as S) ⊆ - domA Δ" by auto
    

    {
    fix x
    have "(FBinds (Δ @ Γ)⋅(ae ⊔ Aheap Δ e⋅a)) x = (FBinds Γ⋅ae) x ⊗⊗ (FBinds Δ⋅(Aheap Δ e⋅a)) x"
    proof (cases "x ∈ domA Δ")
      case True
      have "map_of Γ x = None" using True fresh_distinct[OF ‹atom ` domA Δ ♯* Γ›] by (metis disjoint_iff_not_equal domA_def map_of_eq_None_iff)
      moreover
      have "ae x = ⊥" using True ‹domA Δ ∩ edom ae = {}› by auto
      ultimately
      show ?thesis using True 
          by (auto simp add: Texp.AnalBinds_lookup empty_is_bottom[symmetric] cong: option.case_cong)
    next
      case False
      have "map_of Δ x = None" using False by (metis domA_def map_of_eq_None_iff)
      moreover
      have "(Aheap Δ e⋅a) x = ⊥" using False using edom_Aheap by (metis contra_subsetD edomIff)
      ultimately
      show ?thesis using False
         by (auto simp add: Texp.AnalBinds_lookup empty_is_bottom[symmetric] cong: option.case_cong)
    qed
    }
    note FBinds = ext[OF this]
    
    {
    have "pathsCard (paths (substitute (FBinds (Δ @ Γ)⋅(Aheap Δ e⋅a ⊔ ae)) (thunks (Δ @ Γ)) (Texp e⋅a ⊗⊗ Fstack as S)))
      = pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks (Δ @ Γ)) (substitute (FBinds Δ⋅(Aheap Δ e⋅a))  (thunks (Δ @ Γ))  (Texp e⋅a ⊗⊗ Fstack as S))))"
       by (simp add: substitute_substitute[OF const_on1] FBinds)
    also have "substitute (FBinds Γ⋅ae) (thunks (Δ @ Γ)) = substitute (FBinds Γ⋅ae) (thunks Γ)"
      apply (rule substitute_cong_T)
      using const_on3
      by (auto dest: subsetD[OF thunks_domA])
    also have "substitute (FBinds Δ⋅(Aheap Δ e⋅a)) (thunks (Δ @ Γ)) = substitute (FBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ)"
      apply (rule substitute_cong_T)
      using const_on4
      by (auto dest: subsetD[OF thunks_domA])
    also have "substitute (FBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a ⊗⊗ Fstack as S) = substitute (FBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a) ⊗⊗ Fstack as S"
      by (rule substitute_only_empty_both[OF const_on2])
    also note calculation
    }
    note eq_imp_below[OF this]
    also
    note env_restr_split[where S = "domA Δ"]
    also
    have "pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks Γ) (substitute (FBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a) ⊗⊗ Fstack as S))) f|` domA Δ 
        = pathsCard (paths (ttree_restr (domA Δ) (substitute (FBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a))))"
          by (simp add: filter_paths_conv_free_restr ttree_restr_both ttree_rest_substitute[OF disj1]  ttree_restr_is_empty[OF disj2])
    also
    have "ttree_restr (domA Δ) (substitute (FBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a)) ⊑ Theap Δ e⋅a"  by (rule Theap_substitute)
    also
    have "pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks Γ) (substitute (FBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a) ⊗⊗ Fstack as S))) f|` (- domA Δ) =
          pathsCard (paths (substitute (FBinds Γ⋅ae) (thunks Γ) (ttree_restr (- domA Δ) (substitute (FBinds Δ⋅(Aheap Δ e⋅a)) (thunks Δ) (Texp e⋅a)) ⊗⊗ Fstack as S)))"
          by (simp add: filter_paths_conv_free_restr2 ttree_rest_substitute2[OF disj1' const_on3] ttree_restr_both  ttree_restr_noop[OF disj2'])
    also have "ttree_restr (- domA Δ) (substitute (FBinds Δ⋅(Aheap Δ e⋅a))  (thunks Δ)  (Texp e⋅a)) ⊑ Texp (Terms.Let Δ e)⋅a" by (rule Texp_Let)
    finally
    show "prognosis (Aheap Δ e⋅a ⊔ ae) as a (Δ @ Γ, e, S) ⊑ cHeap Δ e⋅a ⊔ prognosis ae as a (Γ, Terms.Let Δ e, S)"
      by (simp add: cHeap_def del: fun_meet_simp) 
  qed

  sublocale CardinalityPrognosisSafe prognosis cHeap Aheap Aexp ..
end


end