Proof: Minimum Index One

Let's prove the following theorem:

index of the mininum value in stack [ x, [ ] ] = [ 0, [ ] ]

Proof:

View as a tree | View dependent proofs | Try proving it

Proof Table

#	Claim	Reason
1	index of the mininum value in stack [ x, [ ] ] = index of value (minimum value of stack [ x, [ ] ]) in [ x, [ ] ]	index of the mininum value in stack [ x, [ ] ] = index of value (minimum value of stack [ x, [ ] ]) in [ x, [ ] ] (Minimum Index Of A List)
2	minimum value of stack [ x, [ ] ] = x	minimum value of stack [ x, [ ] ] = x (Minimum Of A Single Element List)
3	index of value (minimum value of stack [ x, [ ] ]) in [ x, [ ] ] = index of value x in [ x, [ ] ]	if minimum value of stack [ x, [ ] ] = x, then index of value (minimum value of stack [ x, [ ] ]) in [ x, [ ] ] = index of value x in [ x, [ ] ] (Substitution)
4	index of value x in [ x, [ ] ] = index of value x in [ x, [ ] ] with current index [ 0, [ ] ]	index of value x in [ x, [ ] ] = index of value x in [ x, [ ] ] with current index [ 0, [ ] ] (Find Value Property)
5	x = x	x = x (Reflexive Property of Equality)
6	index of value x in [ x, [ ] ] with current index [ 0, [ ] ] = [ 0, [ ] ]	if x = x, then index of value x in [ x, [ ] ] with current index [ 0, [ ] ] = [ 0, [ ] ] (Find Value Match Property)
7	index of value x in [ x, [ ] ] = [ 0, [ ] ]	if index of value x in [ x, [ ] ] = index of value x in [ x, [ ] ] with current index [ 0, [ ] ] and index of value x in [ x, [ ] ] with current index [ 0, [ ] ] = [ 0, [ ] ], then index of value x in [ x, [ ] ] = [ 0, [ ] ] (Transitive Property of Equality)
8	index of value (minimum value of stack [ x, [ ] ]) in [ x, [ ] ] = [ 0, [ ] ]	if index of value (minimum value of stack [ x, [ ] ]) in [ x, [ ] ] = index of value x in [ x, [ ] ] and index of value x in [ x, [ ] ] = [ 0, [ ] ], then index of value (minimum value of stack [ x, [ ] ]) in [ x, [ ] ] = [ 0, [ ] ] (Transitive Property of Equality)
9	index of the mininum value in stack [ x, [ ] ] = [ 0, [ ] ]	if index of the mininum value in stack [ x, [ ] ] = index of value (minimum value of stack [ x, [ ] ]) in [ x, [ ] ] and index of value (minimum value of stack [ x, [ ] ]) in [ x, [ ] ] = [ 0, [ ] ], then index of the mininum value in stack [ x, [ ] ] = [ 0, [ ] ] (Transitive Property of Equality)

Comments

Please log in to add comments