Nuprl Lemma : flip_identity

[k:ℕ]. ∀[i,j:ℕk].  (i, j) x.x) ∈ (ℕk ⟶ ℕk) supposing j ∈ ℤ

Proof

Definitions occuring in Statement :  flip: (i, j) int_seg: {i..j-} nat: uimplies: supposing a uall: [x:A]. B[x] lambda: λx.A[x] function: x:A ⟶ B[x] natural_number: \$n int: equal: t ∈ T
Definitions unfolded in proof :  flip: (i, j) uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a int_seg: {i..j-} all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q ifthenelse: if then else fi  guard: {T} nat: lelt: i ≤ j < k ge: i ≥  decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A top: Top prop: bfalse: ff sq_type: SQType(T) bnot: ¬bb assert: b nequal: a ≠ b ∈
Lemmas referenced :  eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int int_seg_properties nat_properties decidable__equal_int satisfiable-full-omega-tt intformand_wf intformnot_wf intformeq_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_formula_prop_wf decidable__le intformle_wf itermConstant_wf int_formula_prop_le_lemma int_term_value_constant_lemma decidable__lt intformless_wf int_formula_prop_less_lemma lelt_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int int_seg_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut functionExtensionality extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis lambdaFormation unionElimination equalityElimination because_Cache productElimination independent_isectElimination equalityTransitivity equalitySymmetry natural_numberEquality dependent_functionElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll dependent_set_memberEquality promote_hyp instantiate cumulativity independent_functionElimination axiomEquality

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[i,j:\mBbbN{}k].    (i,  j)  =  (\mlambda{}x.x)  supposing  i  =  j

Date html generated: 2017_04_17-AM-08_06_03
Last ObjectModification: 2017_02_27-PM-04_35_08

Theory : list_1

Home Index