### Nuprl Lemma : sqequal-list_ind

`∀[F:Base]`
`  ∀[G:Base]`
`    ∀[H,J:Base].`
`      ∀as,b1,b2:Base.`
`        F[rec-case(as) of`
`          [] => b1`
`          h::t =>`
`           r.H[h;t;r]] ~ G[rec-case(as) of`
`                           [] => b2`
`                           h::t =>`
`                            r.J[h;t;r]] `
`        supposing F[b1] ~ G[b2] `
`      supposing (∀x,y,r1,r2:Base.  ((F[r1] ≤ G[r2]) `` (F[H[x;y;r1]] ≤ G[J[x;y;r2]])))`
`      ∧ (∀x,y,r1,r2:Base.  ((G[r1] ≤ F[r2]) `` (G[J[x;y;r1]] ≤ F[H[x;y;r2]]))) `
`    supposing strict1(λx.G[x]) `
`  supposing strict1(λx.F[x])`

Proof

Definitions occuring in Statement :  list_ind: list_ind strict1: `strict1(F)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2;s3]` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` lambda: `λx.A[x]` base: `Base` sqle: `s ≤ t` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` all: `∀x:A. B[x]` and: `P ∧ Q` cand: `A c∧ B` prop: `ℙ` so_lambda: `λ2x.t[x]` implies: `P `` Q` so_apply: `x[s]` so_apply: `x[s1;s2;s3]`
Lemmas referenced :  strict1_wf sqle_wf_base all_wf base_wf sqle-list_ind
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation sqequalSqle sqequalHypSubstitution productElimination thin lemma_by_obid isectElimination hypothesisEquality independent_isectElimination hypothesis dependent_functionElimination sqequalRule sqleReflexivity sqequalAxiom sqequalIntensionalEquality baseApply closedConclusion baseClosed lambdaEquality isect_memberEquality because_Cache equalityTransitivity equalitySymmetry productEquality functionEquality

Latex:
\mforall{}[F:Base]
\mforall{}[G:Base]
\mforall{}[H,J:Base].
\mforall{}as,b1,b2:Base.
F[rec-case(as)  of
[]  =>  b1
h::t  =>
r.H[h;t;r]]  \msim{}  G[rec-case(as)  of
[]  =>  b2
h::t  =>
r.J[h;t;r]]
supposing  F[b1]  \msim{}  G[b2]
supposing  (\mforall{}x,y,r1,r2:Base.    ((F[r1]  \mleq{}  G[r2])  {}\mRightarrow{}  (F[H[x;y;r1]]  \mleq{}  G[J[x;y;r2]])))
\mwedge{}  (\mforall{}x,y,r1,r2:Base.    ((G[r1]  \mleq{}  F[r2])  {}\mRightarrow{}  (G[J[x;y;r1]]  \mleq{}  F[H[x;y;r2]])))
supposing  strict1(\mlambda{}x.G[x])
supposing  strict1(\mlambda{}x.F[x])

Date html generated: 2016_05_14-AM-06_29_05
Last ObjectModification: 2016_01_14-PM-08_25_48

Theory : list_0

Home Index