---

Step * of Lemma fan_26_6a_imp_fan_26_7a

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

1
1. fan_26_6a{i:l}()@i'
2. g :  List  @i
3. R :  List  @i'
4. gen_fin_spr(g)@i
5. a: List. (((g a) = 0)  Dec(R a))@i
6. f:  . ((x:. ((g mklist(x;f)) = 0))  (x:. (R mklist(x;f))))@i
 z:. f:  . ((x:. ((g mklist(x;f)) = 0))  (x:. ((R mklist(x;f))  (x  z))))


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


By

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



Home Index