aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Collapse)AuthorAgeFilesLines
* Finish complete evaluability proofYann Herklotz2023-06-101-19/+88
|
* Try to prove main theoremYann Herklotz2023-06-101-0/+5
| | | | Missing some link between forests
* Add more to proof of evaluabilityYann Herklotz2023-06-102-1/+57
|
* Finish abstract_sequence_evaluable_mYann Herklotz2023-06-091-1/+104
|
* Prove abstract_sequence_evaluableYann Herklotz2023-06-091-0/+2
|
* Finish abstract_sequence_evaluable_fold2Yann Herklotz2023-06-091-5/+42
|
* Finish abstract_sequence_evaluable_foldYann Herklotz2023-06-091-12/+68
|
* Add outline of proof of evaluable when predicate is falseYann Herklotz2023-06-091-19/+54
|
* Add proof outline for evaluabilityYann Herklotz2023-06-082-20/+44
|
* Work towards proving evaluabilityYann Herklotz2023-06-053-38/+169
|
* Move around generating functionsYann Herklotz2023-06-032-68/+68
|
* Fix proof of predicates completelyYann Herklotz2023-06-022-7/+24
|
* Fix top-level proof with Isetpred missingYann Herklotz2023-06-021-12/+55
|
* Finished the propert version of from_predicated_sem_pred_expr2Yann Herklotz2023-06-027-44/+316
|
* Finish from_predicated_sem_pred_exprYann Herklotz2023-05-311-8/+97
|
* Remove unnecessary assumption from sem_merge_listYann Herklotz2023-05-301-4/+3
|
* Fix other proofs and attempt from_predicated proofYann Herklotz2023-05-301-7/+26
|
* Prove merge list_translationYann Herklotz2023-05-301-2/+16
|
* Prove fold_right over ElistYann Herklotz2023-05-301-4/+74
|
* Finish second flap2 proofYann Herklotz2023-05-301-1/+9
|
* Finished painful product proofYann Herklotz2023-05-305-13/+127
|
* Prove more admitted theoremsYann Herklotz2023-05-296-47/+190
|
* Finish two AbstrSemIdent false proofsYann Herklotz2023-05-281-11/+50
|
* Finish max predicate proofYann Herklotz2023-05-281-1/+78
|
* Finish proofs in GiblePargenproofForward.vYann Herklotz2023-05-282-5/+49
|
* Work on forward proofsYann Herklotz2023-05-282-1/+18
|
* Finish proofs in GiblePargenproofBackward.vYann Herklotz2023-05-271-26/+101
|
* Add proofs of gather_predicatesYann Herklotz2023-05-261-25/+196
|
* Finish predicate inclusion proofsYann Herklotz2023-05-251-48/+99
|
* Finish gather_predicate proofsYann Herklotz2023-05-241-17/+502
|
* Prove evaluability of predicates throughoutYann Herklotz2023-05-221-61/+126
|
* Work on smaller evaluability proofYann Herklotz2023-05-221-49/+88
|
* Finish abstr_seq_reverse_correct_foldYann Herklotz2023-05-213-35/+116
|
* Add proof about preds_emptyYann Herklotz2023-05-211-3/+12
|
* Add proofs about RBexitYann Herklotz2023-05-211-2/+63
|
* Prove evaluable_pred_expr_exists_RBsetpredYann Herklotz2023-05-215-100/+506
|
* Work on evaluability proofYann Herklotz2023-05-191-0/+37
|
* Prepare work on evaluability of instructionsYann Herklotz2023-05-193-71/+133
|
* Finish evaluability proof of RBopYann Herklotz2023-05-195-210/+338
|
* Add new proofs about semantic identityYann Herklotz2023-05-185-600/+937
|
* Work on scheduling proofYann Herklotz2023-05-164-25/+154
|
* Add start of backward proofYann Herklotz2023-05-161-3/+39
|
* Add example computation to update functionYann Herklotz2023-05-151-0/+11
|
* Add function to reason about executable constraintsYann Herklotz2023-05-152-5/+16
|
* Split correctness lemma into twoYann Herklotz2023-05-141-2/+19
|
* Rename backwards proofYann Herklotz2023-05-123-30/+55
|
* Split proof up into more filesYann Herklotz2023-05-099-3766/+3935
|
* Add assumption and prove assumption that preds are evaluableYann Herklotz2023-05-062-43/+50
|
* Add check for mutexcl and fix top-level proofYann Herklotz2023-05-063-345/+87
|
* Finished proof of beq_pred_expr in both directionsYann Herklotz2023-05-051-12/+108
|
generated by cgit (git 2.34.1) at 2024-07-02 20:42:32 +0000