Nuprl Lemma : permutations-list-1
permutations-list(1) ~ [λx.[0][x]]
Proof
Definitions occuring in Statement :
permutations-list: permutations-list(n),
select: L[n],
cons: [a / b],
nil: [],
lambda: λx.A[x],
natural_number: $n,
sqequal: s ~ t
Definitions unfolded in proof :
it: ⋅,
nil: [],
top: Top,
member: t ∈ T,
all: ∀x:A. B[x],
biject-inverse,
equipollent-set,
equipollent_functionality_wrt_equipollent2,
equipollent-partition,
equipollent-one-iff,
equipollent-one,
equipollent-subtract,
equipollent-subtract-one,
combination_functionality,
id-biject,
combinations_aux: combinations_aux(b;n;m),
combinations: C(n;m),
pi1: fst(t),
cons: [a / b],
btrue: tt,
fact: (n)!,
lt_int: i <z j,
ifthenelse: if b then t else f fi ,
from-upto: [n, m),
upto: upto(n),
list_ind: list_ind,
map: map(f;as),
injections-combinations,
product_functionality_wrt_equipollent_dependent,
product_functionality_wrt_equipollent_right,
equipollent-multiply,
bfalse: ff,
eq_int: (i =z j),
decidable__int_equal,
decidable__equal_int,
subtract: n - m,
primrec: primrec(n;b;c),
count-combinations,
equipollent-nsub,
equipollent_weakening_ext-eq,
equipollent_transitivity,
equipollent_functionality_wrt_equipollent,
equipollent-factorial,
equipollent_inversion,
equipollent-iff-list,
list-permutations,
permutations-list: permutations-list(n)
Lemmas referenced :
map_nil_lemma,
biject-inverse,
equipollent-set,
equipollent_functionality_wrt_equipollent2,
equipollent-partition,
equipollent-one-iff,
equipollent-one,
equipollent-subtract,
equipollent-subtract-one,
combination_functionality,
id-biject,
injections-combinations,
product_functionality_wrt_equipollent_dependent,
product_functionality_wrt_equipollent_right,
equipollent-multiply,
decidable__int_equal,
decidable__equal_int,
count-combinations,
equipollent-nsub,
equipollent_weakening_ext-eq,
equipollent_transitivity,
equipollent_functionality_wrt_equipollent,
equipollent-factorial,
equipollent_inversion,
equipollent-iff-list,
list-permutations
Rules used in proof :
hypothesis,
voidEquality,
voidElimination,
isect_memberEquality,
thin,
dependent_functionElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalRule,
sqequalSubstitution
Latex:
permutations-list(1) \msim{} [\mlambda{}x.[0][x]]
Date html generated:
2018_05_21-PM-08_21_51
Last ObjectModification:
2018_01_02-PM-01_24_53
Theory : general
Home
Index