### Nuprl Lemma : threshold_accum_wf

`∀[S,A,B:Type]. ∀[test:S ─→ A ─→ 𝔹]. ∀[nxt:(S × A) ─→ S]. ∀[step:S ─→ A ─→ S]. ∀[g:(S × A) ─→ (B?)].`
`  (threshold_accum(test;`
`   nxt;`
`   step;`
`   g) ∈ (S × (B?)) ─→ A ─→ (S × (B?)))`

Proof

Definitions occuring in Statement :  threshold_accum: threshold_accum bool: `𝔹` uall: `∀[x:A]. B[x]` unit: `Unit` member: `t ∈ T` function: `x:A ─→ B[x]` product: `x:A × B[x]` union: `left + right` universe: `Type`
Lemmas :  bool_wf eqtt_to_assert eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot it_wf unit_wf2
\mforall{}[S,A,B:Type].  \mforall{}[test:S  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[nxt:(S  \mtimes{}  A)  {}\mrightarrow{}  S].  \mforall{}[step:S  {}\mrightarrow{}  A  {}\mrightarrow{}  S].  \mforall{}[g:(S  \mtimes{}  A)  {}\mrightarrow{}  (B?)].
(threshold\_accum(test;
nxt;
step;
g)  \mmember{}  (S  \mtimes{}  (B?))  {}\mrightarrow{}  A  {}\mrightarrow{}  (S  \mtimes{}  (B?)))

Date html generated: 2015_07_17-AM-08_59_01
Last ObjectModification: 2015_01_27-PM-01_03_50

Home Index