||r1.args|| = ||r2.args||

i:. i < ||r1.args|| [[r1.args[i]]] 1of(e) s1 a tr = [[r2.args[i]]] 1of(e) s1 s2 a tr [[rel_arg_typ(r1.name;i;de)]] rho

list_accum(x,t.x([[t]] 1of(e) s1 a tr);[[r1.name]] rho 2of(e) ;r1.args) list_accum(x,t.x([[t]] 1of(e) s1 s2 a tr);[[r2.name]] rho 2of(e) ;r2.args)

MoveToConcl -1
THEN
RepeatFor 4 (MoveToConcl -3)
THEN
MoveToConcl -1
THEN
Unfolds [`tc`;`trace_consistent_rel`] 0
THEN
Reduce 0
THEN
GenConcl (r1.args = l1)
THEN
Thin -1
THEN
GenConcl (r2.args = l2)
THEN
Thin -1
THEN
RevHypSubstSq -3 0
THEN
Thin -3
THEN
let i 8 , j 9 in (Analyze i) THEN (All Reduce) THEN (Unfold `sig_mng` j) THEN (Unfold `record` j) THEN (Unfold `decl_type` j) THEN (Reduce j) THEN (Unfold `st_list_mng` j) THEN (Analyze 1) THEN (Analyze 1) THEN (Fold `relname_eq` 0 ORELSE Fold `relname_other` 0) THEN (Unfold `relname_mng` 0) THEN (All Reduce) THEN (Thin 2) THEN (Thin 2) THEN (Analyze 0)

1

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))

2

1. y: Label 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])) ||de.rel(y)|| = ||l1|| & (i:. i < ||l1|| (de.rel(y))[i] term_types(ds;da;de;l1[i])) ||de.rel(y)|| = ||l2|| & (i:. i < ||l2|| (de.rel(y))[i] term_types(ds;da;de;l2[i])) (i:. i < ||l1|| [[l1[i]]] e1 s1 a tr = [[l2[i]]] e1 s1 s2 a tr [[rel_arg_typ(relname_other(y);i;de)]] rho) (list_accum(x,t.x([[t]] e1 s1 a tr);e2.y;l1) list_accum(x,t.x([[t]] e1 s1 s2 a tr);e2.y;l2))

About: