Nuprl Lemma : base4-rep_wf
n:
. (base4-rep(n) 
4 List)
Proof not projected
Definitions occuring in Statement :
base4-rep: base4-rep(n),
int_seg: {i..j
},
nat: ,
all: x:A. B[x],
member: t T,
list: type List,
natural_number: $n
Definitions :
equal: s = t,
int_seg: {i..j},
list: type List,
member: t T,
callbyvalueall: callbyvalueall,
implies: P 
Q,
false: False,
not: 
A,
le: A 
B,
int: 
,
set: {x:A| B[x]} ,
nat: ,
base4-rep: base4-rep(n),
function: x:A 
B[x],
all: x:A. B[x],
uall: [x:A]. B[x],
isect: 
x:A. B[x],
subtype_rel: A 
r B,
uiff: uiff(P;Q),
and: P 
Q,
product: x:A 
B[x],
uimplies: b supposing a,
less_than: a < b,
ge: i 
j ,
strong-subtype: strong-subtype(A;B),
vr_base4-ext,
fpf: a:A fp-> B[a],
eclass: EClass(A[eo; e]),
tactic: Error :tactic,
pair: <a, b>,
has-valueall: has-valueall(a),
pi1: fst(t),
rationals: 
,
apply: f a,
exists: 
x:A. B[x],
natural_number: $n,
sum: 
(f[x] | x < k),
length: ||as||,
multiply: n * m,
exp: i^n,
select: l[i],
top: Top,
subtype: S T,
quotient: x,y:A//B[x; y],
prop: 
,
universe: Type,
so_lambda: 
x.t[x],
lambda: x.A[x],
nil: [],
real: 
,
void: Void,
nat_plus: 
,
int_nzero: 
,
lelt: i j < k,
es-E-interface: E(X),
grp_car: |g|,
limited-type: LimitedType,
b-union: A 
B,
bool: 
,
btrue: tt,
union: left + right,
ifthenelse: if b then t else f fi ,
sq_type: SQType(T),
guard: {T},
cons: [car / cdr],
fpf-cap: f(x)?z,
true: True,
bag: bag(T),
isect2: T1 T2,
dataflow: dataflow(A;B),
fset: FSet{T},
record: record(x.T[x]),
record+: record+,
labeled-graph: LabeledGraph(T),
ldag: LabeledDAG(T),
iff: P 
Q,
or: P 
Q,
rev_implies: P Q,
tag-by: zT,
bfalse: ff,
tunion: x:A.B[x],
so_lambda: x y.t[x; y],
qeq: qeq(r;s),
equiv_rel: EquivRel(T;x,y.E[x; y]),
trans: Trans(T;x,y.E[x; y]),
sym: Sym(T;x,y.E[x; y]),
refl: Refl(T;x,y.E[x; y]),
class-program: ClassProgram(T),
ma-state: State(ds),
deq: EqDecider(T),
fpf-sub: f g,
intensional-universe: IType,
bnot: 
b,
assert: 
b,
bor: p q,
band: p q,
bimplies: p q,
es-ble: e loc e',
es-bless: e <loc e',
es-eq-E: e = e',
eq_lnk: a = b,
eq_id: a = b,
deq-all-disjoint: deq-all-disjoint(eq;ass;bs),
deq-disjoint: deq-disjoint(eq;as;bs),
deq-member: deq-member(eq;x;L),
q_le: q_le(r;s),
q_less: q_less(r;s),
l_member: (x l),
Knd: Knd,
so_apply: x[s],
locl: locl(a),
append: as @ bs,
Id: Id,
atom: Atom$n,
valueall-type: valueall-type(T),
rec: rec(x.A[x]),
atom: Atom
Lemmas :
int-valueall-type,
set-valueall-type,
list-valueall-type,
valueall-type_wf,
Id_wf,
Id-has-valueall,
false_wf,
int-equal-in-rationals,
rev_implies_wf,
iff_wf,
assert-qeq,
iff_weakening_uiff,
iff_functionality_wrt_iff,
assert_wf,
true_wf,
iff_imp_equal_bool,
qeq_wf,
intensional-universe_wf,
refl_wf,
sym_wf,
trans_wf,
equiv_rel_wf,
qeq_wf2,
quotient_wf,
tunion_wf,
bfalse_wf,
subtype_rel_wf,
ifthenelse_wf,
btrue_wf,
bool_wf,
b-union_wf,
int_nzero_wf,
Error :pi1_wf,
int-rational,
rational-has-value,
pi1_wf_top,
vr_base4-ext,
nat_properties,
sum_wf,
length_wf_nat,
top_wf,
exp_wf2,
le_wf,
select_wf,
int_seg_properties,
length_wf,
rationals_wf,
int_seg_wf,
member_wf,
nat_wf
\mforall{}n:\mBbbN{}. (base4-rep(n) \mmember{} \mBbbN{}4 List)
Date html generated:
2012_02_20-PM-03_31_29
Last ObjectModification:
2012_02_02-PM-01_55_02
Home
Index