Nuprl Lemma : code-seq1_wf

[k:ℕ]. ∀[s:ℕk ⟶ ℕ].  (code-seq1(k;s) ∈ ℕ)


Proof




Definitions occuring in Statement :  code-seq1: code-seq1(k;s) int_seg: {i..j-} nat: uall: [x:A]. B[x] member: t ∈ T function: x:A ⟶ B[x] natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T code-seq1: code-seq1(k;s) nat: le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) false: False not: ¬A implies:  Q prop: int_seg: {i..j-} all: x:A. B[x] bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  uiff: uiff(P;Q) uimplies: supposing a bfalse: ff exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b
Lemmas referenced :  primrec_wf nat_wf false_wf le_wf eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int int_seg_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int code-pair_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis hypothesisEquality dependent_set_memberEquality natural_numberEquality independent_pairFormation lambdaFormation lambdaEquality setElimination rename unionElimination equalityElimination productElimination independent_isectElimination because_Cache applyEquality functionExtensionality equalityTransitivity equalitySymmetry dependent_pairFormation promote_hyp dependent_functionElimination instantiate cumulativity independent_functionElimination voidElimination axiomEquality functionEquality isect_memberEquality

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[s:\mBbbN{}k  {}\mrightarrow{}  \mBbbN{}].    (code-seq1(k;s)  \mmember{}  \mBbbN{})



Date html generated: 2019_06_20-PM-02_39_40
Last ObjectModification: 2019_06_12-PM-00_27_45

Theory : num_thy_1


Home Index