Def  P  Q == (P  Q) & (P  Q)

is mentioned by

Thm*  ( i:{a..b}. e(i)) = 0  (i:{a..b}. e(i) = 0)	[iter_prod_zero_iff_factor_zero]
Thm*  e:({a..b}). ( i:{a..b}. e(i)) = 1  (i:{a..b}. e(i) = 1)	[iter_nat_prod_one_iff_factors_one]
Thm*  a,b:, P:({a..b}Prop). (i:{a..b}. P(i))  (Or i:{a..b}. P(i))	[exist_intseg_vs_iter_or]
Thm*  a,b:, P:({a..b}Prop). Thm*  a<b  ((i:{a..b}. P(i))  (i:{a..(b-1)}. P(i))  P(b-1))	[or_via_exist_intseg_split_last]
Thm*  a,b:, P:({a..b}Prop). Thm*  a<b Thm*   Thm*  (c:. b = c+1  ((i:{a..b}. P(i))  (i:{a..c}. P(i))  P(c)))	[or_via_exist_intseg_notnull]
Thm*  a,b:, P:({a..b}Prop). (i:{a..b}. P(i))  (And i:{a..b}. P(i))	[all_intseg_vs_iter_and]
Thm*  a,b:, P:({a..b}Prop). Thm*  a<b  ((i:{a..b}. P(i))  (i:{a..(b-1)}. P(i)) & P(b-1))	[and_via_all_intseg_split_last]
Thm*  a,b:, P:({a..b}Prop). Thm*  a<b Thm*   Thm*  (c:. b = c+1  ((i:{a..b}. P(i))  (i:{a..c}. P(i)) & P(c)))	[and_via_all_intseg_notnull]

In prior sections: core well fnd int 1 bool 1 rel 1 quot 1 LogicSupplement int 2 num thy 1 SimpleMulFacts

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html