fact: Definition encodes_config (x: mm2_state) (y: CM1.Config) : Prop := let: (i, (a, b)) := x in CM1.state y = fs i /\ exists c, CM1.value y = κ a b c.
imports: ZArith List PeanoNat Lia Relations.Relation_Operators Relations.Operators_Properties Undecidability.MinskyMachines.MM2 Undecidability.CounterMachines.Util.CM1_facts Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun