Nuprl Lemma : sq_stable__iterated

∀[Info,A,S:Type]. ∀[init:Id ─→ bag(S)]. ∀[f:A ─→ S ─→ S]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:S].

SqStable(iterated_classrel(es;S;A;f;init;X;e;v))

Proof

Definitions occuring in Statement : iterated_classrel: iterated_classrel(es;S;A;f;init;X;e;v), eclass: EClass(A[eo; e]), event-ordering+: EO+(Info), es-E: E, Id: Id, sq_stable: SqStable(P), uall: ∀[x:A]. B[x], function: x:A ─→ B[x], universe: Type, bag: bag(T)
Lemmas : sq_stable__squash, exists_wf, es-first_wf2, bool_wf, eqtt_to_assert, bag-member_wf, es-loc_wf, eqff_to_assert, equal_wf, bool_cases_sqequal, subtype_base_sq, bool_subtype_base, assert-bnot, iterated_classrel_wf, es-pred_wf, or_wf, classrel_wf, all_wf, not_wf, es-E_wf, event-ordering+_subtype, event-ordering+_wf, eclass_wf, Id_wf, bag_wf
\mforall{}[Info,A,S:Type]. \mforall{}[init:Id {}\mrightarrow{} bag(S)]. \mforall{}[f:A {}\mrightarrow{} S {}\mrightarrow{} S]. \mforall{}[X:EClass(A)]. \mforall{}[es:EO+(Info)]. \mforall{}[e:E]. \mforall{}[v:S]. SqStable(iterated\_classrel(es;S;A;f;init;X;e;v)) Date html generated: 2015_07_17-PM-00_23_01 Last ObjectModification: 2015_01_27-PM-11_36_59 Home Index