Nuprl Lemma : comb_for_mon_itop_wf
λg,p,q,E,z. (Π p ≤ i < q. E[i]) ∈ g:IMonoid ⟶ p:ℤ ⟶ q:ℤ ⟶ E:({p..q-} ⟶ |g|) ⟶ (↓True) ⟶ |g|
Proof
Definitions occuring in Statement : 
mon_itop: Π lb ≤ i < ub. E[i]
, 
imon: IMonoid
, 
grp_car: |g|
, 
int_seg: {i..j-}
, 
so_apply: x[s]
, 
squash: ↓T
, 
true: True
, 
member: t ∈ T
, 
lambda: λx.A[x]
, 
function: x:A ⟶ B[x]
, 
int: ℤ
Definitions unfolded in proof : 
member: t ∈ T
, 
squash: ↓T
, 
uall: ∀[x:A]. B[x]
, 
prop: ℙ
, 
imon: IMonoid
Lemmas referenced : 
mon_itop_wf, 
squash_wf, 
true_wf, 
int_seg_wf, 
grp_car_wf, 
imon_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
lambdaEquality, 
sqequalHypSubstitution, 
imageElimination, 
cut, 
lemma_by_obid, 
isectElimination, 
thin, 
hypothesisEquality, 
equalityTransitivity, 
hypothesis, 
equalitySymmetry, 
functionEquality, 
setElimination, 
rename, 
intEquality
Latex:
\mlambda{}g,p,q,E,z.  (\mPi{}  p  \mleq{}  i  <  q.  E[i])  \mmember{}  g:IMonoid  {}\mrightarrow{}  p:\mBbbZ{}  {}\mrightarrow{}  q:\mBbbZ{}  {}\mrightarrow{}  E:(\{p..q\msupminus{}\}  {}\mrightarrow{}  |g|)  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  |g|
Date html generated:
2016_05_15-PM-00_15_51
Last ObjectModification:
2015_12_26-PM-11_39_50
Theory : groups_1
Home
Index