Lines Matching defs:create
249 ;;that create-kripke of this reduced model is bisim-equiv to create-Kripke of
318 (variables (create-kripke C))))
328 (variables (create-kripke
391 (initial-states (create-kripke C))
393 (create-kripke
427 (create-kripke
429 (initial-states (create-kripke C))
726 (circuit-modelp (create-kripke (cone-of-influence-reduction C vars))))
729 create-kripke
766 (implies (memberp r (create-next-states-of-p p states vars equations))
842 (memberp s (create-next-states-of-p q states-cone vars-cone
851 (memberp s (create-next-states-of-p q states-cone vars-cone equations-cone))))
866 (create-next-states-of-p q states-cone vars-cone equations-cone)))
892 s (create-next-states-of-p q states-cone vars-cone equations-cone)
902 (states (create-next-states-of-p
915 (implies (and (memberp r (create-next-states-of-p p states-orig vars-orig
929 r (create-next-states-of-p q states-cone vars-cone equations-cone)
943 (defun create-corresponding-equation (vars equation-record vars-prime eqn eq-rec)
945 (-> (create-corresponding-equation (rest vars) equation-record vars-prime
965 (defthm create-corresponding-equation-is-equation-equal
968 (equation-equal-p eqn-orig (create-corresponding-equation
1015 (create-corresponding-equation vars-cone eqn-cone vars-orig eqn
1020 :induct (create-corresponding-equation vars-cone eqn-cone
1188 (create-corresponding-equation
1236 (implies (and (memberp r (create-next-states-of-p p states-orig vars-orig
1251 r (create-next-states-of-p q states-cone vars-cone equations-cone)
1261 (eqn (create-corresponding-equation
1294 (implies (and (subset l (create-next-states-of-p p states-orig vars-orig
1309 l (create-next-states-of-p q states-cone vars-cone equations-cone)
1329 (create-next-states-of-p p states-orig vars-orig
1331 (create-next-states-of-p q states-cone vars-cone equations-cone)
1336 (l (create-next-states-of-p p states-orig vars-orig
1355 (defthm memberp-to-create-equation-reduction
1358 (equal (<- (create-corresponding-equation vars-orig eqn-orig
1368 (defthm not-memberp-to-create-equation
1370 (equal (<- (create-corresponding-equation vars-orig eqn-orig
1380 (equal (<- (create-corresponding-equation vars-orig eqn-orig
1389 (defthm create-corresponding-equation-is-equation-equal-2
1394 (equation-equal-p (create-corresponding-equation
1419 (create-corresponding-equation
1434 r (create-next-states-of-p p states-orig vars-orig equations-orig)
1442 (inits (create-next-states-of-p
1466 (implies (and (memberp s (create-next-states-of-p q states-cone vars-cone
1507 (implies (and (memberp s (create-next-states-of-p q states-cone vars-cone
1523 s (create-next-states-of-p p states-orig vars-orig equations-orig)
1547 (create-corresponding-equation
1551 :induct (create-corresponding-equation
1563 (implies (and (memberp s (create-next-states-of-p q states-cone vars-cone
1581 s (create-next-states-of-p p states-orig vars-orig equations-orig)
1592 (create-corresponding-equation
1597 (eqn (create-corresponding-equation
1605 (eqn (create-corresponding-equation
1619 (implies (and (subset l (create-next-states-of-p q states-cone vars-cone
1637 l (create-next-states-of-p p states-orig vars-orig equations-orig)
1662 (create-next-states-of-p q states-cone vars-cone
1664 (create-next-states-of-p p states-orig vars-orig equations-orig)
1669 (l (create-next-states-of-p q states-cone vars-cone
1674 (in-theory (disable create-next-states-of-p))
1680 (equal (<- (create-next-states states states-prime vars equations)
1686 (defthm create-next-states-to-next-state-of-p
1688 (equal (<- (create-next-states states states-prime vars equations)
1690 (create-next-states-of-p p states-prime vars equations)))
1713 (<- (create-next-states states-orig states-orig vars-orig
1716 (<- (create-next-states states-cone states-cone vars-cone
1743 (<- (create-next-states states-cone states-cone vars-cone
1746 (<- (create-next-states states-orig states-orig vars-orig
1773 (<- (create-next-states states-cone states-cone vars-cone
1776 (<- (create-next-states states-orig states-orig vars-orig
1792 (in-theory (disable create-all-evaluations find-all-variables
1804 find-all-equations create-label-fn))
1815 (states (create-kripke C))
1816 (transition (create-kripke C))
1818 (create-kripke
1821 (create-kripke
1828 create-kripke-produces-circuit-model)
1830 (states-orig (states (create-kripke C)))
1832 (create-kripke
1843 (states (create-kripke C))
1844 (transition (create-kripke C))
1845 (states (create-kripke
1849 (create-kripke
1855 (states (create-kripke C))
1856 (transition (create-kripke C))
1857 (states (create-kripke
1861 (create-kripke
1865 (:instance create-kripke-produces-circuit-model)
1866 (:instance create-kripke-produces-circuit-model
1876 (create-kripke
1879 (create-kripke
1881 (states (create-kripke C))
1882 (transition (create-kripke C))
1888 create-kripke-produces-circuit-model)
1890 (states-orig (states (create-kripke C)))
1892 (create-kripke
1903 (states (create-kripke
1905 (transition (create-kripke
1908 (states (create-kripke C))
1909 (transition (create-kripke C))
1915 (states (create-kripke
1917 (transition (create-kripke
1920 (states (create-kripke C))
1921 (transition (create-kripke C))
1925 (:instance create-kripke-produces-circuit-model)
1926 (:instance create-kripke-produces-circuit-model
1932 (in-theory (disable well-formed-transition-p create-kripke
1941 (c-bisim-equiv (create-kripke C)
1942 (create-kripke (cone-of-influence-reduction C vars))
1961 ;; (create-kripke (cone-of-influence-reduction C
1963 ;; (ltl-semantics f (create-kripke C))))
1968 ;; (n (create-kripke (cone-of-influence-reduction C
1970 ;; (m (create-kripke C))
1979 ;; (equal (ltl-semantics f (create-kripke
1981 ;; (ltl-semantics f (create-kripke C)))))
1999 (c-bisim-equiv (create-kripke C)
2000 (create-kripke (cone-of-influence-reduction C vars))