Nuprl Lemma : permutations-list-0
permutations-list(0) ~ [λx.⊥]
Proof
Definitions occuring in Statement :
permutations-list: permutations-list(n),
cons: [a / b],
nil: [],
bottom: ⊥,
lambda: λx.A[x],
natural_number: $n,
sqequal: s ~ t
Definitions unfolded in proof :
it: ⋅,
nil: [],
bfalse: ff,
top: Top,
member: t ∈ T,
uall: ∀[x:A]. B[x],
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,
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 :
select-nil,
injections-combinations,
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,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalRule,
sqequalSubstitution
Latex:
permutations-list(0) \msim{} [\mlambda{}x.\mbot{}]
Date html generated:
2018_05_21-PM-08_21_39
Last ObjectModification:
2018_01_02-PM-01_10_45
Theory : general
Home
Index