Nuprl - Pf closed_pred

(3steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

Q:Fmla. closed_pred((Q)') closed_pred(Q)

By: Unfolds [`pred`;`closed_pred`;`pred_addprime`] 0 THEN All (RW ColMemberC) THEN All (Unfold `closed_rel`)

Generated subgoals:

1 1. Q: Collection(rel())
2. r:rel(). (r@0:rel(). r@0 Q & r = (r@0)') rel_free_vars(r) = nil
3. r: rel()
4. r Q
rel_free_vars(r) = nil

2 1. Q: Collection(rel())
2. r:rel(). r Q rel_free_vars(r) = nil
3. r: rel()
4. r@0:rel(). r@0 Q & r = (r@0)'
rel_free_vars(r) = nil

About:

(3steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

1	1. `Q:` `Collection(rel())` 2. `r:rel(). (r@0:rel(). r@0 Q & r = (r@0)') rel_free_vars(r) = nil` 3. `r:` `rel()` 4. `r Q` `rel_free_vars(r) = nil`
2	1. `Q:` `Collection(rel())` 2. `r:rel(). r Q rel_free_vars(r) = nil` 3. `r:` `rel()` 4. `r@0:rel(). r@0 Q & r = (r@0)'` `rel_free_vars(r) = nil`