Changeset 3527 for LTS


Ignore:
Timestamp:
Mar 12, 2015, 12:43:17 PM (5 years ago)
Author:
piccolo
Message:

fixed permutation axioms

Location:
LTS
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3525 r3527  
    12061206
    12071207include "../src/common/Errors.ma".
     1208include "Permutation.ma".
     1209
     1210(*
    12081211
    12091212axiom is_permutation: ∀A.list A → list A → Prop.
     
    12111214axiom is_permutation_cons : ∀A.∀l1,l2,x.is_permutation A l1 l2 →
    12121215                                       is_permutation A (x :: l1) (x :: l2).
    1213 
     1216*)
    12141217(*
    12151218inductive is_permutation (A : Type[0]) : list A → list A → Prop ≝
     
    16781681#S #st1 #st2 #st3 #t1 elim t1 normalize //
    16791682qed.
    1680 
     1683(*
    16811684axiom permute_ok : ∀A.∀l1,l2,l3,l4,l5,l6,l7,l8,l9,x,y.
    16821685  (is_permutation A ((l5 @l1) @l6@l7) ((l4 @[]) @l6@l7)
     
    16851688   (y ::((l6 @((x ::l5) @(l1 @l2))) @l7))
    16861689   (((x ::l4 @y ::l3) @l8) @l9)).
    1687    
     1690*)   
    16881691lemma append_premeasurable : ∀S : abstract_status.
    16891692∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.∀t2: raw_trace … st2 st3.
Note: See TracChangeset for help on using the changeset viewer.