plutus icon indicating copy to clipboard operation
plutus copied to clipboard
verified publisher icon IntersectMBO

Adapt Behavioural proof Red-CC to SOPs in the metatheory

Open ana-pantilie opened this issue 1 year ago • 2 comments

Adapt the following proofs:

  • [ ] Proof of lem62
  • [ ] Proof of unwindVE
  • [ ] Proof of refocus
  • [ ] Proof of lem-→s⋆
  • [ ] Proof of lemmaF'
  • [ ] Proof of thm1b
  • [ ] Proof of thm1bV

ana-pantilie avatar May 24 '24 10:05 ana-pantilie

@ramsay-t do you happen to know the status of this issue?

effectfully avatar Jun 19 '24 01:06 effectfully

@ramsay-t any updates on this one?

effectfully avatar Jun 25 '25 20:06 effectfully