https://github.com/BapMel/4CT-coq-v1.0
Tip revision: 5ef6fd8271f5affb848589956d6e1aad2df3ea72 authored by Georges Gonthier on 23 February 2005, 09:16:00 UTC
Coq proof of the Four Color Theorem, version 1.0 (Coq v7.3.1)
Coq proof of the Four Color Theorem, version 1.0 (Coq v7.3.1)
Tip revision: 5ef6fd8
| File | Mode | Size |
|---|---|---|
| .github | ||
| .swhap | ||
| Make | -rw-r--r-- | 49 bytes |
| Makefile | -rw-r--r-- | 4.0 KB |
| README.md | -rw-r--r-- | 329 bytes |
| approx.v | -rw-r--r-- | 22.3 KB |
| birkhoff.v | -rw-r--r-- | 35.0 KB |
| boolprop.v | -rw-r--r-- | 27.7 KB |
| cfcolor.v | -rw-r--r-- | 32.5 KB |
| cfcontract.v | -rw-r--r-- | 69.5 KB |
| cfmap.v | -rw-r--r-- | 70.1 KB |
| cfquiz.v | -rw-r--r-- | 43.5 KB |
| cfreducible.v | -rw-r--r-- | 3.9 KB |
| chromogram.v | -rw-r--r-- | 9.9 KB |
| color.v | -rw-r--r-- | 18.3 KB |
| coloring.v | -rw-r--r-- | 24.2 KB |
| combinatorial4ct.v | -rw-r--r-- | 1.1 KB |
| configurations.v | -rw-r--r-- | 80.6 KB |
| connect.v | -rw-r--r-- | 27.1 KB |
| contract.v | -rw-r--r-- | 27.4 KB |
| ctree.v | -rw-r--r-- | 22.0 KB |
| ctreerestrict.v | -rw-r--r-- | 17.0 KB |
| cube.v | -rw-r--r-- | 8.6 KB |
| dataset.v | -rw-r--r-- | 12.6 KB |
| dbhub.v | -rw-r--r-- | 5.4 KB |
| dedekind.v | -rw-r--r-- | 35.1 KB |
| discharge.v | -rw-r--r-- | 14.2 KB |
| discretize.v | -rw-r--r-- | 35.4 KB |
| dyck.v | -rw-r--r-- | 1.4 KB |
| embed.v | -rw-r--r-- | 84.9 KB |
| eula.txt | -rw-r--r-- | 5.9 KB |
| file guide.htm | -rw-r--r-- | 56.4 KB |
| finitize.v | -rw-r--r-- | 27.2 KB |
| finset.v | -rw-r--r-- | 24.4 KB |
| fourcolor.v | -rw-r--r-- | 662 bytes |
| frac.v | -rw-r--r-- | 14.6 KB |
| funs.v | -rw-r--r-- | 5.9 KB |
| geometry.v | -rw-r--r-- | 30.6 KB |
| grid.v | -rw-r--r-- | 25.0 KB |
| gridmap.v | -rw-r--r-- | 50.9 KB |
| gtree.v | -rw-r--r-- | 14.3 KB |
| gtreerestrict.v | -rw-r--r-- | 13.5 KB |
| hubcap.v | -rw-r--r-- | 22.5 KB |
| hypermap.v | -rw-r--r-- | 16.9 KB |
| initctree.v | -rw-r--r-- | 10.7 KB |
| initgtree.v | -rw-r--r-- | 5.8 KB |
| job001to106.v | -rw-r--r-- | 288 bytes |
| job107to164.v | -rw-r--r-- | 290 bytes |
| job165to189.v | -rw-r--r-- | 290 bytes |
| job190to206.v | -rw-r--r-- | 290 bytes |
| job207to214.v | -rw-r--r-- | 290 bytes |
| job215to218.v | -rw-r--r-- | 290 bytes |
| job219to222.v | -rw-r--r-- | 290 bytes |
| job223to226.v | -rw-r--r-- | 290 bytes |
| job227to230.v | -rw-r--r-- | 290 bytes |
| job231to234.v | -rw-r--r-- | 290 bytes |
| job235to238.v | -rw-r--r-- | 290 bytes |
| job239to253.v | -rw-r--r-- | 290 bytes |
| job254to270.v | -rw-r--r-- | 290 bytes |
| job271to278.v | -rw-r--r-- | 290 bytes |
| job279to282.v | -rw-r--r-- | 290 bytes |
| job283to286.v | -rw-r--r-- | 290 bytes |
| job287to290.v | -rw-r--r-- | 290 bytes |
| job291to294.v | -rw-r--r-- | 290 bytes |
| job295to298.v | -rw-r--r-- | 290 bytes |
| job299to302.v | -rw-r--r-- | 290 bytes |
| job303to306.v | -rw-r--r-- | 290 bytes |
| job307to310.v | -rw-r--r-- | 290 bytes |
| job311to314.v | -rw-r--r-- | 290 bytes |
| job315to318.v | -rw-r--r-- | 290 bytes |
| job319to322.v | -rw-r--r-- | 290 bytes |
| job323to383.v | -rw-r--r-- | 290 bytes |
| job384to398.v | -rw-r--r-- | 290 bytes |
| job399to438.v | -rw-r--r-- | 290 bytes |
| job439to465.v | -rw-r--r-- | 290 bytes |
| job466to485.v | -rw-r--r-- | 290 bytes |
| job486to489.v | -rw-r--r-- | 290 bytes |
| job490to494.v | -rw-r--r-- | 290 bytes |
| job495to498.v | -rw-r--r-- | 290 bytes |
| job499to502.v | -rw-r--r-- | 290 bytes |
| job503to506.v | -rw-r--r-- | 290 bytes |
| job507to510.v | -rw-r--r-- | 290 bytes |
| job511to516.v | -rw-r--r-- | 290 bytes |
| job517to530.v | -rw-r--r-- | 290 bytes |
| job531to534.v | -rw-r--r-- | 290 bytes |
| job535to541.v | -rw-r--r-- | 290 bytes |
| job542to545.v | -rw-r--r-- | 290 bytes |
| job546to549.v | -rw-r--r-- | 290 bytes |
| job550to553.v | -rw-r--r-- | 290 bytes |
| job554to562.v | -rw-r--r-- | 290 bytes |
| job563to588.v | -rw-r--r-- | 290 bytes |
| job589to610.v | -rw-r--r-- | 290 bytes |
| job611to617.v | -rw-r--r-- | 290 bytes |
| job618to622.v | -rw-r--r-- | 290 bytes |
| job623to633.v | -rw-r--r-- | 290 bytes |
| jordan.v | -rw-r--r-- | 22.4 KB |
| kempe.v | -rw-r--r-- | 23.4 KB |
| kempetree.v | -rw-r--r-- | 23.8 KB |
| matte.v | -rw-r--r-- | 40.7 KB |
| natprop.v | -rw-r--r-- | 18.0 KB |
| part.v | -rw-r--r-- | 54.3 KB |
| patch.v | -rw-r--r-- | 35.5 KB |
| paths.v | -rw-r--r-- | 27.6 KB |
| present.v | -rw-r--r-- | 9.3 KB |
| present10.v | -rw-r--r-- | 51.5 KB |
| present11.v | -rw-r--r-- | 16.6 KB |
| present5.v | -rw-r--r-- | 1.8 KB |
| present6.v | -rw-r--r-- | 23.4 KB |
| present7.v | -rw-r--r-- | 291.9 KB |
| present8.v | -rw-r--r-- | 262.2 KB |
| present9.v | -rw-r--r-- | 175.9 KB |
| quiz.v | -rw-r--r-- | 24.3 KB |
| quiztree.v | -rw-r--r-- | 15.0 KB |
| real.v | -rw-r--r-- | 6.3 KB |
| realcategorical.v | -rw-r--r-- | 24.7 KB |
| realmap.v | -rw-r--r-- | 3.5 KB |
| realprop.v | -rw-r--r-- | 41.9 KB |
| realsyntax.v | -rw-r--r-- | 11.7 KB |
| redpart.v | -rw-r--r-- | 51.6 KB |
| reducibility.v | -rw-r--r-- | 670 bytes |
| revsnip.v | -rw-r--r-- | 25.9 KB |
| rjordan.v | -rw-r--r-- | 30.5 KB |
| seq.v | -rw-r--r-- | 57.8 KB |
| sew.v | -rw-r--r-- | 10.0 KB |
| snip.v | -rw-r--r-- | 21.1 KB |
| tacticext.v | -rw-r--r-- | 79.5 KB |
| task001to214.v | -rw-r--r-- | 458 bytes |
| task215to234.v | -rw-r--r-- | 460 bytes |
| task235to282.v | -rw-r--r-- | 460 bytes |
| task283to302.v | -rw-r--r-- | 460 bytes |
| task303to322.v | -rw-r--r-- | 460 bytes |
| task323to485.v | -rw-r--r-- | 460 bytes |
| task486to506.v | -rw-r--r-- | 460 bytes |
| task507to541.v | -rw-r--r-- | 460 bytes |
| task542to588.v | -rw-r--r-- | 460 bytes |
| task589to633.v | -rw-r--r-- | 426 bytes |
| unavoidability.v | -rw-r--r-- | 1.4 KB |
| walkup.v | -rw-r--r-- | 43.0 KB |
| znat.v | -rw-r--r-- | 21.7 KB |
README.md
Loading README.md ...
