Nuprl Lemma : permutation-invariant2

`∀[T:Type]. ∀[R:(T List) ⟶ (T List) ⟶ ℙ].`
`  (Trans(T List;as,bs.R[as;bs])`
`  `` Refl(T List;as,bs.R[as;bs])`
`  `` (∀as:T List. ∀a:T.  R[[a / as];as @ [a]])`
`  `` (∀as:T List. ∀a1,a2:T.  R[[a1; [a2 / as]];[a2; [a1 / as]]])`
`  `` (∀as,bs:T List.  (permutation(T;as;bs) `` R[as;bs])))`

Proof

Definitions occuring in Statement :  permutation: `permutation(T;L1;L2)` append: `as @ bs` cons: `[a / b]` nil: `[]` list: `T List` trans: `Trans(T;x,y.E[x; y])` refl: `Refl(T;x,y.E[x; y])` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  guard: `{T}` so_lambda: `λ2x y.t[x; y]` prop: `ℙ` so_apply: `x[s1;s2]` uimplies: `b supposing a` so_apply: `x[s]` so_lambda: `λ2x.t[x]` nat: `ℕ` subtype_rel: `A ⊆r B` member: `t ∈ T` and: `P ∧ Q` exists: `∃x:A. B[x]` permutation: `permutation(T;L1;L2)` all: `∀x:A. B[x]` implies: `P `` Q` uall: `∀[x:A]. B[x]` refl: `Refl(T;x,y.E[x; y])` lelt: `i ≤ j < k` int_seg: `{i..j-}` false: `False` satisfiable_int_formula: `satisfiable_int_formula(fmla)` not: `¬A` squash: `↓T` less_than: `a < b` or: `P ∨ Q` decidable: `Dec(P)` trans: `Trans(T;x,y.E[x; y])` cons: `[a / b]` it: `⋅` nil: `[]` list_ind: list_ind length: `||as||` less_than': `less_than'(a;b)` ge: `i ≥ j ` le: `A ≤ B` top: `Top` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` true: `True` subtract: `n - m` select: `L[n]` sq_type: `SQType(T)` flip: `(i, j)` bool: `𝔹` unit: `Unit` btrue: `tt` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` bfalse: `ff` mklist: `mklist(n;f)` permute_list: `(L o f)` rotate: `rot(n)`
Lemmas referenced :  istype-universe trans_wf refl_wf nil_wf append_wf subtype_rel_self cons_wf list_wf permutation_wf istype-less_than member-less_than length_wf int_seg_wf inject_wf permute_list_wf permutation-generators2 int_subtype_base istype-int le_wf set_subtype_base istype-nat length_wf_nat permute_list-identity permute_list-compose decidable__lt istype-le int_formula_prop_wf int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma intformless_wf itermVar_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf full-omega-unsat decidable__le flip_wf compose_wf permute_list_length product_subtype_list list-cases nat_wf less_than_wf lelt_wf int_term_value_add_lemma itermAdd_wf satisfiable-full-omega-tt non_neg_length false_wf length_of_cons_lemma list_extensionality iff_weakening_equal select_wf nat_properties permute_list_select true_wf squash_wf equal_wf not_wf bnot_wf subtype_base_sq assert_wf equal-wf-T-base bool_wf eq_int_wf uiff_transitivity eqtt_to_assert assert_of_eq_int iff_transitivity iff_weakening_uiff eqff_to_assert assert_of_bnot int_term_value_subtract_lemma itermSubtract_wf subtract_wf int_formula_prop_eq_lemma intformeq_wf select_cons_tl rotate_wf primrec0_lemma istype-base stuck-spread length_of_nil_lemma length_cons length-append select_append_front select_cons_tl_sq2 istype-void istype-assert equal-wf-base select-cons-hd length-singleton add-is-int-iff select_append_back
Rules used in proof :  universeEquality instantiate functionIsType applyLambdaEquality hyp_replacement independent_functionElimination because_Cache universeIsType inhabitedIsType setIsType rename setElimination dependent_functionElimination equalitySymmetry sqequalBase independent_isectElimination natural_numberEquality lambdaEquality_alt intEquality sqequalRule applyEquality equalityIstype hypothesisEquality isectElimination extract_by_obid introduction hypothesis dependent_set_memberEquality_alt cut thin productElimination sqequalHypSubstitution lambdaFormation_alt isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution productIsType voidElimination independent_pairFormation Error :memTop,  int_eqEquality dependent_pairFormation_alt approximateComputation imageElimination unionElimination equalityTransitivity hypothesis_subsumption promote_hyp computeAll lambdaEquality dependent_pairFormation addEquality lambdaFormation dependent_set_memberEquality voidEquality isect_memberEquality cumulativity baseClosed imageMemberEquality equalityElimination impliesFunctionality closedConclusion baseApply pointwiseFunctionality

Latex:
\mforall{}[T:Type].  \mforall{}[R:(T  List)  {}\mrightarrow{}  (T  List)  {}\mrightarrow{}  \mBbbP{}].
(Trans(T  List;as,bs.R[as;bs])
{}\mRightarrow{}  Refl(T  List;as,bs.R[as;bs])
{}\mRightarrow{}  (\mforall{}as:T  List.  \mforall{}a:T.    R[[a  /  as];as  @  [a]])
{}\mRightarrow{}  (\mforall{}as:T  List.  \mforall{}a1,a2:T.    R[[a1;  [a2  /  as]];[a2;  [a1  /  as]]])
{}\mRightarrow{}  (\mforall{}as,bs:T  List.    (permutation(T;as;bs)  {}\mRightarrow{}  R[as;bs])))

Date html generated: 2020_05_19-PM-09_44_58
Last ObjectModification: 2019_12_26-AM-11_46_41

Theory : list_1

Home Index