r:rel(), as:(LabelTerm) List, daa:Collection(dec()), rho:Decl, te:(LabelLabel). trace_consistent_rel(rho;daa;te;r) subst_mentions_trace(as) trace_consistent_rel(rho;daa;te;rel_subst(as;r))

Unfold `rel_subst` 0
THEN
RepeatFor 2 ((ParallelOp -2) THEN (All Reduce))
THEN
AssertBY (||map(t.term_subst(as;t);r.args)|| = ||r.args||) (RWO "map_length" 0)

1	1. r: rel() 2. as: (LabelTerm) List 3. daa: Collection(dec()) 4. rho: Decl 5. te: LabelLabel 6. i:||r.args||. trace_consistent(rho;daa;te;r.args[i]) 7. subst_mentions_trace(as) 8. i: ||map(t.term_subst(as;t);r.args)|| 9. ||map(t.term_subst(as;t);r.args)|| = ||r.args|| i < ||r.args||
2	1. r: rel() 2. as: (LabelTerm) List 3. daa: Collection(dec()) 4. rho: Decl 5. te: LabelLabel 6. i:||r.args||. trace_consistent(rho;daa;te;r.args[i]) 7. subst_mentions_trace(as) 8. i: ||map(t.term_subst(as;t);r.args)|| 9. trace_consistent(rho;daa;te;r.args[i]) 10. ||map(t.term_subst(as;t);r.args)|| = ||r.args|| trace_consistent(rho;daa;te;map(t.term_subst(as;t);r.args)[i])

About: