---

Step * of Lemma rel-comp-exp

∀[T:Type]. ∀[R,S:T ⟶ T ⟶ ℙ].  ∀n:ℕ. (R o S)^n ⇐⇒ if (n =z 0) then λx,y. (x = y ∈ T) else (R o ((S o R)^n - 1 o S)) fi\000C 
BY
{ (InductionOnNat THEN RW (AddrC [2] RecUnfoldTopAbC) 0 THEN Reduce 0) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. [S] : T ⟶ T ⟶ ℙ
⊢ λx,y. (x = y ∈ T) ⇐⇒ λx,y. (x = y ∈ T)

2
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. [S] : T ⟶ T ⟶ ℙ
4. n : ℤ
5. [%1] : 0 < n
6. (R o S)^n - 1 ⇐⇒ if (n - 1 =z 0) then λx,y. (x = y ∈ T) else (R o ((S o R)^n - 1 - 1 o S)) fi 
⊢ if (n =z 0) then λx,y. (x = y ∈ T) else λx,y. ∃z:T. ((x (R o S) z) ∧ (z (R o S)^n - 1 y)) fi  ⇐⇒ if (n =z 0)
then λx,y. (x = y ∈ T)
else (R o ((S o R)^n - 1 o S))
fi 

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R,S:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}n:\mBbbN{}.  (R  o  S)\^{}n  \mLeftarrow{}{}\mRightarrow{}  if  (n  =\msubz{}  0)  then  \mlambda{}x,y.  (x  =  y)  else  (R  o  (rel\_exp(T;  (S  o  R);  n  -  1)  o  S))  fi 


By

---

Latex:
(InductionOnNat  THEN  RW  (AddrC  [2]  RecUnfoldTopAbC)  0  THEN  Reduce  0)

---

Home Index