 Ariadne Devos
|
132a718fd6
Define the conatural numbers, coinductively
|
5 年之前 |
|
Ariadne Devos
|
b93471c1ea
Define and proof mapping traces
|
5 年之前 |
|
Ariadne Devos
|
5c69863ade
Define is-a-partition-of for traces
|
5 年之前 |
|
Ariadne Devos
|
11ae667c8e
Proof induction lemma on traces
|
5 年之前 |
|
Ariadne Devos
|
f32fa0fb1f
Specify the conatural numbers, with some addition and ordering
|
5 年之前 |
|
Ariadne Devos
|
fcfb1f0fe1
Specify and prove basic properties about unions of languages
|
5 年之前 |
|
Ariadne Devos
|
9800d1ca59
Specify distributive lattices and their dual
|
5 年之前 |
|
Ariadne Devos
|
6a57a868f9
Specify bounded lattices
|
5 年之前 |
|
Ariadne Devos
|
8ec2cc55d0
Specify concatenation of and single-word languages
|
5 年之前 |
|
Ariadne Devos
|
0321f07fb7
Make use of the equality axiom
|
5 年之前 |
|
Ariadne Devos
|
3a263bf307
Admit an equality axiom for traces
|
5 年之前 |
|
Ariadne Devos
|
7618567a2b
Proof equivalence criterium for equivalence sets
|
5 年之前 |
|
Ariadne Devos
|
ba87fa1893
Prove some morphisms in EquivalenceSets
|
5 年之前 |
|
Ariadne Devos
|
2e3c718cfb
Define equivalence sets
|
5 年之前 |
|
Ariadne Devos
|
9a0a81aab3
Allow constant strings in languages
|
5 年之前 |
|
Ariadne Devos
|
ab5e35276f
Isolate language equivalency
|
5 年之前 |
|
Ariadne Devos
|
d1739a60b2
Make Trace generic in equivalence relation
|
5 年之前 |
|
Ariadne Devos
|
dd6e520253
Define equivalence of formal languages
|
5 年之前 |
|
Ariadne Devos
|
81ac4bfb7e
Concatenate traces
|
5 年之前 |
|
Ariadne Devos
|
26afa068f0
Define coinductive lists with equality
|
5 年之前 |
|
Ariadne Devos
|
28eee2a910
Formulate a queue of work in verification
|
5 年之前 |
|
Ariadne Devos
|
9d6c8f2707
Replace decimal parsing interface and implementation
|
5 年之前 |
|
Ariadne Devos
|
59e884fdc9
Specialise sHT_X_to_u32 for decimal
|
5 年之前 |
|
Ariadne Devos
|
04cc3ff056
State positivity of decimal etc. numbers
|
5 年之前 |
|
Ariadne Devos
|
18876acd63
State bounds on decimal_val etc.
|
5 年之前 |
|
Ariadne Devos
|
a93c558d1c
Generalise sHT_X_to_u32's overflow criterium to other bases
|
5 年之前 |
|
Ariadne Devos
|
df2fb42ed1
State positivity of signless positional representations
|
5 年之前 |
|
Ariadne Devos
|
dc530728da
Correct license of <lex/nat-uphex.c>
|
5 年之前 |
|
Ariadne Devos
|
d7af289127
Add missing mathematical definitions
|
5 年之前 |
|
Ariadne Devos
|
cad4f3bcc6
Abstract sHT_uphex_to_u32 over bases
|
5 年之前 |
