Nuprl Lemma : fpf-union-compatible-property

[T,V:Type].

eq:EqDecider(T)

[X:T

Type]

R:V List

V

(

A,B,C:t:T fp-> X[t] List.
(fpf-union-compatible(T;V;t.X[t];eq;R;A;B)

fpf-union-compatible(T;V;t.X[t];eq;R;C;A)

fpf-union-compatible(T;V;t.X[t];eq;R;C;B)

fpf-union-compatible(T;V;t.X[t];eq;R;C;fpf-union-join(eq;R;A;B)))) supposing
((

L1,L2:V List.

x:V. (

(R (L1 @ L2) x)) supposing ((

(R L2 x)) and (

(R L1 x)))) and
(

L1,L2:V List.

x:V. (L1

L2

(R L1 x) supposing

(R L2 x))))
supposing

t:T. (X[t]

r V)

Proof not projected

Error : references

\mforall{}[T,V:Type]. \mforall{}eq:EqDecider(T) \mforall{}[X:T {}\mrightarrow{} Type] \mforall{}R:V List {}\mrightarrow{} V {}\mrightarrow{} \mBbbB{} (\mforall{}A,B,C:t:T fp-> X[t] List. (fpf-union-compatible(T;V;t.X[t];eq;R;A;B) {}\mRightarrow{} fpf-union-compatible(T;V;t.X[t];eq;R;C;A) {}\mRightarrow{} fpf-union-compatible(T;V;t.X[t];eq;R;C;B) {}\mRightarrow{} fpf-union-compatible(T;V;t.X[t];eq;R;C;fpf-union-join(eq;R;A;B)))) supposing ((\mforall{}L1,L2:V List. \mforall{}x:V. (\muparrow{}(R (L1 @ L2) x)) supposing ((\muparrow{}(R L2 x)) and (\muparrow{}(R L1 x)))) and (\mforall{}L1,L2:V List. \mforall{}x:V. (L1 \msubseteq{} L2 {}\mRightarrow{} \muparrow{}(R L1 x) supposing \muparrow{}(R L2 x)))) supposing \mforall{}t:T. (X[t] \msubseteq{}r V) Date html generated: 2012_02_20-PM-07_50_41 Last ObjectModification: 2010_11_08-AM-11_35_05 Home Index