Nuprl Lemma : dl-aprog?_wf

[x:Prog]. (dl-aprog?(x) ∈ 𝔹)


Proof




Definitions occuring in Statement :  dl-aprog?: dl-aprog?(x) dl-prog: Prog bool: 𝔹 uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T dl-aprog?: dl-aprog?(x) all: x:A. B[x]
Lemmas referenced :  eq_atom_wf dl-label_wf dl-prog-obj_wf dl-prog_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin dependent_functionElimination hypothesisEquality hypothesis tokenEquality axiomEquality equalityTransitivity equalitySymmetry universeIsType

Latex:
\mforall{}[x:Prog].  (dl-aprog?(x)  \mmember{}  \mBbbB{})



Date html generated: 2019_10_15-AM-11_40_04
Last ObjectModification: 2019_03_26-AM-11_24_29

Theory : dynamic!logic


Home Index