Nuprl Lemma : oalist_cases_c
∀a:LOSet. ∀b:AbDMon. ∀Q:|oal(a;b)| ⟶ ℙ.
(Q[00]
⇒ (∀ws:|oal(a;b)|. ∀x:|a|. ∀y:|b|. ((↑before(x;map(λx.(fst(x));ws))) ⇒ (¬(y = e ∈ |b|)) ⇒ Q[oal_cons_pr(x;y;ws)]))
⇒ {∀ws:|oal(a;b)|. Q[ws]})
Proof
Definitions occuring in Statement :
oal_cons_pr: oal_cons_pr(x;y;ws),
oal_nil: 00,
oalist: oal(a;b),
before: before(u;ps),
map: map(f;as),
assert: ↑b,
prop: ℙ,
guard: {T},
so_apply: x[s],
pi1: fst(t),
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
lambda: λx.A[x],
function: x:A ⟶ B[x],
equal: s = t ∈ T,
abdmonoid: AbDMon,
grp_id: e,
grp_car: |g|,
loset: LOSet,
set_car: |p|
Definitions unfolded in proof :
oal_cons_pr: oal_cons_pr(x;y;ws),
oal_nil: 00
Lemmas referenced :
oalist_cases_a
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lemma_by_obid
Latex:
\mforall{}a:LOSet. \mforall{}b:AbDMon. \mforall{}Q:|oal(a;b)| {}\mrightarrow{} \mBbbP{}.
(Q[00]
{}\mRightarrow{} (\mforall{}ws:|oal(a;b)|. \mforall{}x:|a|. \mforall{}y:|b|.
((\muparrow{}before(x;map(\mlambda{}x.(fst(x));ws))) {}\mRightarrow{} (\mneg{}(y = e)) {}\mRightarrow{} Q[oal\_cons\_pr(x;y;ws)]))
{}\mRightarrow{} \{\mforall{}ws:|oal(a;b)|. Q[ws]\})
Date html generated:
2016_05_16-AM-08_16_06
Last ObjectModification:
2015_12_28-PM-06_28_27
Theory : polynom_2
Home
Index