Changeset 3527
 Timestamp:
 Mar 12, 2015, 12:43:17 PM (5 years ago)
 Location:
 LTS
 Files:

 1 added
 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Language.ma
r3525 r3527 1206 1206 1207 1207 include "../src/common/Errors.ma". 1208 include "Permutation.ma". 1209 1210 (* 1208 1211 1209 1212 axiom is_permutation: ∀A.list A → list A → Prop. … … 1211 1214 axiom is_permutation_cons : ∀A.∀l1,l2,x.is_permutation A l1 l2 → 1212 1215 is_permutation A (x :: l1) (x :: l2). 1213 1216 *) 1214 1217 (* 1215 1218 inductive is_permutation (A : Type[0]) : list A → list A → Prop ≝ … … 1678 1681 #S #st1 #st2 #st3 #t1 elim t1 normalize // 1679 1682 qed. 1680 1683 (* 1681 1684 axiom permute_ok : ∀A.∀l1,l2,l3,l4,l5,l6,l7,l8,l9,x,y. 1682 1685 (is_permutation A ((l5 @l1) @l6@l7) ((l4 @[]) @l6@l7) … … 1685 1688 (y ::((l6 @((x ::l5) @(l1 @l2))) @l7)) 1686 1689 (((x ::l4 @y ::l3) @l8) @l9)). 1687 1690 *) 1688 1691 lemma append_premeasurable : ∀S : abstract_status. 1689 1692 ∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.∀t2: raw_trace … st2 st3.
Note: See TracChangeset
for help on using the changeset viewer.