Ignore:
Timestamp:
Dec 3, 2010, 4:47:03 PM (9 years ago)
Author:
mulligan
Message:

Most of critical lemma done. Hole remaining that I can't coax matita into solving.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Vector.ma

    r368 r370  
    415415(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    416416
     417ndefinition mem ≝
     418 λA: Type[0].
     419 λeq_a : A → A → Bool.
     420 λn: Nat.
     421 λl: Vector A n.
     422 λx: A.
     423  fold_right … (λy,v. inclusive_disjunction (eq_a x y) v) false l.
     424
    417425ndefinition subvector_with ≝
    418426  λA: Type[0].
     
    422430  λv: Vector A n.
    423431  λq: Vector A m.
    424     fold_right ? ? ? (λx, v. conjunction v (fold_right ? ? ? (λy, z. inclusive_disjunction z (f x y)) false q)) true v.
     432    fold_right ? ? ? (λx, v. conjunction (mem ? f ? q x) v) true v.
    425433   
    426434(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset for help on using the changeset viewer.