Nuprl - Pf rel mng 2 iff 1 1 1

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

1. x: SimpleType
2. ds: Collection(dec())
3. daa: Collection(dec())
4. da: Collection(SimpleType)
5. de: sig()
6. rho: Decl
7. e1: {1of([[de]] rho)}
8. e2: l:Labelreduce(s,m. [[s]] rhom;Prop;de.rel(l))
9. s1: {[[ds]] rho}
10. s2: {[[ds]] rho}
11. a: [[da]] rho
12. tr: trace_env([[daa]] rho)
13. l1: Term List
14. l2: Term List
15. ||l1|| = ||l2||

(i:||l1||. trace_consistent(rho;daa;tr.proj;l1[i])) (i:||l2||. trace_consistent(rho;daa;tr.proj;l2[i])) ||l1|| = 2 & x term_types(ds;da;de;l1[0]) & x term_types(ds;da;de;l1[1]) ||l2|| = 2 & x term_types(ds;da;de;l2[0]) & x term_types(ds;da;de;l2[1]) (i:. i < ||l1|| [[l1[i]]] e1 s1 a tr = [[l2[i]]] e1 s1 s2 a tr [[rel_arg_typ(relname_eq(x);i;de)]] rho) (list_accum(x,t.x([[t]] e1 s1 a tr);x@0,y. x@0 = y [[x]] rho;l1) list_accum(x,t.x([[t]] e1 s1 s2 a tr);x@0,y. x@0 = y [[x]] rho;l2))

By: RepeatFor 4 (Analyze 0) THEN Analyze -2 THEN Analyze -2 THEN Analyze -1 THEN Analyze -1

Generated subgoal:

1 16. i:||l1||. trace_consistent(rho;daa;tr.proj;l1[i])
17. i:||l2||. trace_consistent(rho;daa;tr.proj;l2[i])
18. ||l1|| = 2
19. x term_types(ds;da;de;l1[0])
20. x term_types(ds;da;de;l1[1])
21. ||l2|| = 2
22. x term_types(ds;da;de;l2[0])
23. x term_types(ds;da;de;l2[1])
(i:. i < ||l1|| [[l1[i]]] e1 s1 a tr = [[l2[i]]] e1 s1 s2 a tr [[rel_arg_typ(relname_eq(x);i;de)]] rho) (list_accum(x,t.x([[t]] e1 s1 a tr);x@0,y. x@0 = y [[x]] rho;l1) list_accum(x,t.x([[t]] e1 s1 s2 a tr);x@0,y. x@0 = y [[x]] rho;l2))

About:

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