Nuprl Lemma : sq_stable__eo_axioms
∀[r:eo_record{i:l}()]. SqStable(eo_axioms(r))
Proof
Definitions occuring in Statement :
eo_axioms: eo_axioms(r),
eo_record: eo_record{i:l}(),
sq_stable: SqStable(P),
uall: ∀[x:A]. B[x]
Lemmas :
subtype_rel_self,
bool_wf,
Id_wf,
nat_wf,
sq_stable__and,
all_wf,
squash_wf,
infix_ap_wf,
less_than_wf,
equal_wf,
not_wf,
isect_wf,
iff_wf,
assert_wf,
sq_stable__all,
sq_stable__less_than,
member-less_than,
sq_stable__equal,
sq_stable__not,
sq_stable__squash,
sq_stable__uall,
sq_stable__iff,
sq_stable__assert,
assert_witness,
eo_record_wf
\mforall{}[r:eo\_record\{i:l\}()]. SqStable(eo\_axioms(r))
Date html generated:
2015_07_17-AM-08_33_53
Last ObjectModification:
2015_01_27-PM-03_00_06
Home
Index