proposition: Lemma notRelPR (n : nat) (R : naryRel n): isPRrel n R -> isPRrel n (notRel n R).
proof: Proof. intros [x p]; assert (H: isPR 1 (fun x : nat => 1 - x)). { apply compose1_2IsPR with (f := fun x : nat => 1) (f' := fun x : nat => x). - apply const1_NIsPR. - apply idIsPR. - apply minusIsPR. } destruct H as [x0 p0]; exists (PRcomp x0 [x])%pr; cbn in |- *; apply extEqualTrans with (evalComposeFunc n 1 (Vector.cons _ (charFunction n R) _ (Vector.nil _)) (fun x : nat => 1 - x)). - apply extEqualCompose. + unfold extEqualVector; simpl; auto. + auto. - clear p0 x0 p x; induction n as [| n Hrecn]. + simpl in |- *; induction R; reflexivity. + simpl; intros c; fold (naryFunc n) in |- *; apply Hrecn. Qed.
imports: Coq(Arith Peano_dec Compare_dec List Eqdep_dec Utf8) hydras(extEqualNat misc Compat815) Coq(Lia)