Nuprl Definition : coW-pos-agree

coW-pos-agree(a.B[a];w;w';p;q) ==
  let u,v = p
  in let u',v' = q
     in ((copath-length(u) ≤ copath-length(u')) ∧ copathAgree(a.B[a];w;u;u'))
        ∧ (copath-length(v) ≤ copath-length(v'))
        ∧ copathAgree(a.B[a];w';v;v')

Definitions occuring in Statement : copathAgree: copathAgree(a.B[a];w;x;y), copath-length: copath-length(p), le: A ≤ B, and: P ∧ Q, spread: spread def
Definitions occuring in definition : copathAgree: copathAgree(a.B[a];w;x;y), copath-length: copath-length(p), le: A ≤ B, and: P ∧ Q, spread: spread def
FDL editor aliases : coW-pos-agree

Latex:
coW-pos-agree(a.B[a];w;w';p;q) == let u,v = p in let u',v' = q in ((copath-length(u) \mleq{} copath-length(u')) \mwedge{} copathAgree(a.B[a];w;u;u')) \mwedge{} (copath-length(v) \mleq{} copath-length(v')) \mwedge{} copathAgree(a.B[a];w';v;v') Date html generated: 2018_07_25-PM-01_42_58 Last ObjectModification: 2018_06_16-PM-00_06_25 Theory : co-recursion Home Index