Nuprl Lemma : loop-class-program_wf

[Info,B:Type].
  ∀[X:EClass(B ⟶ bag(B))]. ∀[init:Id ⟶ bag(B)]. ∀[pr:LocalClass(X)].
    (loop-class-program(init;pr) ∈ LocalClass(loop-class(X;init))) 
  supposing valueall-type(B)


Proof




Definitions occuring in Statement :  loop-class-program: loop-class-program(init;pr) loop-class: loop-class(X;init) local-class: LocalClass(X) eclass: EClass(A[eo; e]) Id: Id valueall-type: valueall-type(T) uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T function: x:A ⟶ B[x] universe: Type bag: bag(T)
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a local-class: LocalClass(X) sq_exists: x:{A| B[x]} loop-class-program: loop-class-program(init;pr) all: x:A. B[x] subtype_rel: A ⊆B so_lambda: λ2x.t[x] implies:  Q so_apply: x[s] prop: so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] strongwellfounded: SWellFounded(R[x; y]) exists: x:A. B[x] nat: false: False ge: i ≥  satisfiable_int_formula: satisfiable_int_formula(fmla) not: ¬A top: Top and: P ∧ Q guard: {T} int_seg: {i..j-} lelt: i ≤ j < k le: A ≤ B less_than': less_than'(a;b) decidable: Dec(P) or: P ∨ Q less_than: a < b squash: T class-ap: X(e) es-before: before(e) bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  bfalse: ff true: True iff: ⇐⇒ Q sq_type: SQType(T) bnot: ¬bb assert: b simple-hdf-buffer: simple-hdf-buffer(X;bs) mk-hdf: mk-hdf(s,m.G[s; m];st.H[st];s0) hdf-ap: X(a) hdf-run: hdf-run(P) Id: Id es-E: E es-base-E: es-base-E(es) rev_implies:  Q ext-eq: A ≡ B callbyvalueall: callbyvalueall evalall: evalall(t) bag-combine: x∈bs.f[x] bag-union: bag-union(bbs) concat: concat(ll) reduce: reduce(f;k;as) list_ind: list_ind bag-map: bag-map(f;bs) map: map(f;as) empty-bag: {} nil: [] bag-null: bag-null(bs) null: null(as) pi1: fst(t) has-value: (a)↓ has-valueall: has-valueall(a) loop-class: loop-class(X;init) eclass2: (X Y) pi2: snd(t) hdf-halt: hdf-halt()

Latex:
\mforall{}[Info,B:Type].
    \mforall{}[X:EClass(B  {}\mrightarrow{}  bag(B))].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].  \mforall{}[pr:LocalClass(X)].
        (loop-class-program(init;pr)  \mmember{}  LocalClass(loop-class(X;init))) 
    supposing  valueall-type(B)



Date html generated: 2016_05_17-AM-09_06_08
Last ObjectModification: 2016_01_17-PM-09_16_12

Theory : local!classes


Home Index