Nuprl Lemma : int-value-type

value-type(ℤ)


Proof




Definitions occuring in Statement :  value-type: value-type(T) int:
Definitions unfolded in proof :  value-type: value-type(T) uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T sq_stable: SqStable(P) implies:  Q all: x:A. B[x] has-value: (a)↓ prop: squash: T
Lemmas referenced :  sq_stable__has-value equal_wf equal-wf-base base_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_functionElimination equalityTransitivity equalitySymmetry intEquality lambdaFormation callbyvalueInt dependent_functionElimination sqequalRule imageMemberEquality baseClosed imageElimination because_Cache

Latex:
value-type(\mBbbZ{})



Date html generated: 2017_04_14-AM-07_15_10
Last ObjectModification: 2017_02_27-PM-02_50_28

Theory : call!by!value_1


Home Index