Nuprl Definition : bar_bwd_fim
bar_bwd_fim(R;A) ==  (a: List. ((R a)  (A a)))  (a: List. ((s:. (A (a @ [s])))  (A a)))  (A [])
Definitions occuring in Statement : 
append: as @ bs, 
nat: , 
all: x:A. B[x], 
implies: P  Q, 
apply: f a
FDL editor aliases : 
bar_bwd_fim
bar\_bwd\_fim(R;A)  ==
    (\mforall{}a:\mBbbN{}  List.  ((R  a)  {}\mRightarrow{}  (A  a)))  {}\mRightarrow{}  (\mforall{}a:\mBbbN{}  List.  ((\mforall{}s:\mBbbN{}.  (A  (a  @  [s])))  {}\mRightarrow{}  (A  a)))  {}\mRightarrow{}  (A  [])
Date html generated:
2013_03_20-AM-10_31_29
Last ObjectModification:
2013_02_23-PM-04_26_26
Home
Index