Nuprl - graph_1_1 Citations of bool

Def

== Unit+Unit

is mentioned by

Thm* k:, f,g:(k), p:(k). sum(if p(i) f(i)+g(i) else f(i) fi | i < k) = sum(f(i) | i < k)+sum(if p(i) g(i) else 0 fi | i < k) [sum-ite]

Thm* f:(TAT), P:(A), L:A List, s:T. list_accum(s',x'.f(s',x');s;filter(P;L)) ~ list_accum(i,y.if P(y) f(i,y) else i fi;s;L) [list_accum_filter]

Thm* P:(T), T':Type, f:({x:T| P(x) }T'), L:T List, x,y:{x:T| P(x) }. x before y L f(x) before f(y) mapfilter(f;P;L) [mapfilter_before]

Thm* P:(T), L2,L1:T List. list_accum(l,x.if P(x) [x / l] else l fi;L1;L2) ~ (rev(filter(P;L2)) @ L1) [filter_list_accum]

Thm* R:(AA'Prop), P:(BA), P':(BA'), F,G,H:(BAA), F',G',H':(BA'A'), N:(BA(B List)), N':(BA'(B List)), M:(A), M':(A'). (i:B, s:A. P(i,s) M(F(i,s))M(s)) (i:B, s:A. M(G(i,s))M(s)) (i:B, s:A. P(i,s) M(H(i,s)) < M(s)) (i:B, s:A'. P'(i,s) M'(F'(i,s))M'(s)) (i:B, s:A'. M'(G'(i,s))M'(s)) (i:B, s:A'. P'(i,s) M'(H'(i,s)) < M'(s)) (j:B, u:A, v:A'. R(u,v) (P(j,u) P'(j,v))) (j:B, u:A, v:A'. R(u,v) P(j,u) P'(j,v) R(F(j,u),F'(j,v))) (j:B, u:A, v:A'. R(u,v) P(j,u) P'(j,v) R(H(j,u),H'(j,v))) (j:B, u:A, v:A'. R(u,v) R(G(j,u),G'(j,v))) (j:B, u:A, v:A'. R(u,v) N(j,u) = N'(j,v)) (j:B, u:A, v:A'. R(u,v) R(process u j where process s i == if P(i,s) then F(i,s) else G(i,s) where xs := N(i,s); s:= H(i,s); while not null xs { s := process s (hd xs); xs := tl xs; } ,process v j where process s i == if P'(i,s) then F'(i,s) else G'(i,s) where xs := N'(i,s); s:= H'(i,s); while not null xs { s := process s (hd xs); xs := tl xs; } )) [accumulate-rel]

Thm* M:(A), Q:(BAAProp), P:(BA), F,G,H:(BAA), N:(BA(B List)). (i:B, s:A. P(i,s) M(F(i,s))M(s)) (i:B, s:A. M(G(i,s))M(s)) (i:B, s:A. P(i,s) M(H(i,s)) < M(s)) (j:B, u:A. P(j,u) Q(j,u,F(j,u))) (j:B, u,z:A. P(j,u) Q(j,H(j,u),z) Q(j,u,G(j,z))) (j:B, u:A. Q(j,u,u)) (i,j:B, u,v,z:A. Q(i,u,v) Q(j,v,z) Q(j,u,z)) (j:B, u:A. Q(j,u,process u j where process s i == if P(i,s) then F(i,s) else G(i,s) where xs := N(i,s); s:= H(i,s); while not null xs { s := process s (hd xs); xs := tl xs; } )) [accumulate-induction1]

Thm* A,B:Type, P:(BA), F,G,H:(BAA), N:(BA(B List)), M:(A). (i:B, s:A. P(i,s) M(F(i,s))M(s)) (i:B, s:A. M(G(i,s))M(s)) (i:B, s:A. P(i,s) M(H(i,s)) < M(s)) (j:B, u:A. process u j where process s i == if P(i,s) then F(i,s) else G(i,s) where xs := N(i,s); s:= H(i,s); while not null xs { s := process s (hd xs); xs := tl xs; } {s:A| M(s)M(u) }) [accumulate_wf]

Thm* P:(T), T':Type, f:({x:T| P(x) }T'), L1,L2:T List. mapfilter(f;P;L1 @ L2) = (mapfilter(f;P;L1) @ mapfilter(f;P;L2)) [mapfilter_append]

Thm* L:T List, P:(T). (xL.P(x)) (i:||L||. P(L[i])) [assert_l_bexists]

Thm* L:T List, P:(T). (xL.P(x)) (i:||L||. P(L[i])) [assert_l_ball]

In prior sections: bool 1 list 1 sqequal 1 rel 1 mb basic mb nat mb list 1 mb list 2 prog 1

Try larger context: Graphs

graph 1 1 Sections Graphs Doc

`Thm* k:, f,g:(k), p:(k). sum(if p(i) f(i)+g(i) else f(i) fi \| i < k) = sum(f(i) \| i < k)+sum(if p(i) g(i) else 0 fi \| i < k)`	[sum-ite]
`Thm* f:(TAT), P:(A), L:A List, s:T. list_accum(s',x'.f(s',x');s;filter(P;L)) ~ list_accum(i,y.if P(y) f(i,y) else i fi;s;L)`	[list_accum_filter]
`Thm* P:(T), T':Type, f:({x:T\| P(x) }T'), L:T List, x,y:{x:T\| P(x) }. x before y L f(x) before f(y) mapfilter(f;P;L)`	[mapfilter_before]
`Thm* P:(T), L2,L1:T List. list_accum(l,x.if P(x) [x / l] else l fi;L1;L2) ~ (rev(filter(P;L2)) @ L1)`	[filter_list_accum]
Thm* R:(AA'Prop), P:(BA), P':(BA'), F,G,H:(BAA), F',G',H':(BA'A'), N:(BA(B List)), N':(BA'(B List)), M:(A), M':(A'). (i:B, s:A. P(i,s) M(F(i,s))M(s)) (i:B, s:A. M(G(i,s))M(s)) (i:B, s:A. P(i,s) M(H(i,s)) < M(s)) (i:B, s:A'. P'(i,s) M'(F'(i,s))M'(s)) (i:B, s:A'. M'(G'(i,s))M'(s)) (i:B, s:A'. P'(i,s) M'(H'(i,s)) < M'(s)) (j:B, u:A, v:A'. R(u,v) (P(j,u) P'(j,v))) (j:B, u:A, v:A'. R(u,v) P(j,u) P'(j,v) R(F(j,u),F'(j,v))) (j:B, u:A, v:A'. R(u,v) P(j,u) P'(j,v) R(H(j,u),H'(j,v))) (j:B, u:A, v:A'. R(u,v) R(G(j,u),G'(j,v))) (j:B, u:A, v:A'. R(u,v) N(j,u) = N'(j,v)) (j:B, u:A, v:A'. R(u,v) R(process u j where process s i == if P(i,s) then F(i,s) else G(i,s) where xs := N(i,s); s:= H(i,s); while not null xs { s := process s (hd xs); xs := tl xs; } ,process v j where process s i == if P'(i,s) then F'(i,s) else G'(i,s) where xs := N'(i,s); s:= H'(i,s); while not null xs { s := process s (hd xs); xs := tl xs; } ))	[accumulate-rel]
Thm* M:(A), Q:(BAAProp), P:(BA), F,G,H:(BAA), N:(BA(B List)). (i:B, s:A. P(i,s) M(F(i,s))M(s)) (i:B, s:A. M(G(i,s))M(s)) (i:B, s:A. P(i,s) M(H(i,s)) < M(s)) (j:B, u:A. P(j,u) Q(j,u,F(j,u))) (j:B, u,z:A. P(j,u) Q(j,H(j,u),z) Q(j,u,G(j,z))) (j:B, u:A. Q(j,u,u)) (i,j:B, u,v,z:A. Q(i,u,v) Q(j,v,z) Q(j,u,z)) (j:B, u:A. Q(j,u,process u j where process s i == if P(i,s) then F(i,s) else G(i,s) where xs := N(i,s); s:= H(i,s); while not null xs { s := process s (hd xs); xs := tl xs; } ))	[accumulate-induction1]
`Thm* A,B:Type, P:(BA), F,G,H:(BAA), N:(BA(B List)), M:(A). (i:B, s:A. P(i,s) M(F(i,s))M(s)) (i:B, s:A. M(G(i,s))M(s)) (i:B, s:A. P(i,s) M(H(i,s)) < M(s)) (j:B, u:A. process u j where process s i == if P(i,s) then F(i,s) else G(i,s) where xs := N(i,s); s:= H(i,s); while not null xs { s := process s (hd xs); xs := tl xs; } {s:A\| M(s)M(u) })`	[accumulate_wf]
`Thm* P:(T), T':Type, f:({x:T\| P(x) }T'), L1,L2:T List. mapfilter(f;P;L1 @ L2) = (mapfilter(f;P;L1) @ mapfilter(f;P;L2))`	[mapfilter_append]
`Thm* L:T List, P:(T). (xL.P(x)) (i:\|\|L\|\|. P(L[i]))`	[assert_l_bexists]
`Thm* L:T List, P:(T). (xL.P(x)) (i:\|\|L\|\|. P(L[i]))`	[assert_l_ball]