Nuprl Lemma : prefix-match_wf
∀[p1,p2:pi_prefix()]. (prefix-match(p1;p2) ∈ 𝔹)
Proof
Definitions occuring in Statement :
prefix-match: prefix-match(p1;p2),
pi_prefix: pi_prefix(),
bool: 𝔹,
uall: ∀[x:A]. B[x],
member: t ∈ T
Lemmas :
pisend?_wf,
bool_wf,
eqtt_to_assert,
pircv?_wf,
uiff_transitivity,
equal-wf-T-base,
assert_wf,
assert_of_band,
name_eq_wf,
pisend-chan_wf,
pircv-chan_wf,
iff_transitivity,
bor_wf,
bnot_wf,
or_wf,
not_wf,
iff_weakening_uiff,
bnot_thru_band,
eqff_to_assert,
assert_of_bor,
assert_of_bnot,
bfalse_wf,
pi_prefix_wf
Latex:
\mforall{}[p1,p2:pi\_prefix()]. (prefix-match(p1;p2) \mmember{} \mBbbB{})
Date html generated:
2015_07_23-AM-11_32_53
Last ObjectModification:
2015_01_29-AM-00_53_51
Home
Index