From f555947184f5295f83094c569b24497f0c99c2a2 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 27 Apr 2024 14:38:07 -0700 Subject: [PATCH] Promote traces through loop Signed-off-by: Danila Fedorin --- Language/Properties.agda | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Language/Properties.agda b/Language/Properties.agda index e018874..ff7bc65 100644 --- a/Language/Properties.agda +++ b/Language/Properties.agda @@ -75,3 +75,9 @@ Trace-↦ʳ g₁ g₂ {idx₁} (Trace-edge ρ₁⇒ρ idx₁→idx tr') Trace-edge ρ₁⇒ρ (ListMemProp.∈-++⁺ʳ (Graph.edges g₁ ↑ˡᵉ Graph.size g₂) (ListMemProp.∈-++⁺ˡ (x∈xs⇒fx∈fxs (Graph.size g₁ ↑ʳ_) idx₁→idx))) (Trace-↦ʳ g₁ g₂ tr') + +Trace-loop : ∀ (g₁ : Graph) {idx₁ idx₂ : Graph.Index g₁} {ρ₁ ρ₂ : Env} → + Trace {g₁} idx₁ idx₂ ρ₁ ρ₂ → Trace {loop g₁} idx₁ idx₂ ρ₁ ρ₂ +Trace-loop g₁ {idx₁} {idx₁} (Trace-single ρ₁⇒ρ₂) = Trace-single ρ₁⇒ρ₂ +Trace-loop g₁ {idx₁} (Trace-edge ρ₁⇒ρ idx₁→idx tr') = + Trace-edge ρ₁⇒ρ (ListMemProp.∈-++⁺ˡ idx₁→idx) (Trace-loop g₁ tr')