Nuprl Lemma : corec-greatest
∀[F:Type ⟶ Type]. ∀[X:Type]. X ⊆r corec(T.F[T]) supposing X ≡ F[X] supposing Monotone(T.F[T])
Proof
Definitions occuring in Statement :
corec: corec(T.F[T]),
type-monotone: Monotone(T.F[T]),
ext-eq: A ≡ B,
uimplies: b supposing a,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
so_apply: x[s],
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
bfalse: ff,
it: ⋅,
unit: Unit,
bool: 𝔹,
type-monotone: Monotone(T.F[T]),
true: True,
less_than': less_than'(a;b),
le: A ≤ B,
uiff: uiff(P;Q),
rev_implies: P ⇐ Q,
not: ¬A,
and: P ∧ Q,
iff: P ⇐⇒ Q,
or: P ∨ Q,
decidable: Dec(P),
btrue: tt,
ifthenelse: if b then t else f fi ,
subtract: n - m,
lt_int: i <z j,
top: Top,
subtype_rel: A ⊆r B,
guard: {T},
ge: i ≥ j ,
false: False,
implies: P ⇒ Q,
nat: ℕ,
all: ∀x:A. B[x],
so_lambda: λ2x.t[x],
prop: ℙ,
so_apply: x[s],
member: t ∈ T,
corec: corec(T.F[T]),
uimplies: b supposing a,
uall: ∀[x:A]. B[x]
Lemmas referenced :
equal_wf,
assert_of_le_int,
bnot_of_lt_int,
assert_functionality_wrt_uiff,
eqff_to_assert,
assert_of_lt_int,
eqtt_to_assert,
uiff_transitivity,
subtype_rel_weakening,
subtype_rel_transitivity,
int_seg_wf,
top_wf,
not-le-2,
primrec_wf,
bnot_wf,
le_wf,
le_int_wf,
assert_wf,
int_subtype_base,
equal-wf-base,
bool_wf,
lt_int_wf,
nat_wf,
le-add-cancel,
add-zero,
add_functionality_wrt_le,
add-commutes,
add-swap,
add-associates,
minus-minus,
minus-add,
minus-one-mul-top,
zero-add,
minus-one-mul,
condition-implies-le,
less-iff-le,
not-ge-2,
false_wf,
subtract_wf,
decidable__le,
primrec-unroll,
less_than_wf,
ge_wf,
less_than_irreflexivity,
less_than_transitivity1,
nat_properties,
type-monotone_wf,
ext-eq_wf
Rules used in proof :
equalitySymmetry,
equalityTransitivity,
equalityElimination,
cumulativity,
functionExtensionality,
dependent_set_memberEquality,
instantiate,
baseClosed,
closedConclusion,
baseApply,
because_Cache,
minusEquality,
intEquality,
addEquality,
productElimination,
independent_pairFormation,
unionElimination,
voidEquality,
isect_memberEquality,
axiomEquality,
dependent_functionElimination,
voidElimination,
independent_functionElimination,
independent_isectElimination,
natural_numberEquality,
intWeakElimination,
rename,
setElimination,
lambdaFormation,
functionEquality,
lambdaEquality,
sqequalRule,
universeEquality,
hypothesis,
applyEquality,
hypothesisEquality,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[F:Type {}\mrightarrow{} Type]. \mforall{}[X:Type]. X \msubseteq{}r corec(T.F[T]) supposing X \mequiv{} F[X] supposing Monotone(T.F[T])
Date html generated:
2018_07_29-AM-09_21_24
Last ObjectModification:
2018_07_25-PM-06_19_46
Theory : co-recursion
Home
Index