Nuprl - Pf tc pred unprime

(4steps) PrintForm Definitions mb automata 4 Sections GenAutomata Doc

P:Fmla, ds:Collection(dec()), da:Collection(SimpleType), de:sig(). tc_pred(P;ds;da;de) tc_pred(pred_unprime(P);ds;da;de)

By: Unfold `tc_pred` 0 THEN Try (Fold `pred` 0)

Generated subgoals:

1 1. P: Fmla
2. ds: Collection(dec())
3. da: Collection(SimpleType)
4. de: sig()
5. r:rel(). r P tc(r;ds;da;de)
6. r: rel()
7. r pred_unprime(P)
tc(r;ds;da;de)

2 1. P: Fmla
2. ds: Collection(dec())
3. da: Collection(SimpleType)
4. de: sig()
5. r:rel(). r pred_unprime(P) tc(r;ds;da;de)
6. r: rel()
7. r P
tc(r;ds;da;de)

About:

(4steps) PrintForm Definitions mb automata 4 Sections GenAutomata Doc

1	1. `P:` `Fmla` 2. `ds:` `Collection(dec())` 3. `da:` `Collection(SimpleType)` 4. `de:` `sig()` 5. `r:rel(). r P tc(r;ds;da;de)` 6. `r:` `rel()` 7. `r pred_unprime(P)` `tc(r;ds;da;de)`
2	1. `P:` `Fmla` 2. `ds:` `Collection(dec())` 3. `da:` `Collection(SimpleType)` 4. `de:` `sig()` 5. `r:rel(). r pred_unprime(P) tc(r;ds;da;de)` 6. `r:` `rel()` 7. `r P` `tc(r;ds;da;de)`