proposition: Lemma orRelPR : forall (n : nat) (R R' : naryRel n), isPRrel n R -> isPRrel n R' -> isPRrel n (orRel n R R').
proof: Proof. intros n R R' [x p] [x0 p0]; assert (H: isPR 2 (fun a b : nat => notZero (a + b))). { apply compose2_1IsPR. - apply plusIsPR. - apply notZeroIsPR. } destruct H as (x1, p1); exists (PRcomp x1 [x; x0])%pr; cbn in |- *. apply extEqualTrans with (evalComposeFunc n 2 (Vector.cons (naryFunc n) (charFunction n R) 1 (Vector.cons (naryFunc n) (charFunction n R') 0 (Vector.nil (naryFunc n)))) (fun a b : nat => notZero (a + b))). - apply replaceCompose2; auto. - clear x p x0 p0 x1 p1; induction n as [| n Hrecn]. + simpl in |- *; destruct R. * reflexivity. * destruct R'; reflexivity. + cbn in |- *; fold (naryFunc n) in |- *. intro c; apply (Hrecn (R c) (R' c)). Qed.
imports: Coq(Arith Peano_dec Compare_dec List Eqdep_dec Utf8) hydras(extEqualNat misc Compat815) Coq(Lia)