Nuprl Lemma : lg-all_functionality

{

[T:Type]

G:LabeledDAG(T)

[P1,P2:T

].
((

x:T. (P1[x]

P2[x]))

{

x

G.P1[x]

x

G.P2[x]}) }

{ Proof }

Definitions occuring in Statement : lg-all:

x

G.P[x], ldag: LabeledDAG(T), uall:

[x:A]. B[x], prop:

, guard: {T}, so_apply: x[s], all:

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

Q, function: x:A

B[x], universe: Type
Definitions : uall:

[x:A]. B[x], all:

x:A. B[x], prop:

, implies: P

Q, so_apply: x[s], guard: {T}, lg-all:

x

G.P[x], member: t

T, so_lambda:

x.t[x], ldag: LabeledDAG(T), nat:

Lemmas : int_seg_wf, lg-size_wf, nat_wf, lg-all_wf, ldag_wf, lg-label_wf_dag, is-dag_wf

\mforall{}[T:Type] \mforall{}G:LabeledDAG(T). \mforall{}[P1,P2:T {}\mrightarrow{} \mBbbP{}]. ((\mforall{}x:T. (P1[x] {}\mRightarrow{} P2[x])) {}\mRightarrow{} \{\mforall{}x\mmember{}G.P1[x] {}\mRightarrow{} \mforall{}x\mmember{}G.P2[x]\}) Date html generated: 2011_08_16-PM-06_45_30 Last ObjectModification: 2011_06_18-AM-10_57_34 Home Index