Nuprl Lemma : swap-exists

n:ℕ. ∀AType:array{i:l}(ℤ;n).  ∃prog:ℕn ⟶ ℕn ⟶ (A-map Unit). ∀[i,j:ℕn].  alt-swap-spec(AType;n;prog)


Proof




Definitions occuring in Statement :  alt-swap-spec: alt-swap-spec(AType;n;prog) A-map: A-map array-model: array-model(AType) array: array{i:l}(Val;n) int_seg: {i..j-} nat: uall: [x:A]. B[x] all: x:A. B[x] exists: x:A. B[x] unit: Unit apply: a function: x:A ⟶ B[x] natural_number: $n int:
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T uall: [x:A]. B[x] exists: x:A. B[x] nat: alt-swap-spec: alt-swap-spec(AType;n;prog) and: P ∧ Q implies:  Q array: array{i:l}(Val;n) simple-swap: simple-swap(AModel;i;j) A-pre-val: A-pre-val(AType;A;i) A-post-val: A-post-val(AType;prog;A;i) idx: idx(AType) array-model: array-model(AType) A-fetch': A-fetch'(AModel) A-coerce: A-coerce(AModel) A-assign: A-assign(AModel) A-bind: A-bind(AModel) A-eval: A-eval(AModel) Arr: Arr(AType) pi1: fst(t) pi2: snd(t) upd: upd(AType) array-monad: array-monad(AType) M-bind: M-bind(Mnd) let: let mk_monad: mk_monad(M;return;bind) cand: c∧ B not: ¬A subtype_rel: A ⊆B int_seg: {i..j-} so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a false: False true: True bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  bfalse: ff or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b nequal: a ≠ b ∈  ge: i ≥  lelt: i ≤ j < k satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top prop: squash: T iff: ⇐⇒ Q rev_implies:  Q decidable: Dec(P)
Lemmas referenced :  array_wf nat_wf simple-swap_wf int_seg_wf set_subtype_base lelt_wf int_subtype_base istype-void istype-universe eq_int_wf eqtt_to_assert assert_of_eq_int eqff_to_assert istype-int bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot neg_assert_of_eq_int int_seg_properties nat_properties full-omega-unsat intformnot_wf intformeq_wf itermVar_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_formula_prop_wf equal_wf squash_wf true_wf subtype_rel_self iff_weakening_equal equal-wf-base assert_wf decidable__equal_int bnot_wf not_wf assert_elim eq_int_eq_true bfalse_wf btrue_neq_bfalse uiff_transitivity iff_transitivity iff_weakening_uiff assert_of_bnot subtype_rel-equal base_wf alt-swap-spec_wf2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt universeIsType cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin intEquality hypothesisEquality hypothesis dependent_pairFormation_alt lambdaEquality_alt inhabitedIsType natural_numberEquality setElimination rename isect_memberFormation_alt sqequalRule dependent_functionElimination productElimination independent_pairEquality axiomEquality functionIsTypeImplies isect_memberEquality_alt because_Cache isectIsType independent_pairFormation productIsType functionIsType equalityIsType4 equalityTransitivity equalitySymmetry applyEquality closedConclusion independent_isectElimination unionElimination equalityElimination equalityIsType2 baseApply baseClosed promote_hyp instantiate cumulativity independent_functionElimination voidElimination approximateComputation int_eqEquality equalityIsType1 imageElimination universeEquality imageMemberEquality

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}AType:array\{i:l\}(\mBbbZ{};n).
    \mexists{}prog:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n  {}\mrightarrow{}  (A-map  Unit).  \mforall{}[i,j:\mBbbN{}n].    alt-swap-spec(AType;n;prog)



Date html generated: 2019_10_15-AM-10_59_39
Last ObjectModification: 2018_10_11-PM-06_53_12

Theory : monads


Home Index