• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
      • Deftreeops
        • Deftreeops-implementation
          • Deftreeops-event-generation
            • Deftreeops-gen-rep-events
            • Deftreeops-gen-conc-events
            • Deftreeops-gen-rulename-events
            • Deftreeops-gen-rulename-alist-events
            • Deftreeops-gen-discriminant-terms
            • Deftreeops-gen-conc-list-events
            • Deftreeops-gen-rep-list-events
            • Deftreeops-gen-numrange-events
            • Deftreeops-gen-conc-info-list
            • Deftreeops-gen-rep-info
            • Deftreeops-gen-cst-list-list-conc-match
            • Deftreeops-gen-cst-list-list-alt-match
            • Deftreeops-gen-conc-info
            • Deftreeops-gen-all-rulename-infos+events
            • Deftreeops-gen-cst-list-rep-match
            • Deftreeops-gen-cst-list-elem-match
            • Deftreeops-gen-rulename-info-alist
            • Deftreeops-gen-cst-match
            • Deftreeops-gen-charval-events
            • Deftreeops-gen-numrange-alist-events
            • Deftreeops-gen-all-numrange-infos+events
            • Deftreeops-gen-all-charval-infos+events
            • Deftreeops-gen-everything
            • Deftreeops-gen-charval-alist-events
            • Deftreeops-gen-charval-info-alist
            • Deftreeops-gen-rulename-info
            • Deftreeops-gen-rep-info-list
            • Deftreeops-gen-numrange-info-alist
            • Deftreeops-gen-matchers
            • Deftreeops-gen-numrange-info
            • Deftreeops-gen-charval-info
            • Deftreeops-elem-match-pred
            • Deftreeops-conc-match-pred
            • Deftreeops-alt-match-pred
            • Deftreeops-rep-match-pred
            • Deftreeops-match-pred
          • Deftreeops-info
          • Deftreeops-process-inputs-and-gen-everything
          • Deftreeops-fn
          • Deftreeops-table
          • Deftreeops-input-processing
          • Deftreeops-macro-definition
        • Deftreeops-show-event
        • Deftreeops-show-info
      • Defdefparse
      • Defgrammar
      • Tree-utilities
      • Notation
      • Grammar-parser
      • Meta-circular-validation
      • Parsing-primitives-defresult
      • Parsing-primitives-seq
      • Operations
      • Examples
      • Differences-with-paper
      • Constructor-utilities
      • Grammar-printer
      • Parsing-tools
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • C
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Ethereum
    • Leftist-trees
    • Java
    • Riscv
    • Taspi
    • Bitcoin
    • Zcash
    • Des
    • X86isa
    • Sha-2
    • Yul
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Axe
    • Poseidon
    • Where-do-i-place-my-book
    • Aleo
    • Bigmems
    • Builtins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Deftreeops-event-generation

Deftreeops-gen-conc-list-events

Lift deftreeops-gen-conc-events to lists.

Signature

(deftreeops-gen-conc-list-events 
     alt infos conc-equivs-thm 
     check-conc-fn nonleaf-thm alt-match-thm 
     alt-singletonp rulename prefix print) 
 
  → 
(mv matching-thm-events 
    check-conc-fn-equiv-thm-events 
    get-tree-list-list-fn-events 
    rep-matching-thmevents 
    get-tree-list-fn-events 
    get-tree-fn-events event-alist) 

Arguments

alt — Guard (alternationp alt).

infos — Guard (deftreeops-conc-info-listp infos).

conc-equivs-thm — Guard (common-lisp::symbolp conc-equivs-thm).

check-conc-fn — Guard (common-lisp::symbolp check-conc-fn).

nonleaf-thm — Guard (common-lisp::symbolp nonleaf-thm).

alt-match-thm — Guard (common-lisp::symbolp alt-match-thm).

alt-singletonp — Guard (booleanp alt-singletonp).

rulename — Guard (rulenamep rulename).

prefix — Guard (common-lisp::symbolp prefix).

print — Guard (evmac-input-print-p print).

Returns

matching-thm-events — Type (pseudo-event-form-listp matching-thm-events).

check-conc-fn-equiv-thm-events — Type (pseudo-event-form-listp check-conc-fn-equiv-thm-events).

get-tree-list-list-fn-events — Type (pseudo-event-form-listp get-tree-list-list-fn-events).

rep-matching-thmevents — Type (pseudo-event-form-listp rep-matching-thmevents).

get-tree-list-fn-events — Type (pseudo-event-form-listp get-tree-list-fn-events).

get-tree-fn-events — Type (pseudo-event-form-listp get-tree-fn-events).

event-alist — Type (symbol-pseudoeventform-alistp event-alist).

Definitions and Theorems

Function: deftreeops-gen-conc-list-events-aux

(defun deftreeops-gen-conc-list-events-aux
       (alt infos i conc-equivs-thm
            check-conc-fn nonleaf-thm alt-match-thm
            alt-singletonp rulename prefix print)
  (declare (xargs :guard (and (alternationp alt)
                              (deftreeops-conc-info-listp infos)
                              (posp i)
                              (common-lisp::symbolp conc-equivs-thm)
                              (common-lisp::symbolp check-conc-fn)
                              (common-lisp::symbolp nonleaf-thm)
                              (common-lisp::symbolp alt-match-thm)
                              (booleanp alt-singletonp)
                              (rulenamep rulename)
                              (common-lisp::symbolp prefix)
                              (evmac-input-print-p print))))
  (declare (xargs :guard (equal (len infos) (len alt))))
  (let ((__function__ 'deftreeops-gen-conc-list-events-aux))
    (declare (ignorable __function__))
    (b* (((when (endp alt))
          (mv nil nil nil nil nil nil nil))
         ((mv matching-thm-event?
              check-conc-fn-equiv-thm-event?
              get-tree-list-list-fn-event?
              rep-matching-thm-events
              get-tree-list-fn-events
              get-tree-fn-events event-alist)
          (deftreeops-gen-conc-events
               (car alt)
               (car infos)
               i conc-equivs-thm
               check-conc-fn nonleaf-thm alt-match-thm
               alt-singletonp rulename prefix print))
         ((mv more-matching-thm-events
              more-check-conc-fn-equiv-thm-events
              more-get-tree-list-list-fn-events
              more-rep-matching-thm-events
              more-get-tree-list-fn-events
              more-get-tree-fn-events
              more-event-alist)
          (deftreeops-gen-conc-list-events-aux
               (cdr alt)
               (cdr infos)
               (1+ i)
               conc-equivs-thm
               check-conc-fn nonleaf-thm alt-match-thm
               alt-singletonp rulename prefix print)))
      (mv (append matching-thm-event?
                  more-matching-thm-events)
          (append check-conc-fn-equiv-thm-event?
                  more-check-conc-fn-equiv-thm-events)
          (append get-tree-list-list-fn-event?
                  more-get-tree-list-list-fn-events)
          (append rep-matching-thm-events
                  more-rep-matching-thm-events)
          (append get-tree-list-fn-events
                  more-get-tree-list-fn-events)
          (append get-tree-fn-events
                  more-get-tree-fn-events)
          (append event-alist more-event-alist)))))

Theorem: pseudo-event-form-listp-of-deftreeops-gen-conc-list-events-aux.matching-thm-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-conc-list-events-aux.matching-thm-events
 (b* (((mv ?matching-thm-events
           ?check-conc-fn-equiv-thm-events
           ?get-tree-list-list-fn-events
           ?rep-matching-thmevents
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-conc-list-events-aux
            alt infos i conc-equivs-thm
            check-conc-fn nonleaf-thm alt-match-thm
            alt-singletonp rulename prefix print)))
   (pseudo-event-form-listp matching-thm-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-conc-list-events-aux.check-conc-fn-equiv-thm-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-conc-list-events-aux.check-conc-fn-equiv-thm-events
 (b* (((mv ?matching-thm-events
           ?check-conc-fn-equiv-thm-events
           ?get-tree-list-list-fn-events
           ?rep-matching-thmevents
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-conc-list-events-aux
            alt infos i conc-equivs-thm
            check-conc-fn nonleaf-thm alt-match-thm
            alt-singletonp rulename prefix print)))
   (pseudo-event-form-listp check-conc-fn-equiv-thm-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-conc-list-events-aux.get-tree-list-list-fn-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-conc-list-events-aux.get-tree-list-list-fn-events
 (b* (((mv ?matching-thm-events
           ?check-conc-fn-equiv-thm-events
           ?get-tree-list-list-fn-events
           ?rep-matching-thmevents
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-conc-list-events-aux
            alt infos i conc-equivs-thm
            check-conc-fn nonleaf-thm alt-match-thm
            alt-singletonp rulename prefix print)))
   (pseudo-event-form-listp get-tree-list-list-fn-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-conc-list-events-aux.rep-matching-thmevents

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-conc-list-events-aux.rep-matching-thmevents
 (b* (((mv ?matching-thm-events
           ?check-conc-fn-equiv-thm-events
           ?get-tree-list-list-fn-events
           ?rep-matching-thmevents
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-conc-list-events-aux
            alt infos i conc-equivs-thm
            check-conc-fn nonleaf-thm alt-match-thm
            alt-singletonp rulename prefix print)))
   (pseudo-event-form-listp rep-matching-thmevents))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-conc-list-events-aux.get-tree-list-fn-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-conc-list-events-aux.get-tree-list-fn-events
 (b* (((mv ?matching-thm-events
           ?check-conc-fn-equiv-thm-events
           ?get-tree-list-list-fn-events
           ?rep-matching-thmevents
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-conc-list-events-aux
            alt infos i conc-equivs-thm
            check-conc-fn nonleaf-thm alt-match-thm
            alt-singletonp rulename prefix print)))
   (pseudo-event-form-listp get-tree-list-fn-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-conc-list-events-aux.get-tree-fn-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-conc-list-events-aux.get-tree-fn-events
 (b* (((mv ?matching-thm-events
           ?check-conc-fn-equiv-thm-events
           ?get-tree-list-list-fn-events
           ?rep-matching-thmevents
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-conc-list-events-aux
            alt infos i conc-equivs-thm
            check-conc-fn nonleaf-thm alt-match-thm
            alt-singletonp rulename prefix print)))
   (pseudo-event-form-listp get-tree-fn-events))
 :rule-classes :rewrite)

Theorem: symbol-pseudoeventform-alistp-of-deftreeops-gen-conc-list-events-aux.event-alist

(defthm
 symbol-pseudoeventform-alistp-of-deftreeops-gen-conc-list-events-aux.event-alist
 (b* (((mv ?matching-thm-events
           ?check-conc-fn-equiv-thm-events
           ?get-tree-list-list-fn-events
           ?rep-matching-thmevents
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-conc-list-events-aux
            alt infos i conc-equivs-thm
            check-conc-fn nonleaf-thm alt-match-thm
            alt-singletonp rulename prefix print)))
   (symbol-pseudoeventform-alistp event-alist))
 :rule-classes :rewrite)

Function: deftreeops-gen-conc-list-events

(defun deftreeops-gen-conc-list-events
       (alt infos conc-equivs-thm
            check-conc-fn nonleaf-thm alt-match-thm
            alt-singletonp rulename prefix print)
  (declare (xargs :guard (and (alternationp alt)
                              (deftreeops-conc-info-listp infos)
                              (common-lisp::symbolp conc-equivs-thm)
                              (common-lisp::symbolp check-conc-fn)
                              (common-lisp::symbolp nonleaf-thm)
                              (common-lisp::symbolp alt-match-thm)
                              (booleanp alt-singletonp)
                              (rulenamep rulename)
                              (common-lisp::symbolp prefix)
                              (evmac-input-print-p print))))
  (declare (xargs :guard (equal (len infos) (len alt))))
  (let ((__function__ 'deftreeops-gen-conc-list-events))
    (declare (ignorable __function__))
    (deftreeops-gen-conc-list-events-aux
         alt infos 1 conc-equivs-thm
         check-conc-fn nonleaf-thm alt-match-thm
         alt-singletonp rulename prefix print)))

Theorem: pseudo-event-form-listp-of-deftreeops-gen-conc-list-events.matching-thm-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-conc-list-events.matching-thm-events
 (b* (((mv ?matching-thm-events
           ?check-conc-fn-equiv-thm-events
           ?get-tree-list-list-fn-events
           ?rep-matching-thmevents
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-conc-list-events
            alt infos conc-equivs-thm
            check-conc-fn nonleaf-thm alt-match-thm
            alt-singletonp rulename prefix print)))
   (pseudo-event-form-listp matching-thm-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-conc-list-events.check-conc-fn-equiv-thm-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-conc-list-events.check-conc-fn-equiv-thm-events
 (b* (((mv ?matching-thm-events
           ?check-conc-fn-equiv-thm-events
           ?get-tree-list-list-fn-events
           ?rep-matching-thmevents
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-conc-list-events
            alt infos conc-equivs-thm
            check-conc-fn nonleaf-thm alt-match-thm
            alt-singletonp rulename prefix print)))
   (pseudo-event-form-listp check-conc-fn-equiv-thm-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-conc-list-events.get-tree-list-list-fn-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-conc-list-events.get-tree-list-list-fn-events
 (b* (((mv ?matching-thm-events
           ?check-conc-fn-equiv-thm-events
           ?get-tree-list-list-fn-events
           ?rep-matching-thmevents
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-conc-list-events
            alt infos conc-equivs-thm
            check-conc-fn nonleaf-thm alt-match-thm
            alt-singletonp rulename prefix print)))
   (pseudo-event-form-listp get-tree-list-list-fn-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-conc-list-events.rep-matching-thmevents

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-conc-list-events.rep-matching-thmevents
 (b* (((mv ?matching-thm-events
           ?check-conc-fn-equiv-thm-events
           ?get-tree-list-list-fn-events
           ?rep-matching-thmevents
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-conc-list-events
            alt infos conc-equivs-thm
            check-conc-fn nonleaf-thm alt-match-thm
            alt-singletonp rulename prefix print)))
   (pseudo-event-form-listp rep-matching-thmevents))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-conc-list-events.get-tree-list-fn-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-conc-list-events.get-tree-list-fn-events
 (b* (((mv ?matching-thm-events
           ?check-conc-fn-equiv-thm-events
           ?get-tree-list-list-fn-events
           ?rep-matching-thmevents
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-conc-list-events
            alt infos conc-equivs-thm
            check-conc-fn nonleaf-thm alt-match-thm
            alt-singletonp rulename prefix print)))
   (pseudo-event-form-listp get-tree-list-fn-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-conc-list-events.get-tree-fn-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-conc-list-events.get-tree-fn-events
 (b* (((mv ?matching-thm-events
           ?check-conc-fn-equiv-thm-events
           ?get-tree-list-list-fn-events
           ?rep-matching-thmevents
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-conc-list-events
            alt infos conc-equivs-thm
            check-conc-fn nonleaf-thm alt-match-thm
            alt-singletonp rulename prefix print)))
   (pseudo-event-form-listp get-tree-fn-events))
 :rule-classes :rewrite)

Theorem: symbol-pseudoeventform-alistp-of-deftreeops-gen-conc-list-events.event-alist

(defthm
 symbol-pseudoeventform-alistp-of-deftreeops-gen-conc-list-events.event-alist
 (b* (((mv ?matching-thm-events
           ?check-conc-fn-equiv-thm-events
           ?get-tree-list-list-fn-events
           ?rep-matching-thmevents
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-conc-list-events
            alt infos conc-equivs-thm
            check-conc-fn nonleaf-thm alt-match-thm
            alt-singletonp rulename prefix print)))
   (symbol-pseudoeventform-alistp event-alist))
 :rule-classes :rewrite)