Matching Logic: Foundation of the K Framework