- λA,R,S,a1. ∀a2. R a1 a2 → S a2 a1.
+ λA,R,S,a1. ∀a2. R a1 a2 → S a1 a2.
definition NF_dec: ∀A. relation A → relation A → Prop ≝
λA,R,S. ∀a1. NF A R S a1 ∨
definition NF_dec: ∀A. relation A → relation A → Prop ≝
λA,R,S. ∀a1. NF A R S a1 ∨
.
lemma NF_to_SN: ∀A,R,S,a. NF A R S a → SN A R S a.
.
lemma NF_to_SN: ∀A,R,S,a. NF A R S a → SN A R S a.
- λA,R,S,a2. ∀a1. R a1 a2 → S a2 a1.
+ λA,R,S,a2. ∀a1. R a1 a2 → S a1 a2.
.
lemma NF_to_SN_sn: ∀A,R,S,a. NF_sn A R S a → SN_sn A R S a.
.
lemma NF_to_SN_sn: ∀A,R,S,a. NF_sn A R S a → SN_sn A R S a.