### Nuprl Lemma : int-seg-case_wf

[i,j:ℤ]. ∀[F,G:{i..j-} ⟶ ℙ]. ∀[d:∀k:{i..j-}. (F[k] ∨ G[k])].
(int-seg-case(i;j;d) ∈ (∃k:{i..j-}. F[k]) ∨ (∀k:{i..j-}. G[k]))

Proof

Definitions occuring in Statement :  int-seg-case: int-seg-case(i;j;d) int_seg: {i..j-} uall: [x:A]. B[x] prop: so_apply: x[s] all: x:A. B[x] exists: x:A. B[x] or: P ∨ Q member: t ∈ T function: x:A ⟶ B[x] int:
Definitions unfolded in proof :  so_lambda: λ2x.t[x] nat_plus: + bfalse: ff btrue: tt it: unit: Unit bool: 𝔹 exposed-it: exposed-it le_int: i ≤j lt_int: i <j ifthenelse: if then else fi  bnot: ¬bb label: ...\$L... t sq_type: SQType(T) gt: i > j rev_implies:  Q iff: ⇐⇒ Q subtract: m uiff: uiff(P;Q) sq_stable: SqStable(P) le: A ≤ B ge: i ≥  nat: prop: subtype_rel: A ⊆B so_apply: x[s] exists: x:A. B[x] uimplies: supposing a guard: {T} lelt: i ≤ j < k cand: c∧ B int_seg: {i..j-} false: False implies:  Q not: ¬A squash: T true: True top: Top less_than': less_than'(a;b) and: P ∧ Q less_than: a < b or: P ∨ Q decidable: Dec(P) all: x:A. B[x] int-seg-case: int-seg-case(i;j;d) member: t ∈ T uall: [x:A]. B[x]
Rules used in proof :  functionExtensionality dependent_pairEquality_alt inlEquality_alt equalityElimination closedConclusion baseApply universeEquality unionIsType functionIsType intEquality cumulativity instantiate multiplyEquality equalityIstype dependent_set_memberEquality_alt minusEquality addEquality functionIsTypeImplies equalitySymmetry equalityTransitivity axiomEquality intWeakElimination applyEquality universeIsType productIsType because_Cache independent_isectElimination rename setElimination lambdaEquality_alt inrEquality_alt independent_functionElimination productElimination imageElimination lambdaFormation_alt baseClosed imageMemberEquality natural_numberEquality voidElimination independent_pairFormation isectIsTypeImplies isect_memberEquality_alt inhabitedIsType axiomSqEquality isectElimination lessCases sqequalRule unionElimination hypothesis hypothesisEquality thin dependent_functionElimination sqequalHypSubstitution extract_by_obid introduction cut isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[i,j:\mBbbZ{}].  \mforall{}[F,G:\{i..j\msupminus{}\}  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[d:\mforall{}k:\{i..j\msupminus{}\}.  (F[k]  \mvee{}  G[k])].
(int-seg-case(i;j;d)  \mmember{}  (\mexists{}k:\{i..j\msupminus{}\}.  F[k])  \mvee{}  (\mforall{}k:\{i..j\msupminus{}\}.  G[k]))

Date html generated: 2019_10_15-AM-10_19_53
Last ObjectModification: 2019_10_02-PM-06_04_50

Theory : call!by!value_2

Home Index