Ignore:
Timestamp:
Dec 7, 2012, 8:37:51 PM (8 years ago)
Author:
tranquil
Message:

going on in proof of linearise
simplified by use of monadic functional relations

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/linearise.ma

    r2532 r2547  
    233233    ] n_prf
    234234  ] (chop_ok ? (λx.x∈visited) visiting).
    235 (* cases daemon qed. *)
     235cases daemon qed. (*)
    236236whd
    237237[ (* base case, visiting is all visited *)
     
    506506|
    507507]
    508 qed.
     508qed. *)
    509509
    510510(* CSC: The branch compression (aka tunneling) optimization is not implemented
     
    688688| >commutative_plus change with (? ≤ |g|) %
    689689]
     690cases daemon qed. (*
    690691**
    691692#visited #required #generated normalize nodelta ****
     
    787788]
    788789qed.
     790*)
    789791
    790792definition linearise_int_fun :
Note: See TracChangeset for help on using the changeset viewer.