]> matita.cs.unibo.it Git - helm.git/log
helm.git
11 years agoquasi finito
Andrea Asperti [Sun, 27 Jan 2013 17:44:49 +0000 (17:44 +0000)]
quasi finito

11 years agowell-foundedness done
Wilmer Ricciotti [Sun, 27 Jan 2013 16:31:44 +0000 (16:31 +0000)]
well-foundedness done

11 years agosem_exec_move completed
Andrea Asperti [Sun, 27 Jan 2013 14:38:20 +0000 (14:38 +0000)]
sem_exec_move completed

11 years agoalmost there
Andrea Asperti [Sun, 27 Jan 2013 12:58:58 +0000 (12:58 +0000)]
almost there

11 years agoA lot of changes
Andrea Asperti [Sat, 26 Jan 2013 21:24:19 +0000 (21:24 +0000)]
A lot of changes

11 years agoSplitted unistep_aux
Andrea Asperti [Fri, 25 Jan 2013 23:18:36 +0000 (23:18 +0000)]
Splitted unistep_aux
Added another semantics for cfg_to_obj

11 years agostarted unistep
Wilmer Ricciotti [Fri, 25 Jan 2013 18:31:33 +0000 (18:31 +0000)]
started unistep

11 years agoprogress in termination
Wilmer Ricciotti [Fri, 25 Jan 2013 14:15:04 +0000 (14:15 +0000)]
progress in termination

11 years ago- paths and left residuals: forth case of the equivalence proved!
Ferruccio Guidi [Fri, 25 Jan 2013 12:12:29 +0000 (12:12 +0000)]
- paths and left residuals: forth case of the equivalence proved!
  The proof is now complete!!

11 years agofinished semantics for termination of match machine
Wilmer Ricciotti [Thu, 24 Jan 2013 15:47:47 +0000 (15:47 +0000)]
finished semantics for termination of match machine

11 years agoprogress
Wilmer Ricciotti [Thu, 24 Jan 2013 12:31:43 +0000 (12:31 +0000)]
progress

11 years agoprogress
Wilmer Ricciotti [Thu, 24 Jan 2013 09:38:30 +0000 (09:38 +0000)]
progress

11 years ago- paths and left residuals: third case of the equivalence proved!
Ferruccio Guidi [Wed, 23 Jan 2013 19:32:59 +0000 (19:32 +0000)]
- paths and left residuals: third case of the equivalence proved!

11 years agoprogress
Wilmer Ricciotti [Wed, 23 Jan 2013 07:41:41 +0000 (07:41 +0000)]
progress

11 years agotermination!
Andrea Asperti [Tue, 22 Jan 2013 14:37:41 +0000 (14:37 +0000)]
termination!

11 years agoUniversal machine
Andrea Asperti [Tue, 22 Jan 2013 12:21:58 +0000 (12:21 +0000)]
Universal machine

11 years agoRemoved all axioms in unistep_aux
Wilmer Ricciotti [Tue, 22 Jan 2013 09:57:18 +0000 (09:57 +0000)]
Removed all axioms in unistep_aux

11 years agoremoved daemons
Wilmer Ricciotti [Mon, 21 Jan 2013 15:53:26 +0000 (15:53 +0000)]
removed daemons

11 years agouniversal
Andrea Asperti [Mon, 21 Jan 2013 12:50:06 +0000 (12:50 +0000)]
universal

11 years agotape_move_obj completed (modulo daemons)
Wilmer Ricciotti [Mon, 21 Jan 2013 12:38:56 +0000 (12:38 +0000)]
tape_move_obj completed (modulo daemons)

11 years agocfg_to_obj completed (modulo daemons)
Wilmer Ricciotti [Mon, 21 Jan 2013 11:06:23 +0000 (11:06 +0000)]
cfg_to_obj completed (modulo daemons)

11 years agoprogress
Wilmer Ricciotti [Mon, 21 Jan 2013 10:01:46 +0000 (10:01 +0000)]
progress

11 years agosemantics of unistep
Andrea Asperti [Sun, 20 Jan 2013 12:31:17 +0000 (12:31 +0000)]
semantics of unistep

11 years ago- paths and left residuals: second case of the equivalence proved!
Ferruccio Guidi [Fri, 18 Jan 2013 23:27:46 +0000 (23:27 +0000)]
- paths and left residuals: second case of the equivalence proved!
- some additions to lstar and Allr

11 years agoprogress in cfg_to_obj
Wilmer Ricciotti [Fri, 18 Jan 2013 15:55:16 +0000 (15:55 +0000)]
progress in cfg_to_obj

11 years agocopy char form obj to cfg at the end
Andrea Asperti [Fri, 18 Jan 2013 12:03:48 +0000 (12:03 +0000)]
copy char form obj to cfg at the end

11 years agohigh level semantics
Andrea Asperti [Fri, 18 Jan 2013 11:41:17 +0000 (11:41 +0000)]
high level semantics

11 years agohigh level semantics
Andrea Asperti [Fri, 18 Jan 2013 11:08:33 +0000 (11:08 +0000)]
high level semantics

11 years agosemantics of uni_step
Andrea Asperti [Fri, 18 Jan 2013 10:32:00 +0000 (10:32 +0000)]
semantics of uni_step

11 years agoprogress
Wilmer Ricciotti [Thu, 17 Jan 2013 16:01:27 +0000 (16:01 +0000)]
progress

11 years agoprogress
Wilmer Ricciotti [Thu, 17 Jan 2013 15:54:07 +0000 (15:54 +0000)]
progress

11 years agoprogress
Wilmer Ricciotti [Thu, 17 Jan 2013 15:34:55 +0000 (15:34 +0000)]
progress

11 years agoprogress
Wilmer Ricciotti [Thu, 17 Jan 2013 14:47:22 +0000 (14:47 +0000)]
progress

11 years agoprogress
Wilmer Ricciotti [Thu, 17 Jan 2013 14:05:02 +0000 (14:05 +0000)]
progress

11 years agoMoved a list comparison function in the list file
Andrea Asperti [Thu, 17 Jan 2013 14:00:11 +0000 (14:00 +0000)]
Moved a list comparison function in the list file

11 years agonormal and tuples
Andrea Asperti [Thu, 17 Jan 2013 12:59:25 +0000 (12:59 +0000)]
normal and tuples

11 years ago- paths and left residuals: first case of the equivalence proved!
Ferruccio Guidi [Wed, 16 Jan 2013 19:05:56 +0000 (19:05 +0000)]
- paths and left residuals: first case of the equivalence proved!
- some corrections and additions
- some "?" removed in customized eliminations

11 years agoadded null character to the alphabet
Wilmer Ricciotti [Wed, 16 Jan 2013 16:01:54 +0000 (16:01 +0000)]
added null character to the alphabet

11 years agoprogress
Wilmer Ricciotti [Wed, 16 Jan 2013 11:02:20 +0000 (11:02 +0000)]
progress

11 years ago- some additions and renaming ...
Ferruccio Guidi [Tue, 15 Jan 2013 20:08:08 +0000 (20:08 +0000)]
- some additions and renaming ...

11 years agoprogress in unistep_aux
Wilmer Ricciotti [Tue, 15 Jan 2013 16:48:30 +0000 (16:48 +0000)]
progress in unistep_aux

11 years agounistep_aux
Wilmer Ricciotti [Tue, 15 Jan 2013 15:38:57 +0000 (15:38 +0000)]
unistep_aux

11 years agomore unistep
Wilmer Ricciotti [Tue, 15 Jan 2013 15:38:11 +0000 (15:38 +0000)]
more unistep

11 years agounistep_aux
Wilmer Ricciotti [Tue, 15 Jan 2013 12:29:35 +0000 (12:29 +0000)]
unistep_aux

11 years agocopy finished
Andrea Asperti [Tue, 15 Jan 2013 11:35:33 +0000 (11:35 +0000)]
copy finished

11 years ago- a few more lemmas ...
Ferruccio Guidi [Tue, 15 Jan 2013 10:34:32 +0000 (10:34 +0000)]
- a few more lemmas ...
- some renaming

11 years agocopy.ma
Andrea Asperti [Tue, 15 Jan 2013 09:45:58 +0000 (09:45 +0000)]
copy.ma

11 years agomatch.ma completed
Wilmer Ricciotti [Mon, 14 Jan 2013 16:45:27 +0000 (16:45 +0000)]
match.ma completed

11 years agomatch termination completed, still a small case ignored in wsem_match
Wilmer Ricciotti [Mon, 14 Jan 2013 16:24:17 +0000 (16:24 +0000)]
match termination completed, still a small case ignored in wsem_match

11 years agowsem_match finished
Wilmer Ricciotti [Mon, 14 Jan 2013 15:47:08 +0000 (15:47 +0000)]
wsem_match finished

11 years agoadvancement in match
Wilmer Ricciotti [Mon, 14 Jan 2013 15:14:11 +0000 (15:14 +0000)]
advancement in match

11 years agoClosed some daemons
Andrea Asperti [Mon, 14 Jan 2013 11:46:18 +0000 (11:46 +0000)]
Closed some daemons

11 years agonth_current_chars
Andrea Asperti [Mon, 14 Jan 2013 10:36:34 +0000 (10:36 +0000)]
nth_current_chars

11 years agostandardization: equivalence between paths and left residuals started
Ferruccio Guidi [Sun, 13 Jan 2013 19:10:32 +0000 (19:10 +0000)]
standardization: equivalence between paths and left residuals started

11 years agomatch almost finished
Wilmer Ricciotti [Fri, 11 Jan 2013 23:28:57 +0000 (23:28 +0000)]
match almost finished

11 years agomore porting to machines that can move without writing
Andrea Asperti [Tue, 8 Jan 2013 12:03:01 +0000 (12:03 +0000)]
more porting to machines that can move without writing

11 years agoparmove based on end of the tape
Wilmer Ricciotti [Tue, 8 Jan 2013 10:26:00 +0000 (10:26 +0000)]
parmove based on end of the tape

11 years agoporting to machine that can move without writing
Wilmer Ricciotti [Tue, 8 Jan 2013 09:16:34 +0000 (09:16 +0000)]
porting to machine that can move without writing

11 years agodependences update
Ferruccio Guidi [Sun, 6 Jan 2013 20:09:18 +0000 (20:09 +0000)]
dependences update

11 years agorefactoring ...
Ferruccio Guidi [Sun, 6 Jan 2013 16:17:47 +0000 (16:17 +0000)]
refactoring ...

11 years agoPorted permutation.ma and fermat_little_theorem.ma
Andrea Asperti [Sat, 5 Jan 2013 16:22:16 +0000 (16:22 +0000)]
Ported permutation.ma and fermat_little_theorem.ma

11 years agorefactoring
Andrea Asperti [Thu, 3 Jan 2013 16:49:01 +0000 (16:49 +0000)]
refactoring

11 years agoRefactoring
Andrea Asperti [Thu, 3 Jan 2013 16:33:59 +0000 (16:33 +0000)]
Refactoring

11 years agoChebishev ported
Andrea Asperti [Thu, 3 Jan 2013 16:15:54 +0000 (16:15 +0000)]
Chebishev ported

11 years agolambda: some refactoring + support for subsets of subterms started
Ferruccio Guidi [Wed, 2 Jan 2013 22:12:53 +0000 (22:12 +0000)]
lambda: some refactoring + support for subsets of subterms started
core_notation: some "term 19" added
predefined_virtuals: an addition

11 years ago- probe: new application to compute some data on the proof objects of
Ferruccio Guidi [Tue, 1 Jan 2013 23:01:20 +0000 (23:01 +0000)]
- probe: new application to compute some data on the proof objects of
a development, such as their net size (aka intrinsinc complexity)
- lambdadelta: Makefile now asks "probe" fore some data

11 years agoupdate in basic_2
Ferruccio Guidi [Sun, 30 Dec 2012 13:11:10 +0000 (13:11 +0000)]
update in basic_2

11 years agocommit completed! some bugs fixed and some instances of auto resized
Ferruccio Guidi [Sun, 30 Dec 2012 13:00:21 +0000 (13:00 +0000)]
commit completed! some bugs fixed and some instances of auto resized

11 years agoxoa: change in naming convenctions for existential quantifies
Ferruccio Guidi [Fri, 28 Dec 2012 16:32:01 +0000 (16:32 +0000)]
xoa: change in naming convenctions for existential quantifies
     to cope with ex2 in lib
lib: some additions
lambdadelta: partial commit in basic_2: just grammar, substitution,
unfold, static

11 years ago- lambda_delta: programmed renaming to lambdadelta
Ferruccio Guidi [Tue, 25 Dec 2012 21:48:14 +0000 (21:48 +0000)]
- lambda_delta: programmed renaming to lambdadelta
- nat: general weight-based eliminator added for lambdadelta

11 years ago- we introduced the pointer_step rc in the perspective of proving
Ferruccio Guidi [Sun, 23 Dec 2012 15:02:32 +0000 (15:02 +0000)]
- we introduced the pointer_step rc in the perspective of proving
results on head normal forms
- some renaming

11 years agosome renaming ...
Ferruccio Guidi [Fri, 21 Dec 2012 18:12:41 +0000 (18:12 +0000)]
some renaming ...

11 years agoone file was missing .... :(
Ferruccio Guidi [Fri, 21 Dec 2012 18:06:10 +0000 (18:06 +0000)]
one file was missing .... :(

11 years agoMany changes
Andrea Asperti [Fri, 21 Dec 2012 12:39:18 +0000 (12:39 +0000)]
Many changes

11 years agomem/append lemmas
Andrea Asperti [Fri, 21 Dec 2012 11:13:51 +0000 (11:13 +0000)]
mem/append lemmas

11 years agobertrand OK.
Andrea Asperti [Fri, 21 Dec 2012 11:10:49 +0000 (11:10 +0000)]
bertrand OK.

11 years ago- nat.ma: cut removed from f_ind :)
Ferruccio Guidi [Thu, 20 Dec 2012 14:52:58 +0000 (14:52 +0000)]
- nat.ma: cut removed from f_ind :)
- lanbda: some refactoring

11 years agoreordering and corrections
Ferruccio Guidi [Wed, 19 Dec 2012 20:27:22 +0000 (20:27 +0000)]
reordering and corrections

11 years agobertrand!
Andrea Asperti [Wed, 19 Dec 2012 17:05:03 +0000 (17:05 +0000)]
bertrand!
-tThis line, and those below, will be ignored--

A    chebyshev/bertrand256.ma
A    chebyshev/bertrand.ma

11 years agowe simplified our proof of standardization
Ferruccio Guidi [Wed, 19 Dec 2012 15:52:59 +0000 (15:52 +0000)]
we simplified our proof of standardization
by removing Kashima's "hap" computation

11 years agosqrt.ma
Andrea Asperti [Wed, 19 Dec 2012 07:10:58 +0000 (07:10 +0000)]
sqrt.ma

11 years ago- star.ma: strip lemma and confluence of star
Ferruccio Guidi [Tue, 18 Dec 2012 16:50:35 +0000 (16:50 +0000)]
- star.ma: strip lemma and confluence of star
- lambda: confluence of labelled sequential reduction completed!

11 years agoaddenda
Andrea Asperti [Tue, 18 Dec 2012 13:41:34 +0000 (13:41 +0000)]
addenda

11 years agochanges
Andrea Asperti [Tue, 18 Dec 2012 11:33:44 +0000 (11:33 +0000)]
changes

11 years agochebyshev_teta
Andrea Asperti [Tue, 18 Dec 2012 11:33:24 +0000 (11:33 +0000)]
chebyshev_teta

11 years ago- lambda: some parts commented out, some refactoring
Ferruccio Guidi [Mon, 17 Dec 2012 22:24:07 +0000 (22:24 +0000)]
- lambda: some parts commented out, some refactoring
  and some notational changes
- lib: some additions from the preamble of "lambda"
- predefined_virtuals: some additions

11 years agoThis line, and those below, will be ignored--
Andrea Asperti [Mon, 17 Dec 2012 12:04:50 +0000 (12:04 +0000)]
This line, and those below, will be ignored--

D    arithmetics/big_pi.ma

11 years agosplitted chebyshev in two parts
Andrea Asperti [Mon, 17 Dec 2012 11:57:48 +0000 (11:57 +0000)]
splitted chebyshev in two parts

11 years agorestructuring
Andrea Asperti [Mon, 17 Dec 2012 11:08:59 +0000 (11:08 +0000)]
restructuring

11 years agobackup copy rm
Andrea Asperti [Mon, 17 Dec 2012 09:00:51 +0000 (09:00 +0000)]
backup copy rm

11 years agoStill porting chebyshev
Andrea Asperti [Mon, 17 Dec 2012 09:00:18 +0000 (09:00 +0000)]
Still porting chebyshev

11 years ago- we added delimiters to the URL in lambdadelta1
Ferruccio Guidi [Thu, 13 Dec 2012 16:00:39 +0000 (16:00 +0000)]
- we added delimiters to the URL in lambdadelta1

11 years ago- bib refactoring
Ferruccio Guidi [Wed, 12 Dec 2012 22:17:31 +0000 (22:17 +0000)]
- bib refactoring
- date correction for lambdadelta5

11 years agolambdadelta1 is now dated with release date of \lambda\delta version 1
Ferruccio Guidi [Wed, 12 Dec 2012 21:52:15 +0000 (21:52 +0000)]
lambdadelta1 is now dated with release date of \lambda\delta version 1

11 years ago- pointer structure simplified
Ferruccio Guidi [Tue, 11 Dec 2012 19:15:02 +0000 (19:15 +0000)]
- pointer structure simplified
- new properties on poiner orders
- last lemma in Kashima's article proved

11 years ago- lambda: - normalization theorem completed!
Ferruccio Guidi [Mon, 10 Dec 2012 20:54:24 +0000 (20:54 +0000)]
- lambda: - normalization theorem completed!
          - binary trees on pointer sequences set up to serve as labels for "st" computations
- lstar: right-oriened eliminator added

11 years agoPorting chebyshev
Andrea Asperti [Mon, 10 Dec 2012 08:56:30 +0000 (08:56 +0000)]
Porting chebyshev

11 years agoPorting chebyshev
Andrea Asperti [Mon, 10 Dec 2012 08:55:22 +0000 (08:55 +0000)]
Porting chebyshev

11 years ago- lambda: first half of the standardization theorem is proved!
Ferruccio Guidi [Sun, 9 Dec 2012 17:59:03 +0000 (17:59 +0000)]
- lambda: first half of the standardization theorem is proved!

11 years ago- list.ma: improved notation for constant lists (a "term 19" was missing)
Ferruccio Guidi [Sat, 8 Dec 2012 23:26:45 +0000 (23:26 +0000)]
- list.ma: improved notation for constant lists (a "term 19" was missing)
- lambda: more properties on pointers, extra xoa quantifier removed,
bugfix in notations and names