proposition: Theorem mm_remove_self_loops : { Q | mm_no_self_loops (1,Q) /\ (forall i x j, (i,DEC x j::nil) <sc (1,Q) -> j < 1+length Q) /\ forall v, (1,P) // (1,v) ↓ <-> (1,Q) // (1,0##v) ↓ }.
proof: Proof. destruct (eq_nat_dec lP 0) as [ HlP | HlP ]. + exists nil. split; [ | split ]. - intros i rho ([ | ] & ? & ? & ?); discriminate. - intros i x j ([ | ] & ? & ? & ?); discriminate. - destruct P; try discriminate. split. * exists (1,0##v); split; simpl; try lia; mm sss stop. * exists (1,v); split; simpl; try lia; mm sss stop. + exists Q; split; auto; split; auto; intros v; split. * intros (s0 & H); revert H; apply P_imp_Q; simpl; lia. * intros (s0 & H); revert H; apply Q_imp_P; simpl; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils pos vec subcode sss) Undecidability.MinskyMachines.MM(mm_defs)