---

Step * of Lemma bar26_4a_imp_fan26_6a

bar_26_4a{i:l}()  fan_26_6a{i:l}()
BY
{ (Unfold `fan_26_6a` 0 THEN Auto) }

1
1. bar_26_4a{i:l}()@i'
2. B :  List  @i
3. R :  List  @i'
4. a: List. Dec(R a)@i
5. f:fin_spr(B). x:. (R mklist(x;f))@i
 z:. f:fin_spr(B). x:. ((x  z)  (R mklist(x;f)))


bar\_26\_4a\{i:l\}()  {}\mRightarrow{}  fan\_26\_6a\{i:l\}()


By

(Unfold  `fan\_26\_6a`  0  THEN  Auto)



Home Index