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 : spread: spread def, and: P ∧ Q, le: A ≤ B, copath-length: copath-length(p), copathAgree: copathAgree(a.B[a];w;x;y)
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: 2019_06_20-PM-00_58_02 Last ObjectModification: 2019_01_02-PM-01_34_39 Theory : co-recursion-2 Home Index