blob: a6232c3d6ea0b04f0131b3949b6860efacfafaa5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
|
//=============================== Core
// ======== Reflexive
// Children: none
// Arguments: (t)
// ---------------------
// Conclusion: (= t t)
proofrule REFL 0 1 ::CVC4::theory::uf::EqProofRuleChecker
// ======== Symmetric
// Children: (P:(= t1 t2))
// Arguments: none
// -----------------------
// Conclusion: (= t2 t1)
proofrule SYMM 1 0 ::CVC4::theory::uf::EqProofRuleChecker
// ======== Transitivity
// Children: (P1:(= t1 t2), ..., Pn:(= t{n-1} tn))
// Arguments: none
// -----------------------
// Conclusion: (= t1 tn)
proofrule TRANS 2: 0 ::CVC4::theory::uf::EqProofRuleChecker
// ======== Congruence (subsumed by Substitute?)
// Children: (P1:(= t1 s1), ..., Pn:(= tn sn))
// Arguments: (f)
// ---------------------------------------------
// Conclusion: (= (f t1 ... tn) (f s1 ... sn))
proofrule CONG 0: 1 ::CVC4::theory::uf::EqProofRuleChecker
//=============================== Boolean conversion
// ======== True intro
// Children: (P:F)
// Arguments: none
// ----------------------------------------
// Conclusion: (= F true)
proofrule TRUE_INTRO 1 0 ::CVC4::theory::uf::EqProofRuleChecker
// ======== True elim
// Children: (P:(= F true)
// Arguments: none
// ----------------------------------------
// Conclusion: F
proofrule TRUE_ELIM 1 0 ::CVC4::theory::uf::EqProofRuleChecker
// ======== False intro
// Children: (P:(not F))
// Arguments: none
// ----------------------------------------
// Conclusion: (= F false)
proofrule FALSE_INTRO 1 0 ::CVC4::theory::uf::EqProofRuleChecker
// ======== False elim
// Children: (P:(= F false)
// Arguments: none
// ----------------------------------------
// Conclusion: (not F)
proofrule FALSE_ELIM 1 0 ::CVC4::theory::uf::EqProofRuleChecker
|
