{ 
[M:Type 
Type]
n:
[T:Type]
(input-codeable(lp.M[lp];n;T) 
(i:Id. ext-codeable(lp.M[lp];n;T))) }
{ Proof }
Definitions occuring in Statement :
ext-codeable: ext-codeable(lp.M[lp];n;T),
input-codeable: input-codeable(lp.M[lp];n;T),
Id: Id,
nat: ,
uall: [x:A]. B[x],
so_apply: x[s],
all: x:A. B[x],
implies: P Q,
function: x:A B[x],
universe: Type
Definitions :
eclass: EClass(A[eo; e]),
fpf: a:A fp-> B[a],
void: Void,
unit: Unit,
limited-type: LimitedType,
assert: 
b,
input-code: input-code(lp.M[lp];n;T;code;decode),
so_apply: x[s],
member: t 
T,
strong-subtype: strong-subtype(A;B),
atom: Atom$n,
ge: i 
j ,
less_than: a < b,
uimplies: b supposing a,
uiff: uiff(P;Q),
subtype_rel: A 
r B,
process-input': process-input'(lp.M[lp];n),
top: Top,
union: left + right,
equal: s = t,
and: P 
Q,
uall: [x:A]. B[x],
isect: 
x:A. B[x],
prop: 
,
all: x:A. B[x],
exists: 
x:A. B[x],
product: x:A 
B[x],
list: type List,
Id: Id,
input-codeable: input-codeable(lp.M[lp];n;T),
universe: Type,
function: x:A B[x],
so_lambda: 
x.t[x],
nat: ,
set: {x:A| B[x]} ,
int: 
,
le: A 
B,
not: 
A,
false: False,
implies: P Q,
ext-codeable: ext-codeable(lp.M[lp];n;T),
MaAuto: Error :MaAuto,
Auto: Error :Auto,
CollapseTHEN: Error :CollapseTHEN,
D: Error :D,
Try: Error :Try,
pi2: snd(t),
apply: f a,
it: 
,
inr: inr x ,
list_ind: list_ind def,
lambda: x.A[x],
nil: [],
pair: <a, b>,
cons: [car / cdr],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
ExRepD: Error :ExRepD
Lemmas :
top_wf,
Id_wf,
process-input'_wf,
ext-codeable_wf,
nat_wf,
input-codeable_wf,
it_wf,
unit_wf,
member_wf,
pi2_wf,
equal-top
\mforall{}[M:Type {}\mrightarrow{} Type]
\mforall{}n:\mBbbN{}. \mforall{}[T:Type]. (input-codeable(lp.M[lp];n;T) {}\mRightarrow{} (\mforall{}i:Id. ext-codeable(lp.M[lp];n;T)))
Date html generated:
2011_08_17-PM-06_39_42
Last ObjectModification:
2011_06_18-PM-12_05_50
Home
Index