Searched refs:ProofNode (Results 1 - 3 of 3) sorted by relevance

/seL4-l4v-10.1.1/graph-refine/
H A Dcheck.py156 class ProofNode: class in inherits:
181 return 'ProofNode (%r, %r, %r)' % (self.kind,
274 return (i + 1, ProofNode ('Leaf'))
283 return (i, ProofNode ('Restr', (point, (kind, (x, y))), [p1]))
292 return (i, ProofNode ('SingleRevInduct', (point, (eqs, n),
302 return (i, ProofNode ('Split', (l_details, r_details, eqs,
309 return (i, ProofNode ('CaseSplit', (n, tag), [p1, p2]))
H A Dstats.py5 from check import ProofNode namespace
23 if line.startswith ('ProofNode '):
H A Dsearch.py12 from check import restr_others, loops_to_split, ProofNode namespace
1716 return ProofNode ('Leaf', None, ())
1742 return ProofNode (kind, details, subpfs)
1778 return ProofNode ('Restr', (sp, (kind, (min_v, max_v))), [subproof])

Completed in 91 milliseconds