Nuprl Lemma : A-loop_wf

[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)].
  ∀lo:ℕn. ∀k:ℕ.  (k < lo  (∀[body:{lo..lo k-} ⟶ (A-map Unit)]. (A-loop(AType;lo;lo k;body) ∈ A-map Unit)))


Proof




Definitions occuring in Statement :  A-loop: A-loop(AType;lo;hi;body) A-map: A-map array-model: array-model(AType) array: array{i:l}(Val;n) int_seg: {i..j-} nat: less_than: a < b uall: [x:A]. B[x] all: x:A. B[x] implies:  Q unit: Unit member: t ∈ T apply: a function: x:A ⟶ B[x] subtract: m add: m natural_number: $n universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] implies:  Q int_seg: {i..j-} nat: prop: false: False ge: i ≥  uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] not: ¬A top: Top and: P ∧ Q decidable: Dec(P) or: P ∨ Q A-loop: A-loop(AType;lo;hi;body) guard: {T} lelt: i ≤ j < k bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  bfalse: ff subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] squash: T label: ...$L... t subtract: m sq_type: SQType(T) true: True iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  int_seg_wf A-map_wf unit_wf2 less_than_wf subtract_wf nat_wf array_wf nat_properties satisfiable-full-omega-tt intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf decidable__le intformnot_wf itermSubtract_wf int_formula_prop_not_lemma int_term_value_subtract_lemma le_int_wf bool_wf equal-wf-T-base assert_wf le_wf A-null_wf lt_int_wf bnot_wf int_seg_properties itermAdd_wf int_term_value_add_lemma uiff_transitivity eqtt_to_assert assert_of_le_int eqff_to_assert assert_functionality_wrt_uiff bnot_of_le_int assert_of_lt_int equal_wf decidable__lt subtype_rel_dep_function int_seg_subtype subtype_rel_self decidable__equal_int intformeq_wf int_formula_prop_eq_lemma member_wf squash_wf true_wf add-swap add-commutes and_wf subtype_base_sq int_subtype_base iff_weakening_equal lelt_wf A-bind_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation sqequalHypSubstitution hypothesis sqequalRule axiomEquality equalityTransitivity equalitySymmetry functionEquality extract_by_obid isectElimination thin setElimination rename hypothesisEquality addEquality because_Cache applyEquality cumulativity natural_numberEquality lambdaEquality dependent_functionElimination isect_memberEquality universeEquality intWeakElimination independent_isectElimination dependent_pairFormation int_eqEquality intEquality voidElimination voidEquality independent_pairFormation computeAll independent_functionElimination unionElimination baseClosed productElimination equalityElimination imageElimination minusEquality dependent_set_memberEquality hyp_replacement applyLambdaEquality instantiate imageMemberEquality functionExtensionality

Latex:
\mforall{}[Val:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[AType:array\{i:l\}(Val;n)].
    \mforall{}lo:\mBbbN{}n.  \mforall{}k:\mBbbN{}.
        (k  <  n  -  lo
        {}\mRightarrow{}  (\mforall{}[body:\{lo..lo  +  k\msupminus{}\}  {}\mrightarrow{}  (A-map  Unit)].  (A-loop(AType;lo;lo  +  k;body)  \mmember{}  A-map  Unit)))



Date html generated: 2017_10_01-AM-08_44_13
Last ObjectModification: 2017_07_26-PM-04_30_10

Theory : monads


Home Index