Nuprl Lemma : ncomplete-test
((∀a:Prop. (localT prop(a) ∈ Prop List)) ∧ (∀n:node. (fst(n) ∈ Prop List)))
∧ (∀n:node. (∀f∈fst(n).f ∈ Prop))
∧ (∀n:node. (∀f1∈fst(n).(∀f∈localT prop(f1).f ∈ Prop)))
∧ (∀n:node. (∀f∈fst(n).(∀f1∈localT prop(f).(∃f1'∈fst(n). dlo_eq(prop(f1);prop(f1')) ∈ 𝔹))))
Proof
Definitions occuring in Statement :
dl-localT: localT,
node: node,
dlo_eq: dlo_eq(a;b),
dl-prop-obj: prop(x),
dl-prop: Prop,
l_exists: (∃x∈L. P[x]),
l_all: (∀x∈L.P[x]),
list: T List,
bool: 𝔹,
pi1: fst(t),
all: ∀x:A. B[x],
and: P ∧ Q,
member: t ∈ T,
apply: f a
Definitions unfolded in proof :
and: P ∧ Q,
cand: A c∧ B,
all: ∀x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
node: node,
top: Top,
l_all: (∀x∈L.P[x]),
pi1: fst(t),
int_seg: {i..j-},
uimplies: b supposing a,
lelt: i ≤ j < k,
le: A ≤ B,
less_than: a < b,
squash: ↓T,
decidable: Dec(P),
or: P ∨ Q,
not: ¬A,
implies: P ⇒ Q,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
false: False,
prop: ℙ,
guard: {T},
l_exists: (∃x∈L. P[x])
Lemmas referenced :
dl-localT_wf,
dl-prop-obj_wf,
dl-prop_wf,
pi1_wf_top,
list_wf,
istype-void,
node_wf,
select_wf,
int_seg_properties,
decidable__le,
full-omega-unsat,
intformand_wf,
intformnot_wf,
intformle_wf,
itermConstant_wf,
itermVar_wf,
istype-int,
int_formula_prop_and_lemma,
int_formula_prop_not_lemma,
int_formula_prop_le_lemma,
int_term_value_constant_lemma,
int_term_value_var_lemma,
int_formula_prop_wf,
decidable__lt,
length_wf,
intformless_wf,
int_formula_prop_less_lemma,
int_seg_wf,
dlo_eq_wf,
bool_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
lambdaFormation_alt,
applyEquality,
introduction,
extract_by_obid,
hypothesis,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
universeIsType,
independent_pairFormation,
isectElimination,
productElimination,
independent_pairEquality,
isect_memberEquality_alt,
voidElimination,
because_Cache,
sqequalRule,
setElimination,
rename,
independent_isectElimination,
imageElimination,
natural_numberEquality,
unionElimination,
approximateComputation,
independent_functionElimination,
dependent_pairFormation_alt,
lambdaEquality_alt,
int_eqEquality,
equalityIstype
Latex:
((\mforall{}a:Prop. (localT prop(a) \mmember{} Prop List)) \mwedge{} (\mforall{}n:node. (fst(n) \mmember{} Prop List)))
\mwedge{} (\mforall{}n:node. (\mforall{}f\mmember{}fst(n).f \mmember{} Prop))
\mwedge{} (\mforall{}n:node. (\mforall{}f1\mmember{}fst(n).(\mforall{}f\mmember{}localT prop(f1).f \mmember{} Prop)))
\mwedge{} (\mforall{}n:node. (\mforall{}f\mmember{}fst(n).(\mforall{}f1\mmember{}localT prop(f).(\mexists{}f1'\mmember{}fst(n). dlo\_eq(prop(f1);prop(f1')) \mmember{} \mBbbB{}))))
Date html generated:
2020_05_20-AM-09_02_13
Last ObjectModification:
2019_11_27-PM-02_31_18
Theory : dynamic!logic
Home
Index