Nuprl Lemma : A-shift-spec_wf

[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. ∀[prog:A-map Unit].  (A-shift-spec(AType; Val; n; prog) ∈ ℙ)


Proof




Definitions occuring in Statement :  A-shift-spec: A-shift-spec(AType; Val; n; prog) A-map: A-map array-model: array-model(AType) array: array{i:l}(Val;n) nat: uall: [x:A]. B[x] prop: unit: Unit member: t ∈ T apply: a universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T A-shift-spec: A-shift-spec(AType; Val; n; prog) so_lambda: λ2x.t[x] nat: prop: and: P ∧ Q implies:  Q int_seg: {i..j-} uiff: uiff(P;Q) uimplies: supposing a lelt: i ≤ j < k ge: i ≥  all: x:A. B[x] decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A top: Top subtract: m guard: {T} le: A ≤ B less_than': less_than'(a;b) so_apply: x[s]
Lemmas referenced :  all_wf Arr_wf int_seg_wf less_than_wf subtract_wf equal_wf A-post-val_wf A-pre-val_wf add-member-int_seg2 nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermSubtract_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_subtract_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf decidable__lt intformless_wf int_formula_prop_less_lemma lelt_wf int_seg_properties false_wf A-map_wf unit_wf2 array_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality hypothesis lambdaEquality natural_numberEquality setElimination rename because_Cache productEquality functionEquality productElimination independent_isectElimination dependent_set_memberEquality independent_pairFormation dependent_functionElimination unionElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality computeAll lambdaFormation axiomEquality equalityTransitivity equalitySymmetry applyEquality universeEquality

Latex:
\mforall{}[Val:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[AType:array\{i:l\}(Val;n)].  \mforall{}[prog:A-map  Unit].
    (A-shift-spec(AType;  Val;  n;  prog)  \mmember{}  \mBbbP{})



Date html generated: 2017_10_01-AM-08_44_46
Last ObjectModification: 2017_07_26-PM-04_30_20

Theory : monads


Home Index