Nuprl Lemma : gammaFIM

g,h:

List

.
(spr(g)

(

a:

List. (((g a) = 0)

((g (a @ [h a])) = 0)))

(

l:

List. (((g l) = 0)

(l = gammaFIM(l;g;h)))))

Proof

Definitions occuring in Statement : gammaFIM: gammaFIM(a;g;h), append: as @ bs, nat:

, all:

x:A. B[x], implies: P

Q, apply: f a, function: x:A

B[x], natural_number: $n, equal: s = t
Definitions : all:

x:A. B[x], nat:

, implies: P

Q, gammaFIM: gammaFIM(a;g;h), member: t

T, prop:

, le: A

B, not:

A, false: False, so_lambda:

x.t[x], ifthenelse: if b then t else f fi , btrue: tt, bfalse: ff, exists:

x:A. B[x], and: P

Q, rev_implies: P

Q, iff: P

Q, uall:

[x:A]. B[x], so_apply: x[s], bool:

, unit: Unit, uimplies: b supposing a, assert:

b, uiff: uiff(P;Q), bnot:

b, or: P

Q, sq_type: SQType(T), guard: {T}, it:

Lemmas : equal_wf, nat_wf, le_wf, Error :list_wf, all_wf, append_wf, Error :cons_wf, Error :nil_wf, spr_wf, Error :list_ind_reverse_wf_dependent, eq_int_wf, subtype_rel_set_simple, bool_wf, eqtt_to_assert, assert_of_eq_int, eqff_to_assert, bool_cases_sqequal, subtype_base_sq, bool_subtype_base, Error :assert-bnot, neg_assert_of_eq_int, Error :list_ind_reverse_wf, spr_down_closed, and_wf, eq_int_eq_true, btrue_wf, ifthenelse_wf
\mforall{}g,h:\mBbbN{} List {}\mrightarrow{} \mBbbN{}. (spr(g) {}\mRightarrow{} (\mforall{}a:\mBbbN{} List. (((g a) = 0) {}\mRightarrow{} ((g (a @ [h a])) = 0))) {}\mRightarrow{} (\mforall{}l:\mBbbN{} List. (((g l) = 0) {}\mRightarrow{} (l = gammaFIM(l;g;h))))) Date html generated: 2013_03_20-AM-10_32_58 Last ObjectModification: 2013_03_08-PM-10_39_33 Home Index