`∀n:ℕ. ∀i,j:ℕn.  ∃L:ℕn - 1 List. ((i, j) = reduce(λi,g. ((i, i + 1) o g);λx.x;L) ∈ (ℕn ⟶ ℕn))`

Proof

Definitions occuring in Statement :  flip: `(i, j)` reduce: `reduce(f;k;as)` list: `T List` compose: `f o g` int_seg: `{i..j-}` nat: `ℕ` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` subtract: `n - m` add: `n + m` natural_number: `\$n` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` so_apply: `x[s]` so_lambda: `λ2x.t[x]` subtract: `n - m` uiff: `uiff(P;Q)` or: `P ∨ Q` decidable: `Dec(P)` prop: `ℙ` top: `Top` false: `False` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` not: `¬A` uimplies: `b supposing a` and: `P ∧ Q` lelt: `i ≤ j < k` ge: `i ≥ j ` nat: `ℕ` int_seg: `{i..j-}` guard: `{T}` member: `t ∈ T` uall: `∀[x:A]. B[x]` implies: `P `` Q` so_apply: `x[s1;s2;s3]` so_lambda: so_lambda3 append: `as @ bs` compose: `f o g` true: `True` squash: `↓T` subtype_rel: `A ⊆r B` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` sq_type: `SQType(T)` le: `A ≤ B` less_than: `a < b` flip: `(i, j)` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` bfalse: `ff` bnot: `¬bb` assert: `↑b`
Lemmas referenced :  istype-nat equal_wf exists_wf le_wf all_wf primrec-wf2 add-member-int_seg2 reduce_wf istype-less_than int_formula_prop_not_lemma intformnot_wf decidable__lt flip_wf compose_wf list_wf decidable__le int_seg_wf subtract_wf istype-le int_formula_prop_wf int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_term_value_subtract_lemma int_formula_prop_le_lemma istype-void int_formula_prop_and_lemma istype-int intformless_wf itermConstant_wf itermVar_wf itermSubtract_wf intformle_wf intformand_wf full-omega-unsat nat_properties int_seg_properties subtract-add-cancel nil_wf cons_wf append_wf reduce_nil_lemma reduce-append reduce_cons_lemma list_ind_nil_lemma list_ind_cons_lemma flip-conjugation1 squash_wf true_wf istype-universe subtype_rel_self iff_weakening_equal int_term_value_add_lemma int_formula_prop_eq_lemma itermAdd_wf intformeq_wf decidable__equal_int int_subtype_base lelt_wf set_subtype_base subtype_base_sq list_subtype_base equal-wf-base-T eq_int_wf eqtt_to_assert assert_of_eq_int eqff_to_assert bool_cases_sqequal bool_wf bool_subtype_base assert-bnot neg_assert_of_eq_int ifthenelse_wf flip_identity
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut introduction extract_by_obid hypothesis inhabitedIsType setIsType functionEquality dependent_set_memberEquality_alt closedConclusion equalityIstype productIsType functionIsType unionElimination because_Cache universeIsType independent_pairFormation sqequalRule voidElimination isect_memberEquality_alt dependent_functionElimination int_eqEquality lambdaEquality_alt dependent_pairFormation_alt independent_functionElimination approximateComputation independent_isectElimination productElimination hypothesisEquality rename setElimination natural_numberEquality isectElimination sqequalHypSubstitution thin addEquality equalitySymmetry equalityTransitivity applyLambdaEquality hyp_replacement applyEquality functionExtensionality_alt equalityIsType1 imageElimination instantiate universeEquality imageMemberEquality baseClosed intEquality cumulativity sqequalBase baseApply Error :memTop,  functionExtensionality equalityElimination promote_hyp

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}i,j:\mBbbN{}n.    \mexists{}L:\mBbbN{}n  -  1  List.  ((i,  j)  =  reduce(\mlambda{}i,g.  ((i,  i  +  1)  o  g);\mlambda{}x.x;L))

Date html generated: 2020_05_19-PM-09_44_10
Last ObjectModification: 2020_01_04-PM-08_18_51

Theory : list_1

Home Index