search

VictorCMiraldo / stdiff

0 stars 1 forks source link

Reconcile Scns and Schg #2

Open arianvp opened 6 years ago

arianvp commented 6 years ago

One is a proper subset of the other. For every Scns we can find an Schg that tells exactly the same.

arianvp commented 6 years ago

Proof that this hypothesis is true:

  All-to-Al : (At : Atom → Set) (π : Prod) → All At π → Al At π π
  All-to-Al At .[] [] = A0
  All-to-Al At .(_ ∷ _) (px ∷ x) = AX px (All-to-Al At _ x)

Also, functions like 

  disj-At-Al : ∀{l₁ l₂} → All (At PatchRec) l₁ → Al (At PatchRec) l₁ l₂ → Set

Will become trivial in the case of l1 == l2