Ignore:
Timestamp:
Dec 2, 2010, 6:27:52 PM (9 years ago)
Author:
mulligan
Message:

All 450 proof obligations closed.

File:
1 edited

Legend:

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

    r364 r368  
    422422  λv: Vector A n.
    423423  λq: Vector A m.
    424     let list_q ≝ list_of_vector A m q in
    425     let list_v ≝ list_of_vector A n v in
    426     let power ≝ power_list A list_q in
    427       member_with ? list_v (λx, y. eq_l ? f x y) power.
     424    fold_right ? ? ? (λx, v. conjunction v (fold_right ? ? ? (λy, z. inclusive_disjunction z (f x y)) false q)) true v.
    428425   
    429426(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset for help on using the changeset viewer.