Quelle  Lasso.thy

section ‹Lassos›
(* Author: Peter Lammich *)
theory Lasso
imports Automata
begin

  record 'v lasso = 
    lasso_reach :: "'v list"
    lasso_va :: "'v"
    lasso_cysfx :: "'v list"
  
  definition "lasso_v0 L ≡ case lasso_reach L of [] ==> lasso_va L | (v0#_) ==> v0"
  definition lasso_cycle where "lasso_cycle L = lasso_va L # lasso_cysfx L"


  definition "lasso_of_prpl prpl ≡ case prpl of (pr,pl) ==> (
    lasso_reach = pr,
    lasso_va = hd pl,
    lasso_cysfx = tl pl )"

  definition "prpl_of_lasso L ≡ (lasso_reach L, lasso_va L # lasso_cysfx L)"

  lemma prpl_of_lasso_simps[simp]: 
    "fst (prpl_of_lasso L) = lasso_reach L"
    "snd (prpl_of_lasso L) = lasso_va L # lasso_cysfx L"
    unfolding prpl_of_lasso_def by auto

  lemma lasso_of_prpl_simps[simp]:
    "lasso_reach (lasso_of_prpl prpl) = fst prpl"
    "snd prpl ≠ [] ==> lasso_cycle (lasso_of_prpl prpl) = snd prpl"
    unfolding lasso_of_prpl_def lasso_cycle_def by (auto split: prod.split)


  definition run_of_lasso :: "'q lasso ==> 'q word"
    ― ‹Run described by a lasso›
    where "run_of_lasso L ≡ lasso_reach L ⌢ (lasso_cycle L)^\<omega>"

  lemma run_of_lasso_of_prpl: 
    "pl ≠ [] ==> run_of_lasso (lasso_of_prpl (pr, pl)) = pr ⌢ pl^\<omega>"
    unfolding run_of_lasso_def lasso_of_prpl_def lasso_cycle_def
    by auto


  definition "map_lasso f L ≡ (
    lasso_reach = map f (lasso_reach L),
    lasso_va = f (lasso_va L),
    lasso_cysfx = map f (lasso_cysfx L)
  )"

  lemma map_lasso_simps[simp]:
    "lasso_reach (map_lasso f L) = map f (lasso_reach L)"
    "lasso_va (map_lasso f L) = f (lasso_va L)"
    "lasso_cysfx (map_lasso f L) = map f (lasso_cysfx L)"
    "lasso_v0 (map_lasso f L) = f (lasso_v0 L)"
    "lasso_cycle (map_lasso f L) = map f (lasso_cycle L)"
    unfolding map_lasso_def lasso_v0_def lasso_cycle_def
    by (auto split: list.split)
  
  lemma map_lasso_run[simp]:
    shows "run_of_lasso (map_lasso f L) = f o (run_of_lasso L)"
    by (auto simp add: map_lasso_def run_of_lasso_def conc_def iter_def
      lasso_cycle_def lasso_v0_def fun_eq_iff not_less nth_Cons'
      nz_le_conv_less)


  context graph begin
    definition is_lasso_pre :: "'v lasso ==> bool" 
      where "is_lasso_pre L ≡
        lasso_v0 L ∈ V0
      ∧ path E (lasso_v0 L) (lasso_reach L) (lasso_va L)
      ∧ path E (lasso_va L) (lasso_cycle L) (lasso_va L)"
    
    definition "is_lasso_prpl_pre prpl ≡ case prpl of (pr, pl) ==> ∃v0 va.
      v0∈V0
      ∧ pl ≠ []
      ∧ path E v0 pr va
      ∧ path E va pl va"

    lemma is_lasso_pre_prpl_of_lasso[simp]: 
      "is_lasso_prpl_pre (prpl_of_lasso L) ⟷ is_lasso_pre L"
      unfolding is_lasso_pre_def prpl_of_lasso_def is_lasso_prpl_pre_def
      unfolding lasso_v0_def lasso_cycle_def
      by (auto simp: path_simps split: list.split)
  
    lemma is_lasso_prpl_pre_conv: 
      "is_lasso_prpl_pre prpl
      ⟷ (snd prpl≠[] ∧ is_lasso_pre (lasso_of_prpl prpl))"
      unfolding is_lasso_pre_def lasso_of_prpl_def is_lasso_prpl_pre_def
      unfolding lasso_v0_def lasso_cycle_def
      apply (cases prpl)
      apply (rename_tac a b)
      apply (case_tac b)
      apply (auto simp: path_simps split: list.splits)
      done

    lemma is_lasso_pre_empty[simp]: "V0 = {} ==> ¬is_lasso_pre L"
      unfolding is_lasso_pre_def by auto


    lemma run_of_lasso_pre: 
      assumes "is_lasso_pre L"  
      shows "is_run (run_of_lasso L)"
      and "run_of_lasso L 0 ∈ V0"
      using assms
      unfolding is_lasso_pre_def is_run_def run_of_lasso_def 
        lasso_cycle_def lasso_v0_def
      by (auto simp: ipath_conc_conv ipath_iter_conv path_cons_conv conc_fst 
        split: list.splits)

  end

  context gb_graph begin
    definition is_lasso
      :: "'Q lasso ==> bool" 
      ― ‹Predicate that defines a lasso›
      where "is_lasso L ≡
        is_lasso_pre L
      ∧ (∀A∈F. (set (lasso_cycle L)) ∩ A ≠ {})"

    definition "is_lasso_prpl prpl ≡
      is_lasso_prpl_pre prpl
      ∧ (∀A∈F. set (snd prpl) ∩ A ≠ {})"
  

    lemma is_lasso_prpl_of_lasso[simp]: 
      "is_lasso_prpl (prpl_of_lasso L) ⟷ is_lasso L"
      unfolding is_lasso_def is_lasso_prpl_def
      unfolding lasso_v0_def lasso_cycle_def
      by auto
  
    lemma is_lasso_prpl_conv: 
      "is_lasso_prpl prpl ⟷ (snd prpl≠[] ∧ is_lasso (lasso_of_prpl prpl))"
      unfolding is_lasso_def is_lasso_prpl_def is_lasso_prpl_pre_conv
      apply safe
      apply simp_all
      done
    
    lemma is_lasso_empty[simp]: "V0 = {} ==> ¬is_lasso L"
      unfolding is_lasso_def by auto

    lemma lasso_accepted:
      assumes L: "is_lasso L"
      shows "is_acc_run (run_of_lasso L)"
    proof -
      obtain "pr" va pls where 
        [simp]: "L = (lasso_reach = pr,lasso_va = va,lasso_cysfx = pls)" 
        by (cases L)

      from L have "is_run (run_of_lasso L)" 
        unfolding is_lasso_def by (auto simp: run_of_lasso_pre)
      moreover from L have "(∀A∈F. set (va#pls) ∩ A ≠ {})"
        by (auto simp: is_lasso_def lasso_cycle_def)
      moreover from L have "(run_of_lasso L) 0 ∈ V0" 
        unfolding is_lasso_def by (auto simp: run_of_lasso_pre)
      ultimately show "is_acc_run (run_of_lasso L)"
        unfolding is_acc_run_def is_acc_def run_of_lasso_def 
          lasso_cycle_def lasso_v0_def
        by (fastforce intro: limit_inter_INF)
    qed

    lemma lasso_prpl_acc_run:
      "is_lasso_prpl (pr, pl) ==> is_acc_run (pr ⌢ iter pl)"
      apply (clarsimp simp: is_lasso_prpl_conv)
      apply (drule lasso_accepted)
      apply (simp add: run_of_lasso_of_prpl)
      done

  end
  
  context gb_graph
  begin
    lemma accepted_lasso:
      assumes [simp, intro]: "finite (E^* `` V0)"
      assumes A: "is_acc_run r"
      shows "∃L. is_lasso L"
    proof -
      from A have 
        RUN: "is_run r" 
        and ACC: "∀A∈F. limit r ∩ A ≠ {}" 
        by (auto simp: is_acc_run_limit_alt)
      from RUN have [simp]: "r 0 ∈ V0" and RUN': "ipath E r" 
        by (simp_all add: is_run_def)

      txt ‹Choose a node that is visited infinitely often›
      from RUN have RAN_REACH: "range r ⊆ E^*``V0"
        by (auto simp: is_run_def dest: ipath_to_rtrancl)
      hence "finite (range r)" by (auto intro: finite_subset)
      then obtain u where "u∈limit r" using limit_nonempty by blast
      hence U_REACH: "u∈E<sup>*</sup>``V0" using RAN_REACH limit_in_range by force
      then obtain v0 "pr" where PR: "v0∈V0" "path E v0 pr u" 
        by (auto intro: rtrancl_is_path)
      moreover
      txt ‹Build a path from ‹u› to ‹u›, that contains nodes from
 each acceptance set›
      have "∃pl. pl≠[] ∧ path E u pl u ∧ (∀A∈F. set pl ∩ A ≠ {})"
        using finite_F ACC
      proof (induction rule: finite_induct)
        case empty
        from run_limit_two_connectedI[OF RUN' ‹u∈limit r› ‹u∈limit r›] 
        obtain p where [simp]: "p≠[]" and P: "path E u p u" 
          by (rule trancl_is_path) 
        thus ?case by blast
      next
        case (insert A F)
        from insert.IH insert.prems obtain pl where 
          [simp]: "pl≠[]" 
            and P: "path E u pl u" 
            and ACC: "(∀A'∈F. set pl ∩ A' ≠ {})"
          by auto
        from insert.prems obtain v where VACC: "v∈A" "v∈limit r" by auto
        from run_limit_two_connectedI[OF RUN' ‹u∈limit r› ‹v∈limit r›] 
        obtain p1 where [simp]: "p1≠[]" 
          and P1: "path E u p1 v" 
          by (rule trancl_is_path) 

        from run_limit_two_connectedI[OF RUN' ‹v∈limit r› ‹u∈limit r›] 
        obtain p2 where [simp]: "p2≠[]" 
          and P2: "path E v p2 u" 
          by (rule trancl_is_path) 

        note P also note P1 also (path_conc) note P2 finally (path_conc)
        have "path E u (pl@p1@p2) u" by simp
        moreover from P2 have "v∈set (p1@p2)" 
          by (cases p2) (auto simp: path_cons_conv)
        with ACC VACC have "(∀A'∈insert A F. set (pl@p1@p2) ∩ A' ≠ {})" by auto
        moreover have "pl@p1@p2 ≠ []" by auto
        ultimately show ?case by (intro exI conjI)
      qed
      then obtain pl where "pl ≠ []" "path E u pl u" "(∀A∈F. set pl ∩ A ≠ {})" 
        by blast
      then obtain pls where "path E u (u#pls) u" "∀A∈F. set (u#pls) ∩ A ≠ {}"
        by (cases pl) (auto simp add: path_simps)
      ultimately show ?thesis
        apply -
        apply (rule 
          exI[where x="(lasso_reach = pr,lasso_va = u,lasso_cysfx = pls)"])
        unfolding is_lasso_def lasso_v0_def lasso_cycle_def is_lasso_pre_def
        apply (cases "pr")
        apply (simp_all add: path_simps)
        done
    qed
  end
  

  context b_graph
  begin
    definition is_lasso where "is_lasso L ≡
      is_lasso_pre L
      ∧ (set (lasso_cycle L)) ∩ F ≠ {}"

    definition is_lasso_prpl where "is_lasso_prpl L ≡
      is_lasso_prpl_pre L
      ∧ (set (snd L)) ∩ F ≠ {}"
    
    lemma is_lasso_pre_ext[simp]: 
      "gbg.is_lasso_pre T m = is_lasso_pre"
      unfolding gbg.is_lasso_pre_def[abs_def] is_lasso_pre_def[abs_def]
      unfolding to_gbg_ext_def
      by auto

    lemma is_lasso_gbg: 
      "gbg.is_lasso T m = is_lasso"
      unfolding is_lasso_def[abs_def] gbg.is_lasso_def[abs_def]
      apply simp
      apply (auto simp: to_gbg_ext_def lasso_cycle_def)
      done

    lemmas lasso_accepted = gbg.lasso_accepted[unfolded to_gbg_alt is_lasso_gbg]
    lemmas accepted_lasso = gbg.accepted_lasso[unfolded to_gbg_alt is_lasso_gbg]

    lemma is_lasso_prpl_of_lasso[simp]: 
      "is_lasso_prpl (prpl_of_lasso L) ⟷ is_lasso L"
      unfolding is_lasso_def is_lasso_prpl_def
      unfolding lasso_v0_def lasso_cycle_def
      by auto
  
    lemma is_lasso_prpl_conv: 
      "is_lasso_prpl prpl ⟷ (snd prpl≠[] ∧ is_lasso (lasso_of_prpl prpl))"
      unfolding is_lasso_def is_lasso_prpl_def is_lasso_prpl_pre_conv
      apply safe
      apply auto
      done

    lemma lasso_prpl_acc_run:
      "is_lasso_prpl (pr, pl) ==> is_acc_run (pr ⌢ iter pl)"
      apply (clarsimp simp: is_lasso_prpl_conv)
      apply (drule lasso_accepted)
      apply (simp add: run_of_lasso_of_prpl)
      done

  end

  context igb_graph begin
    definition "is_lasso L ≡
      is_lasso_pre L
      ∧ (∀i<num_acc. ∃q∈set (lasso_cycle L). i∈acc q)"

    definition "is_lasso_prpl L ≡
      is_lasso_prpl_pre L
      ∧ (∀i<num_acc. ∃q∈set (snd L). i∈acc q)"

    lemma is_lasso_prpl_of_lasso[simp]: 
      "is_lasso_prpl (prpl_of_lasso L) ⟷ is_lasso L"
      unfolding is_lasso_def is_lasso_prpl_def
      unfolding lasso_v0_def lasso_cycle_def
      by auto
  
    lemma is_lasso_prpl_conv: 
      "is_lasso_prpl prpl ⟷ (snd prpl≠[] ∧ is_lasso (lasso_of_prpl prpl))"
      unfolding is_lasso_def is_lasso_prpl_def is_lasso_prpl_pre_conv
      apply safe
      apply auto
      done

    lemma is_lasso_pre_ext[simp]: 
      "gbg.is_lasso_pre T m = is_lasso_pre"
      unfolding gbg.is_lasso_pre_def[abs_def] is_lasso_pre_def[abs_def]
      unfolding to_gbg_ext_def
      by auto

    lemma is_lasso_gbg: "gbg.is_lasso T m = is_lasso"
      unfolding is_lasso_def[abs_def] gbg.is_lasso_def[abs_def]
      apply simp
      apply (simp_all add: to_gbg_ext_def)
      apply (intro ext)
      apply (fo_rule arg_cong | intro ext)+
      apply (auto simp: F_def accn_def intro!: ext)
      done

    lemmas lasso_accepted = gbg.lasso_accepted[unfolded to_gbg_alt is_lasso_gbg]
    lemmas accepted_lasso = gbg.accepted_lasso[unfolded to_gbg_alt is_lasso_gbg]

    lemma lasso_prpl_acc_run:
      "is_lasso_prpl (pr, pl) ==> is_acc_run (pr ⌢ iter pl)"
      apply (clarsimp simp: is_lasso_prpl_conv)
      apply (drule lasso_accepted)
      apply (simp add: run_of_lasso_of_prpl)
      done

    lemma degen_lasso_sound:
      assumes A: "degen.is_lasso T m L"
      shows "is_lasso (map_lasso fst L)"
    proof -
        
      from A have 
        V0: "lasso_v0 L ∈ degen.V0 T m" and
        REACH: "path (degen.E T m)
                 (lasso_v0 L) (lasso_reach L) (lasso_va L)" and
        LOOP: "path (degen.E T m)
                  (lasso_va L) (lasso_cycle L) (lasso_va L)" and
        ACC: "(set (lasso_cycle L)) ∩ degen.F T m ≠ {}"
        unfolding degen.is_lasso_def degen.is_lasso_pre_def by auto

      {
        fix i
        assume "i<num_acc"
        hence "∃q∈set (lasso_cycle L). i ∈ local.acc (fst q) ∧ snd q = i"
        proof (induction i)
          case 0
          thus ?case using ACC unfolding degeneralize_ext_def by fastforce
        next
          case (Suc i)
          then obtain q where "(q,i)∈set (lasso_cycle L)" and "i∈acc q" by auto
          with LOOP obtain pl' where SPL: "set (lasso_cycle L) = set pl'" 
            and PS: "path (degen.E T m) (q,i) pl' (q,i)"
            by (blast elim: path_loop_shift)
          from SPL have "pl'≠[]" by (auto simp: lasso_cycle_def)
          then obtain pl'' where [simp]: "pl'=(q,i)#pl''" 
            using PS by (cases pl') (auto simp: path_simps)
          then obtain q2 pl''' where 
            [simp]: "pl'' = (q2,(i + 1) mod num_acc)#pl'''"
            using PS ‹i∈acc q› ‹Suc i < num_acc›
            apply (cases pl'') 
            apply (auto 
              simp: path_simps degeneralize_ext_def 
              split: if_split_asm)
            done
          from PS have 
            "path (degen.E T m) (q2,Suc i) pl'' (q,i)"
            using ‹Suc i < num_acc›
            by (auto simp: path_simps)
          from degen_visit_acc[OF this] obtain qa 
            where "(qa,Suc i)∈set pl''" "Suc i ∈ acc qa" 
            by auto
          thus ?case
            by (rule_tac bexI[where x="(qa,Suc i)"]) (auto simp: SPL)
        qed
      } note aux=this

      from degen_V0_sound[OF V0] 
        degen_path_sound[OF REACH] 
        degen_path_sound[OF LOOP] aux
      show ?thesis
        unfolding is_lasso_def is_lasso_pre_def
        by auto
    qed

  end


  definition lasso_rel_ext_internal_def: "∧Re R. lasso_rel_ext Re R ≡ {
    (( lasso_reach = r', lasso_va = va', lasso_cysfx = cysfx', …=m' ),
     ( lasso_reach = r, lasso_va = va, lasso_cysfx = cysfx, …=m )) |
      r' r va' va cysfx' cysfx m' m.
      (r',r) ∈ ⟨R⟩list_rel
    ∧ (va',va)∈R
    ∧ (cysfx', cysfx) ∈ ⟨R⟩list_rel
    ∧ (m',m) ∈ Re
    }"


  lemma lasso_rel_ext_def: "∧ Re R. ⟨Re,R⟩lasso_rel_ext = {
    (( lasso_reach = r', lasso_va = va', lasso_cysfx = cysfx', …=m' ),
     ( lasso_reach = r, lasso_va = va, lasso_cysfx = cysfx, …=m )) |
      r' r va' va cysfx' cysfx m' m.
      (r',r) ∈ ⟨R⟩list_rel
    ∧ (va',va)∈R
    ∧ (cysfx', cysfx) ∈ ⟨R⟩list_rel
    ∧ (m',m) ∈ Re
    }"
    unfolding lasso_rel_ext_internal_def relAPP_def by auto

  lemma lasso_rel_ext_sv[relator_props]: 
    "∧ Re R. [ single_valued Re; single_valued R ] ==> single_valued (⟨Re,R⟩lasso_rel_ext)"
    unfolding lasso_rel_ext_def
    apply (rule single_valuedI)
    apply safe
    apply (blast dest: single_valuedD list_rel_sv[THEN single_valuedD])+
    done

  lemma lasso_rel_ext_id[relator_props]: 
    "∧Re R. [ Re=Id; R=Id ] ==> ⟨Re,R⟩lasso_rel_ext = Id"
    unfolding lasso_rel_ext_def
    apply simp
    apply safe
    by (metis lasso.surjective)

  consts i_lasso_ext :: "interface ==> interface ==> interface"

  lemmas [autoref_rel_intf] = REL_INTFI[of lasso_rel_ext i_lasso_ext]

  find_consts "(_,_) lasso_scheme"
  term lasso_reach_update

  lemma lasso_param[param, autoref_rules]:
    "∧Re R. (lasso_reach, lasso_reach) ∈ ⟨Re,R⟩lasso_rel_ext → ⟨R⟩list_rel"
    "∧Re R. (lasso_va, lasso_va) ∈ ⟨Re,R⟩lasso_rel_ext → R"
    "∧Re R. (lasso_cysfx, lasso_cysfx) ∈ ⟨Re,R⟩lasso_rel_ext → ⟨R⟩list_rel"
    "∧Re R. (lasso_ext, lasso_ext)
      ∈ ⟨R⟩list_rel → R → ⟨R⟩list_rel → Re → ⟨Re,R⟩lasso_rel_ext"
    "∧Re R. (lasso_reach_update, lasso_reach_update)
      ∈ (⟨R⟩list_rel → ⟨R⟩list_rel) → ⟨Re,R⟩lasso_rel_ext → ⟨Re,R⟩lasso_rel_ext"
    "∧Re R. (lasso_va_update, lasso_va_update)
      ∈ (R→R) → ⟨Re,R⟩lasso_rel_ext → ⟨Re,R⟩lasso_rel_ext"
    "∧Re R. (lasso_cysfx_update, lasso_cysfx_update)
      ∈ (⟨R⟩list_rel → ⟨R⟩list_rel) → ⟨Re,R⟩lasso_rel_ext → ⟨Re,R⟩lasso_rel_ext"
    "∧Re R. (lasso.more_update, lasso.more_update)
      ∈ (Re→Re) → ⟨Re,R⟩lasso_rel_ext → ⟨Re,R⟩lasso_rel_ext"
    unfolding lasso_rel_ext_def
    by (auto dest: fun_relD)


  lemma lasso_param2[param, autoref_rules]:
    "∧Re R. (lasso_v0, lasso_v0) ∈ ⟨Re,R⟩lasso_rel_ext → R"
    "∧Re R. (lasso_cycle, lasso_cycle) ∈ ⟨Re,R⟩lasso_rel_ext → ⟨R⟩list_rel"
    "∧Re R. (map_lasso, map_lasso)
      ∈ (R→R') → ⟨Re,R⟩lasso_rel_ext → ⟨unit_rel,R'⟩lasso_rel_ext"
    unfolding lasso_v0_def[abs_def] lasso_cycle_def[abs_def] map_lasso_def[abs_def]
    by parametricity+


  lemma lasso_of_prpl_param: "[(l',l)∈⟨R⟩list_rel ×_r ⟨R⟩list_rel; snd l ≠ []]
    ==> (lasso_of_prpl l', lasso_of_prpl l) ∈ ⟨unit_rel,R⟩lasso_rel_ext"
    unfolding lasso_of_prpl_def
    apply (cases l, cases l', clarsimp)
    apply (case_tac b, simp, case_tac ba, clarsimp_all)
    apply parametricity
    done

  context begin interpretation autoref_syn .

  lemma lasso_of_prpl_autoref[autoref_rules]:
    assumes "SIDE_PRECOND (snd l ≠ [])"
    assumes "(l',l)∈⟨R⟩list_rel ×_r ⟨R⟩list_rel"
    shows "(lasso_of_prpl l',
      (OP lasso_of_prpl
        ::: ⟨R⟩list_rel ×_r ⟨R⟩list_rel → ⟨unit_rel,R⟩lasso_rel_ext)$l)
      ∈ ⟨unit_rel,R⟩lasso_rel_ext"
    using assms
    apply (simp add: lasso_of_prpl_param)
    done

  end




  subsection ‹Implementing runs by lassos›
  
  definition lasso_run_rel_def_internal: 
    "lasso_run_rel R ≡ br run_of_lasso (λ_. True) O (nat_rel → R)"
  lemma lasso_run_rel_def: 
    "⟨R⟩lasso_run_rel = br run_of_lasso (λ_. True) O (nat_rel → R)"
    unfolding lasso_run_rel_def_internal relAPP_def by simp

  lemma lasso_run_rel_sv[relator_props]: 
    "single_valued R ==> single_valued (⟨R⟩lasso_run_rel)"
    unfolding lasso_run_rel_def
    by tagged_solver

  consts i_run :: "interface ==> interface"

  lemmas [autoref_rel_intf] = REL_INTFI[of lasso_run_rel i_run]

  definition [simp]: "op_map_run ≡ (o)"

  lemma [autoref_op_pat]: "(o) ≡ op_map_run" by simp

  lemma map_lasso_run_refine[autoref_rules]:
    shows "(map_lasso,op_map_run) ∈ (R→R') → ⟨R⟩lasso_run_rel → ⟨R'⟩lasso_run_rel"
    unfolding lasso_run_rel_def op_map_run_def
  proof (intro fun_relI)
    fix f f' l r
    assume [param]: "(f,f')∈R→R'" and 
      "(l, r) ∈ br run_of_lasso (λ_. True) O (nat_rel → R)"
    then obtain r' where [param]: "(r',r)∈nat_rel → R" 
      and [simp]: "r' = run_of_lasso l" 
      by (auto simp: br_def)
    
    have "(map_lasso f l, f o r') ∈ br run_of_lasso (λ_. True)" 
      by (simp add: br_def)
    also have "(f o r', f' o r) ∈ nat_rel → R'" by parametricity
    finally (relcompI) show 
      "(map_lasso f l, f' o r) ∈ br run_of_lasso (λ_. True) O (nat_rel → R')" 
      .
  qed

end