Skip to content

Commit

Permalink
Merge commit 'e0c9e4e32fea560bd73f5f3077561b59fdf13b0f' into probabil…
Browse files Browse the repository at this point in the history
…ity_dev
  • Loading branch information
binghe committed Jan 6, 2025

Verified

This commit was signed with the committer’s verified signature.
jpkrohling Juraci Paixão Kröhling
2 parents 662ac1b + e0c9e4e commit b794125
Showing 4 changed files with 419 additions and 220 deletions.
6 changes: 6 additions & 0 deletions examples/formal-languages/FormalLangScript.sml
Original file line number Diff line number Diff line change
@@ -281,6 +281,12 @@ Proof
RW_TAC basic_ss [IN_KSTAR] >> METIS_TAC [DOTn_def,IN_INSERT]
QED

Triviality KSTAR_NONEMPTY:
KSTAR A ≠ ∅
Proof
rw[EXTENSION] >> metis_tac[EPSILON_IN_KSTAR]
QED

Theorem KSTAR_SING:
x ∈ KSTAR {x}
Proof
3 changes: 2 additions & 1 deletion examples/formal-languages/regular/Holmakefile
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
INCLUDES = $(HOLDIR)/examples/balanced_bst \
$(HOLDIR)/examples/formal-languages \
$(HOLDIR)/examples/formal-languages/context-free
$(HOLDIR)/examples/formal-languages/context-free \
$(HOLDIR)/src/search

all: $(DEFAULT_TARGETS) regexp2dfa

Loading

0 comments on commit b794125

Please sign in to comment.