fact: Definition ndmm2_imsell_form c := match c with | STOPₙ p => (⌊p⌋ ⊸ ⌊p⌋) ⊸ ⌊p⌋ | INCₙ x p q => (bool2form x ⊸ ⌊q⌋) ⊸ ⌊p⌋ | DECₙ x p q => bool2form x ⊸ ⌊q⌋ ⊸ ⌊p⌋ | ZEROₙ x p q => (![bool2bang_op x]⌊q⌋) ⊸ ⌊p⌋ end.
imports: List Permutation Arith Lia Undecidability.MinskyMachines(ndMM2) Undecidability.ILL(IMSELL imsell) Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.Synthetic(Definitions ReducibilityFacts)