WFFOP : wff operation

OTL Object

• match

Printing

• prw

Printing

• ppw
• pw
• pwscope
• pwtypes

Internal for Printing

• prt-aplicn-p
• prt-associative-p
• prt-infix-op
• prt-prefix-op
• prt-symbol-p

Weak Labels

• create-weak
• delete-weak
• dissolve-weak
• dissolve-weak*
• redef-weak

Saving Wffs

• sv-wff

Recording

• remark-printedtfile

Vpforms

• gwff-to-jform
• gwff-to-prop-jform
• jform-to-gwff
• number-of-horizontal-paths
• number-of-vertical-paths
• print-jlist

wff Primitives

• apply-wff
• bindhead
• binding
• bindvar
• change-print-type
• dupwff
• free-vars-of
• intern-subst
• make-wffschema
• rename-bd-var
• subst-1-type
• substitute-types
• type
• type-of-arg-1

Equality between Wffs

• inmost-gar
• not-wffeq
• wffeq
• wffeq-ab
• wffeq-def
• wffeq-defeq
• wffeq-lnorm
• wffeq-nnf

Predicates on Wffs

• a-bd-wff-p
• abbrev-p
• ae-bd-wff-p
• and-p
• anyabbrev-p
• anypropsym-p
• boundwff-p
• e-bd-wff-p
• equal-type-p
• equals-p
• equiv-p
• free-for
• free-in
• gvar-p
• gwff-p
• implies-p
• infix-op-p
• infix-p
• is-variable
• label-p
• lambda-bd-p
• legal-type-p
• logconst-p
• lsymbol-p
• non-atomic
• non-atomic-or-truthvalue
• not-free-in
• not-free-in-hyps
• not-free-in-wffset
• not-p
• or-p
• pmabbrev-p
• pmpropsym-p
• propsym-p
• r-prime-restr
• reduct-p
• same-modulo-equality
• subst-occs
• subst-some-occurrences
• type-equal
• wff-applic-p

Moving Commands

• find-binder
• find-infix
• gar
• gdr
• glr
• grr
• ntharg
• replace-gar
• replace-gdr
• replace-glr
• replace-grr

Changing Commands

• change-top
• delete-topconn-lscope
• delete-topconn-rscope
• mbed-and-left
• mbed-and-right
• mbed-equiv-left
• mbed-equiv-right
• mbed-existential
• mbed-existential1
• mbed-forall
• mbed-implics-left
• mbed-implics-right
• mbed-lambda
• mbed-or-left
• mbed-or-right
• mbed=left
• mbed=right
• merge-constant
• merge-idempotent
• wff-absorb
• wff-associative-l
• wff-associative-r
• wff-commutative
• wff-dist-contract
• wff-dist-expand
• wff-double-negation
• wff-permute
• wff-sub-equiv
• wff-sub-implies

Recursively Changing Commands

• assoc-l
• merge-constant*
• merge-idempotent*
• wff-absorb*
• wff-associative-l*
• wff-associative-r*
• wff-commutative*
• wff-dist-contract*
• wff-dist-expand*
• wff-double-negation*
• wff-permute*
• wff-sub-equiv*
• wff-sub-implies*

Substitution

• do-primsub
• instantiate-binder
• replace-equiv
• replace-equiv-all
• s
• subst-some-occs
• substitute-l-term-var
• substitute-term-var
• wff-identity

Basic Abbreviations

• abbr-list
• const-list
• contains-defn
• inst-def
• instantiate-1
• instantiate-all
• instantiate-defn
• instantiate-equalities
• instantiate-top-equality
• lib-abbr-list
• new-defs
• rpin
• substitute-bdvar-scope
• top-level-defn

Lambda-Calculus

• ab-change
• ab-normal-p
• ab-normalize
• eta-exp
• eta-to-base
• etacontr
• etanorm
• lambda-norm
• lcontr
• lexpd
• lnorm
• lnorm-beta
• lnorm-eta
• long-eta
• rewrite-all-equivalence
• untyped-lambda-norm
• wffeq-ab-beta
• wffeq-ab-eta
• wffeq-ab-lambda

Negation movers

• neg-norm
• negwff
• pull-negation
• push-negation

Miscellaneous

• conjunctive-normal-form
• find-subformulas
• head
• hvars
• min-quant-scope

RuleP

• sat-p
• valid-p

Quantifier Commands

• delete-binder
• delete-leftmost-binder
• openwffa
• openwffe

Wellformedness

• culprit-p
• find-culprit
• locateunwffs

ETPS documentation homepage

TPS homepage