Nuprl Lemma : mFOLRule_ind_wf_simple
∀[A:Type]. ∀[v:mFOLRule()]. ∀[andI,impI:A]. ∀[allI,existsI:var:ℤ ─→ A]. ∀[orI:left:𝔹 ─→ A]. ∀[hyp:A].
∀[andE,orE,impE:hypnum:ℕ ─→ A]. ∀[allE,existsE:hypnum:ℕ ─→ var:ℤ ─→ A].
(mFOLRule_ind(v;
andI;
impI;
var.allI[var];
var.existsI[var];
left.orI[left];
hyp;hypnum.andE[hypnum];
hypnum.orE[hypnum];
hypnum.impE[hypnum];
hypnum,var.allE[hypnum;var];
hypnum,var.existsE[hypnum;var]) ∈ A)
Proof
Definitions occuring in Statement :
mFOLRule_ind: mFOLRule_ind,
mFOLRule: mFOLRule(),
nat: ℕ,
bool: 𝔹,
uall: ∀[x:A]. B[x],
so_apply: x[s1;s2],
so_apply: x[s],
member: t ∈ T,
function: x:A ─→ B[x],
int: ℤ,
universe: Type
Lemmas :
mFOLRule_ind_wf,
true_wf,
mFOLRule_wf,
subtype_rel_dep_function,
nat_wf,
bool_wf
\mforall{}[A:Type]. \mforall{}[v:mFOLRule()]. \mforall{}[andI,impI:A]. \mforall{}[allI,existsI:var:\mBbbZ{} {}\mrightarrow{} A]. \mforall{}[orI:left:\mBbbB{} {}\mrightarrow{} A].
\mforall{}[hyp:A]. \mforall{}[andE,orE,impE:hypnum:\mBbbN{} {}\mrightarrow{} A]. \mforall{}[allE,existsE:hypnum:\mBbbN{} {}\mrightarrow{} var:\mBbbZ{} {}\mrightarrow{} A].
(mFOLRule\_ind(v;
andI;
impI;
var.allI[var];
var.existsI[var];
left.orI[left];
hyp;hypnum.andE[hypnum];
hypnum.orE[hypnum];
hypnum.impE[hypnum];
hypnum,var.allE[hypnum;var];
hypnum,var.existsE[hypnum;var]) \mmember{} A)
Date html generated:
2015_07_17-AM-07_56_20
Last ObjectModification:
2015_01_27-AM-10_05_28
Home
Index