proposition: Lemma partialApplyWeave : forall {R : ConstructiveReals} (X : Set) (fn gn : nat -> @PartialFunction R X) (n : nat) (x : X) (xH : Domain (fn (n/2)%nat) x) (y : Domain (gn (n/2)%nat) x) (z : Domain (weaveSequences (PartialFunction X) fn gn n) x), partialApply (weaveSequences (PartialFunction X) fn gn n) x z == if Nat.even n then partialApply (fn (n/2)%nat) x xH else partialApply (gn (n/2)%nat) x y.
proof: Proof. intros. unfold weaveSequences. unfold weaveSequences in z. unfold weaveSequences in xH. destruct (Nat.even n); apply DomainProp. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase