API tools faq
paste
Advertisement
Guest User

Untitled

a guest
Jul 16th, 2013
847
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 16.07 KB | None | 0 0
raw download clone embed print report
  1. Require Import Coq.Arith.Arith.
  2. Require Import Coq.Logic.ProofIrrelevance.
  3. Require Import Omega.
  4.  
  5. Inductive game : Set :=
  6. | gameCons : gamelist -> gamelist -> game
  7. with gamelist : Set :=
  8. | emptylist : gamelist
  9. | listCons : game -> gamelist -> gamelist.
  10.  
  11. Fixpoint measGame (g1 : game) : nat :=
  12. match g1 with
  13. | gameCons gl1 gl2 => S (measGameList gl1 + measGameList gl2)
  14. end
  15. with measGameList (gl1 : gamelist) : nat :=
  16. match gl1 with
  17. | emptylist => 0
  18. | listCons g1 gl2 => S (measGame g1 + measGameList gl2)
  19. end.
  20.  
  21. Definition side :=
  22. game -> gamelist.
  23.  
  24. Definition leftSide (g : game) : gamelist :=
  25. match g with
  26. | gameCons gll glr => gll
  27. end.
  28.  
  29. Definition rightSide (g : game) : gamelist :=
  30. match g with
  31. | gameCons gll glr => glr
  32. end.
  33.  
  34. Inductive compare_quest : Set :=
  35. | lessOrEq : compare_quest
  36. | greatOrEq : compare_quest
  37. | lessOrConf : compare_quest
  38. | greatOrConf : compare_quest.
  39.  
  40. Definition g1side (c : compare_quest) : side :=
  41. match c with
  42. | lessOrEq => leftSide
  43. | greatOrEq => rightSide
  44. | lessOrConf => rightSide
  45. | greatOrConf => leftSide
  46. end.
  47.  
  48. Definition g2side (c : compare_quest) : side :=
  49. match c with
  50. | lessOrEq => rightSide
  51. | greatOrEq => leftSide
  52. | lessOrConf => leftSide
  53. | greatOrConf => rightSide
  54. end.
  55.  
  56. Definition combiner :=
  57. Prop -> Prop -> Prop.
  58.  
  59. Definition compareCombiner (c : compare_quest) : combiner :=
  60. match c with
  61. | lessOrEq => and
  62. | greatOrEq => and
  63. | lessOrConf => or
  64. | greatOrConf => or
  65. end.
  66.  
  67. Definition nextCompare (c : compare_quest) : compare_quest :=
  68. match c with
  69. | lessOrEq => lessOrConf
  70. | greatOrEq => greatOrConf
  71. | lessOrConf => lessOrEq
  72. | greatOrConf => greatOrEq
  73. end.
  74.  
  75. Definition cbn_init (cbn : combiner) : Prop :=
  76. ~ (cbn False True).
  77.  
  78. Inductive gameCompareDom : compare_quest -> game -> game -> Prop :=
  79. | gameCompareDom1 : forall c g1 g2, innerGCompareDom (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2) -> gameCompareDom c g1 g2
  80.  
  81. with innerGCompareDom : compare_quest -> combiner -> game -> gamelist -> game -> gamelist -> Prop :=
  82. | innerGCompareDom1 : forall next_c cbn g1 g1s g2 g2s, listGameCompareDom next_c cbn g1s g2 -> gameListCompareDom next_c cbn g1 g2s -> innerGCompareDom next_c cbn g1 g1s g2 g2s
  83.  
  84. with listGameCompareDom : compare_quest -> combiner -> gamelist -> game -> Prop :=
  85. | listGameCompareDom1 : forall c cbn g1s g2, g1s = emptylist -> listGameCompareDom c cbn g1s g2
  86. | listGameCompareDom2 : forall c cbn g1s g2 g1s_car g1s_cdr, g1s = listCons g1s_car g1s_cdr -> gameCompareDom c g1s_car g2 -> listGameCompareDom c cbn g1s_cdr g2 -> listGameCompareDom c cbn g1s g2
  87.  
  88. with gameListCompareDom : compare_quest -> combiner -> game -> gamelist -> Prop :=
  89. | gameListCompareDom1 : forall c cbn g1 g2s, g2s = emptylist -> gameListCompareDom c cbn g1 g2s
  90. | gameListCompareDom2 : forall c cbn g1 g2s g2s_car g2s_cdr, g2s = listCons g2s_car g2s_cdr -> gameCompareDom c g1 g2s_car -> gameListCompareDom c cbn g1 g2s_cdr -> gameListCompareDom c cbn g1 g2s.
  91.  
  92. Lemma gameCompareDom1Inv : forall c g1 g2, gameCompareDom c g1 g2 -> innerGCompareDom (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2).
  93. Proof.
  94. intros. inversion H. apply H0.
  95. Defined.
  96.  
  97. Lemma innerGCompareDom1Inv1 : forall next_c cbn g1 g1s g2 g2s, innerGCompareDom next_c cbn g1 g1s g2 g2s -> listGameCompareDom next_c cbn g1s g2.
  98. Proof.
  99. intros. inversion H. apply H0.
  100. Defined.
  101.  
  102. Lemma innerGCompareDom1Inv2 : forall next_c cbn g1 g1s g2 g2s, innerGCompareDom next_c cbn g1 g1s g2 g2s -> gameListCompareDom next_c cbn g1 g2s.
  103. Proof.
  104. intros. inversion H. apply H1.
  105. Defined.
  106.  
  107. Lemma listGameCompareDom2Inv1 : forall c cbn g1s g2 g1s_car g1s_cdr, listGameCompareDom c cbn g1s g2 -> g1s = listCons g1s_car g1s_cdr -> gameCompareDom c g1s_car g2.
  108. Proof.
  109. intros. subst. inversion H.
  110. inversion H0.
  111. inversion H0. apply H1.
  112. Defined.
  113.  
  114. Lemma listGameCompareDom2Inv2 : forall c cbn g1s g2 g1s_car g1s_cdr, listGameCompareDom c cbn g1s g2 -> g1s = listCons g1s_car g1s_cdr -> listGameCompareDom c cbn g1s_cdr g2.
  115. Proof.
  116. intros. subst. inversion H.
  117. inversion H0.
  118. inversion H0. apply H2.
  119. Defined.
  120.  
  121. Lemma gameListCompareDom2Inv1 : forall c cbn g1 g2s g2s_car g2s_cdr, gameListCompareDom c cbn g1 g2s -> g2s = listCons g2s_car g2s_cdr -> gameCompareDom c g1 g2s_car.
  122. Proof.
  123. intros. subst. inversion H.
  124. inversion H0.
  125. inversion H0. apply H1.
  126. Defined.
  127.  
  128. Lemma gameListCompareDom2Inv2 : forall c cbn g1 g2s g2s_car g2s_cdr, gameListCompareDom c cbn g1 g2s -> g2s = listCons g2s_car g2s_cdr -> gameListCompareDom c cbn g1 g2s_cdr.
  129. Proof.
  130. intros. subst. inversion H.
  131. inversion H0.
  132. inversion H0. apply H2.
  133. Defined.
  134.  
  135. Fixpoint gameCompareAux (c : compare_quest) (g1 : game) (g2 : game) (H1 : gameCompareDom c g1 g2) : Prop :=
  136. innerGCompareAux (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2) (gameCompareDom1Inv _ _ _ H1)
  137.  
  138. with innerGCompareAux (next_c : compare_quest) (cbn : combiner) (g1 : game) (g1s : gamelist) (g2 : game) (g2s : gamelist) (H1 : innerGCompareDom next_c cbn g1 g1s g2 g2s) : Prop :=
  139. cbn (listGameCompareAux next_c cbn g1s g2 (innerGCompareDom1Inv1 _ _ _ _ _ _ H1)) (gameListCompareAux next_c cbn g1 g2s (innerGCompareDom1Inv2 _ _ _ _ _ _ H1))
  140.  
  141. with listGameCompareAux (c : compare_quest) (cbn : combiner) (g1s : gamelist) (g2 : game) (H1 : listGameCompareDom c cbn g1s g2) : Prop :=
  142. match g1s as gl1 return g1s = gl1 -> Prop with
  143. | emptylist => fun H2 => cbn_init cbn
  144. | listCons g1s_car g1s_cdr => fun H2 => cbn (gameCompareAux c g1s_car g2 (listGameCompareDom2Inv1 _ _ _ _ _ _ H1 H2)) (listGameCompareAux c cbn g1s_cdr g2 (listGameCompareDom2Inv2 _ _ _ _ _ _ H1 H2))
  145. end eq_refl
  146.  
  147. with gameListCompareAux (c : compare_quest) (cbn : combiner) (g1 : game) (g2s : gamelist) (H1 : gameListCompareDom c cbn g1 g2s) : Prop :=
  148. match g2s as gl1 return g2s = gl1 -> Prop with
  149. | emptylist => fun H2 => cbn_init cbn
  150. | listCons g2s_car g2s_cdr => fun H2 => cbn (gameCompareAux c g1 g2s_car (gameListCompareDom2Inv1 _ _ _ _ _ _ H1 H2)) (gameListCompareAux c cbn g1 g2s_cdr (gameListCompareDom2Inv2 _ _ _ _ _ _ H1 H2))
  151. end eq_refl.
  152.  
  153. Lemma Triv1 : forall n1 n2 n3 n4 n5 n6, n1 + n2 + n3 + n6 < n1 + n2 + S (S (n3 + n4 + n5)) + n6.
  154. Proof. intros. omega. Qed.
  155.  
  156. Lemma Triv2 : forall n1 n2 n3 n4 n5 n6, n1 + n2 + n4 + n6 < n1 + n2 + S (S (n3 + n4 + n5)) + n6.
  157. Proof. intros. omega. Qed.
  158.  
  159. Lemma Triv3 : forall n1 n2 n3 n4 n5 n6, n1 + n2 + n3 + n4 < n2 + S (n5 + n4) + S (n1 + n6) + n3.
  160. Proof. intros. omega. Qed.
  161.  
  162. Lemma Triv4 : forall n1 n2 n3 n4 n5 n6, n1 + n2 + n3 + n4 < n2 + S (n4 + n5) + S (n1 + n3) + n6.
  163. Proof. intros. omega. Qed.
  164.  
  165. Lemma Triv5 : forall n1 n2 n3 n4 n5, n1 + n2 + n3 + n4 < n1 + n2 + S (n5 + n3) + n4.
  166. Proof. intros. omega. Qed.
  167.  
  168. Lemma Triv6 : forall n1 n2 n3 n4 n5 n6, n1 + n2 + n3 + n4 < S (n3 + n5 + n1 + n6 + S (n2 + n4)).
  169. Proof. intros. omega. Qed.
  170.  
  171. Lemma Triv7 : forall n1 n2 n3 n4 n5 n6, n1 + n2 + n3 + n4 < S (n5 + n3 + n1 + n6 + S (n2 + n4)).
  172. Proof. intros. omega. Qed.
  173.  
  174. Lemma Triv8 : forall n1 n2 n3 n4 n5 n6, n1 + n2 + n3 + n4 < n1 + n2 + n3 + S (S (n5 + n4 + n6)).
  175. Proof. intros. omega. Qed.
  176.  
  177. Lemma Triv9 : forall n1 n2 n3 n4 n5 n6, n1 + n2 + n3 + n4 < n1 + n2 + n3 + S (S (n4 + n5 + n6)).
  178. Proof. intros. omega. Qed.
  179.  
  180. Lemma Triv10 : forall n1 n2 n3 n4 n5, n1 + n2 + n3 + n4 < n1 + n2 + n3 + S (n5 + n4).
  181. Proof. intros. omega. Qed.
  182.  
  183. Lemma listGameGameListCompareTot : forall g1 g2 g1s g2s,
  184. (forall c cbn, listGameCompareDom c cbn g1s g2) /\
  185. (forall c cbn, gameListCompareDom c cbn g1 g2s).
  186. Proof.
  187. intros.
  188. remember (measGame g1 + measGame g2 + measGameList g1s + measGameList g2s) as n1.
  189. revert g1 g2 g1s g2s Heqn1.
  190. induction n1 using lt_wf_ind.
  191. intros.
  192. subst.
  193. split.
  194.  
  195. intros.
  196. destruct g1s.
  197.  
  198. apply listGameCompareDom1.
  199. apply eq_refl.
  200.  
  201. eapply listGameCompareDom2.
  202.  
  203. apply eq_refl.
  204.  
  205. apply gameCompareDom1.
  206. apply innerGCompareDom1.
  207.  
  208. destruct g.
  209. destruct c.
  210.  
  211. simpl in *.
  212. assert (H2 := H (measGame g1 + measGame g2 + measGameList g + measGameList g2s) (Triv1 _ _ _ _ _ _) _ _ _ _ eq_refl).
  213. inversion H2 as [H3 H4].
  214. apply H3.
  215.  
  216. simpl in *.
  217. assert (H2 := H (measGame g1 + measGame g2 + measGameList g0 + measGameList g2s) (Triv2 _ _ _ _ _ _) _ _ _ _ eq_refl).
  218. inversion H2 as [H3 H4].
  219. apply H3.
  220.  
  221. simpl in *.
  222. assert (H2 := H (measGame g1 + measGame g2 + measGameList g0 + measGameList g2s) (Triv2 _ _ _ _ _ _) _ _ _ _ eq_refl).
  223. inversion H2 as [H3 H4].
  224. apply H3.
  225.  
  226. simpl in *.
  227. assert (H2 := H (measGame g1 + measGame g2 + measGameList g + measGameList g2s) (Triv1 _ _ _ _ _ _) _ _ _ _ eq_refl).
  228. inversion H2 as [H3 H4].
  229. apply H3.
  230.  
  231. destruct g2.
  232. destruct c.
  233.  
  234. simpl in *.
  235. assert (H2 := H (measGame g + measGame g1 + measGameList g2s + measGameList g2) (Triv3 _ _ _ _ _ _) _ _ _ _ eq_refl).
  236. inversion H2 as [H3 H4].
  237. apply H4.
  238.  
  239. simpl in *.
  240. assert (H2 := H (measGame g + measGame g1 + measGameList g1s + measGameList g0) (Triv4 _ _ _ _ _ _) _ _ _ _ eq_refl).
  241. inversion H2 as [H3 H4].
  242. apply H4.
  243.  
  244. simpl in *.
  245. assert (H2 := H (measGame g + measGame g1 + measGameList g1s + measGameList g0) (Triv4 _ _ _ _ _ _) _ _ _ _ eq_refl).
  246. inversion H2 as [H3 H4].
  247. apply H4.
  248.  
  249. simpl in *.
  250. assert (H2 := H (measGame g + measGame g1 + measGameList g2s + measGameList g2) (Triv3 _ _ _ _ _ _) _ _ _ _ eq_refl).
  251. inversion H2 as [H3 H4].
  252. apply H4.
  253.  
  254. simpl in *.
  255. assert (H2 := H (measGame g1 + measGame g2 + measGameList g1s + measGameList g2s) (Triv5 _ _ _ _ _) _ _ _ _ eq_refl).
  256. inversion H2 as [H3 H4].
  257. apply H3.
  258.  
  259. intros.
  260. destruct g2s.
  261.  
  262. apply gameListCompareDom1.
  263. apply eq_refl.
  264.  
  265. eapply gameListCompareDom2.
  266.  
  267. apply eq_refl.
  268.  
  269. apply gameCompareDom1.
  270. apply innerGCompareDom1.
  271.  
  272. destruct g1.
  273. destruct c.
  274.  
  275. simpl in *.
  276. assert (H2 := H (measGame g2 + measGame g + measGameList g0 + measGameList g2s) (Triv6 _ _ _ _ _ _) _ _ _ _ eq_refl).
  277. inversion H2 as [H3 H4].
  278. apply H3.
  279.  
  280. simpl in *.
  281. assert (H2 := H (measGame g2 + measGame g + measGameList g1 + measGameList g2s) (Triv7 _ _ _ _ _ _) _ _ _ _ eq_refl).
  282. inversion H2 as [H3 H4].
  283. apply H3.
  284.  
  285. simpl in *.
  286. assert (H2 := H (measGame g2 + measGame g + measGameList g1 + measGameList g2s) (Triv7 _ _ _ _ _ _) _ _ _ _ eq_refl).
  287. inversion H2 as [H3 H4].
  288. apply H3.
  289.  
  290. simpl in *.
  291. assert (H2 := H (measGame g2 + measGame g + measGameList g0 + measGameList g2s) (Triv6 _ _ _ _ _ _) _ _ _ _ eq_refl).
  292. inversion H2 as [H3 H4].
  293. apply H3.
  294.  
  295. destruct g.
  296. destruct c.
  297.  
  298. simpl in *.
  299. assert (H2 := H (measGame g1 + measGame g2 + measGameList g1s + measGameList g0) (Triv8 _ _ _ _ _ _) _ _ _ _ eq_refl).
  300. inversion H2 as [H3 H4].
  301. apply H4.
  302.  
  303. simpl in *.
  304. assert (H2 := H (measGame g1 + measGame g2 + measGameList g1s + measGameList g) (Triv9 _ _ _ _ _ _) _ _ _ _ eq_refl).
  305. inversion H2 as [H3 H4].
  306. apply H4.
  307.  
  308. simpl in *.
  309. assert (H2 := H (measGame g1 + measGame g2 + measGameList g1s + measGameList g) (Triv9 _ _ _ _ _ _) _ _ _ _ eq_refl).
  310. inversion H2 as [H3 H4].
  311. apply H4.
  312.  
  313. simpl in *.
  314. assert (H2 := H (measGame g1 + measGame g2 + measGameList g1s + measGameList g0) (Triv8 _ _ _ _ _ _) _ _ _ _ eq_refl).
  315. inversion H2 as [H3 H4].
  316. apply H4.
  317.  
  318. simpl in *.
  319. assert (H2 := H (measGame g1 + measGame g2 + measGameList g1s + measGameList g2s) (Triv10 _ _ _ _ _) _ _ _ _ eq_refl).
  320. inversion H2 as [H3 H4].
  321. apply H4.
  322. Qed.
  323.  
  324. Lemma listGameCompareTot : forall g2 g1s c cbn,
  325. listGameCompareDom c cbn g1s g2.
  326. Proof.
  327. intros.
  328. apply (listGameGameListCompareTot g2 g2 g1s g1s).
  329. Qed.
  330.  
  331. Lemma gameListCompareTot : forall g1 g2s c cbn,
  332. gameListCompareDom c cbn g1 g2s.
  333. Proof.
  334. intros.
  335. apply (listGameGameListCompareTot g1 g1 g2s g2s).
  336. Qed.
  337.  
  338. Lemma innerGCompareTot : forall next_c cbn g1 g1s g2 g2s,
  339. innerGCompareDom next_c cbn g1 g1s g2 g2s.
  340. Proof.
  341. intros.
  342. apply innerGCompareDom1.
  343.  
  344. apply listGameCompareTot.
  345.  
  346. apply gameListCompareTot.
  347. Qed.
  348.  
  349. Lemma gameCompareTot : forall c g1 g2, gameCompareDom c g1 g2.
  350. Proof.
  351. intros.
  352. apply gameCompareDom1.
  353. apply innerGCompareTot.
  354. Qed.
  355.  
  356. Definition gameCompare (c : compare_quest) (g1 : game) (g2 : game) : Prop :=
  357. gameCompareAux c g1 g2 (gameCompareTot _ _ _).
  358.  
  359. Definition innerGCompare (next_c : compare_quest) (cbn : combiner) (g1 : game) (g1s : gamelist) (g2 : game) (g2s : gamelist) : Prop :=
  360. innerGCompareAux next_c cbn g1 g1s g2 g2s (innerGCompareTot _ _ _ _ _ _).
  361.  
  362. Definition listGameCompare (c : compare_quest) (cbn : combiner) (g1s : gamelist) (g2 : game) : Prop :=
  363. listGameCompareAux c cbn g1s g2 (listGameCompareTot _ _ _ _).
  364.  
  365. Definition gameListCompare (c : compare_quest) (cbn : combiner) (g1 : game) (g2s : gamelist) : Prop :=
  366. gameListCompareAux c cbn g1 g2s (gameListCompareTot _ _ _ _).
  367.  
  368. Lemma gameCompareEq : forall c g1 g2, gameCompare c g1 g2 =
  369. innerGCompare (nextCompare c) (compareCombiner c) g1 (g1side c g1) g2 (g2side c g2).
  370. Proof.
  371. intros.
  372. unfold gameCompare.
  373. unfold innerGCompare.
  374. destruct (gameCompareTot c g1 g2).
  375. simpl.
  376. apply f_equal.
  377. apply proof_irrelevance.
  378. Qed.
  379.  
  380. Lemma innerGCompareEq : forall next_c cbn g1 g1s g2 g2s, innerGCompare next_c cbn g1 g1s g2 g2s =
  381. cbn (listGameCompare next_c cbn g1s g2) (gameListCompare next_c cbn g1 g2s).
  382. Proof.
  383. intros.
  384. unfold innerGCompare.
  385. unfold listGameCompare.
  386. unfold gameListCompare.
  387. destruct (innerGCompareTot next_c cbn g1 g1s g2 g2s).
  388. simpl.
  389. assert (H1 : cbn (listGameCompareAux next_c cbn g1s g2 l) = cbn (listGameCompareAux next_c cbn g1s g2 (listGameCompareTot g2 g1s next_c cbn))).
  390.  
  391. apply f_equal.
  392. apply f_equal.
  393. apply proof_irrelevance.
  394.  
  395. rewrite H1.
  396. apply f_equal.
  397. apply f_equal.
  398. apply proof_irrelevance.
  399. Qed.
  400.  
  401. Lemma listGameCompareEq : forall c cbn g1s g2, listGameCompare c cbn g1s g2 =
  402. match g1s with
  403. | emptylist => cbn_init cbn
  404. | listCons g1s_car g1s_cdr => cbn (gameCompare c g1s_car g2) (listGameCompare c cbn g1s_cdr g2)
  405. end.
  406. Proof.
  407. intros.
  408. unfold listGameCompare.
  409. unfold gameCompare.
  410. destruct (listGameCompareTot g2 g1s c cbn).
  411.  
  412. simpl.
  413. rewrite e.
  414. apply eq_refl.
  415.  
  416. simpl.
  417. rewrite e.
  418. assert (H1 : cbn (gameCompareAux c g1s_car g2 (listGameCompareDom2Inv1 c cbn (listCons g1s_car g1s_cdr) g2 g1s_car g1s_cdr (listGameCompareDom2 c cbn (listCons g1s_car g1s_cdr) g2 g1s_car g1s_cdr eq_refl g l) eq_refl)) = cbn (gameCompareAux c g1s_car g2 (gameCompareTot c g1s_car g2))).
  419.  
  420. apply f_equal.
  421. apply f_equal.
  422. apply proof_irrelevance.
  423.  
  424. rewrite H1.
  425. apply f_equal.
  426. apply f_equal.
  427. apply proof_irrelevance.
  428. Qed.
  429.  
  430. Lemma gameListCompareEq : forall c cbn g1 g2s, gameListCompare c cbn g1 g2s =
  431. match g2s with
  432. | emptylist => cbn_init cbn
  433. | listCons g2s_car g2s_cdr => cbn (gameCompare c g1 g2s_car) (gameListCompare c cbn g1 g2s_cdr)
  434. end.
  435. Proof.
  436. intros.
  437. unfold gameListCompare.
  438. unfold gameCompare.
  439. destruct (gameListCompareTot g1 g2s c cbn).
  440.  
  441. simpl.
  442. rewrite e.
  443. apply eq_refl.
  444.  
  445. simpl.
  446. rewrite e.
  447. assert (H1 : cbn (gameCompareAux c g1 g2s_car (gameListCompareDom2Inv1 c cbn g1 (listCons g2s_car g2s_cdr) g2s_car g2s_cdr (gameListCompareDom2 c cbn g1 (listCons g2s_car g2s_cdr) g2s_car g2s_cdr eq_refl g g0) eq_refl)) = cbn (gameCompareAux c g1 g2s_car (gameCompareTot c g1 g2s_car))).
  448.  
  449. apply f_equal.
  450. apply f_equal.
  451. apply proof_irrelevance.
  452.  
  453. rewrite H1.
  454. apply f_equal.
  455. apply f_equal.
  456. apply proof_irrelevance.
  457. Qed.
  458.  
  459. Definition game_eq (g1 : game) (g2 : game) : Prop :=
  460. (gameCompare lessOrEq g1 g2) /\ (gameCompare greatOrEq g1 g2).
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!