Nuprl Lemma : wfd-tree-induction-ext
∀[A:Type]. ∀[P:wfd-tree(A) ⟶ ℙ].
(P[w-nil()] ⇒ (∀f:A ⟶ wfd-tree(A). ((∀a:A. P[f a]) ⇒ P[mk-wfd-tree(f)])) ⇒ (∀w:wfd-tree(A). P[w]))
Proof
Definitions occuring in Statement :
mk-wfd-tree: mk-wfd-tree(f),
w-nil: w-nil(),
wfd-tree2: wfd-tree(A),
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
member: t ∈ T,
so_lambda: λ2x.t[x],
wfd-tree-induction,
bool-bar-induction,
list_induction
Lemmas referenced :
wfd-tree-induction,
bool-bar-induction,
list_induction
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}[A:Type]. \mforall{}[P:wfd-tree(A) {}\mrightarrow{} \mBbbP{}].
(P[w-nil()]
{}\mRightarrow{} (\mforall{}f:A {}\mrightarrow{} wfd-tree(A). ((\mforall{}a:A. P[f a]) {}\mRightarrow{} P[mk-wfd-tree(f)]))
{}\mRightarrow{} (\mforall{}w:wfd-tree(A). P[w]))
Date html generated:
2018_05_21-PM-10_18_22
Last ObjectModification:
2018_05_19-PM-04_13_07
Theory : bar!induction
Home
Index